Some properties of conversion

Abstract

Our purpose is to establish the properties of conversion which are expressed in Theorems 1 and 2 below. We shall consider first conversion defined by Church's Rules I, II, Ulf and shall then extend our results to several other kinds of-conversion.| 1. Conversion defined by Church's Rules I, II, III. In our study of conversion we are particularly interested in the effects of Rules II and III and consider that applications of Rule I, though often necessary to prevent confusion of free and bound variables, do not essentially change the structure of a formula. Hence we shall omit mention of applications of Rule I whenever it seems that no essential ambiguity will result. Thus when we speak of replacing {\x.M] (iV) by S^M| it shall be understood that any applications of I are made which are needed to make this substitution an application of II. Also we may write bound variables as unchanged throughout discussions even though tacit applications of I in the discussion may have changed them.