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

74
D3 - Prop.
113 621 oel (NCU, t' A"'') D. (a X l)-a. [73-611 ]
11762 - (67XtI)ElC.?,~-( X0..( X T)>.
1
[l1 7571.53. 113.621.]
113-601 g- fiMNCD.(XOX) =0.
113-602 1. ( X zT) 0.-:. a O. V. =0:.
2Q Q
113-4 - ((x J ) X o')-X((x X o') U (o XA oi')) [40o31]
113-43 -.a '(+,T)V. 1' = 0:. D ((7+ T)X') = ((X') + ( X')).
Dem - 113-601.117 -51-4. 110 62 D
-'t '=O: ~ '((X') + (XT')). ),('(a+ ) (1)
- 101o1001.113-4.73-71. D - [ '(a 4- T).((~ + t) X T')
(( X T') + ( X ')). (2)
|- (1).(2). D - Prop.
1 shall use the following abbreviations:
113-501 X(w) = ((("i CnVA (a ), R)I ((tw 1)k w))
dJf a A a,A a AA
113-502 Y(t) =(((cw 1 nvaw(t4))| CHvAS)I (( ai kw"))
df a A a A a A
113503 Zx=
a a a
P[(, ')P[(^ P((4(')I ") I X())() (Y(U') (wo"1 Cnv (Ju))))]Q]
A A A,a A a,A a A
113-51 |- *[a)'] '"<-(')A —(x X Ao). [(a&)'i w/"(S)-(x' XC))
A A.{RS, S, B} )s. m (" X, ')sml (o" XdA )
Dem |- 72'184.7 1252. Ze 1 - 1: JAZ== (x" XA '):. Q,,Z
A A
(w)" X4): {'ZY, B}.
[10-24] 3 - Prop.
113-54 (-. ['(aXt) a'(Xz.. D ((oXT)XT') (X(Xt')).
[113-51. 1036. 113-27]
113-66 1- (aX2) == (a+ a) [1.10-643.113-43621. 10132]
113 l 771 U'(.-L 1.+)V.. 0: ti0. ((X(a +- 1)) = ((Xa)+,))
[113-43 621]