Proof Search in the Intuitionistic Sequent Calculus

N. Shankar^{∗} Computer Science Laboratory SRI International Menlo Park, CA 94025 email: shankar@csl.sri.com

November 8, 1991

Abstract

The use of Herbrand functions (more popularly known as Skolemization) plays an important role in classical theorem proving and logic programming. We define a notion of Herbrand functions for the full intuitionistic predicate calculus. The definition is based on the view that the proof-theoretic role of Herbrand functions (to replace universal quantifiers), and of unification (to find instances corresponding to existential quantifiers), is to ensure that the eigenvariable conditions on a sequent proof are respected. The propositional impermutabilities that arise in the intuitionistic but not the classical sequent calculus motivate a generalization of the classical notion of Herbrand functions. Proof search using generalized Herbrand functions also provides a framework for generalizing logic programming to subsets of intuitionistic logic that are larger than Horn clauses. The search procedure described here has been implemented and observed to work effectively in practice. The generalization of Herbrand functions can also be applied to sequent calculi formalizations of logics other than intuitionistic predicate calculus.

1 Introduction

Proof search is an effective way to do automated theorem proving since there is more meaningful information in a proof or a failed proof than there is in a theorem or a failed conjecture. Intuitionistic proofs are interesting because they contain more information than the corresponding classical proofs. Intuitionistic logics can be shown to contain classical logic via Gödel’s double-negation interpretation [Göd86b]. However, proof search (and theorem proving) is significantly more difficult for the intuitionistic predicate calculus than for the classical predicate calculus. There are no convenient normal forms such as the prenex, conjunctive, disjunctive forms.

This paper describes an effective technique for carrying out automated proof search in the intuitionistic sequent calculus. Sequent calculi are an excellent foundational medium for studying the mathematics of proof search for several reasons. There is a vast body of proof-theoretic research on sequent calculi and the significant metatheorems turn out to be simpler in the context of sequent calculi. Many other proof search techniques such as the tableau and matrix methods can be viewed as optimizations of sequent calculus proof search and the sequent calculus makes it possible to study these optimizations in their full generality. The technique described here is actually extremely general and can be applied to proof search in any sequent calculus with conventional quantifier rules and a cut-elimination theorem. The technique is described just for the intuitionistic calculus in order to keep the exposition concrete.

∗Part of this work was performed while the author was at Stanford University and was funded by NSF Grant No. CCR-8718605. The preparation of this paper has been supported by the SRI International Computer Science Laboratory.

Proof search techniques for classical sequent calculi are fairly well-known [BB74, Bow82, KW84]. These techniques work by Herbrandizing^{1} the goal sequent to eliminate quantifiers and then use propositional reasoning and unification to carry out the proof search on the resulting quantifier-free sequent. Consider the attempt to search for a proof of the following sequent which is unprovable in classical logic:

(∀y: (∃x: p(x, y))) ⊢ (∃x: (∀y: p(x, y))).

In its Herbrandized form, the quantiers of existential strength have been replaced by variables (to be instantiated during proof search) and the quantifiers of universal strength have been replaced by terms, f(u) and g(v) where f and g are newly chosen. The result is:

p(f(u), u) ⊢ p(v, g(v)).

Here, f and g are the Herbrand functions, and u and v are called the Herbrand variables. The Herbrand terms f(u) and g(v) mention only the Herbrand variables corresponding to the surrounding quantifiers of existential strength. The propositional rules of Gentzen’s sequent calculus are applied backwards, i.e., from conclusion to premise(s). A branch of the proof is successfully terminated when a formula to the right of the sequent arrow unifies with a formula to the left of the sequent arrow. The resulting unifier is propagated to the next remaining branch and the process is repeated. Proof search on the example above fails because p(f(u), u) and p(v, g(v)) do not unify.^{2}

The above system of proof search has several advantages. Proof search is transparent, since it closely follows the proof rules of the sequent calculus. User interaction becomes more manageable. The choice of the term to be existentially generalized is postponed to the axiom case where the term can be constructed by means of unification. This means that there is less backtracking and less wasted effort in constructing a proof. In fact in the classical case, there is backtracking only on the selection of unifiers and not on the order of the proof steps. It is worth emphasizing this point: naive sequent calculus proof search without the use of Herbrand functions would be entirely impractical due to the amount of backtracking involved.

The present paper demonstrates that the above classical sequent based method can be adapted for theorem proving in the intuitionistic predicate calculus. The modifications require a careful proof-theoretic analysis of the role of Herbrand functions and variables, and of unification in proof search [Her67]. The crucial aspect of our proof-theoretic approach is the observation that Herbrand functions along with unification, serve to enforce the eigenvariable conditions on a sequent calculus derivation. The approach of Herbrandizing the goal formula prior to proof search does not work for nonclassical calculi such as the intuitionistic one. Herbrand functions have to be introduced during the proof search. One obvious approach to introducing a Herbrand function f corresponding to universal quantifier steps is to make the Herbrand term f(u_{1}, …, u_{n}) depend on all the Herbrand variables u_{1}, …, u_{n}, introduced in the existential quantifier steps in the previous steps of the proof search. This approach^{3} does take the guesswork out of discovering the term to be existentially generalized but has no other advantage over nondeterministically guessing the entire proof. What is missing is the ability to also ignore the order of the quantifier steps during the proof search. As an example, consider the use of this technique for proof search on the (classically and intuitionistically) provable sequent

1Skolemization is the process of eliminating quantifiers from a sentence so that free variables replace (essentially)

universally quantified variables, and Skolem terms of the form f(u_{1}, …, u_{n}) replace (essentially) existentially quantified variables that are within the scope of the universal quantifiers binding the u_{i}. A sentence is satisfiable iff the universal closure of its Skolemized form is satisfiable. The Herbrandized form of a sentence is the Skolemization of its negation. It is also the case that Herbrand and Gentzen deserve the credit for the proof-theoretic insights, whereas Skolem paid scant attention to proof theory and missed claiming important results such as the completeness of first-order logic.

