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

21
Then, by ouri hypothesis we must have:
93 f/
Hence w get: yp fp. 3 yO j -/'
No() put r-) r for pr and r ~)p for i/'r We get:; 3 D P = P D P ) 9 -: ) P
Here the hypothesis being true, we must have
q D g O - ~ 9 D) PS
which is evidently false,
Now, we must conclude that there is no such logical operation
':'{'} ~is consists in getting?pq out of cpp. To avoid such false
interpretations of symbols as we have seen above. we need some
directions for their meanning.
When we assume the Theory of Types, our contradiction disappears at once. This is clear when w note that if {:ip} is a fuanc
tion of Dp, we can take for cpp any proposition of the same type
as ip, e. g Q.. No w, f{q} can have no meaning, as there is no
variable argument in q. Therefore -{yp} cannot be a function of pp.
The Theory of Types of Whitehead and Russell contains some
philosophical theories which seem to be useless. Now, it is important to have some directions for working with symbols. Therefore,
in this part I cannot follow the method of Principia,
The theory of expressions to be given below is as a matter
of fact that conforms to the theory of Principia. I assume..letters
denoting individuals, but I do not assume any analysis. of the idea
of an individual, these objects never being used for any actual
substitution and their oily use consisting in their being of the same
type. An analogous remark may be made about predicative functions 1).
The essential difference of the actual theory from that of Principia consists ini the assumption of variable functions of assigned
types. Many direction, which seem to be tacitly assumed in Prileipia are here explicitly given.
To avoid ambiguity in the notation of the functions, I use
symbols analogous ta those which Whitehead and Russell use for
classes and relations.
1) For this remlark as 'or lmanl- other valuable pieces of advice 1 alm lost
indebted to Prof. Wilkosz,