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

24-24 I-: UA - -.
24-26 1l-:a A.-.
22-57 I- U: U =PU:
2251 - f-. r n
22-69 -1:.u. LJf UU. U-.,:2268 [-:. n. pl,. n Y =.. UY
24-21 1- n-.=A.
24-22: U- - = V.
241 I-.A+V.
Analogous propositions are to be asserted for (~, T,; an
analogous set of propositions is to be stated for relations:
I?, N, or R,(, [9, P(,, P) etc.
D. Descriptions.
I cannot agree with the theory of descriptions of Principia
this theory being based on modifications of defined symbols,
which are not simple substitutions. Now, a general theory
of descriptions seems to be superfluous, as we need only the
following abbreviations:
14-01.î t- R'(a,b)V.-=.'lR(^,) V. (w).w R(a,,b). w=U:
14'011. R(a, ^v t=. U(a, )V.')W R(a, ) V.= w:
dl
14-012. R'(a,) v - u. = (3 w): R'(a, ) v = w:. w =- R(, u) u
(a, ) d/
14-02 R(cbt) X;(a (3w):k(ab)= w:VwE(^.
14-02 RC(, ( ) v s zP (, ) = ( ) V w): W, h,) =w w 2 (a),.
df
df
14-022 U P(,, c) R'a, ) v = (I w) RI, )7 b =V-: wu P cac) w.
df
With these definitions we can prove the following propositions:
14-1 g:t RU (a, b) V. R(2, 6) U:
Dem. 1-1317 |I-:'=w.. w-= u:
[4-85] 3 D-: rl t(~, b) v D. u - w: =. w ((,, b) v J. v =u:.
[10-271] 3 l-. (w). w R(,, v).u=: = (w)., R((,,) v 3, t - u.
[4-36] - g-.Prop.
14-11 S: h(R, )v-( = T, b). R'(,,,) = R (ba, ) v:
Dem g-.14-1. 433
-:. R(,,b v-=:.U= R(,b,,u: - 'R % =' ---w:. w — R (,,bV:.