2The actual explanation of proof search is a little more complicated since it needs to account for the copying of formulas corresponding to the use of the contraction rule in a proof. Proof search on the formula, (∃x: (∀y: A(x) ⊃ A(y))), is illustrative of the need for copying, renaming Herbrand variables, etc.. The examples chosen in this paper skirt these issues. We hope to discuss the extremely rich subject of classical proof search in a future paper.

(∃x: (∀y: p(x, y))) ⊢ (∀y: (∃x: p(x, y))).

If proof search on this sequent proceeds by first applying the left quantifier rules and then the right quantifier rules, we would arrive at the sequent p(a, y) ⊢ p(x, f(y)) where unification fails due to the occurs-check as a result of the spurious dependency between f and y. This form of Herbrand function introduction would make proof search hopelessly inefficient since it could require backtracking over all the possible orders in which the quantifier steps could occur. Our observation is that a Herbrand term does not have to depend on all the currently active Herbrand variables but only on a minimal set of these variables. The set of these Herbrand variables can be computed using the impermutabilities between the sequent calculus rules. The use of Herbrandization to record just the impermutabilities in the intuitionistic sequent calculus reduces (but clearly does not eliminate) the amount of backtracking since the relative order of the permutable inferences in the proof search are rendered irrelevant. We show how the unifier returned by a successful proof search can be used to derive the order of introduction of quantifier rules in order to to construct a correct sequent calculus proof by permuting the propositional proof returned by the search procedure. We can also show that the the dependencies between Herbrand functions and variables cannot (in a sense) be further minimized since this would make the search procedure unsound. Our results also indicate which classes of formulas can and cannot be Herbrandized initially as can be done with classical logic. For example in classical logic, since all the non-quantifier rules can be permuted, Herbrandization is a sound step in proof search. We can also demonstrate the failure of the Herbrand theorem for heriditary Harrop sentences [MNPS91].

There are a number of results in the literature directed at mechanical theorem proving for intuitionistic logic. We list only a few of these below. Mints [Min88] describes a resolutionstyle proof method for intuitionistic logic and a general technique for deriving resolution-style systems from sequent calculi. Beeson [Bee88], for example has implemented a Prolog proof search procedure called gentzen for an intuitionistic sequent calculus. Felty and Miller [FM88] have written a λ-Prolog procedure for proof search in the intuitionistic sequent calculus that maintains the eigenvariable conditions through the use of higher-order unification and hereditary Harrop program clauses [MNPS91, NM90]. The procedure we describe has a significant efficiency advantage over the approaches of Beeson, and Felty and Miller, since it postpones commitments on the order of introduction of certain quantifiers until the terminal nodes of the search tree are reached. Wallen [Wal90] uses Gödel’s translation [Göd86a] of intuitionistic logic into the modal logic S4 to define a matrix proof procedure for intuitionistic logic that employs string unification to ensure that the introduction rules for S4 modalities are respected. While Wallen’s method is an ingenious and effective one, the translation into S4, whether implicit or explicit, complicates the intuitive reading of the given intuitionistic formula and its proof. Pym and Wallen [PW90] present an approach to proof search in an intuitionistic type theory that is similar to our approach but they do not exploit Herbrand functions to encode impermutabilities during the proof search.

3The technique of introducing Herbrand functions in this manner is fairly well-known in automated reasoning.

Fitting [Fit90] describes this technique as applied to tableau systems.

2 Proof Theoretic Background

We first fix some of the syntax. The alphabet (along with the metavariable conventions) consists of

• the logical symbols: ¬, ⊃, ∨, ∧, ∀, ∃;

• the punctuation symbols: ‘(’, ‘,’, ‘:’, ‘)’;

• the variable symbols represented by the metavariables x, y, z;

• the function symbols (with arity) represented by f, g, h;

• the constant symbols represented by c, d, e;

• the predicate symbols (with non-negative arity) represented by p, q, r;

• the parameters represented by a, b.

A term is either a constant, a variable or of the form f(t_{1}, …, t_{n}), where f is an n-ary function symbol and t_{1}, …, t_{n} are terms. The metavariables s and t range over terms. An atomic formula is an n-ary predicate symbol followed by n terms. A formula is either an atomic formula or of the form ¬A, A ⊃ B, A ∨ B, A ∧ B, (∀x:A), (∃x: A), where A and B are smaller formulas and x is a variable. A sequent is of the form Γ ⊢ Δ, where Γ and Δ are multisets of formulas. If Γ is of the form A_{1}, …, A_{m} and Δ is of the form B_{1}, …, B_{n}, then the sequent Γ ⊢ Δ can be interpreted as

A_{1} ∧ … ∧ A_{m} ⊃ B_{1} ∨ … ∨ B_{n}

where the empty conjunction is taken to be logically true, and the empty disjunction is logically false.

The notions of positive and negative occurrences of subformulas in a formula and in a sequent should be clear. A positive occurrence of ∃ or a negative occurrence of ∀ is labelled an existential quantifier. Correspondingly, a positive ∀ occurrence or a negative ∃ occurrence is an universal quantifier. So existential and universal quantification refer to the strengths of the quantification and not to the quantifier symbol that is used.

It should be noted that Γ and Δ are viewed as (possibly empty) multisets of formulas rather than lists or sets. Both Γ, A and A, Γ represent the multiset union of {A} and Γ, and Γ_{1}, Γ_{2} represents the multiset union of Γ_{1} and Γ_{2}. An additional piece of syntax is required for these rules: terms are extended to include parameters a, b, used in the quantifier rules below.

It is useful to present the sequent calculi for both classical logic, called LK, and for intuitionistic logic, called LJ [Sza69]. The presentation of LK in Figure 2 is essentially the same as Kleene’s G3 [Kle52a].

Figure 2 displays the rules for LJ and these are similar to those of LK with the important restriction that the right hand side of any sequent in a proof can contain at most one formula.

