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

46
[10.2811 )|- (3w.):R'(, v)=-l:.:-=R(a,:,)u:(1W):RXa, Z=bl'-t=,:.WR (a, v.
114-012] 3D-. Prop.
14 12:. ib., v =:. R (, R ) ab- t: 3. R (,) V (,a, 7,)
Dem I-.14 1.10-243 - Hp (i,t): R - T()-t. t: t R(,,
[14-0121 3D-.Prop.
14-13 -:. R',,) v -t:-. R(,,t,) v zt:. a= t:
Dem.- 14-011.3-27.10'1
[- R27,-: Ru.' R,,v t. t R(, )v.u t: (1)
-. (1). 3(2).43..- HpD.: R (a,, b) v. t R(a, ) V ). i, - t: t R v:
[3-35-27] D I. Prop.
14-2 I-:. t - u: R'(a,,) v =:. R().( v t:
Dem '- 13-122 3D-. t =.. R(,,, ) v t R(l,,) v: (1)
a, a
3 -: t: Z. 3: "R( I(,b, )V D 3. 0 -.' -.t:. R(,v 3.w = t:
[g-. 422. 3. (w). w' R(,,, )v 3. '- =' ':- l (w). R, b) v ). t = t::
[(l)] 3 -. Prop.
14-21 -:. R(,t, ) l- R= (a, ) v:. R( ) b ) t:. R ab) _ R(a, b) t:
Dem - 4-32 -::' R'(a, ) ui = w:. l = -R(, b) v:. R '(, ) v -
= Wv':. w='-.R, ) t. Z:.' R'(,,,) w --- == '.: =
- Re(a,, ) v R',: ), w':. R' ) =- *, R ) t:
[4'321 Z3: BR(, ) u =w:. w-: - h.,, b) v::.R'(a, b) vU = w1 (), — R(c. )t:
[14 13]: R'(,,) = 1-. /' = w:: w' = R%,,) t:
a, a
[14 21 Z:R'(a) - = w:. w R'(,, )t:
[14'13] R'(,,, b -- R(,,,) t.
[11-351 3D.-. Prop.
Our method of dealing with descriptions implies the following
modification of definitions of the theory of relations. Take e. g. the
definition of the Converses of relations. In Principia we have first
the definition: Cnv = QP[\.x Qy_ y, Px-.] Df., and by this definition, the converse P is Cnv' P.- Nevertheless it is to be remarbed that the relation Cnv is never used unless in Cnv' P. Therefore it seems better to have no such relation as Cnv, but siniply
the relation Cnv' P. - This method will be applied to all analogoxTs problems. Then we have: