Combinatory and propositional logic.

The relationship between combinatory and propositional logic is dealt with at length in [l] and tangentially in [2], The present paper adds nothing essentially new to previous results.It does, however, offer a straightforward procedure, which for any λ-expression in normal form will either lead to its propositional correspondent or determine that this is null.Section 1 presents the hypothesis upon which the correspondence between λ-expressions and propositional formulae is based; our translation procedure is described in section 2, and illustrated in section 3.1 Hypothesis.In dealing with λ-expressions we assume Church's rules and conventions as given in [3].With respect to propositional formulae, Ά' denotes the null class of formulae, and <Γ' is used for C. A. Meredith's operator D: 'TPQ' denotes the most general result that can be obtained when Modus Ponens is applied with P, or some substitution in it, as major premiss, and Q, or some substitution in it, as minor premiss.'~' denotes correspondence between a λ-expression and a propositional formula.Our basic hypothesis is the following.Hypothesis Where L, M and N are λ-expressions, P, Q and R are propositional formulae, and Σ is an operation under the substitution rule which may be null, 1.Let L ~ P, then for M with no free variables in common with L, and all N, Q, R. If M ~ Q, LM = N, and N ~ R, then either TPQ = ΣR or TPQ = Λ. 2. Let N ~ Λ, then for L, M with no free variables in common, and all P, Q.If L ~ P, M ~ Q, and LM = N, then TPQ = Λ.The need for the two cases under the first section (a) L ~ P,M ~ Q, LM = N and Γ PQ = ΣR for Σ non-null (b) L ~ P, M ~ Q, LM = N, N ~ R and TPQ = A is unfortunate but unavoidable.