A proof using these rules of LK or LJ is a tree rooted from below by the conclusion sequent, where the leaf sequents are all axioms, and each non-leaf sequent is derived from its premise sequents by a rule application. The systems LK and LJ have some important properties [Kle52a, Sza69].

Proposition 2.1 (Cut Elimination) The Cut rule is redundant in both LK and LJ:

1. If Γ ⊢_{LK} Δ, then Γ ⊢_{{LK−Cut}} Δ.

2. If Γ ⊢_{LJ} Δ, then Γ ⊢_{{LJ−Cut}} Δ.

Left  Right

\overline{Γ, A ⊢ A, Δ} ^{(Ax)}

\frac{Γ, ¬A ⊢ A, Δ}{Γ, ¬A ⊢ Δ} ^{(¬ ⊢)}  \frac{Γ, A ⊢ ¬A, Δ}{Γ ⊢ ¬A, Δ} (⊢ ¬)
\begin{matrix}\underline{Γ, (A ⊃ B), B ⊢ Δ  Γ ⊢ A, Δ} & (⊃⊢) \\ Γ, (A ⊃ B) ⊢ Δ \end{matrix}  \frac{Γ, A ⊢ B, (A ⊃ B), Δ}{Γ ⊢ (A ⊃ B), Δ} (⊢⊃)
\begin{matrix}\underline{Γ, (A ∨ B), A ⊢ Δ  Γ, (A ∨ B), B ⊢ Δ} & (∨ ⊢) \\ Γ, (A ∨ B) ⊢ Δ \end{matrix}  \frac{Γ ⊢ A, B, (A ∨ B), Δ}{Γ ⊢ (A ∨ B), Δ} (⊢ ∨)
\frac{Γ, (A ∧ B), A, B ⊢ Δ}{Γ, (A ∧ B) ⊢ Δ} ^{(∧ ⊢)}  \begin{matrix}\underline{Γ ⊢ A, (A ∧ B), Δ  Γ ⊢ B, (A ∧ B), Δ} & (⊢ ∧) \\ Γ ⊢ (A ∧ B), Δ \end{matrix}

\begin{matrix}\underline{Γ ⊢ C, Δ Γ, C ⊢ Δ} & Cut(C) \\ Γ ⊢ Δ \end{matrix}

\frac{Γ, (∀x: A), A\{t/x\} ⊢ Δ}{Γ, (∀x: A) ⊢ Δ} ^{(∀ ⊢)}  \frac{Γ ⊢ A\{a/x\}, (∀x: A), Δ}{Γ ⊢ (∀x: A), Δ} (⊢ ∀)^{∗}
\frac{Γ, (∃x: A), A\{a/x\} ⊢ Δ}{Γ, (∃x: A) ⊢ Δ} ^{(∃ ⊢)^{∗}}  \frac{Γ ⊢ A\{t/x\}, (∃x: A), Δ}{Γ ⊢ (∃x: A), Δ} (⊢ ∃)

∗: a not free in Γ, Δ (eigenvariable condition).

Figure 1: Rules for LK

Note that |Δ| ≤ 1.

Left  Right

\overline{Γ, A ⊢ A} ^{(Ax)}

\frac{Γ, ¬A ⊢ A}{Γ, ¬A ⊢ Δ} ^{(¬ ⊢)}  \frac{Γ, A ⊢ ¬A}{Γ ⊢ ¬A} (⊢ ¬)
\begin{matrix}\underline{Γ, (A ⊃ B), B ⊢ Δ  Γ ⊢ A} & (⊃⊢) \\ Γ, (A ⊃ B) ⊢ Δ \end{matrix}  \frac{Γ, A ⊢ B}{Γ ⊢ (A ⊃ B)} (⊢⊃)
\begin{matrix}\underline{Γ, (A ∨ B), A ⊢ Δ  Γ, (A ∨ B), B ⊢ Δ} & (∨ ⊢) \\ Γ, (A ∨ B) ⊢ Δ \end{matrix}  \frac{Γ ⊢ A}{Γ ⊢ (A ∨ B)} (⊢ ∨_{1})  \frac{Γ ⊢ B}{Γ ⊢ (A ∨ B)} (⊢ ∨_{2})
\frac{Γ, (A ∧ B), A, B ⊢ Δ}{Γ, (A ∧ B) ⊢ Δ} ^{(∧ ⊢)}  \begin{matrix}\underline{Γ ⊢ A  Γ ⊢ B} & (⊢ ∧) \\ Γ ⊢ (A ∧ B) \end{matrix}

\begin{matrix}\underline{Γ ⊢ C Γ, C ⊢ Δ} & Cut(C) \\ Γ ⊢ Δ \end{matrix}

\frac{Γ, (∀x: A), A\{t/x\} ⊢ Δ}{Γ, (∀x: A) ⊢ Δ} ^{(∀ ⊢)}  \frac{Γ ⊢ A\{a/x\}}{Γ ⊢ (∀x: A)} (⊢ ∀)^{∗}
\frac{Γ, (∃x: A), A\{a/x\} ⊢ Δ}{Γ, (∃x: A) ⊢ Δ} ^{(∃ ⊢)^{∗}}  \frac{Γ ⊢ A\{t/x\}}{Γ ⊢ (∃x: A)} (⊢ ∃)

∗: a not free in Γ, Δ (eigenvariable condition condition). Figure 2: Rules for LJ

The cut rule is the only rule in which there is a formula appearing in the premise sequent(s) that is not a subformula of its conclusion sequent. Substituting the term t for the free occurrences of x in A yields A{t/x}, where the bound variables in A are renamed to avoid any clashes. Note that A{t/x} for any t is taken to be a subformula of both (∀x: A) and (∃x: A). Cut-free proofs therefore have the subformula property, i.e., every formula occurrence in the proof is a subformula of all the sequents appearing below it, and in particular, of the conclusion sequent of the proof. Each of the non-cut rules introduces exactly one formula into the conclusion sequent, the principal formula of the rule.

Proposition 2.2 (Subformula Property) The formulas in a sequent in a cut-free LK or LJ proof are all subformulas of the conclusion sequent of the proof.

