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

28
to imply vicious circle, because to define the idea of being
of the same type, we rnust use the very same idea. Now,
verbal directions are essentially different from the proper
propositions of the system. Therefore, there is no adventage
in putting them in the form of a definition.
0~29 If ihere'is a significant expression, which contains functional
expressions J: G as corresponding arguments of lhe same
functional sign: then Ei' F denote fnn ctions of t h e
sa me type 1).
0'30 Definitions
03 Given any expression -. we can use instead of E any other
expression 2,- if it has 1~ no meaning in isolation, 20 if it
contains no significant letters or expressions unless real appa..
rent or noted variables, elementary letters or funtional expressions present in E1 3~ if it has no such components X, Y
that Q is X Y and Xi or Y is a functional (or propositional)
expression, iE being a functional (or propositional) expression.
Thon we write:
— = E.
dt
This expression is a de fin i t i on. Here E is the defining
expression, Gi the defined sym bol.
031 In a defined symbol f2 we can turn real variables into noted
or apparent variables and we can take a functional expression
for a determined' real variable, but no other m o d i fi c a t i o n s
t-f th e defi ned synibols can be allowed.2)
0~32 If f2 E and F(E) is a propositional (-or functional) expression. then Fi(iî) has the same meaning as l'(E).
0'321 If ~f E. arnd if F (E'), i('t., are propositional expressions,
E' having the sirae meaning as.h, the expressions E'(E'),
P'(2l) have the same mIeaning.
0'33 — p -, P.
0)34.*2z \/V '.pl)ilipl..- )
dj
1o01.pD.-.q pV.
1) rhis direction corresponds -partly to: 9' i. of Principia.
') Without such a direction we could never be sure to avoid iambigaitii e
as noted in Chap. 1. a3) cf 1. c.