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

t is easy to see that ouri notation will inipiy iontrradictions. Let
us take the function /'(t>I: a) of the variable (>! x, and let us write:
Now by.9'1.,if for omt:r e a th ere is a proposition I'a then there
is a function fx 5l" we have thle flowing/ fJunction o' x:
On the other hand, isven an funeti() /1'P I 0.) Of; ' )of x!l,.- the
expression:
~j!{(,/(,'p!"^:4il'
denotes a proposition,. hus thi sa me expression den otes a furetion
of,x: and does not denote it.
The same contradiction ca-n 1be eonstruleted for miatrices, if we
agree that 1 l! a t i, e. the function oi one variable function l)! x of'
individuals, is a iatrix (Cf. Principi-a, Vol I. p. 17(), No'w, we cau,
tasake /-\(f' e ) foi tl a (Cf. Prince ipa Vol I, p. ) f Therefore
j! r
f1!<(l (t! a) 1s a Inatrîx, To avoid t-lis alMbigu ity I shall write xzjl )t for
lts x and ayi [(rI){x } y or y t,} tor <, },
B. If we have no otiert varia.blee als matrices, we cannot use
the axiom of reducibcility as a general hypothesis. like Zermelo's
axiom, because we cannot write wi.th meaning'
(<P) 5([.) e; MX:~ x -tP x.
If we assume functions of any type as v ariables, then iwe
must have means of speakin' of,all fttnctions of the same type
as a given funeltion t1) x'-". A.s ta.mtter of fa-ct it will hbe seen below
that w n e can ostiut f x esi
(<)), alx: '
ire (<P), mn means,for fail fuet ions of the s aae type as cP t:
Such propositions as tbhos, given above, can be used as hypo,
theses, like ZerTnelo' axioi, therefore if e assume functions of
any type as variables, there is no serionts reason to have the axio
of redieiblit;yr among our primitive propositions, even if we are
willing to pass over all the other objections t have stated above.
Tt is to be reniarked that there are hardiy1 any propositions
of n.mathenicatis to be fouani, whiih require a Axiiom of redaciL., Ch-isteF,.