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

27
is a functional expression. it denotes a fu n action o f th e
s a e ty pe..
0243 If 1[E], )[G] denote functions of the same type. thon if
\[. E\jI H.] [. G H.] are functional expressions, they denote
functions of the same type.
0'25 If E(), I), G(v6 p) are expressions containing noted variables,, or V, p. and if. A (),?) j ((v,) ). is a propositional expression, the expressions: tv[E(S,.)], vp[G(v,: )] denoting fu, etions of the saine type, then the expressions:,[()J.)E(k, î?)1,
v[(p) (G(v, p)] denote fu nation s of the same type.
0'26 If E(\), G(;,.) are expressions denoting f lin tions of the
same type, and c containing the real variables o, or,: the
expression v {i(k), ) (?.))J, where v is a primitive or fundamiental letter absent in E'(I:) and G((J.) being a propositional
expression, the expressions: i E(I):, (.(, ) denote f u n c t i o n s
of the sale type.
0'261 Given the individual, or fundamental letter. or the functional
expression F and the expressions E(G,), G(Ç) containing the
noted variable ), then if E À E(À), T(G (,) denote functions of
the same t y pe, and if 1E(.). G (Fl') are functional expressions, these expressions denote functions of the same
ty pe.
0'27 If E(?,) is any expression containing the variable;, and i
and H is any propositional expression, then if AY[(,). 1I E'(?,). ]
j[. H (jp) '(p, ). are functional expressions, tley denote f u 1 etions of the same type1.
0'271 If E (A) is any expression coiltaining the fundamental real
variable -, then the expressions )\ikE(';). [.A{}l '(I).], respctively A [/L'(0j), )1 I. {c{, i} j E). denoteo functions of the
saime type, if they are functional expressions.
0 28 If i. P G( are any expressions suchll that the expression.Ejl.. F G. conl ains the noted variable A; and if the
expressions:. [. Ei. F 1..],... AF.i' (' 1. are functional
expressions, they denote fnoetions of the same type.
Remark: Statements 0.2 —0'28 concern the idea of,,being of the
same type". In Principia, we have a definition of this idea
(.:- ' *131). Nevertheless. it is 1I~ a verbal definition. 20 it seems
'This direction corresponds to the definitions x- 9)03*0- of Principia.