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

paradoxes as Richard's or Kionig's, it is quite sufficient to assume
a direction excluding from the scope of the system any function
which is not constructed with the symbols of the system itself. An
analogous method is used by mathematicians dealing with the system of axioms ot Zermelo ). Such a method, though very convevenient, is nevertheless inconsistent with certain fundamental problems of Logic and Semeiotics. Moreover the simplified theory of
types implies the existence of functions which cannot be built up,
unless we assume that all functions are extensional functions (the
Axiom of Extension).
Now, a purely formal system of Logic ought never to imply
the existence of such functions; otherwise it might be asked why
the axiom of infinity, or other existence-axioms are not to be assumed as primitive propositions.
The practical elimination of the Leibnizian idea of identity
is an essential simplification of Logic, this idea being of no use
in Mathematics, as we have no means to prove with it the identity
of objects given by two different expressions.
Now, here is a most interesting metaphysical problem: Can
an object be denoted by two different expressions?
This problem cannot be discussed in a system of formal Logic, as such a system does not contain the primitive idea,expression". On the other hand it is easy to see that such a problem cannot be solved at all, as we always get two contradictory solutions.
If you suppose that two different expressions denote two different objects, you cannot prove that two equivalent classes are identical. To prove that any equivalent classes are identical, we ought
to suppose that there are objects denoted by two different expressions. The first hypothesis may form the base of a Nominalist i c system of Metaphysics (Ontology), the other of a Rea i s t i c
system. The Realistic Hypothesis, i. e the axiom of ex t e n s i o n
would be formulated as follows:.(x). a{S} _{fx}. D.f{a} =f{é}:
This axiom seems to have had great success in recent years. I never should care to discuss its truth. I am convinced we never get
a contradiction from using this axiom, but I am also convinced
1) Cf. Fraenkel: Der Begriff ~definit~ und die. Unabhtingigkeit des Auswahlaxioms, Sitzungsberichte der preuBischen Akademie der Wissenschaften, Berlin 1922.