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

The Pr inci ple of Deduction [Ded.]
10-1.( )/M '{y}
The Principle of Disjunction [Disj.
101o2 a-. (x). p V.f{x} D. V (C) /f{x}
It o Logiceal Caleulus. Fuietions of tie samie Type,
A. Logical Calculus.
With our directions and primitive propositions we get the
Logical Calculus of elementary propositions by applying the
method of Principia numberss b- 1 5). There is no reason
to repeat this; here. I shall simply quote the definitions and
propositions to be nesed below as lemmas..
2-001 =.
dt
202 I-.qD.pD:
2.08 ~-.p-Dp.
2.21 i.,p D.pD.
3 e 01 \p.q.= ^ ^ p) D * P ) -i
d.!
3-26 a:p.q,)p.
3,33 p-:.p- q _D D pD'
3-35:p:pD qD.
4-01.p q. =:p j qq p~
~4' 9-2
4'2 ^i=p-po
5'21 'p —q -- q1p'
4-22 g ae.p=5:. 5:3.p= t o
4-3 -:p.q.-.q.
4~32 p!. q: =. '..p ~ '.
4'36 [ p q.):. r.. q.'"
4-83 [=:.p q'.-_p 4:
4-85 |-:pq=.D q p.O'....D.
534 h p. -pot: p. q t b. p ir. 3 n)p
) rThis proposition seems to be absent in -Principia.