The subformula property can be used to argue the nonprovability of ⊢ A ∨ ¬A in LJ since the final rule of inference in a cut-free proof must be (⊢ ∨), but neither of the premises of the rule application are provable in LJ.

Proposition 2.3 (Permutability) The order in which the rules occur in a cut-free LK proof can be permuted without changing the conclusion of the proof, provided:

1. The eigenvariable conditions are not violated.

2. The subformula property is not violated.

In particular, the order of the rules in a propositional proof is permutable so long as the subformula property is maintained. For instance, the rules in the proof

\underline{\begin{matrix}\underline{A, B ⊢ B A, B ⊢ A} & (⊢ ∧) \\ A, B ⊢ B ∧ A \end{matrix}}_{(∧ ⊢)} ; A ∧ B ⊢ B ∧ A

can be permuted as

\underline{\begin{matrix}A, B ⊢ B & A, B ⊢ A \\ \overline{A ∧ B ⊢ B}^{(∧ ⊢)} & \overline{A ∧ B ⊢ A}^{(∧ ⊢)} \end{matrix}}_{(⊢ ∧)} ; A ∧ B ⊢ B ∧ A

There are certain additional impermutable pairs of inferences in LJ as will be described in Section 3 below. The properties of the sequent calculi play a significant role in justifying the proof search procedures.

3 Proof Search in LJ

In this section, we present and analyze a proof search predicate, Search, that searches for LJ proofs. We omit the details of classical proof search though we do make informal references to it.

To examine why intuitionistic proof search is different from classical proof search, we consider the following sentence that is classically provable but is not intuitionistically provable:

(∀x: (p(x) ∨ q)) ⊃ (q ∨ (∀x: p(x))).

A classical proof search would proceed by Herbrandizing this formula to form the sequent

⊢ (p(u) ∨ q) ⊃ (q ∨ p(c))

then applying the (⊢⊃) and (⊢ ∨) rule to get

(p(u) ∨ q) ⊢ q, p(c)

which by (∨ ⊢) reduces to the two subgoals

p(u) ⊢ q, p(c)
q ⊢ q, p(c).

The second of these subgoals is a propositional axiom. The first subgoal is established by instantiating the Herbrand variable u with the Herbrand constant c.

In searching for a sequent calculus proof as shown above, each application of a proof rule to transform a sequent matching the conclusion of the rule to the corresponding premises of the rule is termed a reduction.

We can attempt a similar proof search with the Herbrandized sentence using only the rules of LJ. Starting with

⊢ (p(u) ∨ q) ⊃ (q ∨ p(c))

we apply (∨ ⊢) to get the subgoals

p(u) ⊢ q ∨ p(c)
q ⊢ q ∨ p(c).

The first subgoal can be completed by applying (⊢ ∨_{1}) instantiating x with c. Applying (⊢ ∨_{2}) to the second subgoal reduces it to an axiom, and completes the proof search successfully.

Since we started with an intuitionistically unprovable sentence, there must be a flaw in the above approach to intuitionistic proof search that caused it to terminate successfully. The flaw is highlighted when we attempt to reconstruct the proof found by the search procedure as shown below:

\underline{\begin{matrix}p(a) ⊢ p(a) \\ \overline{p(a) ⊢ (∀x: p(x))} & (⊢ ∀) \\ \overline{p(a) ⊢ q ∨ (∀x: p(x))} & (⊢ ∨) \end{matrix} \begin{matrix}q ⊢ q \\ \overline{q ⊢ q ∨ (∀x: p(x))} & (⊢ ∨) \end{matrix}}_{(∨ ⊢)}

(∀x: (p(x) ∨ q)) ⊢ (q ∨ (∀x: p(x)))
\overline{⊢ (∀x: (p(x) ∨ q)) ⊃ (q ∨ (∀x: p(x)))}^{(⊢⊃)}

The above “proof” obviously violates the eigenvariable condition in the (⊢ ∀) step. The crucial observation however is that there is no way to repair this violation of the eigenvariable condition by changing the order of inferences in the proof. In the classical sequent calculus LK, it would be possible to change the order of the rules as required since (∨ ⊢) rule permutes above the (⊢ ∨) rule. The reordered LK proof does satisfy the eigenvariable condition. A similar reordering of inferences is not permitted in LJ since the only way to prove p(c) ∨ q ⊢ q ∨ p(c) is with the (∨ ⊢) rule applied below the (⊢ ∨) rule.

We therefore observe that the impermutability of certain pairs of inferences in LJ makes it incorrect to directly use Herbrandization for proof search. Our solution to this problem is to dynamically introduce Herbrand functions to replace universal quantifiers during the proof search so that the variables u_{1}, …, u_{n} in the Herbrand term f(u_{1}, …, u_{n}) can encode the propositional impermutabilities that arise in LJ proofs. In the above example, the corrected form of proof search proceeds as follows. We start with the sequent

⊢ (∀x: (p(x) ∨ q)) ⊃ (q ∨ (∀x: p(x)))

applying (⊢⊃) to get

(∀x: (p(x) ∨ q)) ⊢ (q ∨ (∀x: p(x)))

then introducing the Herbrand variable u corresponding to the (∀ ⊢) rule to get

p(u) ∨ q ⊢ (q ∨ (∀x: p(x))).

The (∨ ⊢) rule must then be applied to yield the subgoals

p(u) ⊢ (q ∨ (∀x: p(x)))
q ⊢ (q ∨ (∀x: p(x))).

The second of these subgoals is easily proved by applying the (⊢ ∨_{1}) rule. For the first subgoal, we clearly will apply the reduction corresponding to the (⊢ ∨_{2}) rule, but in doing so we note that the (∨ ⊢) rule might not permute above a (⊢ ∨) rule and the Herbrand variable u governs the (∨ ⊢) step. Therefore the Herbrand term corresponding to the (⊢ ∀) rule is introduced as

p(u) ⊢ p(f(u)).

