Supplement to Lambda Logic

Michael Beeson ^{∗}

San José State University, San Jose, CA, USA

Abstract

This document contains some explanations and proofs that had to be omitted from (4) to meet the length limitation. It is meant to be read only as a supplement to (4).

KEYWORDS: automated deduction, computer proofs, unification, second order, Otter

1. Predicate Abstraction

Should we allow the formation of new predicates by λ-abstraction, such as λy. P (x, y)? This is used in Otter2 (5). It is, however, not necessary to build this into the syntax of lambda logic. Indeed, omitting it offers greater flexibility: we can then selectively allow predicate abstraction over certain predicates, while not allowing it over others. To allow predicate abstraction over P, include a function symbol χ_{P} and an axiom expressing that χ_{P} is the characteristic function of P.

5. Proof of Theorem 5.3

We repeat the statement of the theorem and then give a complete proof; (4) gives only a sketch.

Theorem 5.3 (Axiomatization of first-order theorems): Let T be a first order theory, and let A be a first order sentence. Then T proves A in lambda logic if and only if for some positive integer n, T plus “there exist n distinct things” proves A in first order logic.

Proof. First suppose A is provable from T plus “there exist n distinct things”. We show A is provable in lambda logic, by induction on the length of the proof of A. Since lambda logic includes first order logic, the induction step is rivial.

∗Research supported by NSF grant number CCR-0204362.

Lambda Logic

For the basis case we must show that lambda logic proves “there exist n distinct things” for each positive integer n. The classical constructions of numerals in lambda calculus produce infinitely many distinct things. However, it must be checked that their distinctness is provable in lambda logic. Defining numerals as on p. 130 of (1) we verify by induction on n that for all m < n, ⌈m⌉ ≠ ⌈n⌉ is provable in lambda logic. If m < n + 1 then either m = n, in which case we are done by the induction hypothesis, or m = n. So what has to be proved is that for each n, lambda logic proves ⌈n⌉ ≠ ⌈n + 1⌉. This in turn is verifiable by induction on n.

Conversely, suppose that A is not provable in T plus “there exist n distinct things” for any n. Then by the completeness theorem for first order logic, there is an infinite model M of ¬A; indeed we may assume that M has infinitely many elements not denoted by closed terms of T. We will show that M can be expanded to a lambda model M̂ satisfying the same first order formulas, by defining arbitrarily the required operation λ^{∗} on M-terms, and then inductively defining relations E(x, y) and Ap_{M} to serve as the interpretations of equality and Ap in M̂.

To do this we define the relation Ap_{M} and a binary relation E on M by simultaneous induction. Ap_{M} will serve as the interpretation of Ap and E will serve as the interpretation of equality.^{†} Since M is infinite we can define an element 0 and a pairing function ⟨a, b⟩ on M in such a way that the interpretations of the losed terms of T are never pairs, and 0 is not a pair. Define < a, b, c >=< a, < b, c >>, etc. Define the successor of x to be s(x) =< 0, x >, and define the “numeral” m̄ inductively by ¯0 = 0 and m̄ + 1 = s(m̄). Henceforth we drop the bars, writing for example ⟨1, k⟩ instead of ⟨¯1, k̄⟩. An element of the form < 1, j, k > will be used as an “index” of the k-th function symbol of arity j in T, which we denote by f_{k}^{j}.

Tuples are defined from pairs by ⟨x_{1}, …, x_{n+1}⟩ = ⟨⟨x_{1}, …, x_{n}⟩, x_{n+1}⟩. The members of a tuple ⟨x_{1}, …, x_{n} are the x_{i} for i = 1, …, n. When y and w are two tuples of length at least m we write E_{m}(y, w) for the conjunction of the formulas E(y_{i}, w_{i}) for i ≤ m.

To produce a λ-model we must define an operation λ^{∗}, which takes a variable and an M-term. An M-term (as explained in (1), p. 86 ff.), is a term with “parameters from M”; more precisely, a closed term in a language containing a constant c_{a} for each element a of M. A convenient notation for M-terms is t[y], where y is a tuple of elements of M whose length is the number of free variables of t. This means the following: if x_{1}, …, x_{n} are the free variables of t, in order of their occurrence, then t[y] is t[x_{i} := c_{y_{i}}]. We also need the following notation: t[y, x] where x is a variable, and y is a tuple of elements of M whose length is the number of free variables of t different from x, means the following: if x_{1}, …, x_{n}

†If one insists on interpreting equality as identity instead of by an equivalence relation, one may use the equivalence classes of E as the elements of the model.

M. J. Beeson

are the free variables of t different from x, in order of their occurrence, then t[y] is t[x_{i} := c_{y_{i}}]. Note that x may or may not occur free in t.

