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

43
13-042 extens [L(Xa,b)] [(ij V, w: t):. v =V. î: w t
a ftX(a.( b, b
x, (a ), 7 J (a)}
13-043 exteus [R(p (a,,>) l f [, v, t)):: =.w -. t
d?,(ac) te ' d (c), (,c) ',
D i(a, c), w{,ui /P(~ > {, 7T, t): &{J, J$a, ) }:1
Now we can prove the following proposition:
312 j J:?= v. *D3: fa {at}.. extend [lZj] {/},{}. extends [i)] {f}
Dem 1..5-34)
-:- extens ['(a)]{} 3.:/;, {,u}. extels [a)]{f}..f,/ {y}, estens L^x,ln] {/}:
I.4-2,
gh. extens |K (\ {}.} ()u (jv: u y: _}- v{ }: f{ (t (, = t v:.
[101]: Mu=v 2:f, {~ = /, {}: 4 f, 'a}:
a, n
15-32.12-1]
au =-. V3: t/ {l} extens [,](< {}. _. f{V}. extends [I (j{f}
[(1). 4'830 D 1-. Prop.
I add the following important propositions:
13 16 |': v =. =. =:
13-17:. u =v:. v -= w:.~ '- '=:
As we shall have to do only with extensional functions, the
following definitions are very important:
20-02 t s n =. () {u}. extends I aj {Xz/)}}.
df
21-02 uRca,? v=..,B,,I), v}. estens Rl{,,)}21 -021. R xT>)Vi=. Lf-)T {u, v}. extends [11a,}1 {T())}
ai
21'021 'u PKi,) )v. Rt pg,. ^ {, v }. extens lR (Pa, \, {R,(p, ) }.
Note that with our definition of Ri,,> no conventions based
on the alphabetical order of letters, or on tlie order of letters
occurring in a given expression are needed. 1)
The definition 20-02 (21-02) enable us to prove the following
propositions by a simple substitution in 13-12 of the symbol
U E i, (Pnia) IR ).
1) Cf. Principia 1. p. 211.