Occurs-checking during unification ensures that the Herbrand variable u cannot be instantiated with a term containing f. In the above case, the proof search rightly fails since occurs-checking prevents u from being unified with f(u). There are of course other directions in which the above proof search could have proceeded but they all fail rather more easily. We will show that if a Herbrand variable u is instantiated with a term t containing a Herbrand function f, the proof structure returned by a successful proof search can always be permuted so that the existential quantifier corresponding to u can be introduced above the universal quantifier corresponding to f in order to satisfy the eigenvariable condition.

The restrictions on the succedent of LJ sequents leads to a number of impermutabilities that are not present in LK. Kleene [Kle52b] lists the basic impermutabilities along with examples of theorems whose LJ proofs can only be constructed with R1 above R2 (i.e., R1/R2). These are displayed in Figure 3. In each instance of R1/R2, the rule R2 cannot be permuted above the rule R1 in any proof of the corresponding example. It can be checked that for any pair of rules R1 and R2 not listed below, an occurrence of R2 can always be moved above an occurrence of R1 in an LJ proof.

We call the impermutabilities 4–11 the LJ impermutabilities since they are peculiar to LJ. We first observe certain uniformities in the LJ impermutabilities above:

• In any propositional impermutability R1/R2 above, the only Left rule in the R2 position is (∨ ⊢).

• The only Right rules are (⊢⊃) and (⊢ ¬).

• In both the cases (when R2 is either (⊢⊃) or (⊢ ¬)), R1 is either (⊃⊢) or (¬ ⊢).

These uniformities are exploited in the proof search procedure below. The proof search procedure is presented as a predicate that takes five arguments:

1. A (partially Herbrandized) sequent consisting of a set of zero or more antecedent forms and at most one succedent form. Each form is a pair [X: A] consisting of a formula A and the set X of governing Herbrand variables. The initial sequent to the proof search should not contain any free variables, and the set of governing variables in each form is empty.

R1/R2  Example
1. (∀ ⊢)/(⊢ ∀) (∀x: A(x)) ⊢ (∀x: (A(x) ∨ B))
2. (∀ ⊢)/(∃ ⊢)  (∀x: A(x)), (∃x: ¬A(x)) ⊢
3. (⊢ ∃)/(∃ ⊢) (∃x: (A(x) ∧ B)) ⊢ (∃x: A(x))
4. (⊃⊢)/(⊢⊃)  (A ⊃ ¬A) ⊢ (A ⊃ B)
5. (¬ ⊢)/(⊢⊃)  ¬A ⊢ (A ⊃ B)
6. (⊃⊢)/(⊢ ¬)  (A ⊃ ¬A) ⊢ ¬A
7. (¬ ⊢)/(⊢ ¬)  ¬A ⊢ ¬(A ∧ A)
8. (⊃⊢)/(∨ ⊢)  A ∨ B, A ⊃ B ⊢ B
9. (⊢ ∨)/(∨ ⊢)  (A ∨ B) ⊢ (B ∨ A)
10. (¬ ⊢)/(∨ ⊢)  (A ∨ B), ¬A ⊢ B
11. (⊢ ∃)/(∨ ⊢)  A(a) ∨ A(b) ⊢ (∃x: A(x))

Figure 3: Impermutabilities in LJ

2. A set of Herbrand variables, lvars, that govern any forms to which the (∨ ⊢) rule has been applied in the course of the proof search so far.

3. A set of Herbrand variables, rvars, that govern any forms to which the (⊢⊃) or (⊢ ¬) has been applied in the course of proof search so far.

4. The input unifier, which is initially the empty unifier.

5. The output unifier that is the outcome of the proof search.

The predicate Search(sequent; lvars; rvars; input; output) can then be described by a collection of Horn clauses. The search sequent is represented as Σ ⊢ Θ, where Σ is a (possibly empty) multiset of forms, and Θ contains at most one form. Sets of variables are represented by X, Y, L, R. Multisets of forms are represented by Σ, Θ, etc. Substitutions are represented by the letter U, V, W, etc. We omit the definition of Unify(A; B; U; V) while noting that V is required to be a unifier for A and B that extends U. That is, V is of the form U′ ∘ U for some substitution U′. If such a unifier does not exist, then the result V is No. The parameter U is not used in any essential way in the definition below, but does permit a variation of Search in which the unifier returned from one successful branch of the search can be given as the input to the other branch. The parameter U also turns out to be useful for the proof of completeness in Lemma 4.8. The relation Search can be defined inductively by the following scheme:

1. Unifier: Search(Σ ⊢ Θ; L; R; No; No).

2. Axiom:

Search([X: A], Σ ⊢ [Y: B]; L; R; U; V) if
Unify(A; B; U; V) and V ≠ No.

3. Negation:

(a) Left: Note that X is augmented with L ∪ R to encode the impermutabilities of the form (¬ ⊢)/R2.

Search([X: ¬A], Σ ⊢ Θ; L; R; U; V) if
Search([X: ¬A], Σ ⊢ [X ∪ L ∪ R: A]; L; R; U; V).

(b) Right: Note that R is augmented with X to encode the impermutabilities of the form R1/(⊢ ¬).

Search(Σ ⊢ [X: ¬B]; L; R; U; V) if
Search([X; B], Σ ⊢ ; L; X ∪ R; U; V).

4. Implication:

(a) Left: X is augmented with L ∪ R to encode the impermutabilities of the form (⊃⊢)/R2. The construction of the unifier V can be carried out in stages by renaming V in one subgoal and U in the other to both be W. The same applies to the left-disjunction and right-conjunction steps.

Search([X: (A ⊃ B)], Σ ⊢ Θ; L; R; U; V) if
Search([X: (A ⊃ B)], Σ ⊢ [X ∪ L ∪ R: A]; L; R; U; V),
and Search([X ∪ L ∪ R: B], [X: (A ⊃ B)], Σ ⊢ Θ; L; R; U; V).

(b) Right: R is augmented with X to encode the impermutabilities of the form R1/(⊢⊃).

