Of course the matter of interpretation is in any case irrelevant to the abstract construction of the theory, and indeed other and quite different interpretations are possible (formal consistency assumed).
In the intended interpretation of the formal system [lambda] will have the role of an abstraction operator, Noo will denote negation, A.., will denote disjunction, Io(oa) will denote the universal quantifier (as a propositional function of proposi- tional functions), a will denote a selection operator (as a function of proposi- tional functions), and juxtaposition, between parentheses, will denote applica- tion of a function to its argument
Then Sa'a' will denote the successor function of natural numbers; or, more exactly, it will denote a function which has the entire type a' as the range of its argument and which operates as a suc- cessor function in the case that the argument is a natural number. Moreover, Noa' will denote the propositional function "to be a natural number (of type a')." If Na, denotes a natural number of type a", then Na"1Sa'a'Oa' denotes the same (more exactly, the corresponding) natural number in the type a'. Hence if Na' denotes a natural number of type a', the same natural number in the type a" will be denoted by Ta" a'N
I. To replace any part M. of a formula by the result of substituting ye for xp throughout Ma, provided that x# is not a free variable of Ma and ye does not occur in Ma. (I.e., to infer from a given formula the formula obtained by this replacement.) II. To replace any part ((Xx#Ma)N#) of a formula by the result of substituting No for x# throughout Ma, provided that the bound variables of Ma are distinct both from x# and from the free variables of No. III. Where Aa is the result of substituting No for x# throughout Ma, to replace any part Aa of a formula by ((x#Ma) N#), provided that the bound variables of Ma are distinct both from x# and from the free variables of N
The rules I-III are called rules of [Lambda]-conversion, and any chain of applications of these rules is called a X-conversion, or briefly, a conversion