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

Application to the construction of significant expressions.
0'43 If,, '/,, 0. are any compatible functional expressions or individual letters, and?) is any primitive, or fundamental letter
absent from }, ',, 1, then: k{c}, k{:,}, A{.^~, r} and ),{L., ',, }
are propositional expressions.
E. g. the following expressions are propositional expressions.
9\X}?{, y}, p{x J,>,: x, {, Y, 2 X'}
/{^}, /{x, y}, z, f' {xy, x,}
o{x[h{x} } x, o z[,[ih{z}] },.{?[p( }] }.
Subordinate expressions.
0'44 In any expression E, take for any elementary letters, any
propositional expressions compatible one with another and
with E. We get a subordinate expression E' 1).
E. g. the following expressions are propositionaal expressions:
~-.~{g V - x [h{x x}]}.:4{1}}.
- s~ h {r} f } V { [ 04] 1
~ ~[\h{}1\{a} V~(?)Y-'.~{æ[J7{æ}] } \/jq {x[h{x}}j>..
~.g{a} V (9)~ O-{g} V {-[{ (h{x}]}. [0-41
0.441 Given any propositional (or functional) expression E containing an individual (or primitive) real variable E, or a fundlamental real variable, determined by a functional expression H, take for C any individual (or primitive) letter absent
in 'E or used in E as a real variable, and for 'q, any fundamental real variable absent in E, or determined by HI or any
functional expression compatible with E and denoting a, function of the same type as the function denoted by H, We get
a subordinate propositional (or functional) expression E',
compatible with E. 2)
E. g. if E is (?->)-.- {g}V {xlh{x])}., then E' eau. be:
(r ) {x - h {x}]} V ( {x [h {x}]}.
Derived expressions.
0'45 In any propositional expression l take for some elementary
letters any propositional expressions compatible one with
another and with E. We get a derived expression O/.
1) This direction corresponds to. 9'61'62'63:x 10'13 of Principia.
2) Directions 0'29'341 correspond to. 9'14 of Prinepia.