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

being determined by the same functional expressions, or being individual letters; and
20 if they contain the same elementary letters, and the same
undetermined variables occurring in both as constituents of the same
functional or propositional expression.
With this direction we can write significantly C, (E, G), without using the directions 02, by simply looking on the letters occurring in the expressions E, G.
In consequence of our direction, an intuitive use of the pure
Theory of Types appears to be possible. Nevertheless I still keep to
directions 02, as being more convenient in symbolic practice.
Note that by the direction D, we have:
5 {u [. ~ {u, a} I (W) W {v, ] [, {U, a}]},
a formula impossible to attain by the directions 0'2. We see at
once that this difference is not essential. The first method is most
in harmony with practice; the second with the primitive idea of a
logical type. Tn Principia we have an analogous difference between
first-order matrices and first-order functions.
The pure Theory of Types does not eliable us to prove the
existence of functions of a given property, without having an instance of such a function. Nevertheless, it enables us to prove the
existence of individuals, without having any instance of them. Now,
Prof. Wilkosz has remarked that a purely formal system of Logic
ought not to be of any. use in proving the existence of objects
which are not explicitly given in the system. To have such a system, it is sufficient to deal with individuals in conformity with
the method we have applied to classes. We begin with introducing
the letters, m, 1, which shall be called in dividual constant s.
We suppose that these letters denote individuals; and we agree
that these letters can never be used as noted or apparent variables.
As there are metaphysical reasons to admit the existence of individuals of different types, we shall never use such expressions as
c{/, m}; or similarly as x [f{x}] or (x) f{x}. To have noted or
apparent variables, we shall be obliged to begin with such expression as./{x}. CI {x, m}.1), where the real variable x is determined
1) Mr Skarienski, has remarked that we get a serious simplification of the
system, if we use f(m) {x} as a fundamental idea. I see that this method would be
most conformable to the real meaning of the idea of a propositional function.