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

94
Note that Infinax by no means implies the existence of so.
The existence of any aleph must be assumed separately. - It is
easy to see that if we deal with alephs, we assume the reducibility
of the corresponding classes, and by this method we get a system
which is practically equivalent to the simplified theory of types.
We then see that Cantor's theory is closely connected with the
simplified Theory of Types.
The fundamental idea of this work being that there are no
other primitive propositions than those belonging to the Logical
calculus, we are obliged never to deal with an hypothesis without
having a parallel system based on a contradictory hypothesis Now
it is interesting to see what is to be done, if we assume an hypothesis inconsistent with the multiplicative axiom. Such an hypothesis being somewhat connected with the ideology of Realism, we
can deal with it by means of the simplified Theory of Types. This
matter will form the subject of a separate paper1. Here I wish
to expound only the fundamental ideas of this work. On the other
hand, I shall prove the fundamental proposition of Nominalism
which I have mentioned above. I begin with this proof.
A. Nominalism.
I shall use the following definitions:
13 41 i = xv[(lt): -{u} - (v = u): {,U V}. {, (;'}.]
df L
13-42 (iva) = u[(u = a). ~{u, a, V}.]
df L
The direction 04, enabling us to take functions in any type
for all individuals occurring explicitly or implicitly in a given expression, we can use any function instead of a. Then our Theory
of Cardinals applies to classes of any type. Now we shall have to
deal with classes of the type [-"]" Ct)tt') instead of K and with
corresponding cardinals and inductive numbers. This Theory enables
us to prove the fundamental theorem of Nominalism, which I call
the theorem of M. Greniewski. I use the following abbreviations:
13"43 P= 4{[./{}\ V{K}.]
dt
1),Über die Hypothesen der Mengenlehre", to be printed in,Mathematische Zeitschrift".