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

29
)-40 Substitution.
0-4 In any significant expression E take for any individual (primitive or fundamental) letter used as an apparent (or noted)
variable, any other individual (primitive or funidanental) letter
absent in E. Mre get au expression E' having the same meaning as E.
0-41 In any propositional (or functional) expression E, take for
aly functional expressiou,,1). or any individual (2), (or primitive (3), or u- d et ex;rmî ini ef fundamental (4~)) real variable,
in some of its. occurrences, any fundamental letter absent
from E, which appears after the substitution Lo
be a determined variable (1), or any 'individual (2),
(or primitive. (3). or fundamental (4)) real variable, beingabsent from E. We get'a propo(sitional (or functional) expression I,'.
(.Com.patible expressions.
0'42 If two. significant expressions are present in a given significant expression. 'they are compatible express on s.
0'4201 A.ny significant expressions are o m p a t i b 1 e i n r e sp e t
of a common ele mentary letter.
0'421'Two signifies nt expressions are compatible in respect
of a co mmoni individual letter, if this letter is in both
expressions used as a real, (respectively noted, or apparent)
variable.
0 422 Two significant expressions are c o np a t i be i n r e s p e t
of a common primitive or fundamental letter, if
this letter is in both expressions used as real, (respectively
noted, or apparent) variable, and if it occurs in both expressions as a part of a common functional expression. 1).
0'423 Two significant expressions are compatible in resp ect
o f a c o m on o i f un d a m ent a l t e tr, if it occurs in both
expressions as a real, (noted, or apparent) variable, or if
it; is determined in both expressions by the same expression.
04Ç24 Two signiificant expressions are e o pati ble if there are
compatible in respeet of all ommon e letter.
1) Directions 0'42-0422 tre conforin to the practice of Principia,