Search(Σ ⊢ [X: (A ⊃ B)]; L; R; U; V) if
Search([X: A], Σ ⊢ [X: B]; L; X ∪ R; U; V).

5. Disjunction:

(a) Left: L is augmented with X to encode the impermutabilities of the form R1/(∨ ⊢).

Search([X: (A ∨ B)], Σ ⊢ Θ; L; R; U; V) if
Search([X: B], [X: (A ∨ B)], Σ ⊢ Θ; X ∪ L; R; U; V),
and Search([X: A], [X: (A ∨ B)], Σ ⊢ Θ; X ∪ L; R; U; V).

(b) Right: X is augmented with L to encode the impermutability (⊢ ∨)/(∨ ⊢).

Search(Σ ⊢ [X: (A ∨ B)]; L; R; U; V) if
Search(Σ ⊢ [L ∪ X: A]; L; R; U; V) and V ≠ No
or  Search(Σ ⊢ [L ∪ X: B]; L; R; U; V) and V ≠ No
otherwise V = No.

6. Conjunction: Since neither (∧ ⊢) nor (⊢ ∧) is involved in any impermutability, the ∧-steps behave normally.

(a) Left:

Search([X: (A ∧ B)], Σ ⊢ Θ; L; R; U; V) if
Search([X: A], [X: B], [X: (A ∧ B)], Σ ⊢ Θ; L; R; U; V).

(b) Right:

Search(Σ ⊢ [X: (A ∧ B)]; L; R; U; V) if
Search(Σ ⊢ [X: B]; L; R; U; V)
and Search(Σ ⊢ [X: A]; L; R; U; V).

7. Existential Quantifiers:

(a) Left:

Search([X: (∃x: A)], Σ ⊢ Θ; L; R; U; V) if
Search([X: A{x ← f(X)}], Σ ⊢ Θ; L; R; U; V),

where f is a new n-ary function symbol, and if X is {u_{1}, …, u_{n}} then f(X) represents f(u_{1}, …, u_{n}).

(b) Right: X is augmented with u since u now becomes a governing Herbrand variable, and

with L due to the impermutability (⊢ ∃)/(∨ ⊢).

Search(Σ ⊢ [X: (∃x: A)]; L; R; U; V) if

Search(Σ ⊢ [{u} ∪ L ∪ X: A{x ← u}]; L; R; U; V),

where u is a new Herbrand variable.

8. Universal Quantifiers:

(a) Left:

Search([X: (∀x: A)], Σ ⊢ Θ; L; R; U; V) if
Search([{y} ∪ X: A{x ← y}], [X: (∀x: A)], Σ ⊢ Θ; L; R; U; V),

where y is a new variable.

(b) Right:

Search(Σ ⊢ [X: (∀x: A)]; L; R; U; V) if
Search(Σ ⊢ [X: A{x ← f(X)}]; L; R; U; V),

where f, X, and f(X) are as in (∃ ⊢). The reader might wish to apply the procedure Search to the following sequents that are clas-

sically valid, but not intuitionistically. 1. (A ⊃ (∃x: B(x))) ⊢ (∃x: A ⊃ B(x)).

2. ¬(∀x: A(x)) ⊢ (∃x: ¬A(x)).

3. ((∀x: A(x)) ⊃ B) ⊢ (∃x: A(x) ⊃ B). The next step is to argue that Search is sound and complete.

4 Soundness and Completeness

Search is sound if whenever it returns a unifier other than No on a sequent, there is an LJ proof of that sequent. Search is complete if when given any sequent provable in LJ, Search nondeterministically returns a unifier (other than No). It is easy to see that Search is both sound and complete on the propositional part of LJ since it is a nondeterministic search procedure for cut-free proofs in this fragment.

For demonstrating completeness, we restrict the Herbrand functions to be taken from h_{1}, h_{2}, …, and to each h_{i} we associate the parameter a_{i}. We restrict LJ proofs to only contain parameters a_{i}. If Σ is a multiset of forms, let \underline{Σ} represent the corresponding multiset of formulas, but where any terms of the form h_{i}(…) in Σ have been replaced by the corresponding parameter a_{i}. Applying the substitution U to Σ yields the multiset of forms U(Σ).

Lemma 4.1 If Γ ⊢ Δ is provable in LJ, then for any multisets of forms Σ and Θ such that Γ is \underline{U(Σ)} and Δ is \underline{U(Θ)}, we can find a V distinct from No where Search(Σ ⊢ Θ; L; R; U; V).

Proof. By induction on cut-free LJ proofs of Γ ⊢ Δ. Note that L and R do not play any role in this proof. We consider only a single case of the proof.

In the (⊢ ∃) case, the given proof derives Γ ⊢ (∃x: A) from Γ ⊢ A{t/x}. The corresponding step in the search replaces (∃x: A) with A{u/x}. Let U in the induction hypothesis be replaced with U\{t/u\} so that \underline{U\{t/u\}([\{y\} ∪ L ∪ X: A\{u/x\}])} is just A\{t/x\} and it can be shown that the required V is provided by the induction hypothesis.

The other cases are similar

When all the forms in Σ and Θ are of the form [{}: A], and U is the empty substitution ∅ (which, of course, is idempotent), then \underline{U(Σ)} ⊢ \underline{U(Θ)} is just the original sequent, and we get the completeness theorem below, where \overline{Γ} represents the multiset of forms got by replacing each A in Γ with [{}: A].

Theorem 4.2 (Completeness) If Γ ⊢ Δ is provable in LJ, then there is a V distinct from No such that Search(\overline{Γ} ⊢ \overline{Δ}; L; R; ∅; V) holds.

The soundness argument is more delicate since it sheds light on the use of Herbrand functions. The goal is to show that if proof search succeeds on a sequent, then that sequent has a proof in LJ. The proof proceeds by constructing a proof search tree from a successful proof search and extracting an ordering on the quantifiers from the output unifier. We then show that the proof search tree can be permuted so as to respect the ordering on the quantifiers and that the resulting proof obeys the eigenvariable condition. Let Π be an LJ proof structure if it is an LJ proof that possibly violates the eigenvariable condition. A proof structure Π is hygienic in its use of parameter names if each parameter name a_{i} is associated with at most one quantifier step in Π.