The operation λ^{∗} is given by

λ^{∗}(x, t[y, x]) :=< 2, j,^{⌈}t^{⌉}, y >

where y is a tuple whose length is the number of free variables of λx. t, and x is the j-th variable, and ^{⌈}t^{⌉} is the (numeral for the) Gödel number of the closed term t. The definitions of Ap, E, and the interpretation t[y]_{M} of each M-term t[y] are given in one simultaneous inductive definition. The inductive conditions are as follows. In (iii) and (iv), m is the number of free variables of t.

(i) E(x, y) if x = y.

(ii) E(λ^{∗}(x, t[y, x]), λ^{∗}(z, t[x := z][y])).

(iii) Ap_{M}(λ^{∗}(x, t[y, x]), r_{M}) = t[x := r][y]_{M}.

(iv) E(λ^{∗}(x, t[y, x]), λ^{∗}(x, s[w, x]) if E(t[x := a][y]_{M}, s[x := a][w_{M}), and E_{m}(y, w) where a is a the first constant not occurring in t or s.

(v) E(Ap_{M}(a, b), Ap_{M}(c, d)) if E(a, c) and E(b, d).

(vi) Ap(a, b)_{M} = Ap_{M}(a_{M}, b_{M}).

(vii) E(f(t[y])_{M}, f(s[w])_{M}) if E(t[y]_{M}, s[w]_{M}), and similarly for several variables x.

(viii) (λx. t[y, x])_{M} = λ^{∗}(x, t[y, x]).

(ix) f(x)_{M} = f_{M}(x_{M}) and similarly for several variables x.

(x) (c_{a})_{M} = a where c_{a} is the constant for a.

(xi) E(a, c) if E(a, b) and E(b, c).

Since E and Ap occur only positively in these clauses, this is a legitimate inductive definition. We interpret equality in M as the relation E. For each predicate P of arity n in the language of T, we define a relation P̂ on M by

P̂(x_{1}, …, x_{n}) := M ⊧ P (y_{1}, …, y_{n}) ∧ E_{n}(x, y)

and we define M̂ ⊧ P (x_{1}, …, x_{n}) if and only if P̂(x_{1}, …, x_{n}).

We start with the following lemma: if E(r, q) then E(t[x := r], t[x := q]) for terms t, q, and r. This is proved by induction on the complexity of the M-term t. When t begins with λ or Ap, the corresponding induction step follows from (iv) and (v). When t begins with a function symbol f, we use (vii). When t is atomic, either it is a constant c_{a} for an element a = y_{1} of M, in which case there is nothing to prove, or else it is a variable, in which case we have to prove that E(r, q) from the assumption E(r, q), which is immediate.

We next verify the substitutivity of equality, namely: if E(r, s) and M̂ ⊧ A[x := r] then M̂ ⊧ A[x := s], where A is a formula of lambda logic with constants for elements of M. We prove this by induction on the complexity of A. Since substitution for free variables commutes with the logical connectives and quantifiers, only the case of atomic A needs a proof. If A is an equality t = q, then A[x := r] is t[x := r] = q[x := r] and A[x := s] is t[x := s] = q[x := s]. By the lemma we have t[x := r] = t[x := s] in M, and q[x := r] = q[x := s]. Assume M̂ ⊧ A[x := r]. Then by (xi) we have M̂ ⊧ t[x := s] = q[x := s]. The remaining case is when A is an atomic formula P (x) (x can be several variables.) This is taken care of by the definition of P̂ above.

Because of (ii) and (iii), axioms (α) and (β) are satisfied. Now to verify axioms (ξ). Let t[y] be an M-term, i.e. a term with constants for elements y of M substituted for its free variables. Suppose M̂ ⊧ ∀x(t[y]x = s[y]x). Then let c be the first constant not occurring in t or s; we have M̂ ⊧ t[x := c] = s[x := c]. Then by (iv), we have M̂ ⊧ λx. t[y] = λx. s[y]. Hence (ξ) holds in M.

We have now proved that M̂ is a model of lambda logic. We still must prove it satisfies the theory T in first order logic. This follows from the following lemma: For each M-formula A(x_{1}, …, x_{n}) with n parameters from M, we have M̂ ⊧ A(x) if and only if there exists y with E_{n}(x, y) and M ⊧ A(y). To prove the lemma: The case when A is an atomic formula P (x) is true by definition of P̂. The case of an atomic formula t = q follows from what has been proved above. The proof is completed by induction on the complexity of A; the quantifiers do not offer any difficulty since the carrier sets of M and M̂ are the same. That completes the proof of the theorem.

9. Lambda Completeness for LPT

Completeness of first-order LPT was proved in (3), by reduction of LPT to ordinary first order logic. Incidentally, completeness was also proved for intuitionistic LPT, which does not concern us here.

Here we provide the proof of theorem 9.1 of (4).

Theorem 9.1 (Lambda Completeness Theorem for LPT): Let T be a consistent theory in partial lambda logic. Then T has a partial lambda model.

Proof. Again we imitate the Henkin proof of completeness for first order logic. If T does not contain infinitely many constant symbols, we begin by adding them; this does not destroy the consistency of T since in any proof of contradiction, we could replace the new constants by variables not occurring elswhere in the proof. We construct the “canonical structure” M for a theory T. The elements of M are equivalence classes of closed terms of T under the equivalence relation of provable equality: t ∼ r iff T ⊢ t = r. But now, we take only those closed terms t for which T proves t ↓; that ensures the validity of the axiom x = x, and of the axioms x ↓ for variables x and of the axioms c ↓ for constants c. Let [t] be the equivalence class of t. We define the interpretations of constants, function symbols, and predicate symbols in M as follows:

c^{M} = [c]
f^{M}([t_{1}], …, [t_{n}]) = [f(t_{1}, …, t_{n})]
P^{M}([t_{1}], …, [t_{n})] = [P (t_{1}, …, t_{n})]

In this definition, the right sides depend only on the equivalence classes [t_{i}] (as shown in (6), p. 44). The atomic formula t ↓ is satisfied in M if and only if T proves t ↓. It follows by induction on the complexity of the closed first-order term t that if T proves t ↓ then the interpretation t^{M} of t in M is the equivalence class [t] of t. The strictness axiom for first order function symbols is used in the induction step, so this does not apply to terms containing Ap unless we have strictness for Ap.

Exactly as in (6) one then verifies that M is a first order model of T in the sense of LPT. Thus the completeness theorem for first order LPT (with strictness) is proved (again).

To turn M into a λ-model, we must define λ^{∗}(x, t), where t is an M-term, i.e. a closed term with parameters from M. The “parameters from M” are constants c_{[}q], where [q] is the equivalence class of a closed term q of T. If [t] is the equivalence class of an M-term t, let [t]^{∘} be a closed term of T obtained from t by replacing each constant c_{[}q] by some closed term q in the equivalence class [q]. Which closed term we select does not affect the equivalence class [t]^{∘}. In other words, [t]^{∘} is a well-defined operation on equivalence classes.

We define λ^{∗}(x, t) = [λx. [t]^{∘}]. Because of the axiom λx. t ↓, λ^{∗}(x, t) is indeed defined for M-terms t. We must show that the value depends only on the equivalence class [t]. Suppose T proves t = s. Then by axiom (xi), T proves λx. [t] = λx. [s].

We verify that the axioms of partial lambda logic hold in M. First, the beta axiom: Ap(λx. t, r) ≅ t[x := r]. It suffices to consider the case when t has only x free. Suppose that the left hand side is defined in M. Its interpretation is the equivalence class of Ap(λx. t, r). By axiom (β), the right side is provably equal to the left side, so it is defined in M, and its interpretation is the class of t[x := r]. On the other hand if the right hand side is defined in M, then it is provably equal to the left side and so both are defined and equal in M. This verifies axiom (β).

Now for axiom (ξ). Suppose t and s are closed terms defined in M, and Ap(t, x) ≅ Ap(s, x) is valid in M. Then for each closed term r such that T proves r ↓, we have tr provably equal to sr. Since T contains infinitely many constant symbols, we can select a constant c that does not occur in t or s, so tc = sc is provable. Replacing the constant c by a variable in the proof, tx = sx is provable. Hence by axiom (ξ), λx. t = λx. s is probable, and hence that equation holds in M. In verifying axiom (ξ), it suffices to consider the case when s and t are closed terms. The axiom (α) holds in M since it simply asserts the equality of pairs of provably equal terms. The axiom T ≠ F holds since T does not prove T = F, because T is consistent. That completes the proof.

References

1. Barendregt, H., The Lambda Calculus: Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics 103, Elsevier Science Ltd. Revised

Lambda Logic

edition (October 1984).

2. Beeson, M., Foundations of Constructive Mathematics, Springer-Verlag, Berlin Heidelberg New York (1985).

3. Beeson, M., Proving programs and programming proofs, in: Barcan, Marcus, Dorn, and Weingartner (eds.), Logic, Methodology, and Philosophy of Science VII, proceedings of the International Congress, Salzburg, 1983, pp. 51-81, North-Holland, Amsterdam (1986).

4. Beeson, M., Lambda Logic, submitted to IJCAR2004

5. Beeson, M., Otter Two System Description, submitted to IJCAR 2004.

6. Shoenfield, J. R., Mathematical Logic, Addison-Wesley, Reading, Mass.