The theory of constructive types (principles of logic and mathematics). By Leon Chwistek.

58
pressions which are by no means an essential modification of our
directions, and may without any difficulty be omitted in a complete
system. E. g. we shall omit one external dot on both sides of our
assertions; likewise the brackets in defined symbols,'in cases excluding any ambiguity; we shall also omit the letter a in defined symbols, by a proceeding to be explained later.
VI. Prolegomena to Cardinal Arithmetie.
This chapter contains certain définitions and propositions to
be explicitly used in Cardinal Arithmetic. In spite of the general
method expounded in Part I., we shall have to deal with definitions
built up for special types.
a. Complements of the Theory of Deduction:
3'02.p.q.r.=-:p q:r.. df
3'021.p.q.r.s. ==:p.q.r: s.
df
3'022.p.q.r.s.p'.=:p.q.r.s:p'.
df
3,44 l-': p::'.r3p::qV D. P3-47 1-:p:.q~ s:):p.q..r.s:
4'1 i.p/__ = q_.) p iq.[to be called: Transp,]
55 - pD:pD q.= q.
5.75 1-:r ~ q:'.p -.q r \ r:V.: p.- q.5 r.
10.28 x-./x D g {x}.D.3x {/}(-D 1 )g{x.
1o~~s 0 i 2 8 | ) f( S {x} 2 {x} *. (H X) J X} ( H )g (xv
10-34 - (x).g{x}D p.=-. ( x)g{x} p.
b. Classes and Relations.
We shall use the following abbreviations:
2004 extensa (x) = (u. v): =. U.x {u} = {v }:
df: aa
20;041 extens (z=) extensa (X)
df
21-04 extens (R) = (u,, w, t):. u v:.= R {u: w{ } {v. t}:
df a,, a
21-041 extens (R) = extens (B)
The difference between the use of extens, () and extens (z), (or
extens. (R) and extens(R)), is that the first symbol can be automa