Lemma 4.3 If Search(Σ ⊢ Θ; L; R; U; V) succeeds with V ≠ No, we can construct a corresponding hygienic LJ proof structure Π of \underline{V (Σ)} ⊢ \underline{V (Θ)}.

Proof. By induction on the computation corresponding to Search. We only deal with a single case.

Consider the (⊢ ∀) case when the induction hypothesis yields a proof structure Π_{1} for V (Σ) ⊢ V ([X: A{x ← h_{i}(X)}]) corresponding to Search(Σ ⊢ [X: A{x ← h_{i}(X)}]; L; R; U; V). Note that \underline{V ([X: A\{x ← h_{i}(X)\}])} is just \underline{V ([X: A\{x ← a_{i}\}])}. It is, however, possible for \underline{V (Σ)} to contain occurrences of a_{i} so that the proof tree below could violate the eigenvariable condition.

Π_{1}
⋮
\underline{\underline{V (Σ)} ⊢ \underline{V ([X: A\{x ← h_{i}(X)\}])}}_{(⊢ ∀)}
\underline{V (Σ)} ⊢ \underline{V ([X: (∀x: A)])}

The other cases are similar.

Given a proof structure Π, if a rule occurrence R1 occurs above a rule occurrence R2 in Π, then R1>R2 in Π iff either

• R1/R2 is one of the LJ impermutabilities 1–11

• the principal formula of R1 is a proper subformula of the principal formula of R2

• or there is a rule occurrence R3 such that R1>R3>R2

Lemma 4.4 If for any n, rule R1 occurs n steps above R2 in proof structure Π and R1≯R2 in Π, then the order of rules in Π can be permuted to yield a new proof structure Π′ with the same conclusion as Π, so that R2 occurs above R1 in Π′. If Π is hygienic, then there are no new pairs of quantifier rule occurrences that violate the eigenvariable condition in Π′.

Proof. By induction on n. The details are omitted.

In a hygienic proof structure, the only way to introduce new violations of the eigenvariable condition would be to invert the order of an existential quantifier step R1 that was above an universal quantifier step R2 in Π. This never happens since we would have R1>R2 in this case.

Lemma 4.5 Let U be an idempotent substitution such that for any i, the search sequent U(Σ) ⊢ U(Θ) contains (zero or more occurrences of) at most one term of the form h_{i}(X). If Search(Σ ⊢ Θ; L; R; U; V) returns an idempotent substitution V such that V ≠ No, then we can find an idempotent V′ such that Search(Σ ⊢ Θ; L; R; U; V′) and V′ contains at most one term of the form h_{i}(…) for any Herbrand function h_{i}, namely h_{i}(V′(X)).

Proof. By induction on the computation of Search taking care to return the most general idempotent unifier at every stage.

Denote the quantifier step corresponding to the Herbrand term h_{i}(X) as ∀_{i}, and the quantifer step corresponding to the Herbrand variables u_{j} as ∃_{j}.

Lemma 4.6 If ∀_{i} > ∃_{j} in a proof structure Π corresponding to a computation of Search, then u_{j} ∈ X for the Herbrand term h_{i}(X) introduced in the computation of Search.

Proof. By induction according to the definition of R1>R2.

Lemma 4.7 Given that U satisfies the conditions of Lemma 4.5, Search(Σ ⊢ Θ; L; R; U; V) holds, and V is an idempotent unifier, if u_{j} ∈ X for the Herbrand term h_{i}(X) in the computation of Search, then h_{i} does not occur in V (u_{j}).

Proof. Since by Lemma 4.5, we can ensure that V is such that h_{i} only occurs in the form h_{i}(V (X)) in V. If h_{i} occurs in V (u_{j}), then either V is not idempotent or contains an infinite term since no finite term can be a proper subterm of itself. Both these possibilities are ruled out.

Theorem 4.8 (Soundness) If \underline{U(Σ)} ⊢ \underline{U(Θ)} contains no parameters and Search(Σ ⊢ Θ; L; R; U; V) succeeds with V ≠ No, then \underline{V (Σ)} ⊢ \underline{V (Θ)} is provable in LJ.

Proof. By Lemma 4.3, we can derive a proof structure Π corresponding to Search(Σ ⊢ Θ; L; R; U; V). The proof of Theorem 4.8 is by induction on the number of pairs of quantifier rules that violate the eigenvariable condition in the proof structure Π. By Lemma 4.6, for any rule occurrences ∀_{i} and ∃_{j} in Π, if ∀_{i} > ∃_{j} then u_{j} ∈ h_{i}(X). Here h_{i}(X) is the Herbrand term introduced in the quantifier step ∀_{i}. By Lemma 4.7, h_{i} does not occur in V (u_{j}). Therefore, if h_{i} does occur in V (u_{j}), then ∀_{i} ≯ ∃_{j} and by Lemma 4.4, ∀_{i} can be permuted below ∃_{j} in Π to yield the proof structure Π′ with the same conclusion as Π.

Note that by Lemma 4.4, no new violations of the eigenvariable condition are introduced into Π′. We have thus succeeded in reducing the number of violations of eigenvariable condition and the induction hypothesis can be applied to the resulting proof structure Π′.

5 Observations

We have given a search procedure for proofs in the intuitionistic sequent calculus and proved it to be sound and complete. The key aspect of the search procedure is that we have generalized the notion of a Herbrand function so that the Herbrand term introduced for a universal quantifier depends only on those Herbrand variables corresponding to existential quantifier steps that cannot always be permuted above the universal quantifier step. This makes it possible to reconstruct the proof from the search structure and the unifier by permuting the search structure to reorder the quantifier steps to satisfy the order induced by the unifier.

