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

31
0)451 nl any propositional expression iE containing no implicit individual letters, i. e. no symbol 12 defined by an expression
i containing individual letters absent in 51, take for all individual letters any functional expressions denoting functions
of the same type and compatible one with another and with E.
Then we get an expression E'. If E' is a propositional
expression, it is a derived expression in respect of E.
0-452 Given any prepositional expression E, containing fundamental
real variables,.whch never occur as arguments. of a
fu n c t i o n a s i g n (undetermined variables), take for these
letters any functional expressions, compatible one with another
and with L, whose variables appear after the substitution
to be determined by functional expressions denoting functions
of the same type as those denoted by the connexed arguments,
or to be individual, or primitive variables at the same time
as the connexed arguments, then we get a derived propositional expression E1' ).
The Logical Calculus.
B. Directions concerning the use of symbols.
Any Logical Calculus must follow fundamental directions of
the use of symbols, i. e. the M o dus Ponens, the Law
of Generalisation and the Law of Substitution.
As an abbreviation, useful for avoiding the repetition of primitive propositions and proofs for functions of the same type
as a given function, 1 also assume the Law of the Automat'ieci. construction of Assertions. To understand
the use of these directions the following remarks seem to
be necessary. Directions concerning the meaning of symbols
enable us to have as many significant expressions as we choose.
Suppose we have a list of expressions denoting o g i c al
p r o p o s i t i o n s. It is interesting to have a method of discerning the expressions denoting true 1 o g i c a 1 p r o p o s i t i o n s
from other expressions present in olr list. Now, we assume
some pri m i t i v e propositio ins,l which are common rules
of the Logical Calculus. The expressions denoting. these propositions are expressions denoting t r u e p r o p o i i o n s. Other
1) The use of the derived expressions is conform to the practice of Principia.