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

13
have such synbols for functions, Whitehead and Russell build up
the idea of a matrix. i.e. of a functiion having no such constituent
as ( (l) or ([t4.). Such fullctions are to be denoted by symbols like
(t!r, p!(.:. y). etc. Having these functions. we cau use symbols
(0), (U >) for them, and build up matrices of the 2d type, whose
arguments are f!.r, and of which there are no such constituents
as (x), (.xr), (0), (r ). These matrices are to be denoted with symbols:
/"(&î:), /!(<.!,, ) etc.
Other functions are to be obtained from matrices, using symbols
like (x), t x), (0), ( ) O), e. g.
ix). f!(xS y), (r.X)!,. x ),
( ).,f' (0! x. x) etc.
This part of lte Whitehead-Russellian Theory of Types. we
shall eall thc purc theory of types, or the theory of constructive types. Ths ory with form modiatiois tey th fma odo be developed in
the present paper.
The theorv of Whitehead and Russell. as assuened in their,Principia Mathematica", cannot be treated as a pulcr theory o:f types;
these authors having supplemented this theory with an "existence
axiom" 1) they call the axiom of reducibility, and this axiom being
neither a purely logical axiom, nor a simple application of the ideas
of the pure theory of types. This axium states that:
i. e.,every function of a variable is equivalent for all values, to
some predicative function" 2), i. e. to a rnatrix.
Now it is obvious that, given any fulnctiorn q)x we have
sometimes no means of building up a matrix equivalent to this funeetion. So, if we affirm the existence of such a function, we must
suppose that there are matrices which we cannot build up, i. e. matrices which are not constructive. Now, we can prove, by the method
used by Richard, that, if there are only constructive ftinctions, the
1) Cf. Trzy odczyty odnoszqce sic do pojçcia istnienia, Przeg'ld filozoficzny 1917.
2) Princ'pia Vol 1. p. 177.