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

54
that this hypothesis, not less inconsistent with Cantor's theory
than with the simplified Theory of Types, is nevertheless very natural and quite simple. It conforms to Poincaré's postulate, stating
that there are no other mathematical objects than those we can
build up into a given system. It is interesting to note that with
the Axiom of Nominalism, we can prove the axiom of Zermelo ),,
and we have nevertheless to do with a continuum conceived as an
ambiguous symbol (Cf. Part I, p. 19).
The researches concerning this subject seem to be very important, many interesting theorems of modern Mathematical Analysis being based on Zermelo's axiom. Note that with the axiom of
Nominalism we prove, e. g. that a limit point of a class of points
is a limit point of a progression of points, contained in the given
class. As the Intax enables us to prove the Axiom of Infinity, it is
obvious that a system based on the Axiom of Nominalism and on
Intax should embody modern Mathematical Analysis.
B. Types.
It is to be remarked that the use of primitive letters is very
limited. As a matter of fact, they are only used to build up the
expression C{x,y>. Now, there is another method of obtaining an
equivalent expression. Let us expunge the primitive letters from.
our system and assume the following definitions:
1_2 001 ' (x)=. a {x} a {.
12-002 ( ) =. a (x). (y).
d/
It is obvious that the symbol C~ (x, y) denotes the proposition,x is of the same type as y" as much as the symbol C{x, y}. The
elimination of primitive letters would be an essential simplification
of the Pure Theory of Types. If we omit the primitive letters, we
can have a very simple direction for the construction of functions
of the same type, i. e:
D. Two functional- expressions, containing no primitive letters
denote functions of the same type,
10 if they denote at the same time functions with I variable
(or with II, or with III, or with IV), their corresponding variables
1) Cf. Trzy odczyty od noszTqce sic do pojçcia istnienia. Przeglqd fil. 1917.