The first observation is that both the search algorithm and proof can be generalized for any sequent calculus with a cut elimination theorem and conventional quantifier rules. The generalized procedure is to first identify the impermutabilities other than those given by the eigenvariable conditions in the given sequent calculus, and fashion a search procedure similar to Search to take note of these impermutabilities in forming Herbrand terms corresponding to universal quantifier steps. The above proof sketch would essentially apply without change. Note that in Search, we have taken advantage of certain patterns in the impermutability pairs to reduce the number of auxiliary parameters for accumulating Herbrand variables, and such optimizations may not always be possible.

The second observation is that we cannot improve upon this form of Herbrandization without examining the bodies of the quantified formulas themselves. In other words, if any Herbrand variables that are included in Herbrand terms in the search procedure above are dropped, then the procedure is unsound. It is possible to construct a counterexample of an unprovable sequent on which the search procedure would succeed. This does not preclude optimizations where the internal structure of the quantified formula is examined in order to rule out such counterexamples.

The generalization above explains why in classical logic, the goal sequent can be Herbrandized prior to proof search. In the classical sequent calculus, there are no impermutabilities other than those given by the eigenvariable conditions. So the Herbrand term corresponding to a universal quantifier depends on a Herbrand variable for an existential quantifier only if the universally quantified formula is a subformula of the existentially quantified formula. It might, of course, be necessary to make copies of formulas (while relabelling certain Herbrand variables) corresponding to the use of the contraction rule. Copying and relabelling are complicated issues that are beyond the scope of the current paper.

We can thus identify certain classes of formulas where Herbrandization will always succeed. These are classes of formulas that are defined solely by syntactic restrictions on the positive and negative occurrences of various connectives and quantifiers. Herbrandization will always work for a class of formulas that does not admit an LJ impermutability R1/R2, where an existential quantifier can govern the principal formula of R2, and the principal formula of R1 contains a universally quantified subformula. For example, Herbrandization fails for the class of hereditary Harrop formulas [MNPS91] since the unprovable formula

((∀x: p(x)) ⊃ q) ⊃ (∃y: (p(y) ⊃ q))

has the Herbrandized form

(p(c) ⊃ q) ⊃ (p(u) ⊃ q)

which is easily seen to be intuitionistically provable with c instantiating Herbrand variable u. This counterexample arises from the (⊃⊢)/(⊢⊃) impermutability permitted by the class of hereditary Harrop formulas.

6 Conclusion

Proof search in the intuitionistic sequent calculus is relevant to logic programming [MNPS91]. We have presented a notion of Herbrand functions that is appropriate for proof search in the intuitionistic sequent calculus. A proof search procedure was described and proved to be sound and complete. This procedure has been implemented in Common Lisp. The implementation optimizes Search in some small ways but there are a number of deeper optimizations that remain to be implemented. The extent to which Search can be optimized without destroying the transparency of the proof search deserves further exploration.

Acknowledgements: The ideas and comments of Michael Beeson, Jussi Ketonen, Lincoln Wallen, Gianluigi Bellin, Dale Miller, Patrick Lincoln, and Sam Owre have contributed to this presentation. Sol Feferman’s course on proof theory provided the initial stimulus for this work.

References

[BB74] W.W. Bledsoe and P. Bruell. A man-machine theorem-proving system. In Advance Papers of Third International Joint Conference on Artificial Intelligence. W.W. Bledsoe, 1974.

[Bee88] M. J. Beeson. Some applications of Gentzen’s proof theory in automated deduction. Manuscript, 1988.

[Bow82] K. A. Bowen. Programming with full first-order logic. In J. E. Hayes, D. Michie, and Y.-H. Pao, editors, Machine Intelligence 10, pages 421–440. Halsted Press, 1982.

[Fit90] M. Fitting. First-Order Logic and Automated Theorem Proving. Springer-Verlag, 1990.

[FM88] A. Felty and D. Miller. Specifying theorem provers in a higher-order logic programming language. In E. Lusk and R. Overbeek, editors, Ninth International Conference on Automated Deduction, pages 61–80, Argonne, Illinois, May 1988.

[Göd86a] K. Gödel. An interpretation of the intuitionistic propositional calculus. In S. Feferman, editor, Kurt Gödel: Collected Works Vol. 1, pages 301–303. Oxford University Press, 1986.

[Göd86b] K. Gödel. On intuitionistic arithmetic and number theory. In S. Feferman, editor, Kurt Gödel: Collected Works Vol. 1, pages 287–295. Oxford University Press, 1986.

[Her67] J. Herbrand. Investigations in proof theory. In J. van Heijenoort, editor, From Frege to Gödel: A Source Book of Mathematical Logic, pages 525–581. Harvard University Press, Cambridge, Mass., 1967.

[Kle52a] S. C. Kleene. Introduction to Metamathematics. North-Holland, Amsterdam, 1952.

[Kle52b] S. C. Kleene. Permutability of inferences in Gentzen’s calculi LK and LJ. Memoirs of the A.M.S., 10, 1952.

[KW84] J. Ketonen and R. Weyhrauch. A decidable fragment of predicate calculus. The Journal of Theoretical Computer Science, 32:297–307, 1984.

[Min88] G. Mints. Gentzen-type systems and resolution rules, Part I: Propositional logic. In P. Martin-Löf and G. Mints, editors, COLOG-88, Lecture Notes in Computer Science 417, pages 198–231. Springer-Verlag, 1988.

[MNPS91] D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.

[NM90] G. Nadathur and D. Miller. Higher-order Horn clauses. Journal of the ACM, 37(4):777– 814, 1990.

[PW90] D. J. Pym and L. A. Wallen. Investigations into proof-search in a system of first-order dependent function types. In M. E. Stickel, editor, 10th International Conference on Automated Deduction, pages 236–250. Springer-Verlag, 1990.

[Sza69] M. E. Szabo, editor. The Collected Papers of Gerhard Gentzen. North-Holland, 1969.

[Wal90] L. A. Wallen. Automated Proof Search in Non-Classical Logics. MIT Press, 1990.