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

11
with the help of rnnetamathematical' methods that they imply no
contradiction. Nevertheless Hilbert must either explicitly or implîcitly use the primitive propositions and ideas of the Logical Calculus. Suppose he has proved by means of these primitive ideas and
propositions that a system of propositions (say p, q, r) is compatible
with them. Then, he has simply proved these propositions. If he
has used (explicitly or tacitly) other ideas or propositions, then he
has assumed some Iew hypotheses which appear as more general
than Zermelo's axiom etc. At any rate, the system of primitive
propositions of Symbolic Logic and its consequences remains as
basis of any further investigation. Note, that Hilbert does not assune
the Theory of Types. Nevertheless I can hardly assume that, we
have a,Meta-mathematic" at our disposition, which could be really
free from problems connected with the Theory of Types ). To see
this clearly, note, that such a,Meta-nmathematie cannot be essentially different from the Logical Calculus. this calculus being as
a matter of fact a simple consequence of the laws of our thinking.
Now, as we shall see below, we can not employ any self-consiste'nt
Logical Caleulus at all, if we do not asume the Theory of Types.
Therefore there seems to be no means of avoiding the said theory,
I. A Critieal examination of te theory of Prof. A. N.e Whi
tehead and lion B. B ussell.
A. Functions.
The fundamental hypothesis of the Theory of Types of Whitehead and Russell, as developed in their classic work: Principia
Mathematica2) consists in the statement that the idea of,all objects"
is meaningless. As a matter of fact, there seems to be no means
of preserving this idea, because it is easy to build up a propositional function Qx based on this idea, and being a contradictory object.
Suppose all objects are possible values of a propositional function
Ox, and suppose we can speak about all properties of x (i. e. all
propositional functions Ox such that either qx or -~0x, [which is
1) As we shall see below, there is a Meta-mathematic, dealing only with the
meaning of symbols, but never with the truth or falsehood of propositions. Thercfore there is no meaus of proving a mathematical or logical proposition with such
a Metamathematic.
21 Vol. I. Cambridge 1910,