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

26
0'17 Fundame tlal class-letters are undetermined functional signs
of fmlictional patterns with I argument.
0~17 Functional class-letters are uiidetermined functional signs of
functional pal;ternls with I argument being an individual variable.
0 172 Fundamental relation-letters are unldeterrined functional signs
of functional patterns with II arguments.
0 i73 Functional relation-leott;ers are undetermined funetioal aigni
of functioiial patterns with II arguments beiig individual
variables.
0~18 The funetional class-let;er ') stands for [)X{C}], where i is
any individual letter.
0o181 The functional relation-letter X stands for J P [l{ )}]j where,?.,
are individual letters,
019 Determiined letters are funidamental letters determined bv a
functional class-letter or a functional relation-letter~
0'20 Types.
0.2 AUll primitive iunetional expressions with I (or II, or II, (or IV)
individual variables denote p r e di at iv e f u t i o l s o f
the;ame type.
023 If ir a given functional expression we change the order of
iloted variables preceding th angular brackets. we get a funci
tii na. expression denoting a func tion of the sanme type.
E. g. expressions: xx[({}pX, xl[XL{x'}] denote functions of
the same type.
0'24 If.', (G are any expressions such that.E G. contains the
noted variable A and if M..E\G.] is a functional expression:
Lhen [. GIE. denotes a fun c t ion o f the same typ e.
0'241. If E;, G are any expressions such that. [ G. contains the:noted variable a., and if,[. Ei G.] is a functional expression,
then [.. E I C. G -.7 denotes a fun. tion of the same
type.
0.2411 If E, G are any expressions such that )[.Elp.],. G\p.\ doe-note functions of t;he same type, the expressions \J\ll, 1\Gr
denote functions of the same type.
0Q2IS2 I-f J, G are aly ex)ress(ions iand, anly real variable, lhen
if A1l ], \[GJ denote functions of the saimne type. anld i:f )i. 'l G.