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

12
n\ot-.x]). Now let us write r ()p) instead oi,,for some O4xe
instead of,is identical with alnd c i. Ix îistead of,x: and tpx".
With the help of these ideas. which seem to be essential to anly
system of symbolic logic, we can build up the proposition:
(ao?). (x = — a ~ SC
which we shall denote by Qa. Now, it is easy to see that Qx is a contradictory object, we having propositions Q(Qx) and - QQx)1). To
avoid such objects, there seems to be no other means than to suppose with Whitehead and Russell, that Qx can be no possible value
of the argument of Qx, the idea of,all values of the argument of
0x" being not equivalent to the idea of,all objects". Moreover,
we should assume that the idea of,all objects" is meaningless, we
having a hierarchy of types of objects. Suppose we can speak ahout,,all properties of x" i. e., about;all propositional functions Ox such,
that either ~x or -JO x". We shall have to deal 1~ with individuals
i. e. objects being neither propositions lor propositional functions; 2~,
with propositional functions whose arguments take individuals as possible values, i. e. propositional functions of the 1s type; 30, with propositional functions whose arguments take functions of the 1 type as
possible values, i. e. propositional functions of the 2d type... and
so on. Such a simple hierarchy of. types would be, as a matter of
fact, sufficient to build up a self-consistent system of Symbolic Logic,
there being no purely Logical paradoxes based on the idea of,all properties of x". Nevertheless, as this last idea does not exclude such
contradictions, as Richard's paradox, or KI5nig's, it seems to be interesting to get a system of Symbolic Logic, free from such contradictions. To avoid these we must agree with Whitehead and
Russell that the idea of,,all properties of x' is meaningless.
Then we catnot speak about,all functi.,ns Ox such, that
either qx or -SX", we having moreover a hierarchy of functions
of different types (or, as we callI them, futnetions of different orders)
having x as a possible value of their argument.
We see that this seriously complicates the primitive theory
of types. Now, such symbols as (x) i. e.,for ail x's" or (3x) i. e.,for some x's" have meaning only if x denotes individuals. To
1) Cf. Über die Antinomieen der Prinzipien der Mathematik, Mathemnatische
Zeitschrift 1922,