Automated Theorem Proving

Frank Pfenning Carnegie Mellon University

Draft of November 12, 1999

Material for the course Automated Theorem Proving at Carnegie Mellon University, Fall 1999. This includes revised versions from the course notes on Linear Logic (Spring 1998) and Computation and Deduction (Spring 1997). Material for this course is available at

   http://www.cs.cmu.edu/~fp/courses/atp/.

Please send comments to fp@cs.cmu.edu

This material is in rough draft form and is likely to contain errors. Furthermore, citations are in no way adequate or complete. Please do not cite or distribute this document.

This work was supported by NSF Grants CCR-9303383 and CCR-9619684.

Copyright \begin{matrix}c \\ ◯ \end{matrix} 1999, Frank Pfenning \underline{ii}

Draft of November 12, 1999

Contents

1 Introduction 1

2 Natural Deduction 3 2.1 Intuitionistic Natural Deduction . . . . . . . . . . . . . . . . . . 5 2.2 Classical Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.3 Localizing Hypotheses . . . . . . . . . . . . . . . . . . . . . . . . 17 2.4 Proof Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 2.5 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

3 Sequent Calculus 29 3.1 Intercalation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3.2 Compact Proof Terms . . . . . . . . . . . . . . . . . . . . . . . . 35 3.3 Sequent Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 3.4 Cut Elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 3.5 Applications of Cut Elimination . . . . . . . . . . . . . . . . . . . 48 3.6 Proof Terms for Sequent Derivations . . . . . . . . . . . . . . . . 49 3.7 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52

4 Focused Derivations 55 4.1 Inversion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 4.2 Focusing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 4.3 Unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 4.4 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80

5 The Inverse Method 81 5.1 Forward Sequent Calculus . . . . . . . . . . . . . . . . . . . . . . 82 5.2 Negation and Empty Succedents . . . . . . . . . . . . . . . . . . 85 5.3 The Subformula Property . . . . . . . . . . . . . . . . . . . . . . 88 5.4 Naming Subformulas . . . . . . . . . . . . . . . . . . . . . . . . . 89 5.5 Forward Subsumption . . . . . . . . . . . . . . . . . . . . . . . . 91 5.6 Proof Terms for the Inverse Method . . . . . . . . . . . . . . . . 91 5.7 Inverse Focusing . . . . . . . . . . . . . . . . . . . . . . . . . . . 92 5.8 Inverse Focusing with Negation . . . . . . . . . . . . . . . . . . . 95 5.9 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 6 Resolution 99

6.1 Forward Sequent Calculus . . . . . . . . . . . . . . . . . . . . . . 99 6.2 Factoring . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104

7 Equality 107 7.1 Natural Deduction . . . . . . . . . . . . . . . . . . . . . . . . . . 107 7.2 Sequent Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . 110

Bibliography 117

Chapter 1

Introduction

Logic is a science studying the principles of reasoning and valid inference. Automated deduction is concerned with the mechanization of formal reasoning, following the laws of logic. The roots of the field go back to the end of the last century when Frege developed his Begriffsschrift^{1}, the first comprehensive effort to develop a formal language suitable as a foundation for mathematics. Alas, Russell discovered a paradox which showed that Frege’s system was inconsistent, that is, the truth of every proposition can be derived in it. Russell then devised his own system based on a type theory and he and Whitehead demonstrated in the monumental Principia Mathematica how it can serve as a foundation of mathematics. Later, Hilbert developed a simpler alternative, the predicate calculus. Gentzen’s formulation of the predicate calculus in a system of natural deduction provides a major milestone for the field. In natural deduction, the meaning of each logical connective is explained via inference rules, an approach later systematically refined by Martin-Löf. This is the presentation we will follow in these notes.

Gentzen’s seminal work also contains the first^{2} consistency proof for a formal logical system. As a technical device he introduced the sequent calculus and showed that it derives the same theorems as natural deduction. The famous Hauptsatz^{3} establishes that all proofs in the sequent calculus can be found according to a simple strategy. It is immediately evident that there are many propositions which have no proof according to this strategy, thereby guaranteeing consistency of the system.

Most search strategies employed by automated deduction systems are either directly based on or can be derived from the sequent calculus. We can broadly classify procedures as either working backwards from the proposed theorem toward the axioms, or forward from the axioms toward the theorem. Among the backward searching procedures we find tableaux, connection methods, matrix methods and some forms of resolution. Among the forward searching procedures we find classical resolution and the inverse method. The prominence of resolution among these methods is no accident, since Robinson’s seminal paper represented a major leap forward in the state of the art. It is natural to expect that a combination of forward and backward search could improve the efficiency of theorem proving system. Such a combination, however, has been elusive up to now, due to the largely incompatible basic choices in design and implementation of the two kinds of search procedures.

1literally translated as concept notation

2[?]

3literally just “main theorem”, often called the cut elimination theorem

Draft of November 12, 1999

In this course we study both types of procedures. We investigate high-level questions, such as how these procedures relate to the basic sequent calculus. We also consider low-level issues, such as techniques for efficient implementation of the basic inference engine.

There is one further dimension to consider: which logic do we reason in? In philosophy, mathematics, and computer science many different logics are of interest. For example, there are classical logic, intuitionistic logic, modal logic, relevance logic, higher-order logic, dynamic logic, temporal logic, linear logic, belief logic, and lax logic (to mention just a few). While each logic requires its own considerations, many techniques are shared. This can be attributed in part to the common root of different logics in natural deduction and the sequent calculus. Another reason is that low-level efficiency improvements are relatively independent of higher-level techniques.

For this course we chose intuitionistic logic for a variety of reasons. First, intuitionistic propositions correspond to logical specifications and proofs to functional programs, which means intuitionistic logic is of central interest in the study of programming languages. Second, intuitionistic logic is more complex than classical logic and exhibits phenomena obscured by special properties which apply only to classical logic. Third, there are relatively straightforward interpretations of classical in intuitionistic logic which permits us to study logical interpretations in connection with theorem proving procedures.

The course is centered around a project, namely the joint design and implementation of a succession of theorem provers for intuitionistic logic. We start with natural deduction, followed by a sequent calculus, and a simple tableau prover. Then we turn toward the inverse method and introduce successive refinements consisting of both high-level and low-level optimizations.^{4} The implementation component is important to gain a deeper understanding of the techniques introduced in our abstract study.

The goal of the course is to give students a thorough understanding of the central techniques in automated theorem proving. Furthermore, they should understand the systematic development of these techniques and their correctness proofs, thereby enabling them to transfer methods to different logics or applications. We are less interested here in an appreciation of the pragmatics of highly efficient implementations or performance tuning.

4The precise order and extent of the improvements possible in a one-semester graduate course has yet to be determined.

Draft of November 12, 1999

Natural Deduction

Ich wollte zunächst einmal einen Formalismus aufstellen, der dem wirklichen Schließen möglichst nahe kommt. So ergab sich ein ,,Kalkül des natürlichen Schließens“.^{1}

— Gerhard Gentzen

Untersuchungen über das logische Schließen [Gen35]

In this chapter we explore ways to define logics, or, which comes to the same thing, ways to give meaning to logical connectives. Our fundamental notion is that of a judgment based on evidence. For example, we might make the judgment “It is raining” based on visual evidence. Or we might make the judgment “‘A implies A’ is true for any proposition A” based on a derivation. The use of the notion of a judgment as conceptual prior to the notion of proposition has been advocated by Martin-Löf [ML85a, ML85b]. Certain forms of judgments frequently recur and have therefore been investigated in their own right, prior to logical considerations. Two that we will use are hypothetical judgments and parametric jugments (the latter is sometimes called general judgment or schematic judgment).

A hypothetical judgment has the form “J_{2} under hypothesis J_{1}”. We consider this judgment evident if we are prepared to make the judgment J_{2} once provided with evidence for J_{1}. Formal evidence for a hypothetical judgment is a hypothetical derivation where we can freely use the hypothesis J_{1} in the derivation of J_{2}. Note that hypotheses need not be used, and could be used more than once.

A parametric judgment has the form “J for any a” where a is a parameter which may occur in J. We make this judgment if we are prepared to make the judgment [O/a]J for arbitrary objects O of the right category. Here [O/a]J is our notation for substituting the object O for parameter a in the judgment J. Formal evidence for a parametric judgment J is a parametric derivation with free occurrences of the parameter a.

1First I wanted to construct a formalism which comes as close as possible to actual reasoning. Thus arose a “calculus of natural deduction”.

Draft of November 12, 1999

Formal evidence for a judgment in form of a derivation is usually written in two-dimensional notation:

\begin{matrix}D \\ J \end{matrix}

if D is a derivation of J. For the sake of brevity we sometimes use the alternative notation D :: J. A hypothetical judgment is written as

\frac{u}{J_{1}} ; ⋮ ; J_{2}

where u is a label which identifies the hypothesis J_{1}. We use the labels to guarantee that hypotheses which are introduced during the reasoning process are not used outside their scope.

The separation of the notion of judgment and proposition and the corresponding separation of the notion of evidence and proof sheds new light on various styles that have been used to define logical systems.

An axiomatization in the style of Hilbert [Hil22], for example, arises when one defines a judgment “A is true” without the use of hypothetical judgments. Such a definition is highly economical in its use of judgments, which has to be compensated by a liberal use of implication in the axioms. When we make proof structure explicit in such an axiomatization, we arrive at combinatory logic [Cur30].

A categorical logic [LS86] arises when the basic judgment is not truth, but entailment “A entails B”.^{2} Once again, presentations are highly economical and do not need to seek recourse in complex judgment forms (at least for the propositional fragment). But derivations often require many hypotheses, which means that we need to lean rather heavily on conjunction here. Proofs are realized by morphisms which are an integral part of the machinery of category theory.

While these are interesting and in many ways useful approaches to logic specification, neither of them comes particularly close to capturing the practice of mathematical reasoning. This was Gentzen’s point of departure for the design of a system of natural deduction [Gen35]. From our point of view, this system is based on the simple judgment “A is true”, but relies critically on hypothetical and parametric judgments. In addition to being extremely elegant, it has the great advantage that one can define all logical connectives without reference to any other connective. This principle of modularity extends to the meta-theoretic study of natural deduction and simplifies considering fragments and extension of logics. Since we will consider many fragments and extension, this orthogonality of the logical connectives is a critical consideration. There is another advantage to natural deduction, namely that its proofs are isomorphic to the terms in a λcalculus via the so-called Curry-Howard isomorphism [How69], which establishes many connections to functional programming.

2[This has been disputed by practitioners of the field and should be re-evaluated.]

Draft of November 12, 1999

Finally, we arrive at the sequent calculus (also introduced by Gentzen in his seminal paper [Gen35]) when we split the single judgment of truth into two: “A is an assumption” and “A is true”. While we still employ the machinery of parametric and hypothetical judgments, we now need an explicit rule to state that “A is an assumption” is sufficient evidence for “A is a true”. The reverse, namely that if “A is true” then “A may be used as an assumption” is the Cut rule which he proved to be redundant in his Hauptsatz. For Gentzen the sequent calculus was primarily a technical device to prove consistency of his system of natural deduction, but it exposes many details of the fine structure of proofs in such a clear manner that many logic presentations employ sequent calculi. The laws governing the structure of proofs, however, are more complicated than the Curry-Howard isomorphism for natural deduction might suggest and are still the subject of study [Her95, Pfe95].

We choose natural deduction as our definitional formalism as the purest and most widely applicable. Later we justify the sequent calculus as a calculus of proof search for natural deduction and explicitly relate the two forms of presentation.

We begin by introducing natural deduction for intuitionistic logic, exhibiting its basic principles.

2.1 Intuitionistic Natural Deduction

The system of natural deduction we describe below is basically Gentzen’s system NJ [Gen35] or the system which may be found in Prawitz [Pra65]. The calculus of natural deduction was devised by Gentzen in the 1930’s out of a dissatisfaction with axiomatic systems in the Hilbert tradition, which did not seem to capture mathematical reasoning practices very directly. Instead of a number of axioms and a small set of inference rules, valid deductions are described through inference rules only, which at the same time explain the meaning of the logical quantifiers and connectives in terms of their proof rules.

A language of (first-order) terms is built up from variables x, y, etc., function symbols f, g, etc., each with a unique arity, and parameters a, b, etc. in the usual way.

Terms t ::= x | a | f(t_{1}, …, t_{n})

A constant c is simply a function symbol with arity 0 and we write c instead of c(). Exactly which function symbols are available is left unspecified in the general development of predicate logic and only made concrete for specific theories, such as the theory of natural numbers. However, variables and parameters are always available. We will use t and s to range over terms.

The language of propositions is built up from predicate symbols P, Q, etc. and terms in the usual way.

Propositions A ::= P (t_{1}, …, t_{n}) | A_{1} ∧ A_{2} | A_{1} ⊃ A_{2} | A_{1} ∨ A_{2} | ¬A

| ⊥ | ⊤ | ∀x. A | ∃x. A A propositional constant P is simply a predicate symbol with no arguments and we write P instead of P (). We will use A, B, and C to range over propositions. Exactly which predicate symbols are available is left unspecified in the general development of predicate logic and only made concrete for specific theories.

The notions of free and bound variables in terms and propositions are defined in the usual way: the variable x is bound in propositions of the form ∀x. A and ∃x. A. We use parentheses to disambiguate and assume that ∧ and ∨ bind more tightly than ⊃. It is convenient to assume that propositions have no free individual variables; we use parameters instead where necessary. Our notation for substitution is [t/x]A for the result of substituting the term t for the variable x in A. Because of the restriction on occurrences of free variables, we can assume that t is free of individual variables, and thus capturing cannot occur.

The main judgment of natural deduction is “C is true” written as ⊢ C, from hypotheses ⊢ A_{1}, …, ⊢ A_{n}. We will model this as a hypothetical judgment. This means that certain structural properties of derivations are tacitly assumed, independently of any logical inferences. In essence, these assumptions explain what hypothetical judgments are.

Hypothesis. If we have a hypothesis ⊢ A than we can conclude ⊢ A.

Weakening. Hypotheses need not be used.

Duplication. Hypotheses can be used more than once.

Exchange. The order in which hypotheses are introduced is irrelevant.

In natural deduction each logical connective and quantifier is characterized by its introduction rule(s) which specifies how to infer that a conjunction, disjunction, etc. is true. The elimination rule for the logical constant tells what other truths we can deduce from the truth of a conjunction, disjunction, etc. Introduction and elimination rules must match in a certain way in order to guarantee that the rules are meaningful and the overall system can be seen as capturing mathematical reasoning.

The first is a local soundness property: if we introduce a connective and then immediately eliminate it, we should be able to erase this detour and find a more direct derivation of the conclusion without using the connective. If this property fails, the elimination rules are too strong: they allow us to conclude more than we should be able to know.

The second is a local completeness property: we can eliminate a connective in a way which retains sufficient information to reconstitute it by an introduction rule. If this property fails, the elimination rules are too weak: they do not allow us to conclude everything we should be able to know.

We provide evidence for local soundness and completeness of the rules by means of local reduction and expansion judgments, which relate proofs of the same proposition.

One of the important principles of natural deduction is that each connective should be defined only in terms of inference rules without reference to other logical connectives or quantifiers. We refer to this as orthogonality of the connectives. It means that we can understand a logical system as a whole by understanding each connective separately. It also allows us to consider fragments and extensions directly and it means that the investigation of properties of a logical system can be conducted in a modular way.

We now show the introduction and elimination rules, local reductions and expansion for each of the logical connectives in turn. The rules are summarized on page 2.1.

Conjunction. A ∧ B should be true if both A and B are true. Thus we have the following introduction rule.

⊢ A ⊢ B ∧I ⊢ A ∧ B

If we consider this as a complete definition, we should be able to recover both A and B if we know A ∧ B. We are thus led to two elimination rules.

\begin{aligned}⊢ A ∧ B \\ & ∧E_{L} \\ ⊢ A \end{aligned}  \begin{aligned}⊢ A ∧ B \\ & ∧E_{R} \\ ⊢ B \end{aligned}

To check our intuition we consider a deduction which ends in an introduction followed by an elimination:

\begin{matrix}D \\ ⊢ A \end{matrix}  \begin{matrix}E \\ ⊢ B \end{matrix}

∧I ⊢ A ∧ B

∧E_{L}

⊢ A

Clearly, it is unnecessary to first introduce the conjunction and then eliminate it: a more direct proof of the same conclusion from the same (or fewer) assumptions would be simply

\begin{matrix}D \\ ⊢ A \end{matrix}

Formulated as a transformation or reduction between derivations we have

\begin{aligned}\begin{matrix}D \\ ⊢ A \end{matrix} & & \begin{matrix}E \\ ⊢ B \end{matrix} \\ & & & ∧I \\ & ⊢ A ∧ B \end{aligned} ; ∧E_{L} ; ⊢ A⟹_{R} \begin{matrix}D \\ ⊢ A \end{matrix}

and symmetrically

\begin{aligned}\begin{matrix}D \\ ⊢ A \end{matrix} & & \begin{matrix}E \\ ⊢ B \end{matrix} \\ & & & ∧I \\ & ⊢ A ∧ B \end{aligned} ; ∧E_{R} ; ⊢ B ⟹_{R} \begin{matrix}E \\ ⊢ B \end{matrix}

Draft of November 12, 1999

The new judgment

\begin{matrix}D \\ ⊢ A \end{matrix} ⟹_{R} \begin{matrix}E \\ ⊢ A \end{matrix}

relates derivations with the same conclusion. We say D locally reduces to E. Since local reductions are possible for both elimination rules for conjunction, our rules are locally sound. To show that the rules are locally complete we show how to reintroduce a conjunction from its components in the form of a local expansion.

\begin{matrix}D \\ ⊢ A ∧ B \end{matrix} ⟹_{E} \begin{aligned}\begin{matrix}D \\ ⊢ A ∧ B \end{matrix} ; ∧E_{L} ; ⊢ A & \begin{matrix}D \\ ⊢ A ∧ B \end{matrix} ; ∧E_{R} ; ⊢ B \\ & ∧I \\ ⊢ A ∧ B \end{aligned}

Implication. To derive ⊢ A ⊃ B we assume ⊢ A and then derive ⊢ B. Written as a hypothetical judgment:

\frac{u}{⊢ A} ; ⋮ ; ⊢ B ; ⊃I^{u} ; ⊢ A ⊃ B

We must be careful that the hypothesis ⊢ A is available only in the derivation above the premiss. We therefore label the inference with the name of the hypothesis u, which must not be used already as the name for a hypothesis in the derivation of the premiss. We say that the hypothesis ⊢ A labelled u is discharged at the inference labelled ⊃I^{u}. A derivation of ⊢ A ⊃ B describes a construction by which we can transform a derivation of ⊢ A into a derivation of ⊢ B: we substitute the derivation of ⊢ A wherever we used the assumption ⊢ A in the hypothetical derivation of ⊢ B. The elimination rule expresses this: if we have a derivation of ⊢ A ⊃ B and also a derivation of ⊢ A, then we can obtain a derivation of ⊢ B.

⊢ A ⊃ B ⊢ A ⊃E

⊢ B

The local reduction rule carries out the substitution of derivations explained above.

\begin{aligned}\frac{u}{⊢ A} ; D ; ⊢ B ; ⊃I^{u} ; ⊢ A ⊃ B & \begin{matrix}E \\ ⊢ A \end{matrix} \\ & & ⊃E \\ ⊢ B \end{aligned} ⟹_{R}  \begin{aligned}E \\ & u \\ ⊢ A \end{aligned} ; D ; ⊢ B

Draft of November 12, 1999

The final derivation depends on all the hypotheses of E and D except u, for which we have substituted E. An alternative notation for this substitution of derivations for hypotheses is [E/u]D :: ⊢ B. The local reduction described above may significantly increase the overall size of the derivation, since the deduction E is substituted for each occurrence of the assumption labeled u in D and may thus be replicated many times. The local expansion simply rebuilds the implication.

\begin{matrix}D \\ ⊢ A ⊃ B \end{matrix} ⟹_{E}  \begin{aligned}\begin{matrix}D \\ ⊢ A ⊃ B \end{matrix} & \frac{u}{⊢ A} \\ & ⊃E \\ ⊢ B \end{aligned} ; ⊃I^{u} ; ⊢ A ⊃ B

Disjunction. A ∨ B should be true if either A is true or B is true. Therefore we have two introduction rules.

\begin{aligned}⊢ A \\ & ∨I_{L} \\ ⊢ A ∨ B \end{aligned}  \begin{aligned}⊢ B \\ & ∨I_{R} \\ ⊢ A ∨ B \end{aligned}

If we have a hypothesis ⊢ A ∨ B, we do not know how it might be inferred. That is, a proposed elimination rule

\begin{aligned}⊢ A ∨ B \\ & ? \\ ⊢ A \end{aligned}

would be incorrect, since a deduction of the form

\begin{matrix}E \\ ⊢ B \end{matrix} ; ∨I_{R} ; ⊢ A ∨ B ; ? ; ⊢ A

cannot be reduced. As a consequence, the system would be inconsistent: if we have at least one theorem (B, in the example) we can prove every formula (A, in the example). How do we use the assumption A ∨ B in informal reasoning? We often proceed with a proof by cases: we prove a conclusion C under the assumption A and also show C under the assumption B. We then conclude C, since either A or B by assumption. Thus the elimination rule employs two hypothetical judgments.

⊢ A ∨ B  \frac{u}{⊢ A} ; ⋮ ; ⊢ C  \frac{w}{⊢ B} ; ⋮ ; ⊢ C

∨E^{u,w} ⊢ C

Draft of November 12, 1999

Now one can see that the introduction and elimination rules match up in two reductions. First, the case that the disjunction was inferred by ∨I_{L}.

\begin{aligned}\begin{matrix}D \\ ⊢ A \end{matrix} ; ∨I_{L} ; ⊢ A ∨ B & \frac{u}{⊢ A} ; E_{1} ; ⊢ C & \frac{w}{⊢ B} ; E_{2} ; ⊢ C \\ & & ∨E^{u,w} \\ & ⊢ C \end{aligned} ⟹_{R}  \begin{aligned}D \\ & u \\ ⊢ A \end{aligned} ; E_{1} ; ⊢ C

The other reduction is symmetric.

\begin{aligned}\begin{matrix}D \\ ⊢ B \end{matrix} ; ∨I_{R} ; ⊢ A ∨ B & \frac{u}{⊢ A} ; E_{1} ; ⊢ C & \frac{w}{⊢ B} ; E_{2} ; ⊢ C \\ & & ∨E^{u,w} \\ & ⊢ C \end{aligned} ⟹_{R}  \begin{aligned}D \\ & w \\ ⊢ B \end{aligned} ; E_{2} ; ⊢ C

As in the reduction for implication, the resulting derivation may be longer than the original one. The local expansion is more complicated than for the previous connectives, since we first have to distinguish cases and then reintroduce the disjunction in each branch.

\begin{matrix}D \\ ⊢ A ∨ B \end{matrix} ⟹_{E} \begin{aligned}\begin{matrix}D \\ ⊢ A ∨ B \end{matrix} & \frac{u}{⊢ A} ; ∨I_{L} ; ⊢ A ∨ B & \frac{w}{⊢ B} ; ∨I_{R} ; ⊢ A ∨ B \\ & & ∨E^{u,w} \\ & ⊢ A ∨ B \end{aligned}

Negation. In order to derive ¬A we assume A and try to derive a contradiction. Thus it seems that negation requires falsehood, and, indeed, in most literature on constructive logic, ¬A is seen as an abbreviation of A ⊃ ⊥. In order to give a self-contained explanation of negation by an introduction rule, we employ a judgment that is parametric in a propositional parameter p: If we can derive any p from the hypothesis A we conclude ¬A.

\frac{u}{⊢ A} ; ⋮ ; ⊢ p ; ¬I^{p,u} ; ⊢ ¬A  \begin{aligned}⊢ ¬A  ⊢ A \\ & ¬E \\ ⊢ C \end{aligned}

Draft of November 12, 1999

The elimination rule follows from this view: if we know ⊢ ¬A and ⊢ A then we can conclude any formula C is true. In the form of a local reduction:

\begin{aligned}\frac{u}{⊢ A} ; D ; ⊢ p ; ¬I^{p,u} ; ⊢ ¬A & \begin{matrix}E \\ ⊢ A \end{matrix} \\ & & ¬E \\ ⊢ C \end{aligned} ⟹_{R}  \begin{aligned}E \\ & u \\ ⊢ A \end{aligned} ; [C/p]D ; ⊢ C

The substitution [C/p]D is valid, since D is parametric in p. The local expansion is similar to the case for implication.

\begin{matrix}D \\ ⊢ ¬A \end{matrix} ⟹_{E}  \begin{aligned}\begin{matrix}D \\ ⊢ ¬A \end{matrix} & & \frac{u}{⊢ A} \\ & & ¬E \\ & ⊢ p \end{aligned} ; ¬I^{p,u} ; ⊢ ¬A

Truth. There is only an introduction rule for ⊤:

\frac{⊤I}{⊢ ⊤}

Since we put no information into the proof of ⊤, we know nothing new if we have an assumption ⊤ and therefore we have no elimination rule and no local reduction. It may also be helpful to think of ⊤ as a 0-ary conjunction: the introduction rule has 0 premisses instead of 2 and we correspondingly have 0 elimination rules instead of 2. The local expansion allows the replacement of any derivation of ⊤ by ⊤I.

\begin{matrix}D \\ ⊢ ⊤ \end{matrix} ⟹_{E} \frac{⊤I}{⊢ ⊤}

Falsehood. Since we should not be able to derive falsehood, there is no introduction rule for ⊥. Therefore, if we can derive falsehood, we can derive everything.

\begin{aligned}⊢ ⊥ \\ & ⊥E \\ ⊢ C \end{aligned}

Note that there is no local reduction rule for ⊥E. It may be helpful to think of ⊥ as a 0-ary disjunction: we have 0 instead of 2 introduction rules and we correspondingly have to consider 0 cases instead of 2 in the elimination rule. Even though we postulated that falsehood should not be derivable, falsehood could clearly be a consequence of contradictory assumption. For example, ⊢ A ∧ ¬A ⊃ ⊥ is derivable. While there is no local reduction rule, there still is a local expansion in analogy to the case for disjunction.

\begin{matrix}D \\ ⊢ ⊥ \end{matrix} ⟹_{E}  \begin{matrix}D \\ ⊢ ⊥ \end{matrix} ; ⊥E ; ⊢ ⊥

Universal Quantification. Under which circumstances should ⊢ ∀x. A be true? This clearly depends on the domain of quantification. For example, if we know that x ranges over the natural numbers, then we can conclude ∀x. A if we can prove [0/x]A, [1/x]A, etc. Such a rule is not effective, since it has infinitely many premisses. Thus one usually retreats to rules such as induction. However, in a general treatment of predicate logic we would like to prove statements which are true for all domains of quantification. Thus we can only say that ∀x. A should be provable if [a/x]A is provable for a new parameter a about which we can make no assumption. Conversely, if we know ∀x. A, we know that [t/x]A for any term t.

\begin{aligned}⊢ [a/x]A \\ & ∀I^{a} \\ ⊢ ∀x. A \end{aligned}  \begin{aligned}⊢ ∀x. A \\ & ∀E \\ ⊢ [t/x]A \end{aligned}

The label a on the introduction rule is a reminder the parameter a must be “new”, that is, it may not occur in any undischarged assumption in the proof of [a/x]A or in ∀x. A itself. In other words, the derivation of the premiss must be parametric in a. The local reduction carries out the substitution for the parameter.

\begin{matrix}D \\ ⊢ [a/x]A \end{matrix} ; ∀I ; ⊢ ∀x. A ; ∀E ; ⊢ [t/x]A ⟹_{R} \begin{matrix}[t/a]D \\ ⊢ [t/x]A \end{matrix}

Here, [t/a]D is our notation for the result of substituting t for the parameter a throughout the deduction D. For this substitution to preserve the conclusion, we must know that a does not already occur in A. Similarly, we would change the hypotheses if a occurred free in any of the undischarged hypotheses of D. This might render a larger proof incorrect. As an example, consider the formula ∀x. ∀y. P (x) ⊃ P (y) which should clearly not be true for all predicates P. The following is not a deduction of this formula.

\frac{u}{⊢ P (a)} ; ∀I^{a}? ; ⊢ ∀x. P (x)

∀E ⊢ P (b)

⊃I^{u} ⊢ P (a) ⊃ P (b)

∀I^{b} ⊢ ∀y. P (a) ⊃ P (y)

∀I^{a} ⊢ ∀x. ∀y. P (x) ⊃ P (y)

The flaw is at the inference marked with “?,” where a is free in the hypothesis labelled u. Applying a local proof reduction to the (incorrect) ∀I inference followed by ∀E leads to the the assumption [b/a]P (a) which is equal to P (b). The resulting derivation

\frac{u}{⊢ P (b)}

⊃I^{u} ⊢ P (a) ⊃ P (b)

∀I^{b} ⊢ ∀y. P (a) ⊃ P (y)

∀I^{a} ⊢ ∀x. ∀y. P (x) ⊃ P (y)

is once again incorrect since the hypothesis labelled u should read P (a), not P (b).

The local expansion for universal quantification is much simpler.

\begin{matrix}D \\ ⊢ ∀x. A \end{matrix} ⟹_{E}  \begin{matrix}D \\ ⊢ ∀x. A \end{matrix} ; ∀E ; ⊢ [a/x]A ; ∀I^{a} ; ⊢ ∀x. A

Existential Quantification. We conclude that ∃x. A is true when there is a term t such that [t/x]A is true.

\begin{aligned}⊢ [t/x]A \\ & ∃I \\ ⊢ ∃x. A \end{aligned}

When we have an assumption ∃x. A we do not know for which t it is the case that [t/x]A holds. We can only assume that [a/x]A holds for some parameter a about which we know nothing else. Thus the elimination rule resembles the one for disjunction.

⊢ ∃x. A  \frac{u}{⊢ [a/x]A} ; ⋮ ; ⊢ C

∃E^{a,u} ⊢ C

The restriction is similar to the one for ∀I: the parameter a must be new, that is, it must not occur in ∃x. A, C, or any assumption employed in the derivation of the second premiss. In the reduction rule we have to perform two substitutions: we have to substitute t for the parameter a and we also have to substitute for the hypothesis labelled u.

\begin{aligned}\begin{matrix}D \\ ⊢ [t/x]A \end{matrix} ; ∃I ; ∃x. A & \frac{u}{⊢ [a/x]A} ; E ; ⊢ C \\ & ∃E^{a,u} \\ ⊢ C \end{aligned} ⟹_{R}  \begin{aligned}D \\ & u \\ ⊢ [t/x]A \end{aligned} ; [t/a]E ; ⊢ C

The proviso on occurrences of a guarantees that the conclusion and hypotheses of [t/a]E have the correct form. The local expansion for existential quantification is also similar to the case for disjunction.

\begin{matrix}D \\ ⊢ ∃x. A \end{matrix} ⟹_{E} \begin{aligned}\begin{matrix}D \\ ⊢ ∃x. A \end{matrix} & \frac{u}{⊢ [a/x]A} ; ∃I ; ⊢ ∃x. A \\ & ∃E^{a,u} \\ ⊢ ∃x. A \end{aligned}

Here is a simple example of a natural deduction. We attempt to show the process by which such a deduction may have been generated, as well as the final deduction. The three vertical dots indicate a gap in the derivation we are trying to construct, with hypotheses and their consequences shown above and the desired conclusion below the gap.

⋮ ; ⊢ A ∧ (A ⊃ B) ⊃ B  ⇝ \frac{u}{⊢ A ∧ (A ⊃ B)} ; ⋮ ; ⊢ B ; ⊃I^{u} ; ⊢ A ∧ (A ⊃ B) ⊃ B

Draft of November 12, 1999

⇝ \frac{u}{⊢ A ∧ (A ⊃ B)} ; ∧E_{L} ; ⊢ A ; ⋮ ; ⊢ B ; ⊃I^{u} ; ⊢ A ∧ (A ⊃ B) ⊃ B ⇝\frac{u}{⊢ A ∧ (A ⊃ B)} ; ∧E_{L} ; ⊢ A  \frac{u}{⊢ A ∧ (A ⊃ B)} ; ∧E_{R} ; ⊢ A ⊃ B ; ⋮ ; ⊢ B ; ⊃I^{u} ; ⊢ A ∧ (A ⊃ B) ⊃ B

⇝  \begin{aligned}\frac{u}{⊢ A ∧ (A ⊃ B)} ; ∧E_{R} ; ⊢ A ⊃ B & \frac{u}{⊢ A ∧ (A ⊃ B)} ; ∧E_{L} ; ⊢ A \\ & ⊃E \\ ⊢ B \end{aligned} ; ⋮ ; ⊢ B ; ⊃I^{u} ; ⊢ A ∧ (A ⊃ B) ⊃ B

⇝  \begin{aligned}\frac{u}{⊢ A ∧ (A ⊃ B)} ; ∧E_{R} ; ⊢ A ⊃ B & \frac{u}{⊢ A ∧ (A ⊃ B)} ; ∧E_{L} ; ⊢ A \\ & ⊃E \\ ⊢ B \end{aligned} ; ⊃I^{u} ; ⊢ A ∧ (A ⊃ B) ⊃ B

The symbols A and B in this derivation stand for arbitrary propositions; we can thus established a judgment parametric in A and B. In other words, every instance of this derivation (substituting arbitrary propositions for A and B) is a valid derivation.

Below is a summary of the rules of intuitionistic natural deduction.

Introduction Rules  Elimination Rules

\begin{aligned}⊢ A  ⊢ B \\ & ∧I \\ ⊢ A ∧ B \end{aligned}  \begin{aligned}⊢ A ∧ B \\ & ∧E_{L} \\ ⊢ A \end{aligned}  \begin{aligned}⊢ A ∧ B \\ & ∧E_{R} \\ ⊢ B \end{aligned}

\begin{aligned}⊢ A \\ & ∨I_{L} \\ ⊢ A ∨ B \end{aligned}  \begin{aligned}⊢ B \\ & ∨I_{R} \\ ⊢ A ∨ B \end{aligned}  \begin{matrix}⊢ A ∨ B  \frac{u}{⊢ A} ; ⋮ ; ⊢ C  \frac{w}{⊢ B} ; ⋮ ; ⊢ C \\ ∨E^{u,w} \\ ⊢ C \end{matrix}

\frac{u}{⊢ A} ; ⋮ ; ⊢ B ; ⊃I^{u} ; ⊢ A ⊃ B  \begin{aligned}⊢ A ⊃ B  ⊢ A \\ & ⊃E \\ ⊢ B \end{aligned}

\frac{u}{⊢ A} ; ⋮ ; ⊢ p ; ¬I^{p,u} ; ⊢ ¬A  \begin{aligned}⊢ ¬A  ⊢ A \\ & ¬E \\ ⊢ C \end{aligned}
\frac{⊤I}{⊢ ⊤}  no ⊤ elimination

no ⊥ introduction  \begin{aligned}⊢ ⊥ \\ & ⊥E \\ ⊢ C \end{aligned}

\begin{aligned}⊢ [a/x]A \\ & ∀I^{a} \\ ⊢ ∀x. A \end{aligned}  \begin{aligned}⊢ ∀x. A \\ & ∀E \\ ⊢ [t/x]A \end{aligned}

\begin{aligned}⊢ [t/x]A \\ & ∃I \\ ⊢ ∃x. A \end{aligned}  \begin{matrix}⊢ ∃x. A  \frac{u}{⊢ [a/x]A} ; ⋮ ; ⊢ C \\ ∃E^{a,u} \\ ⊢ C \end{matrix}

Draft of November 12, 1999

2.2 Classical Logic

The inference rules so far only model intuitionistic logic, and some classically true propositions such as A ∨ ¬A (for an arbitrary A) are not derivable, as we will see in Section 3.5. There are three commonly used ways one can construct a system of classical natural deduction by adding one additional rule of inference. ⊥_{C} is called Proof by Contradiction or Rule of Indirect Proof, ¬¬_{C} is the Double Negation Rule, and XM is referred to as Excluded Middle.

\frac{u}{¬A} ; ⋮ ; ⊥ ; ⊥_{C}^{u} ; A  \begin{aligned}¬¬A \\ & ¬¬_{C} \\ A \end{aligned}  \frac{XM}{A ∨ ¬A}

The rule for classical logic (whichever one chooses to adopt) breaks the pattern of introduction and elimination rules. One can still formulate some reductions for classical inferences, but natural deduction is at heart an intuitionistic calculus. The symmetries of classical logic are much better exhibited in sequent formulations of the logic. In Exercise 2.3 we explore the three ways of extending the intuitionistic proof system and show that they are equivalent.

Another way to obtain a natural deduction system for classical logic is to allow multiple conclusions (see, for example, Parigot [Par92]).

2.3 Localizing Hypotheses

In the formulation of natural deduction from Section 2.1 correct use of hypotheses and parameters is a global property of a derivation. We can localize it by annotating each judgment in a derivation by the available parameters and hypotheses. We give here a formulation of natural deduction for intuitionistic logic with localized hypotheses, but not parameters. For this we need a notation for hypotheses which we call a context.

Contexts Γ ::= · | Γ, u:A

Here, “·” represents the empty context, and Γ, u:A adds hypothesis ⊢ A labelled u to Γ. We assume that each label u occurs at most once in a context in order to avoid ambiguities. The main judgment can then be written as Γ ⊢ A, where

·, u_{1}:A_{1}, …, u_{n}:A_{n} ⊢ A

stands for

\frac{u_{1}}{⊢ A_{1}} … \frac{u_{n}}{⊢ A_{n}}
⋮
⊢ A

in the notation of Section 2.1.

We use a few important abbreviations in order to make this notation less cumbersome. First of all, we may omit the leading “·” and write, for example, u_{1}:A_{1}, u_{2}:A_{2} instead of ·, u_{1}:A_{1}, u_{2}:A_{2}. Secondly, we denote concatenation of contexts by overloading the comma operator as follows.

\begin{aligned}Γ, · & = & Γ \\ Γ, (Γ′, u:A) & = & (Γ, Γ′), u:A \end{aligned}

With these additional definitions, the localized version of our rules are as follows.

Introduction Rules  Elimination Rules

\begin{aligned}Γ ⊢ A  Γ ⊢ B \\ & ∧I \\ Γ ⊢ A ∧ B \end{aligned}  \begin{aligned}Γ ⊢ A ∧ B \\ & ∧E_{L} \\ Γ ⊢ A \end{aligned}  \begin{aligned}Γ ⊢ A ∧ B \\ & ∧E_{R} \\ Γ ⊢ B \end{aligned}

\begin{aligned}Γ ⊢ A \\ & ∨I_{L} \\ Γ ⊢ A ∨ B \end{aligned}  \begin{aligned}Γ ⊢ B \\ & ∨I_{R} \\ Γ ⊢ A ∨ B \end{aligned}  \begin{aligned}Γ ⊢ A ∨ B  Γ, u:A ⊢ C  Γ, w:B ⊢ C \\ & ∨E^{u,w} \\ Γ ⊢ C \end{aligned}

\begin{matrix}Γ, u:A ⊢ B \\ ⊃I & u \\ Γ ⊢ A ⊃ B \end{matrix}  \begin{aligned}Γ ⊢ A ⊃ B  Γ ⊢ A \\ & ⊃E \\ Γ ⊢ B \end{aligned}

\begin{matrix}Γ, u:A ⊢ p \\ ¬I & p,u \\ Γ ⊢ ¬A \end{matrix}  \begin{aligned}Γ ⊢ ¬A  Γ ⊢ A \\ & ¬E \\ Γ ⊢ C \end{aligned}
\frac{⊤I}{Γ ⊢ ⊤}  no ⊤ elimination

no ⊥ introduction  \begin{aligned}Γ ⊢ ⊥ \\ & ⊥E \\ Γ ⊢ C \end{aligned}

\begin{aligned}Γ ⊢ [a/x]A \\ & ∀I^{a} \\ Γ ⊢ ∀x. A \end{aligned}  \begin{aligned}Γ ⊢ ∀x. A \\ & ∀E \\ Γ ⊢ [t/x]A \end{aligned}

\begin{aligned}Γ ⊢ [t/x]A \\ & ∃I \\ Γ ⊢ ∃x. A \end{aligned}  \begin{aligned}Γ ⊢ ∃x. A  Γ, u:[a/x]A ⊢ C \\ & ∃E^{a,u} \\ Γ ⊢ C \end{aligned}

We also have a new rule for hypotheses which was an implicit property of the hypothetical judgments before.

\frac{u}{Γ_{1}, u:A, Γ_{2} ⊢ A}

Other general assumptions about hypotheses, namely that they may be used arbitrarily often in a derivation and that their order does not matter, are indirectly reflected in these rules. Note that if we erase the context Γ from the judgments throughout a derivation, we obtain a derivation in the original notation.

When we discussed local reductions in order to establish local soundness, we used the notation

\begin{aligned}D \\ & u \\ ⊢ A \end{aligned} ; E ; ⊢ C

for the result of substituting the derivation D of ⊢ A for all uses of the hypothesis ⊢ A labelled u in E. We would now like to reformulate the property with localized hypotheses. In order to prove that the (now explicit) hypotheses behave as expected, we use the principle of structural induction over derivations. Simply put, we prove a property for all derivations by showing that, whenever it holds for the premisses of an inference, it holds for the conclusion. Note that we have to show the property outright when the rule under consideration has no premisses. Such rules are the base cases for the induction.

Theorem 2.1 (Structural Properties of Hypotheses) The following properties hold for intuitionistic natural deduction.

1. (Exchange) If Γ_{1}, u_{1}:A, Γ_{2}, u_{2}:B, Γ_{3} ⊢ C then Γ_{1}, u_{2}:B, Γ_{2}, u_{1}:A, Γ_{3} ⊢ C.

2. (Weakening) If Γ_{1}, Γ_{2} ⊢ C then Γ_{1}, u:A, Γ_{2} ⊢ C.

3. (Contraction) If Γ_{1}, u_{1}:A, Γ_{2}, u_{2}:A, Γ_{3} ⊢ C then Γ_{1}, u:A, Γ_{2}, Γ_{3} ⊢ C.

4. (Substitution) If Γ_{1}, u:A, Γ_{2} ⊢ C and Γ_{1} ⊢ A then Γ_{1}, Γ_{2} ⊢ C.

Proof: The proof is in each case by straightforward induction over the structure of the first given derivation.

In the case of exchange, we appeal to the inductive assumption on the derivations of the premisses and construct a new derivation with the same inference rule. Algorithmically, this means that we exchange the hypotheses labelled u_{1} and u_{2} in every judgment in the derivation.

In the case of weakening and contraction, we proceed similarly, either adding the new hypothesis u:A to every judgment in the derivation (for weakening), or replacing uses of u_{1} and u_{2} by u (for contraction).

For substitution, we apply the inductive assumption to the premisses of the given derivation D until we reach hypotheses. If the hypothesis is different from u we can simply erase u:A (which is unused) to obtain the desired derivation. If the hypothesis is u:A the derivation looks like

D = \frac{u}{Γ_{1}, u:A, Γ_{2} ⊢ A}

so C = A in this case. We are also given a derivation E of Γ_{1} ⊢ A and have to construct a derivation F of Γ_{1}, Γ_{2} ⊢ A. But we can just repeatedly apply weakening to E to obtain F. Algorithmically, this means that, as expected, we substitute the derivation E (possibly weakened) for uses of the hypotheses u:A in D. Note that in our original notation, this weakening has no impact, since unused hypotheses are not apparent in a derivation. □

It is also possible to localize the derivations themselves, using proof terms. As we will see in Section 2.4, these proof terms form a λ-calculus closely related to functional programming. When parameters, hypotheses, and proof terms are all localized our main judgment becomes decidable. In the terminology of Martin-Löf [ML94], the main judgment is then analytic rather than synthetic. We no longer need to go outside the judgment itself in order to collect evidence for it: An analytic judgment encapsulates its own evidence.

2.4 Proof Terms

The basic judgment of the system of natural deduction is the derivability of a formula A, written as ⊢ A. It has been noted by Howard [How69] that there is a strong correspondence between (intuitionistic) derivations and λ-terms. The formulas A then act as types classifying λ-terms. In the propositional case, this correspondence is an isomorphism: formulas are isomorphic to types and derivations are isomorphic to simply-typed λ-terms. These isomorphisms are often called the propositions-as-types and proofs-as-programs paradigms.

If we stopped at this observation, we would have obtained only a fresh interpretation of familiar deductive systems, but we would not be any closer to the goal of providing a language for reasoning about properties of programs. However, the correspondences can be extended to first-order and higher-order logics. Interpreting first-order (or higher-order) formulas as types yields a significant increase in expressive power of the type system. However, maintaining an isomorphism during the generalization to first-order logic is somewhat unnatural and cumbersome. One might expect that a proof contains more information than the corresponding program. Thus the literature often talks about extracting programs from proofs or contracting proofs to programs. We do not discuss program extraction further in these notes.

We now introduce a notation for derivations to be carried along in deductions. For example, if M represents a proof of A and N represents a proof of B, then the pair ⟨M, N⟩ can be seen as a representation of the proof of A ∧ B by ∧-introduction. We write Γ ⊢ M : A to express the judgment M is a proof term for A under hypotheses Γ. We also repeat the local reductions and expansions from the previous section in the new notation. For local expansion we state the proposition whose truth must established by the proof term on the left-hand side. This expresses restrictions on the application of the expansion rules.

Conjunction. The proof term for a conjunction is simply the pair of proofs of the premisses.

Γ ⊢ M : A Γ ⊢ N : B ∧I Γ ⊢ ⟨M, N⟩ : A ∧ B

\begin{aligned}Γ ⊢ M : A ∧ B \\ & ∧E_{L} \\ Γ ⊢ fst M : A \end{aligned}  \begin{aligned}Γ ⊢ M : A ∧ B \\ & ∧E_{R} \\ Γ ⊢ snd M : B \end{aligned}

The local reductions now lead to two obvious local reductions of the proof terms. The local expansion is similiarly translated.

fst ⟨M, N⟩ ⟶_{R} M
snd ⟨M, N⟩ ⟶_{R} N
M : A ∧ B ⟶_{E} ⟨fst M, snd M⟩

Implication. The proof of an implication A ⊃ B will be represented by a function which maps proofs of A to proofs of B. The introduction rule explicitly forms such a function by λ-abstraction and the elimination rule applies the function to an argument.

\begin{matrix}Γ, u:A ⊢ M : B \\ ⊃I & u \\ Γ ⊢ (λu:A. M) : A ⊃ B \end{matrix}  \begin{aligned}Γ ⊢ M : A ⊃ B  Γ ⊢ N : A \\ & ⊃E \\ Γ ⊢ M N : B \end{aligned}

The binding of the variable u in the conclusion of ⊃I correctly models the intuition that the hypothesis is discharged and not available outside deduction of the premiss. The abstraction is labelled with the proposition A so that we can later show that the proof term uniquely determines a natural deduction. If A were not given then, for example, λu. u would be ambigous and serve as a proof term for A⊃A for any formula A. The local reduction rule is β-reduction; the local expansion is η-expansion.

\begin{matrix}(λu:A. M) N & ⟶_{R} & [N/u]M \\ M : A ⊃ B & ⟶_{E} & λu:A. M u \end{matrix}

In the reduction rule, bound variables in M that are free in N must be renamed in order to avoid variable capture. In the expansion rule u must be new—it may not already occur in M.

Disjunction. The proof term for disjunction introduction is the proof of the premiss together with an indication whether it was inferred by introduction on the left or on the right. We also annotate the proof term with the formula which did not occur in the premiss so that a proof term always proves exactly one proposition.

\begin{aligned}Γ ⊢ M : A \\ & ∨I_{L} \\ Γ ⊢ inl^{B} M : A ∨ B \end{aligned}  \begin{aligned}Γ ⊢ N : B \\ & ∨I_{R} \\ Γ ⊢ inr^{A} N : A ∨ B \end{aligned}

Draft of November 12, 1999

The elimination rule corresponds to a case construction.

Γ ⊢ M : A ∨ B  Γ, u:A ⊢ N_{1} : C  Γ, w:B ⊢ N_{2} : C
∨E^{u,w}
Γ ⊢ ( case M of inl u ⇒ N_{1} | inr w ⇒ N_{2}) : C

Since the variables u and w label assumptions, the corresponding proof term variables are bound in N_{1} and N_{2}, respectively. The two reduction rules now also look like rules of computation in a λ-calculus.

case inl^{B} M of inl u ⇒ N_{1} | inr w ⇒ N_{2} ⟶_{R} [M/u]N_{1}
case inr^{A} M of inl u ⇒ N_{1} | inr w ⇒ N_{2} ⟶_{R} [M/w]N_{2}
M : A ∨ B ⟶_{E} case M of inl u ⇒ inl^{B} u | inr w ⇒ inr^{A} w

The substitution of a deduction for a hypothesis is represented by the substitution of a proof term for a variable.

Negation. This is similar to implication. Since the premise of the rule is parametric in p the corresponding proof constructor must bind a propositional variable p, indicated by μ^{p}. Similarly, the elimination construct must record the formula to maintain the property that every valid term proves exactly one proposition. This is indicated as a subscript C to the infix operator “·”.

\begin{matrix}Γ, u:A ⊢ M : p \\ ¬I & p,u \\ Γ ⊢ μ^{p}u:A. M : ¬A \end{matrix}  \begin{aligned}Γ ⊢ M : ¬A  Γ ⊢ N : A \\ & ¬E \\ Γ ⊢ M ·_{C} N : C \end{aligned}

The reduction performs formula and proof term substitutions.

\begin{matrix}(μ^{p}u:A. M) ·_{C} N & ⟶_{R} & [N/u][C/p]M \\ M : ¬A & ⟶_{E} & μ^{p}u:A. M ·_{p} u \end{matrix}

Truth. The proof term for ⊤I is written ⟨ ⟩.

\frac{⊤I}{Γ ⊢ ⟨ ⟩ : ⊤}

Of course, there is no reduction rule. The expansion rule reads

M : ⊤ ⟶_{E} ⟨ ⟩

Falsehood. Here we need to annotate the proof term abort with the formula being proved to avoid ambiguity.

Γ ⊢ M : ⊥ ⊥E

Γ ⊢ abort^{C} M : C

Again, there is no reduction rule, only an expansion rule.

M : ⊥ ⟶_{E} abort^{⊥} M

In summary, we have

Terms M ::= u  Hypotheses
| ⟨M_{1}, M_{2}⟩ | fst M | snd M  Conjunction
| λu:A. M | M_{1} M_{2}  Implication
| inl^{A} M | inr^{A} M  Disjunction
| ( case M of inl u_{1} ⇒ M_{1} | inr u_{2} ⇒ M_{2})
| μ^{p}u:A. M | M_{1} ·_{A} M_{2}  Negation
| ⟨ ⟩  Truth
| abort^{A} M  Falsehood

and the reduction rules

fst ⟨M, N⟩ ⟶_{R}  M
snd ⟨M, N⟩ ⟶_{R}  N
(λu:A. M) N ⟶_{R}  [N/u]M
case inl^{B} M of inl u ⇒ N_{1} | inr w ⇒ N_{2} ⟶_{R}  [M/u]N_{1}
case inr^{A} M of inl u ⇒ N_{1} | inr w ⇒ N_{2} ⟶_{R} [M/w]N_{2}
(μ^{p}u:A. M) ·_{C} N ⟶_{R} [N/u][C/p]M

no rule for truth no rule for falsehood

The expansion rules are given below.

M : A ∧ B ⟶_{E} ⟨fst M, snd M⟩
M : A ⊃ B ⟶_{E} λu:A. M u
M : A ∨ B ⟶_{E} case M of inl u ⇒ inl^{B} u | inr w ⇒ inr^{A} w
M : ¬A ⟶_{E} μ^{p}u:A. M ·_{p} u
M : ⊤ ⟶_{E} ⟨ ⟩
M : ⊥ ⟶_{E} abort^{⊥} M

We can now see that the formulas act as types for proof terms. Shifting to the usual presentation of the typed λ-calculus we use τ and σ as symbols for types, and τ ×σ for the product type, τ → σ for the function type, τ +σ for the disjoint sum type, 1 for the unit type and 0 for the empty or void type. Base types b remain unspecified, just as the basic propositions of the propositional calculus remain unspecified. Types and propositions then correspond to each other as indicated below.

Types τ ::= b | τ_{1} × τ_{2} | τ_{1} → τ_{2} | τ_{1} + τ_{2} | 1 | 0
Propositions A ::= p | A_{1} ∧ A_{2} | A_{1} ⊃ A_{2} | A_{1} ∨ A_{2} | ⊤ | ⊥

We omit here the negation type which is typically not used in functional programming and thus does not have a well-known counterpart. We can think of ¬A as corresponding to τ → 0, where τ corresponds to A. We now summarize and restate the rules above, using the notation of types instead of propositions (omitting only the case for negation). Note that contexts Γ now declare variables with their types, rather than hypothesis labels with their proposition.

Γ ▷ M : τ Term M has type τ in context Γ

Γ ▷ M : τ Γ ▷ N : σ pair

Γ ▷ ⟨M, N⟩ : τ × σ

Γ ▷ M : τ × σ ; fst ; Γ ▷ fst M : τ  Γ ▷ M : τ × σ ; snd ; Γ ▷ snd M : σ

\begin{aligned}Γ, u:τ ▷ M : σ \\ & lam \\ Γ ▷ (λu:τ. M) : τ → σ \end{aligned}  \begin{aligned}u : τ in Γ \\ & var \\ Γ ▷ u : τ \end{aligned}

Γ ▷ M : τ → σ Γ ▷ N : τ app

Γ ▷ M N : σ

Γ ▷ M : τ

inl

Γ ▷ inl^{σ} M : τ + σ

Γ ▷ N : σ

inr

Γ ▷ inr^{τ} N : τ + σ

Γ ▷ M : τ + σ  Γ, u:τ ▷ N_{1} : ν  Γ, w:σ ▷ N_{2} : ν case

Γ ▷ ( case M of inl u ⇒ N_{1} | inr w ⇒ N_{2}) : ν

\frac{unit}{Γ ▷ ⟨ ⟩ : 1}

Γ ▷ M : 0

abort

Γ ▷ abort^{ν} M : ν

2.5 Exercises

Exercise 2.1 Prove the following by natural deduction using only intuitionistic rules when possible. We use the convention that ⊃, ∧, and ∨ associate to the right, that is, A⊃B⊃C stands for A⊃(B⊃C). A ≡ B is a syntactic abbreviation for (A ⊃ B) ∧ (B ⊃ A). Also, we assume that ∧ and ∨ bind more tightly than ⊃, that is, A ∧ B ⊃ C stands for (A ∧ B) ⊃ C. The scope of a quantifier extends as far to the right as consistent with the present parentheses. For example, (∀x. P (x) ⊃ C) ∧ ¬C would be disambiguated to (∀x. (P (x) ⊃ C)) ∧ (¬C).

1. ⊢ A ⊃ B ⊃ A.

2. ⊢ A ∧ (B ∨ C) ≡ (A ∧ B) ∨ (A ∧ C).

3. (Peirce’s Law). ⊢ ((A ⊃ B) ⊃ A) ⊃ A.

4. ⊢ A ∨ (B ∧ C) ≡ (A ∨ B) ∧ (A ∨ C).

5. ⊢ A ⊃ (A ∧ B) ∨ (A ∧ ¬B).

6. ⊢ (A ⊃ ∃x. P (x)) ≡ ∃x. (A ⊃ P (x)).

7. ⊢ ((∀x. P (x)) ⊃ C) ≡ ∃x. (P (x) ⊃ C).

8. ⊢ ∃x. ∀y. (P (x) ⊃ P (y)).

Exercise 2.2 We write A ⊢ B if B follows from hypothesis A and A ⊣⊢ B for A ⊢ B and B ⊢ A. Which of the following eight parametric judgments are derivable intuitionistically?

1. (∃x. A) ⊃ B ⊣⊢ ∀x. (A ⊃ B)

2. A ⊃ (∃x. B) ⊣⊢ ∃x. (A ⊃ B)

3. (∀x. A) ⊃ B ⊣⊢ ∃x. (A ⊃ B)

4. A ⊃ (∀x. B) ⊣⊢ ∀x. (A ⊃ B)

Provide natural deductions for the valid judgments. You may assume that the bound variable x does not occur in B (items 1 and 3) or A (items 2 and 4).

Exercise 2.3 Show that the three ways of extending the intuitionistic proof system for classical logic are equivalent, that is, the same formulas are deducible in all three systems.

Exercise 2.4 Assume we had omitted disjunction and existential quantification and their introduction and elimination rules from the list of logical primitives. In the classical system, give a definition of disjunction and existential quantification (in terms of other logical constants) and show that the introduction and elimination rules now become admissible rules of inference. A rule of inference is admissible if any deduction using the rule can be transformed into one without using the rule.

Exercise 2.5 Assume we would like to design a system of natural deduction for a simple temporal logic. The main judgment is now “A is true at time t” written as

⊢^{t} A.

1. Explain how to modify the given rules for natural deduction to this more general judgment and show the rules for implication and universal quantification.

2. Write out introduction and elimination rules for the temporal operator ◯A which should be true if A is true at the next point in time. Denote the “next time after t” by t + 1.

3. Show the local reductions and expansions which show the local soundness and completness of your rules.

4. Write out introduction and elimination rules for the temporal operator □A which should be true if A is true at all times.

5. Show the local reductions and expansions.

Exercise 2.6 Design introduction and elimination rules for the connectives 1. A ≡ B, usually defined as (A ⊃ B) ∧ (B ⊃ A),

2. A | B (exclusive or), usually defined as (A ∧ ¬B) ∨ (¬A ∧ B), without recourse to other logical constants or operators. Also show the corresponding local reductions and expansions. For each of the following proposed connectives, write down appropriate introduction and eliminations rules and show the local reductions and expansion or indicate that no such rule may exist.

3. A\overline{∧}B for ¬(A ∧ B),

4. A\overline{∨}B for ¬(A ∨ B),

5. A\overline{⊃}B for ¬(A ⊃ B),

6. +A for ¬¬A,

7. ∃^{∗}x. A for ¬∀x. ¬A,

8. ∀^{∗}x. A for ¬∃x. ¬A,

9. A ⇒ B | C for (A ⊃ B) ∧ (¬A ⊃ C). Exercise 2.7 A given introduction rule does not necessarily uniquely determine matching elimination rules and vice versa. Explore if the following alternative rules are also sound and complete.

1. Replace the two elimination rules for conjunction by

⊢ A ∧ B  \frac{u}{⊢ A} \frac{w}{⊢ B} ; ⋮ ; ⊢ C

∧E^{u,w} ⊢ C

2. Add the following elimination rule for truth.

⊢ ⊤ ⊢ C ⊤E ⊢ C

3. Add the following introduction rule for falsehood.

\begin{aligned}⊢ p \\ & ⊥I^{p} \\ ⊢ ⊥ \end{aligned}

Consider if any other of the standard connectives might permit alternative introduction or elimination rules which preserve derivability.

Draft of November 12, 1999

Exercise 2.8 For each of 14 following proposed entailments either write out a proof term for the corresponding implication or indicate that it is not derivable.

1. A ⊃ (B ⊃ C) ⊣⊢ (A ∧ B) ⊃ C

2. A ⊃ (B ∧ C) ⊣⊢ (A ⊃ B) ∧ (A ⊃ C)

3. A ⊃ (B ∨ C) ⊣⊢ (A ⊃ B) ∨ (A ⊃ C)

4. (A ⊃ B) ⊃ C ⊣⊢ (A ∨ C) ∧ (B ⊃ C)

5. (A ∨ B) ⊃ C ⊣⊢ (A ⊃ C) ∧ (B ⊃ C)

6. A ∧ (B ∨ C) ⊣⊢ (A ∧ B) ∨ (A ∧ C)

7. A ∨ (B ∧ C) ⊣⊢ (A ∨ B) ∧ (A ∨ C) Exercise 2.9 The de Morgan laws of classical logic allow negation to be distributed over other logical connectives. Investigate which directions of the de Morgan equivalences hold in intuitionistic logic and give proof terms for the valid entailments.

1. ¬(A ∧ B) ⊣⊢ ¬A ∨ ¬B

2. ¬(A ∨ B) ⊣⊢ ¬A ∧ ¬B

3. ¬(A ⊃ B) ⊣⊢ A ∧ ¬B

4. ¬(¬A) ⊣⊢ A

5. ¬⊤ ⊣⊢ ⊥

6. ¬⊥ ⊣⊢ ⊤

7. ¬∀x. A ⊣⊢ ∃x. ¬A

8. ¬∃x. A ⊣⊢ ∀x. ¬A Exercise 2.10 An alternative approach to negation is to introduce another judgment, A is false, and develop a system of evidence for this judgment. For example, we might say that A ∧ B is false if either A is false or B is false. Similarly, A ∨ B is false if both A and B are false. Expressed as inference rules:

\frac{A false}{A ∧ B false} \frac{B false}{A ∧ B false}  \frac{A false  B false}{A ∨ B false}

1. Write out a complete set of rules defining the judgment A false for the conjunction, implication, disjunction, truth, and falsehood.

2. Verify local soundness and completeness of your rules, if these notions

make sense.

Draft of November 12, 1999

3. Now we define that ¬A true if A false. Complete the set of rules and verify soundness and completeness if appropriate.

4. Does your system satisfy that every proposition A is either true or false? If so, prove it. Otherwise, show a counterexample.

5. Compare this notion of negation with the standard notion in intuitionistic logic.

6. Extend your system to include universal and existential quantification (if possible) and discuss its properties.

Sequent Calculus

In this chapter we develop the sequent calculus as a formal system for proof search in natural deduction. The sequent calculus was originally introduced by Gentzen [Gen35], primarily as a technical device for proving consistency of predicate logic. Our goal of describing a proof search procedure for natural deduction predisposes us to a formulation due to Kleene [Kle52] called G_{3}.

We introduce the sequent calculus in two steps. The first step is based on the simple strategy of building a natural deduction by using introduction rules bottom-up and elimination rules top-down. The result is an intercalation calculus which applies both to intuitionistic and classical logic [Byr99]. The second step consists of reformulating the rules for intercalation so that both forms of rules work bottom-up, resulting in the sequent calculus.

We also show how intercalation derivations lead to more compact proof terms, and how to extract proof terms from sequent calculus derivations.

3.1 Intercalation

A simple strategy in the search for a natural deduction is to use introduction rules reasoning bottom-up (from the proposed theorem towards the hypotheses) and the elimination rules top-down (from the assumptions towards the proposed theorem). When they meet in the middle we have found a normal deduction. Towards the end of this chapter we show that this strategy is in fact complete: if a proposition A has a natural deduction then it has a normal deduction. First, however, we need to make this strategy precise.

A general technique for representing proof search strategies is to introduce new judgments which permit only those derivations which can be found by the intended strategy. We then prove the correctness of the new, restricted judgments by appropriate soundness and completeness theorems.

In this case, we introduce two judgments:

A ⇑ Proposition A has a normal deduction, and
A ↓ Proposition A is extracted from a hypothesis.

They are defined by restricting the rules of natural deduction according to their status as introduction or elimination rules. Hypotheses can be trivially extracted. Therefore the necessary hypothetical judgments (in localized form, see Section 2.3) are

\begin{matrix}u_{1}:A_{1} ↓, …, u_{n}:A_{n} ↓ ⊢ A ⇑ and \\ u_{1}:A_{1} ↓, …, u_{n}:A_{n} ↓ ⊢ A ↓. \end{matrix}

We write Γ^{↓} for a context of the form shown above.

Hypotheses. The general rule for hypotheses simply reflects the nature of hypothetical judgments.

\frac{u}{Γ_{1}^{↓}, u:A ↓, Γ_{2}^{↓} ⊢ A ↓}

Coercion. The bottom-up and top-down derivations must be able to meet in the middle.

\begin{aligned}Γ^{↓} ⊢ A ↓ \\ & ↓⇑ \\ Γ^{↓} ⊢ A ⇑ \end{aligned}

Looked at another way, this rule allows us to coerce any extraction derivation to a normal deduction. Of course, the opposite coercion would contradict the intended strategy.

Conjunction. The rules for conjunction exhibit no unexpected features: the introduction rule is classified as a bottom-up rule, the elimination rule is classified as a top-down rule.

Γ^{↓} ⊢ A ⇑ Γ^{↓} ⊢ B ⇑
∧I
Γ^{↓} ⊢ A ∧ B ⇑

\begin{aligned}Γ^{↓} ⊢ A ∧ B ↓ \\ & ∧E_{L} \\ Γ^{↓} ⊢ A ↓ \end{aligned}  \begin{aligned}Γ^{↓} ⊢ A ∧ B ↓ \\ & ∧E_{R} \\ Γ^{↓} ⊢ B ↓ \end{aligned}

Truth. For truth, there is only an introduction rule which is classified as normal.

\frac{⊤I}{Γ^{↓} ⊢ ⊤ ⇑}

Implication. The introduction rule for implication is straightforward. In the elimination rule we require that the the second premise is normal. It is only the first premise (whose primary connective is eliminated in this rule) which must be extracted from a hypothesis.

\begin{matrix}Γ^{↓}, u:A ↓ ⊢ B ⇑ \\ ⊃I & u \\ Γ^{↓} ⊢ A ⊃ B ⇑ \end{matrix}  \begin{aligned}Γ^{↓} ⊢ A ⊃ B ↓  Γ^{↓} ⊢ A ⇑ \\ & ⊃E \\ Γ^{↓} ⊢ B ↓ \end{aligned}

Draft of November 12, 1999

Disjunction. The introduction rules for disjunction are straightforward. For the elimination rule, again the premise with the connective which is eliminated must have a top-down derivation. The new assumptions in each branch also are top-down derivations. Overall, for the derivation to be normal we must require the derivations of both premises to be normal.

\begin{aligned}Γ^{↓} ⊢ A ⇑ \\ & ∨I_{L} \\ Γ^{↓} ⊢ A ∨ B ⇑ \end{aligned}  \begin{aligned}Γ^{↓} ⊢ B ⇑ \\ & ∨I_{R} \\ Γ^{↓} ⊢ A ∨ B ⇑ \end{aligned}
Γ^{↓} ⊢ A ∨ B ↓  Γ^{↓}, u:A ↓ ⊢ C ⇑  Γ^{↓}, w:B ↓ ⊢ C ⇑
∨E^{u,w}
Γ^{↓} ⊢ C ⇑

It would also be consistent to allow the derivations of C to be extractions, but it is not necessary to obtain a complete search procedure and complicates the relation to the sequent calculus (see Exercise 3.1).

Falsehood. Falsehood corresponds to a disjunction with no alternatives. Therefore there is no introduction rule, and the elimination rule has no cases. This consideration yields

\begin{aligned}Γ^{↓} ⊢ ⊥ ↓ \\ & ⊥E. \\ Γ^{↓} ⊢ C ⇑ \end{aligned}

For this rule, it does not appear to make sense to allow the conclusion as having been constructed top-down, since the proposition C would be completely unrestricted.

Negation. Negation combines elements from implication and falsehood, since we may think of ¬A as A ⊃ ⊥.^{1}

\begin{matrix}Γ^{↓}, u:A ↓ ⊢ p ⇑ \\ ¬I & p,u \\ Γ^{↓} ⊢ ¬A ⇑ \end{matrix}  \begin{aligned}Γ^{↓} ⊢ ¬A ↓  Γ^{↓} ⊢ A ⇑ \\ & ¬E \\ Γ^{↓} ⊢ C ⇑ \end{aligned}

Universal Quantification. Universal quantification does not introduce any new considerations.

\begin{aligned}Γ^{↓} ⊢ [a/x]A ⇑ \\ & ∀I^{a} \\ Γ^{↓} ⊢ ∀x. A ⇑ \end{aligned}  \begin{aligned}Γ^{↓} ⊢ ∀x. A ↓ \\ & ∀E \\ Γ^{↓} ⊢ [t/x]A ↓ \end{aligned}

Existential Quantification. Existential quantification is similar to disjunction and a more lenient view of extraction is possible here, too (see Exercise 3.1).

\begin{aligned}Γ^{↓} ⊢ [t/x]A ⇑ \\ & ∃I \\ Γ^{↓} ⊢ ∃x. A ⇑ \end{aligned}  \begin{aligned}Γ^{↓} ⊢ ∃x. A ↓  Γ^{↓}, u:[a/x]A ↓ ⊢ C ⇑ \\ & ∃E^{a,u} \\ Γ^{↓} ⊢ C ⇑ \end{aligned}

1[reconsider]

Draft of November 12, 1999

It is quite easy to see that normal and extraction derivations are sound with respect to natural deduction. In order to state and prove this theorem, we introduce some conventions. Given a context

Γ^{↓} = u_{1}:A_{1} ↓, …, u_{n}:A_{n} ↓

we denote

u_{1}:A_{1}, …, u_{n}:A_{n}

by Γ and vice versa.

Theorem 3.1 (Soundness of Normal Deductions)

1. If Γ^{↓} ⊢ A ⇑ then Γ ⊢ A, and

2. if Γ^{↓} ⊢ A ↓ then Γ ⊢ A.

Proof: By induction on the structure of the given derivations. We show only three cases, since the proof is absolutely straightforward. Case:

E = \frac{u}{Γ_{1}^{↓}, u:A ↓, Γ_{2}^{↓} ⊢ A ↓}

The we construct directly Γ_{1}, u:A, Γ_{2} ⊢ A.

Case:

N = \begin{matrix}E \\ Γ^{↓} ⊢ A ↓ \end{matrix} ; ↓⇑ ; Γ^{↓} ⊢ A ⇑

Then Γ ⊢ A by induction hypothesis on E.

Case:

N = \begin{matrix}N_{2} \\ Γ^{↓}, u:A_{1} ↓ ⊢ A_{2} ⇑ \end{matrix} ; ⊃I^{u} ; Γ^{↓} ⊢ A_{1} ⊃ A_{2} ⇑

Γ, u:A_{1} ⊢ A_{2}  By i.h. on N_{2}
Γ ⊢ A_{1} ⊃ A_{2}  By rule ⊃I
□

When trying to give a translation in the other direction we encounter a difficulty: certain patterns of inference cannot be annotated directly. For example, consider

\begin{matrix}D \\ Γ ⊢ A \end{matrix}  \begin{matrix}E \\ Γ ⊢ B \end{matrix}

∧I Γ ⊢ A ∧ B

∧E_{L}.

Γ ⊢ A

If we try to classify each judgment, we obtain a conflict:

\begin{matrix}D′ \\ Γ ⊢ A ⇑ \end{matrix}  \begin{matrix}E′ \\ Γ ⊢ B ⇑ \end{matrix}

∧I Γ ⊢ A ∧ B ?

∧E_{L}.

Γ ⊢ A ↓

In this particular case, we can avoid the conflict: in order to obtain the derivation of A ⇑ we can just translate the derivation D and avoid the final two inferences! In general, we can try to apply local reductions to the given original derivation until no situations of the form above remain. This approach is called normalization. It is not easy to prove that normalization terminates, and the situation is complicated by the fact that the local reductions alone do not suffice to transform an arbitrary natural deduction into normal form (see Exercise 3.2).

Here, we follow an alternative approach to prove completeness of normal deductions. First, we temporarily augment the system with another rule which makes the translation from natural deductions immediate. Then we relate the resulting system to a sequent calculus and show that the additional rule was redundant.

A candidate for the additional rule is easy to spot: we just add the missing coercion from normal to extraction deductions. Since all rules are present, we can just coerce back and forth as necessary in order to obtain a counterpart for any natural deduction in this extended system. Of course, the resulting derivations are no longer normal, which we indicate by decorating the turnstile with a “+”. The judgments Γ^{↓} ⊢^{+} A ⇑ and Γ^{↓} ⊢^{+} A ↓ are defined by all counterparts of all rules which define normal and extracting derivations, plus the rule

\begin{aligned}Γ^{↓} ⊢^{+} A ⇑ \\ & ⇑↓ \\ Γ^{↓} ⊢^{+} A ↓ \end{aligned}

Now the annotation in the example above can be completed.

\begin{matrix}D′ \\ Γ ⊢^{+} A ⇑ \end{matrix}  \begin{matrix}E′ \\ Γ ⊢^{+} B ⇑ \end{matrix}
∧I
Γ ⊢^{+} A ∧ B ⇑
⇑↓
Γ ⊢^{+} A ∧ B ↓
∧E_{L}
Γ ⊢^{+} A ↓

Both soundness and completeness of the extended calculus with respect to natural deduction is easy to see.

Theorem 3.2 (Soundness of Annotated Deductions)

1. If Γ^{↓} ⊢^{+} A ⇑ then Γ ⊢ A, and

2. if Γ^{↓} ⊢^{+} A ↓ then Γ ⊢ A.

Proof: By simultaneous induction over the structure of the given derivations. □

The constructive proof of the completeness theorem below will contain an algorithm for annotating a given natural deduction.

Theorem 3.3 (Completeness of Annotated Deductions)

1. If Γ ⊢ A then Γ^{↓} ⊢^{+} A ⇑, and

2. if Γ ⊢ A then Γ^{↓} ⊢^{+} A ↓.

Proof: By induction over the structure of the given derivation. We show only two cases.

Case:

D = \begin{aligned}\begin{matrix}D \\ Γ ⊢ B ⊃ A \end{matrix} & \begin{matrix}E \\ Γ ⊢ B \end{matrix} \\ & & ⊃E \\ Γ ⊢ A \end{aligned}

Γ^{↓} ⊢^{+} B ⊃ A ↓  By i.h. (2) on D
Γ^{↓} ⊢^{+} B ⇑  By i.h. (1) on E
Γ^{↓} ⊢^{+} A ↓  By rule ⊃E, proving (2)
Γ^{↓} ⊢^{+} A ⇑  By rule ↓⇑, proving (1)

Case:

D = \begin{matrix}D_{2} \\ Γ, u:A_{1} ⊢ A_{2} \end{matrix} ; ⊃I^{u} ; Γ ⊢ A_{1} ⊃ A_{2}

Γ^{↓}, u:A_{1} ↓ ⊢^{+} A_{2} ⇑  By i.h. (1) on D_{2}
Γ^{↓} ⊢^{+} A_{1} ⊃ A_{2} ⇑  By rule ⊃I^{u}, proving (1)
Γ^{↓} ⊢^{+} A_{1} ⊃ A_{2} ↓  By rule ⇑↓, proving (2)
□

Even though natural deductions and annotated deductions are very similar, they are not in bijective correspondence. For example, in an annotated deduction we can simply alternate the two coercions an arbitrary number of times. Under the translation to natural deduction, all of these are identified.

Before we introduce the sequent calculus, we make a brief excursion to study the impact of annotations on proof terms.

3.2 Compact Proof Terms

The proof terms introduced in Section 2.4 sometimes contain significant amounts of redundant information. The reason are the propositions which label λabstractions and also occur in the inl^{A}, inr^{A}, μ^{p}u:A, ·_{A}, and abort^{A} constructs. For example, assume we are given a proof term λu:A. M and we are supposed to check if it represents a proof of A′ ⊃B. We then have to check that A = A′ and, moreover, the information is duplicated. The reason for this duplication was the intended invariant that every term proves a unique proposition. Under the interpretations of propositions as types, this means we can always synthesize a unique type for every valid term. However, we can improve this if we alternate between synthesizing a type and checking a term against a given type.

Therefore we introduce two classes of terms: those whose type can be synthesized, and those which can be checked against a type. Interestingly, this corresponds precisely with the annotations as introduction or elimination rules given above. We ignore negation again, thinking of ¬A as A ⊃ ⊥. We already discussed why the eliminations for disjunction and falsehood appear among the intro terms.

Intro Terms I ::= ⟨I_{1}, I_{2}⟩  Conjunction
| λu. I  Implication
| inl I | inr I  Disjunction
| ( case E of inl u_{1} ⇒ I_{1} | inr u_{2} ⇒ I_{2})
| ⟨ ⟩  Truth
| abort E  Falsehood
| E  Coercion
Elim Terms E ::= u  Hypotheses
| E I  Implication
| fst E | snd E  Conjunction
| (I : A)  Coercion

The presence of E as an intro term corresponds to the coercion ↓⇑ which is present in normal deductions. The presence of (I : A) as an elim term corresponds to the coercion ⇑↓ which is present only in the extended system. Therefore, a normal deduction can be represented without any internal type information, while a general deduction requires information at the point where an introduction rule is directly followed by an elimination rule. It is easy to endow the annotated natural deduction judgments with the modified proof terms from above. We leave the details to Exercise 3.3. The two judgments are Γ^{↓} ⊢^{+} I : A ⇑ and Γ^{↓} ⊢^{+} E : A ↓.

Now we can prove the correctness of bi-directional type-checking.

Theorem 3.4 (Bi-Directional Type-Checking)

1. Given Γ^{↓}, I, and A. Then either Γ^{↓} ⊢^{+} I : A ⇑ or not.

2. Given Γ^{↓} and E. Then either there is a unique A such that Γ^{↓} ⊢^{+} E : A ↓ or there is no such A.

Proof: See Exercise 3.3. □

3.3 Sequent Calculus

In Section 3.1 we introduced normal deductions which embody the strategy that proof search should proceed only bottom-up via introduction rules and top-down via elimination rules. The bi-directional nature of this calculus makes it somewhat unwieldy when it comes to the study of meta-theoretic properties and, in particular, complicates its completeness proof. In this section we develop a closely related calculus in which all proof search steps proceed bottom-up. Pictorially, we would like to flip the elimination rules upside-down.

[figure: Hypotheses; Eliminations; ↓⇑; Introductions; ⇝; Initial Sequents; Right Rules; Left Rules]

This transformation turns introduction rules into so-called right rules, and upside-down elimination rules into so-called left rules. We have two judgments, A left (A is a proposition on the left) and A right (A is a proposition on the right). They are assembled into the form of a hypothetical judgment

u_{1}:A_{1} left, …, u_{n}:A_{n} left ⊢ A right.

We call such a hypothetical judgment a sequent.

Note that the proposition A on the right directly corresponds to the proposition whose truth is established by a natural deduction. On the other hand, propositions on the left do not directly correspond to hypotheses in natural deduction, since in general they include hypotheses and propositions derived from them by elimination rules.

Keeping this intuition in mind, the inference rules for sequents can now be constructed mechanically from the rules for normal and extracting derivations. To simplify the notation, we denote the sequent above by

A_{1}, …, A_{n} ⟹ A

where the judgments left and right are implied by the position of the propositions. Moreover, labels u_{i} are suppressed until we introduce proof terms. Finally, left rules may be applied to any left proposition. Since the order of the left propositions is irrelevant, we write Γ, A instead of the more pedantic Γ, A, Γ′.

Initial Sequents. These correspond to the coercion from extraction to normal derivations, and not to the use of hypotheses in natural deductions.

\frac{init}{Γ, A ⟹ A}

Conjunction. The right and left rules are straightforward and provide a simple illustration of the translation, in particular in the way the elimination rules are turned upside-down.

Γ ⟹ A Γ ⟹ B ∧R Γ ⟹ A ∧ B

\begin{aligned}Γ, A ∧ B, A ⟹ C \\ & ∧L_{1} \\ Γ, A ∧ B ⟹ C \end{aligned}  \begin{aligned}Γ, A ∧ B, B ⟹ C \\ & ∧L_{2} \\ Γ, A ∧ B ⟹ C \end{aligned}

In the introduction rule (read bottom-up), we propagate Γ to both premises. This reflects that in natural deduction we can use any available assumption freely in both subdeductions. Furthermore, in the elimination rule the hypothesis A ∧ B left persists. This reflects that assumptions in natural deduction may be used more than once. Later we analyze which of these hypotheses are actually needed and eliminate some redundant ones. For now, however, they are useful because they allow us to give a very direct translation to and from normal natural deductions.

Implication. The right rule for implication is straightforward. The left rule requires some thought. Using an extracted implication A ⊃ B gives rise to two subgoals: we have to find a normal proof of A, but we also still have to prove our overall goal, now with the additional extracted proposition B.

\begin{aligned}Γ, A ⟹ B \\ & ⊃R \\ Γ ⟹ A ⊃ B \end{aligned}  \begin{aligned}Γ, A ⊃ B ⟹ A  Γ, A ⊃ B, B ⟹ C \\ & ⊃L \\ Γ, A ⊃ B ⟹ C \end{aligned}

Disjunction. This introduces no new considerations.

\begin{aligned}Γ ⟹ A \\ & ∨R_{1} \\ Γ ⟹ A ∨ B \end{aligned}  \begin{aligned}Γ ⟹ B \\ & ∨R_{2} \\ Γ ⟹ A ∨ B \end{aligned}
Γ, A ∨ B, A ⟹ C Γ, A ∨ B, B ⟹ C

∨L Γ, A ∨ B ⟹ C

Negation. Negation requires a judgment parametric in a proposition. Sometimes, this is encoded as an empty right-hand side (see Exercise 3.6).

\begin{aligned}Γ, A ⟹ p \\ & ¬R^{p} \\ Γ ⟹ ¬A \end{aligned}  \begin{aligned}Γ, ¬A ⟹ A \\ & ¬L \\ Γ, ¬A ⟹ C \end{aligned}

Truth. By our general method, there is no left rule, only a right rule which models the introduction rule.

\frac{⊤R}{Γ ⟹ ⊤}

Falsehood. Again by our general method, there is no right rule, only a left rule which models the (upside-down) elimination rule.

\frac{⊥L}{Γ, ⊥ ⟹ C}

Universal Quantification. These require only a straightforward transcription, with the appropriate translation of the side condition.

\begin{aligned}Γ ⟹ [a/x]A \\ & ∀R^{a} \\ Γ ⟹ ∀x. A \end{aligned}  \begin{aligned}Γ, ∀x. A, [t/x]A ⟹ C \\ & ∀L \\ Γ, ∀x. A ⟹ C \end{aligned}

Existential Quantification. Again, the rules can be directly constructed from the introduction and elimination rule of natural deduction.

\begin{aligned}Γ ⟹ [t/x]A \\ & ∃R \\ Γ ⟹ ∃x. A \end{aligned}  \begin{aligned}Γ, ∃x. A, [a/x]A ⟹ C \\ & ∃L^{a} \\ Γ, ∃x. A ⟹ C \end{aligned}

The intended theorem describing the relationship between sequent calculus and natural deduction states that Γ^{↓} ⊢ A ⇑ if and only if Γ ⟹ A. Prima facie is unlikely that we can prove either of these directions without further generalization, since the judgments Γ^{↓} ⊢ A ⇑ and Γ^{↓} ⊢ A ↓ are mutually recursive, and the statement above does not even mention the latter.

In preparation for the upcoming proof, we recall the general property of hypothetical judgments, namely that we can substitute a derivation of the appropriate judgment for a hypothesis. When applied to normal and extracting derivations, this yields the following property.

Lemma 3.5 (Substitution Property for Extractions)

1. If Γ_{1}^{↓}, u:A ↓, Γ_{2}^{↓} ⊢ C ⇑ and Γ_{1}^{↓} ⊢ A ↓ then Γ_{1}^{↓}, Γ_{2}^{↓} ⊢ C ⇑.

2. If Γ_{1}^{↓}, u:A ↓, Γ_{2}^{↓} ⊢ C ↓ and Γ_{1}^{↓} ⊢ A ↓ then Γ_{1}^{↓}, Γ_{2}^{↓} ⊢ C ↓.

Proof: By induction on the structure of the given derivations of C ⇑ and C ↓. In the case where the hypothesis is used we employ weakening, that is, we adjoin the additional hypotheses Γ_{2}^{↓} to every judgment in the derivation of Γ_{1}^{↓} ⊢ A ↓. □

Using this lemma, a direct proof goes through (somewhat surprisingly).

Theorem 3.6 (Soundness of Sequent Calculus) If Γ ⟹ C then Γ^{↓} ⊢ C ⇑.

Proof: By induction on the structure of the given derivation S. We show a few representative cases.

Case: Initial sequents.

\frac{init}{Γ, C ⟹ C}

Γ^{↓}, u:C ↓ ⊢ C ↓  By hypothesis u
Γ^{↓}, u:C ↓ ⊢ C ⇑  By rule ↓⇑

This case confirms that initial sequents correspond to the coercion from extractions to normal deductions.

Case: Implication right rule.

\begin{matrix}S_{2} \\ Γ, C_{1} ⟹ C_{2} \end{matrix}

⊃R

Γ ⟹ C_{1} ⊃ C_{2}

Γ^{↓}, u:C_{1} ↓ ⊢ C_{2} ⇑  By i.h. on S_{2}
Γ^{↓} ⊢ C_{1} ⊃ C_{2} ⇑  By rule ⊃I^{u}

This case exemplifies how right rules correspond directly to introduction rules.

Case: Implication left rule.

\begin{matrix}S_{1} \\ Γ, A_{1} ⊃ A_{2} ⟹ A_{1} \end{matrix}  \begin{matrix}S_{2} \\ Γ, A_{1} ⊃ A_{2}, A_{2} ⟹ C \end{matrix}
⊃L
Γ, A_{1} ⊃ A_{2} ⟹ C
Γ^{↓}, u:A_{1} ⊃ A_{2} ↓ ⊢ A_{1} ⇑  By i.h. on S_{1}
Γ^{↓}, u:A_{1} ⊃ A_{2} ↓ ⊢ A_{1} ⊃ A_{2} ↓  By hypothesis u
Γ^{↓}, u:A_{1} ⊃ A_{2} ↓ ⊢ A_{2} ↓  By rule ⊃E
Γ^{↓}, u:A_{1} ⊃ A_{2} ↓, w:A_{2} ↓ ⊢ C ⇑  By i.h. on S_{2}
Γ^{↓}, u:A_{1} ⊃ A_{2} ↓ ⊢ C ⇑  By substitution property (Lemma 3.5)

This case illustrates how left rules correspond to elimination rules. The general pattern is that the result of applying the appropriate elimination rule is substituted for a hypothesis.

□

The proof of completeness is somewhat trickier—we first need to generalize the induction hypothesis. Generalizing a desired theorem so that a direct inductive proof is possible often requires considerable ingenuity and insight into the problem. In this particular case, the generalization is of medium difficulty.

The reader who has not seen the proof is invited to test his understanding by carrying out the generalization and proof himself before reading on.

The nature of a sequent as a hypothetical judgment gives rise to several general properties we will take advantage of. We make two of them, weakening and contraction, explicit in the following lemma.

Lemma 3.7 (Structural Properties of Sequents)

1. (Weakening) If Γ ⟹ C then Γ, A ⟹ C.

2. (Contraction) If Γ, A, A ⟹ C then Γ, A ⟹ C.

Proof: First, recall our general convention that we consider the hypotheses of a sequent modulo permutation. We prove each property by a straightforward induction over the structure of the derivation. In the case of weakening we adjoin an unused hypothesis A left to each sequent in the derivation. In the case of contraction we replace any use of either of the two hypotheses by a common hypothesis. □

The theorem below only establishes the completeness of sequent derivations with respect to normal deductions. That is, at this point we have not established the completeness of sequents with respect to arbitrary natural deductions which is more difficult.

Theorem 3.8 (Completeness of Sequent Derivations)

1. If Γ^{↓} ⊢ C ⇑ then Γ ⟹ C.

2. If Γ^{↓} ⊢ A ↓ and Γ, A ⟹ C then Γ ⟹ C.

Proof: By induction on the structure of the given derivations I and E. We show some representative cases.

Case: Use of hypotheses.

E = \frac{u}{Γ_{1}^{↓}, u:A ↓, Γ_{2}^{↓} ⊢ A ↓}

Γ_{1}, A, Γ_{2}, A ⟹ C  Assumption
Γ_{1}, A, Γ_{2} ⟹ C  By contraction (Lemma 3.7)

Case: Coercion.

I = \begin{matrix}E \\ Γ^{↓} ⊢ C ↓ \end{matrix} ; ↓⇑ ; Γ^{↓} ⊢ C ⇑

Γ, C ⟹ C  By rule init
Γ ⟹ C  By i.h. on E

Case: Implication introduction.

I = \begin{matrix}I_{2} \\ Γ^{↓}, u:C_{1} ↓ ⊢ C_{2} ⇑ \end{matrix} ; ⊃I^{u} ; Γ^{↓} ⊢ C_{1} ⊃ C_{2} ⇑

Γ, C_{1} ⟹ C_{2}  By i.h. on I_{2}
Γ ⟹ C_{1} ⊃ C_{2}  By rule ⊃R

Case: Implication elimination.

E = \begin{aligned}\begin{matrix}E_{2} \\ Γ^{↓} ⊢ A_{1} ⊃ A_{2} ↓ \end{matrix} & \begin{matrix}I_{1} \\ Γ^{↓} ⊢ A_{1} ⇑ \end{matrix} \\ & & ⊃E \\ Γ^{↓} ⊢ A_{2} ↓ \end{aligned}

Γ, A_{2} ⟹ C  Assumption
Γ, A_{1} ⊃ A_{2}, A_{2} ⟹ C  By weakening (Lemma 3.7)
Γ ⟹ A_{1}  By i.h. on I_{1}
Γ, A_{1} ⊃ A_{2} ⟹ A_{1}  By weakening (Lemma 3.7)
Γ, A_{1} ⊃ A_{2} ⟹ C  By rule ⊃L
Γ ⟹ C  By i.h. on E_{2}
□

In order to establish soundness and completeness with respect to arbitrary natural deductions we establish a connection to annotated natural deductions. Recall that this is an extension of normal deductions which we showed sound and complete with respect to arbitrary natural deduction in Theorems 3.2 and 3.3. We related annotated natural deductions to the sequent calculus by adding a rule called cut.

We write the extended judgment of sequent derivations with cut as Γ ⟹^{+} C. It is defined by copies of all the rules for Γ ⟹ C, plus the rule of cut:

Γ ⟹^{+} A Γ, A ⟹^{+} C

cut

Γ ⟹^{+} C

Thought of from the perspective of bottom-up proof construction, this rule corresponds to proving and then assuming a lemma A during a derivation.

Theorem 3.9 (Soundness of Sequent Calculus with Cut) If Γ ⟹^{+} C then Γ^{↓} ⊢^{+} C ⇑.

Proof: As in Theorem 3.6 by induction on the structure of the given derivation S, with one additional case.

Case: Cut.

S = \begin{aligned}\begin{matrix}S_{1} \\ Γ ⟹ A \end{matrix} & \begin{matrix}S_{2} \\ Γ, A ⟹ C \end{matrix} \\ & & cut \\ & Γ ⟹ C \end{aligned}

Γ^{↓} ⊢^{+} A ⇑  By i.h. on S_{1}
Γ^{↓} ⊢^{+} A ↓  By rule ⇑↓
Γ^{↓}, u:A ↓ ⊢^{+} C ⇑  By i.h. on S_{2}
Γ^{↓} ⊢^{+} C ⇑  By substitution (Lemma 3.5, generalized)

We see that, indeed, cut corresponds to the coercion from normal to extraction derivations.

□

Theorem 3.10 (Completeness of Sequent Calculus with Cut)

1. If Γ^{↓} ⊢^{+} C ⇑ then Γ ⟹^{+} C.

2. If Γ^{↓} ⊢^{+} A ↓ and Γ, A ⟹^{+} C then Γ ⟹^{+} C.

Proof: As in the proof of Theorem 3.10 with one additional case.

Case: Coercion from normal to extraction derivations.

E = \begin{matrix}I \\ Γ^{↓} ⊢^{+} A ⇑ \end{matrix} ; ⇑↓ ; Γ^{↓} ⊢^{+} A ↓

Γ ⟹ A  By i.h. on I
Γ, A ⟹ C  By assumption
Γ ⟹ C  By rule cut
□

The central property of the sequent calculus is that the cut rule is redundant. That is, if Γ ⟹^{+} C then Γ ⟹ C. This so-called cut elimination theorem (Gentzen’s Hauptsatz [Gen35]) is one of the central theorems of logic. As an immediately consequence we can see that not every proposition has a proof, since no rule is applicable to derive · ⟹ ⊥. In the system with cut, a derivation of this sequent might end in the cut rule and consistency is not at all obvious. The proof of cut elimination and some of its many consequences are the subject of the next section.

3.4 Cut Elimination

This section is devoted to proving that the rule of cut is redundant in the sequent calculus. First we prove that cut is admissible: whenever the premises of the cut rule are derivable in the sequent calculus without cut, then the conclusion is. It is a simple observation that adding an admissible rule to a deductive system does not change the derivable judgments. Formally, this second step is an induction over the structure of a derivation that may contain cuts, proving that if Γ ⟹^{+} C then Γ ⟹ C.

There is a stronger property we might hope to prove for cut: it could be a derived rule of inference. Derived rules have a direct deduction of the conclusion from the premises within the given system. For example,

\frac{Γ ⊢ A  Γ ⊢ B  Γ ⊢ C}{Γ ⊢ A ∧ (B ∧ C)}

is a derived rule, as evidenced by the following deduction:

Γ ⊢ A \begin{aligned}Γ ⊢ B Γ ⊢ C \\ & ∧I \\ Γ ⊢ B ∧ C \end{aligned}

∧I. Γ ⊢ A ∧ (B ∧ C)

Derived rules have the property that they remain valid under all extensions of a given system. Admissible rules, on the other hand, have to be reconsidered when new connectives or inference rules are added to a system, since these rules may invalidate the proof of admissibility.

It turns out that cut is only admissible, but not derivable in the sequent calculus. Therefore, we will prove the following theorem:

If Γ ⟹ A and Γ, A ⟹ C then Γ ⟹ C.

We call A the cut formula. Also, each left or right rule in the sequent calculus focuses on an occurrence of a proposition in the conclusion, called the principal formula of the inference.

The proof combines two ideas: induction over the structure of the cut formula with induction over the structures of the two given derivations. They are combined into one nested induction: an outer induction over the structure of the cut formula and an inner induction over the structure of the derivations of the premises. The outer induction over the structure of the cut formula is related to local reductions in natural deduction (see Exercise 3.7).

Theorem 3.11 (Admissibility of Cut) If Γ ⟹ A and Γ, A ⟹ C then Γ ⟹ C.

Proof: By nested inductions on the structure of A, the derivation D of Γ ⟹ A and E of Γ, A ⟹ C. More precisely, we appeal to the induction hypothesis either with a strictly smaller cut formula, or with an identical cut formula and two derivations, one of which is strictly smaller while the other stays the same. The proof is constructive, which means we show how to transform

\begin{matrix}D \\ Γ ⟹ A \end{matrix}  and  \begin{matrix}E \\ Γ, A ⟹ C \end{matrix}  to  \begin{matrix}F \\ Γ ⟹ C. \end{matrix}

The proof is divided into several classes of cases. More than one case may be applicable, which means that the algorithm for constructing the derivation of Γ ⟹ C from the two given derivations is naturally non-deterministic.

Case: D is an initial sequent.

D = \frac{init}{Γ′, A ⟹ A}

Γ = Γ′, A  This case
Γ′, A, A ⟹ C  Derivation E
Γ′, A ⟹ C  By contraction (Lemma 3.7)
Γ ⟹ C  By equality

Case: E is an initial sequent using the cut formula.

E = \frac{init}{Γ, A ⟹ A}

C = A  This case
Γ ⟹ A  Derivation D

Case: E is an initial sequent not using the cut formula.

E = \frac{init}{Γ′, C, A ⟹ C}

Γ = Γ′, C  This case
Γ′, C ⟹ C  By rule init
Γ ⟹ C  By equality

Case: A is the principal formula of the final inference in both D and E. There are a number of subcases to consider, based on the last inference in D and E. We show some of them. Subcase:

D = \begin{aligned}\begin{matrix}D_{1} \\ Γ ⟹ A_{1} \end{matrix} & \begin{matrix}D_{2} \\ Γ ⟹ A_{2} \end{matrix} \\ & ∧R \\ Γ ⟹ A_{1} ∧ A_{2} \end{aligned}

and E = \begin{matrix}E_{1} \\ Γ, A_{1} ∧ A_{2}, A_{1} ⟹ C \end{matrix} ; ∧L_{1} ; Γ, A_{1} ∧ A_{2} ⟹ C

Draft of November 12, 1999

Γ, A_{1} ⟹ C  By i.h. on A_{1} ∧ A_{2}, D and E_{1}
Γ ⟹ C  By i.h. on A_{1} from above and D_{1}

Actually we have ignored a detail: in the first appeal to the induction hypothesis, E_{1} has an additionaly hypothesis (A_{1} left) and therefore does not match the statement of the theorem precisely. However, we can always weaken D to include this additional hypothesis without changing the structure of D (see the proof of Lemma 3.7) and then appeal to the induction hypothesis. We will not be explicit about these trivial weakening steps in the remaining cases.

Subcase:

D = \begin{matrix}D_{2} \\ Γ, A_{1} ⟹ A_{2} \end{matrix} ; ⊃R ; Γ ⟹ A_{1} ⊃ A_{2}

and E = \begin{aligned}\begin{matrix}E_{1} \\ Γ, A_{1} ⊃ A_{2} ⟹ A_{1} \end{matrix} & \begin{matrix}E_{2} \\ Γ, A_{1} ⊃ A_{2}, A_{2} ⟹ C \end{matrix} \\ & ⊃L \\ Γ, A_{1} ⊃ A_{2} ⟹ C \end{aligned}

Γ ⟹ A_{1}  By i.h. on A_{1} ⊃ A_{2}, D and E_{1}
Γ ⟹ A_{2}  By i.h. on A_{1} from above and D_{2}
Γ, A_{2} ⟹ C  By i.h. on A_{1} ⊃ A_{2}, D and E_{2}
Γ ⟹ C  By i.h. on A_{2} from above

Subcase:

D = \begin{matrix}D_{1} \\ Γ, A_{1} ⟹ p \end{matrix} ; ¬R^{p} ; Γ ⟹ ¬A_{1}

and E = \begin{matrix}E_{1} \\ Γ, ¬A_{1} ⟹ A_{1} \end{matrix} ; ¬L ; Γ, ¬A_{1} ⟹ C

Γ ⟹ A_{1}  By i.h. on D and E_{1}
Γ, A_{1} ⟹ C  By substitution for parameter C in D_{1}
Γ ⟹ C  By i.h. on A_{1} from above

Note that the condition that p be a new parameter in D_{1} is necessary to guarantee that in the substitution step above we have [C/p]A_{1} = A_{1} and [C/p]Γ = Γ.

Subcase:

D = \begin{matrix}D_{1} \\ Γ ⟹ [t/x]A_{1} \end{matrix} ; ∃R ; Γ ⟹ ∃x. A_{1}

and E = \begin{matrix}E_{1} \\ Γ, ∃x. A_{1}, [a/x]A_{1} ⟹ C \end{matrix} ; ∃L^{a} ; Γ, ∃x. A_{1} ⟹ C

Γ, [t/x]A_{1} ⟹ C  By substitution for parameter a in E_{1}
Γ, [t/x]A_{1} ⟹ C  By i.h. on ∃x. A_{1}, D and [t/a]E_{1}
Γ ⟹ C  By i.h. on [t/x]A_{1} from D_{1} and above

Note that this case requires that [t/x]A_{1} is considered smaller than ∃x. A_{1}. Formally, this can be justified by counting the number of quantifiers and connectives in a proposition and noting that the term t does not contain any. A similar remark applies to check that [t/a]E_{1} is smaller than E. Also note how the side condition that a must be a new parameter in the ∃L rule is required in the substitution step to conclude that [t/a]Γ = Γ, [t/a][a/x]A_{1} = [t/x]A_{1}, and [t/a]C.

Case: A is not the principal formula of the last inference in D. In that case D must end in a left rule and we can appeal to the induction hypothesis on one of its premises. We show some of the subcases.

Subcase:

D = \begin{matrix}D_{1} \\ Γ′, B_{1} ∧ B_{2}, B_{1} ⟹ A \end{matrix} ; ∧L_{1} ; Γ′, B_{1} ∧ B_{2} ⟹ A

Γ = Γ′, B_{1} ∧ B_{2}  This case
Γ′, B_{1} ∧ B_{2}, B_{1} ⟹ C  By i.h. on A, D_{1} and E
Γ′, B_{1} ∧ B_{2} ⟹ C  By rule ∧L_{1}
Γ ⟹ C  By equality

Subcase:

D = \begin{aligned}\begin{matrix}D_{1} \\ Γ′, B_{1} ⊃ B_{2} ⟹ B_{1} \end{matrix} & \begin{matrix}D_{2} \\ Γ′, B_{1} ⊃ B_{2}, B_{2} ⟹ A \end{matrix} \\ & ⊃L \\ Γ′, B_{1} ⊃ B_{2} ⟹ A \end{aligned}

Γ = Γ′, B_{1} ⊃ B_{2}  This case
Γ′, B_{1} ⊃ B_{2}, B_{2} ⟹ C  By i.h. on A, D_{2} and E
Γ′, B_{2} ⊃ B_{2} ⟹ C  By rule ⊃L on D_{1} and above
Γ ⟹ C  By equality

Case: A is not the principal formula of the last inference in E. This overlaps with the previous case, since A may not be principal on either side. In this case, we appeal to the induction hypothesis on the subderivations of E and directly infer the conclusion from the results. We show some of the subcases. Subcase:

E = \begin{aligned}\begin{matrix}E_{1} \\ Γ, A ⟹ C_{1} \end{matrix} & \begin{matrix}E_{2} \\ Γ, A ⟹ C_{2} \end{matrix} \\ & ∧R \\ Γ, A ⟹ C_{1} ∧ C_{2} \end{aligned}

C = C_{1} ∧ C_{2}  This case
Γ ⟹ C_{1}  By i.h. on A, D and E_{1}
Γ ⟹ C_{2}  By i.h. on A, D and E_{2}
Γ ⟹ C_{1} ∧ C_{2}  By rule ∧R on above

Subcase:

E = \begin{matrix}E_{1} \\ Γ′, B_{1} ∧ B_{2}, B_{1}, A ⟹ C \end{matrix} ; ∧L_{1} ; Γ′, B_{1} ∧ B_{1}, A ⟹ C

Γ = Γ′, B_{1} ∧ B_{2}  This case
Γ′, B_{1} ∧ B_{2}, B_{1} ⟹ C  By i.h. on A, D and E_{1}
Γ′, B_{1} ∧ B_{2} ⟹ C  By rule ∧L_{1} from above
□

As mentioned above, it is a general property of deductive system that adding an admissible rule does not change the derivable judgments. We show the argument in this special case.

Theorem 3.12 (Cut Elimination) If Γ ⟹^{+} C then Γ ⟹ C.

Proof: In each case except cut we simply appeal to the induction hypotheses and reapply the same rule on the resulting cut-free derivations. So we write out only the case of cut. Case:

D^{+} = \begin{aligned}\begin{matrix}D_{1}^{+} \\ Γ ⟹^{+} A \end{matrix} & \begin{matrix}D_{2}^{+} \\ Γ, A ⟹^{+} C \end{matrix} \\ & & cut \\ & Γ ⟹^{+} C \end{aligned}

Γ ⟹ A  By i.h. on D_{1}^{+}
Γ, A ⟹ C  By i.h. on D_{2}^{+}
Γ ⟹ C  By admissibility of cut (Theorem 3.11)
□

3.5 Applications of Cut Elimination

The cut elimination theorem is the final piece needed to complete our study of natural deduction and normal natural deduction and at the same time the springboard to the development of efficient theorem proving procedures. Our proof in the previous section is constructive and therefore contains an algorithm for cut elimination. Because the cases are not mutually exclusive, the algorithm is non-deterministic. However, the resulting derivation should always be the same. While this property does not quite hold, the different derivations can be shown to be equivalent in a natural sense. This is called the confluence property for intuitionistic cut elimination modulo commutative conversions. It it is not implicit in our proof, but has to be established separately.^{2} On the other hand, our proof shows that any possible execution of the cut-elimination algorithm terminates. This is called the strong normalization property for the sequent calculus.

By putting the major results of this chapter together we can now prove the normalization theorem for natural deduction.

Theorem 3.13 (Normalization for Natural Deduction) If Γ ⊢ A then Γ^{↓} ⊢ A ⇑.

Proof: Direct from previous theorems.

Γ ⊢ A  Assumption
Γ^{↓} ⊢^{+} A ⇑  By completeness of annotated deductions (Theorem 3.3)
Γ ⟹^{+} A  By completeness of sequent calculus with cut (Theorem 3.10)
Γ ⟹ A  By cut elimination (Theorem 3.12)
Γ^{↓} ⊢ A ⇑  By soundness of sequent calculus (Theorem 3.6)
□

Among the other consequences of cut elimination are consistency and various independence results.

Corollary 3.14 (Consistency) There is no deduction of ⊢ ⊥.

Proof: Assume there is a deduction ⊢ ⊥. By the results of this chapter then · ⟹ ⊥. However, this sequent cannot be the conclusion of any inference rule in the (cut-free) sequent calculus. Therefore ⊢ ⊥ cannot be derivable. □

In the same category are the following two properties. As in the proof above, we analyze the inference rules which may have led to a given conclusion. This proof technique is called inversion.

Corollary 3.15 (Disjunction and Existential Property)

1. If ⊢ A ∨ B then either ⊢ A or ⊢ B.

2[reference?]

Draft of November 12, 1999

2. If ⊢ ∃x. A then ⊢ [t/x]A for some t.

Proof: Direct by inversion on possible sequent derivations in both cases.

1. Assume ⊢ A ∨ B. Then · ⟹ A ∨ B. By inversion, either · ⟹ A or · ⟹ B. Therefore ⊢ A or ⊢ B.

2. Assume ∃x. A. then · ⟹ ∃x. A. By inversion, · ⟹ [t/x]A for some t. Hence ⊢ [t/x]A.

□

Note that the disjunction and existential properties rely on a judgment without hypotheses. For example, we have B∨A ⟹ A∨B, but neither B∨A ⟹ A for B ∨ A ⟹ B hold.

The second class of properties are independence results which demonstrate that certain judgments are not derivable. As a rule, these are parametric judgments some instances of which may be derivable. For example, we will show that the law of excluded middle is independent. Nonetheless, there are some propositions A for which we can show ⊢ A ∨ ¬A (for example, take A = ⊥).

Corollary 3.16 (Independence of Excluded Middle) There is no deduction of ⊢ A ∨ ¬A for arbitrary A.

Proof: Assume there is a deduction of ⊢ A ∨ ¬A. By the result of this section then · ⟹ A ∨ ¬A. By inversion now either · ⟹ A or · ⟹ ¬A. The former judgment (which is parametric in A) has no derivation. By inversion, the latter can only be infered from A ⟹ p for a new parameter p. But there is no inference rule with this conclusion, and hence there cannot be a deduction of ⊢ A ∨ ¬A. □

3.6 Proof Terms for Sequent Derivations

In this section we address the question of how to assign proof terms to sequent calculus derivations. There are essentially two possibilities: we can either develop a new proof term calculus specifically for sequent derivations, or we can directly assign natural deduction proof terms. The former approach can be found, for example, in [Pfe95]. The latter is more appropriate for our purposes here, since we view natural deductions as defining truth and since we already devised methods for compact representations in Section 3.2.

We define a new judgment, Γ ⟹ I : A, maintaining that Γ ⊢ I : A. For this purpose we abandon the previous convention of omitting labels for hypotheses, since proof terms need to refer to them. On the other hand, we still consider assumptions modulo permutations in order to simplify notation. We use the compact proof terms here only for simplicity.

The proof terms to be assigned to each inference rule can be determined by a close examination of the soundness proof for the sequent calculus (Theorem 3.6).

Since that proof is constructive, it contains an algorithm for translating a sequent derivation to a normal natural deduction. We just have to write down the corresponding proof terms.

Initial Sequents. These are straightforward.

\frac{init}{Γ, u:A ⟹ u : A}

Note that there may be several hypotheses A with different labels. In the shorthand notation without labels before, it is ambiguous which one was used.

Conjunction. The right rule is straightforward, since it is isomorphic to the introduction rule for natural deduction. The left rules require a substitution to be carried out, just as in the proof of Theorem 3.6.

Γ ⟹ I : A Γ ⟹ J : B ∧R Γ ⟹ ⟨I, J⟩ : A ∧ B

\begin{aligned}Γ, u:A ∧ B, w:A ⟹ I : C \\ & ∧L_{1} \\ Γ, u:A ∧ B ⟹ [fst u/w]I : C \end{aligned}  \begin{aligned}Γ, u:A ∧ B, w:B ⟹ I : C \\ & ∧L_{2} \\ Γ, u:A ∧ B ⟹ [snd u/w]I : C \end{aligned}

There are two potential efficiency problems in the proof term assignment for the left rule. The first is that if w is used many times in I, then fst u or snd u may be replicated many times, leading to a large proof. The second is that when a number of successive left rules are encountered, the term I we substitute into will be traversed many times. These problems can be avoided in several ways (see Exercise ??).

Implication. The pattern of the previous right and left rules continues here.

\begin{aligned}Γ, u:A ⟹ I : B \\ & ⊃R \\ Γ ⟹ λu. I : A ⊃ B \end{aligned} ; \begin{aligned}Γ, u:A ⊃ B ⟹ J : A Γ, u:A ⊃ B, w:B ⟹ I : C \\ & ⊃L \\ Γ, u:A ⊃ B ⟹ [u J/w]I : C \end{aligned}

Disjunction. This introduces no new considerations.

\begin{aligned}Γ ⟹ I : A \\ & ∨R_{1} \\ Γ ⟹ inl I : A ∨ B \end{aligned}  \begin{aligned}Γ ⟹ J : B \\ & ∨R_{2} \\ Γ ⟹ inr J : A ∨ B \end{aligned}
Γ, u:A ∨ B, v:A ⟹ I : C Γ, u:A ∨ B, w:B ⟹ J : C
∨L
Γ, u:A ∨ B ⟹ ( case u of inl v ⇒ I | inr w ⇒ J) : C

Negation. This is similar to implication.^{3}

\begin{aligned}Γ, u:A ⟹ I : p \\ & ¬R^{p} \\ Γ ⟹ μ^{p}u. I : ¬A \end{aligned}  \begin{aligned}Γ, u:¬A ⟹ I : A \\ & ¬L \\ Γ, u:¬A ⟹ u · I : C \end{aligned}

Truth. This is trivial, since there is no left rule.

\frac{⊤R}{Γ ⟹ ⟨ ⟩ : ⊤}

Falsehood. Again, this is immediate.

\frac{⊥L}{Γ, u:⊥ ⟹ abortu : C}

To treat the quantifiers we extend our proof term calculus to handle the quantifier rules.^{4} We overload the notation by reusing λ-abstraction and pairing. There is no ambiguity, because the proof term for universal quantification binds a term variable x (rather than a proof variable u), and the first component of the pair for existential quantification is a first-order term, rather than a proof term as for conjunction.

First, we show the assignment of these terms to natural deductions, then to the sequent calculus.

Universal Quantification. The proof term for a universal quantifier ∀x. A is a function from a term t to a proof of [t/x]A. The elimination term applies this function.

\begin{aligned}Γ ⊢ [a/x]M : [a/x]A \\ & ∀I^{a} \\ Γ ⊢ λx. M : ∀x. A \end{aligned} ; \begin{aligned}Γ ⊢ M : ∀x. A \\ & ∀E \\ Γ ⊢ M t : [t/x]A \end{aligned}

The local reductions and expansions just mirror the corresponding operations on natural deductions.

(λx. M) t ⟶_{R} [t/x]M
M : ∀x. A ⟶_{E} λx. M x (x not free in M)

Existential Quantification. The proof term for an existential ∃x. A is a pair consisting of a witness term t and the proof of [t/x]A.

Γ ⊢ M : [t/x]A

∃I Γ ⊢ ⟨t, M⟩ : ∃x. A

Γ ⊢ M : ∃x. A Γ, u:[a/x]A ⊢ [a/x]N : C

∃E^{a,u} Γ ⊢ let ⟨x, u⟩ = M in N : C

4[move earlier]

3[add to compact proof term section]

Draft of November 12, 1999

The local reduction for the existential quantifier has to perform two substitutions, just as on natural deductions.

let ⟨x, u⟩ = ⟨t, M⟩ in N ⟶_{R} [M/u][t/x]N
M : ∃x. A ⟶_{E} let ⟨x, u⟩ = M in ⟨x, u⟩

It is once again easy to see how to divide the proof terms into introduction and elimination forms. We only show the resulting definition of compact proof terms.

Intro Terms I ::= …
| λx. I  Universal Quantification
| ⟨t, I⟩  Existential Quantification
| let ⟨x, u⟩ = E in I
Elim Terms E ::= … | E t  Universal Quantification

On sequent calculus derivations, we follow the same strategy as in the preceding propositional rules.

Universal Quantification.

\begin{aligned}Γ ⟹ [a/x]I : [a/x]A \\ & ∀R^{a} \\ Γ ⟹ λx. I : ∀x. A \end{aligned}  \begin{aligned}Γ, u:∀x. A, w:[t/x]A ⟹ I : C \\ & ∀L \\ Γ, u:∀x. A ⟹ [u t/w]I : C \end{aligned}

Existential Quantification.

\begin{aligned}Γ ⟹ I : [t/x]A \\ & ∃R \\ Γ ⟹ ⟨t, I⟩ : ∃x. A \end{aligned} Γ, u:∃x. A, w:[a/x]A ⟹ [a/x]I : C

∃L^{a} Γ, u:∃x. A ⟹ (let ⟨x, w⟩ = u in I) : C

3.7 Exercises

Exercise 3.1 Consider a system of normal deduction where the elimination rules for disjunction and existential are allowed to end in an extraction judgment.

Γ^{↓} ⊢ A ∨ B ↓  Γ^{↓}, u:A ↓ ⊢ C ↓  Γ^{↓}, w:B ↓ ⊢ C ↓
∨E^{u,w}
Γ^{↓} ⊢ C ↓
Γ^{↓} ⊢ ∃x. A ↓ Γ^{↓}, u:[a/x]A ↓ ⊢ C ↓
∃E^{a,u}
Γ^{↓} ⊢ C ↓

Discuss the relative merits of allowing or disallowing these rules and show how they impact the subsequent development in this Chapter (in particular, bidirectional type-checking and the relationship to the sequent calculus).

Exercise 3.2 1. Give an example of a natural deduction which is not normal (in the sense

defined in Section 3.1), yet contains no subderivation which can be locally reduced.

2. Generalizing from the example, devise additional rules of reduction so that any natural deduction which is not normal can be reduced. You should introduce no more and no fewer rules than you need for this purpose.

3. Prove that your rules satisfy the specification in part (2).

Exercise 3.3 Write out the rules defining the judgments Γ^{↓} ⊢^{+} I : A ⇑ and Γ^{↓} ⊢^{+} E : A ↓ and prove Theorem 3.4. Make sure to carefully state the induction hypothesis (if it is different from the statement of the theorem) and consider all the cases.

Exercise 3.4 Fill in the missing subcases in the proof of the admissibility of cut (Theorem 3.11) where A is the principal formula in both D and E.

Exercise 3.5 Consider an extension of intuitionistic logic by a universal quantifier over propositions, written as ∀^{2}p. A, where p is variable ranging over propositions.

1. Show introduction and elimination rules for ∀^{2}.

2. Extend the calculus of normal and extraction derivations.

3. Show left and right rules of the sequent calulus for ∀^{2}.

4. Extend the proofs of soundness and completeness for the sequent calculus and sequent calculus with cut to accomodate the new rules.

5. Point out why the proof for admissibility of cut does not extend to this logic.

Exercise 3.6 Gentzen’s original formulation of the sequent calculus for intuitionistic logic permitted the right-hand side to be empty. The introduction rule for negation then has the form

\begin{aligned}Γ, A ⟹ \\ & ¬R. \\ Γ ⟹ ¬A \end{aligned}

Write down the corresponding left rule and detail the changes in the proof for admissibility of cut. Can you explain sequents with empty right-hand sides as judgments?

Exercise 3.7 The algorithm for cut elimination implicit in the proof for admissibility of cut can be described as a set of reduction rules on sequent derivations containing cut.

1. Write out all reduction rules on the fragment containing only implication.

2. Show the extracted proof term before and after each reduction.

3. If possible, formulate a strategy of reduction on proof terms for natural deduction which directly models cut elimination under our translation.

4. Either formulate and prove a theorem about the connection of the strategies for cut elimination and reduction, or show by example why such a connection is difficult or impossible.

Exercise 3.8

1. Prove that we can restrict initial sequents in the sequent calculus to have the form Γ, P ⟹ P where P is an atomic proposition without losing completeness.

2. Determine the corresponding restriction in normal and extraction derivations and prove that they preserve completeness.

3. If you see a relationship between these properties and local reductions or expansions, explain. If you can cast it in the form of a theorem, do so and prove it.

Exercise 3.9 For each of the following propositions, prove that they are derivable in classical logic using the law of excluded middle. Furthermore, prove that they are not true in intuitionistic logic for arbitrary A, B, and C.

1. ((A ⊃ B) ⊃ A) ⊃ A.

2. Any entailment in Exercise 2.8 which is only classically, but not intuitionistically true.

Focused Derivations

The sequent calculus as presented in the previous chapter is an excellent foundation for proof search strategies, but it is not yet practical. For a typical sequent there are many choices, such as which left or right rule to use to reduce the goal in the bottom-up construction of a proof. After one step, similar choices arise again, and so on. Without techniques to eliminate some of this non-determinism one would be quickly overwhelmed with multiple choices.

In this chapter we present two techniques to reduce the amount of nondeterminism in search. The first are inversion properties which hold when the premises of an inference rule are derivable if and only if the conclusion is. This means that we do not lose completeness when applying an invertible rule as soon as it is applicable. The second are focusing properties which allow us to chain together non-invertible inference rules with consecutive principal formulas, once again without losing completeness.

While inversion and focusing are motivated by bottom-up proof search, they generally reduce the number of derivations in the search space. For this reason they also apply in top-down search procedures such as the inverse method introduced in Chapter 5.

4.1 Inversion

The simplest way to avoid non-determinism is to consider those propositions on the left or right for which there is a unique way to apply a corresponding left or right rule. For example, to prove A ∧ B we can immediately apply the right rule without losing completeness. On the other hand, to prove A∨B we can not immediately apply a left rule. As a counterexample consider B ∨ A ⟹ A ∨ B, where we first need to apply a left rule.

On a given sequent, a number of invertible rules may be applicable. However, the order of this choice does not matter. In other words, we have replaced don’tknow non-determinism by don’t-care non-determinism.

Determining the invertibility of left rules in order to support this strategy requires some additional considerations. The pure inversion property states that the premises should be derivable if and only if the conclusion is. However, in left rule the principal formula is still present in the premises, which means we can continue to apply the same left rule over and over again leading to nontermination. So we require in addition that the principal formula of a left rule is no longer needed, thereby guaranteeing the termination of the inversion phase of the search.

Theorem 4.1 (Inversion)

1. If Γ ⟹ A ∧ B then Γ ⟹ A and Γ ⟹ B.

2. If Γ ⟹ A ⊃ B then Γ, A ⟹ B.

3. If Γ ⟹ ∀x. A then Γ ⟹ [a/x]A for a new individual parameter a.

4. If Γ ⟹ ¬A then Γ, A ⟹ p for a new propositional parameter p.

5. If Γ, A ∧ B ⟹ C then Γ, A, B ⟹ C.

6. If Γ, ⊤ ⟹ C then Γ ⟹ C.

7. If Γ, A ∨ B ⟹ C then Γ, A ⟹ C and Γ, B ⟹ C.

8. If Γ, ∃x. A ⟹ C then Γ, [a/x]A ⟹ C for a new individual parameter a.

Proof: By induction over the structure of the given derivations. Parts (5) and (6) are somewhat different in that they extract and inversion property from two and zero left rules, respectively. The proof is nonetheless routine. □

There is an alternative proof which contains somewhat less information about the derivations whose existence is asserted (see Exercise 4.1).

The rules ⊤R and ⊥L are a special case: they can be applied eagerly without losing completeness, but these rules have no premises and therefore do not admit a theorem of the form above. None of the other rules permit an inversion property, as the following counterexamples show. These counterexamples can easily be modifed so that they are not initial sequents.

1. A ∨ B ⟹ A ∨ B (both ∨R_{1} or ∨R_{2} lead to an unprovable sequent).

2. ⊥ ⟹ ⊥ (no right rule applicable).

3. ∃x. A ⟹ ∃x. A (∃R leads to an unprovable sequent).

4. A ⊃ B ⟹ A ⊃ B (⊃L leads to an unprovable sequent).

5. ¬A ⟹ ¬A (¬L leads to an unprovable sequent).

6. ∀x. A ⟹ ∀x. A (∀L leads to an unprovable sequent if we erase the original copy of ∀x. A).

Now we can write out a pure inversion strategy in the form of an inference system. One difficulty with such a system is that the don’t-care non-determinism is not directly visible and has to be remarked on separately. We also refer to don’t-care non-determinism as conjunctive non-determinism: eventually, all applicable rules have to be applied, but their order is irrelevant as far as provability is concerned.

First, we distinguish those kinds of propositions for which either the left or the right rule is not invertible. We call them passive propositions (either on the left or on the right).^{1}

Left passive propositions L ::= P | A_{1} ⊃ A_{2} | ∀x. A
Right passive propositions R ::= P | A_{1} ∨ A_{2} | ⊥ | ∃x. A
Passive antecedents Δ ::= · | Δ, L

We also write L^{+} and R^{+} for non-atomic left and right passive propositions, respectively. Sequents are then composed of four judgments: left and right propositions, each of which may be active or passive. In order to simplify the notation, we collect like judgments into zones, keeping in mind that there can only be one proposition on the right. Sequents are then written as

Δ; Γ ⟹ A; · or Δ; Γ ⟹ ·; R

where the outer zones containing Δ or R are passive and the inner zones containing Γ or A are active. We still think of Δ and Γ as unordered and omit labels for the sake of brevity. We break down the principal connectives in the active propositions eagerly until we have reduced the sequent to one with only passive propositions. At that point we have to choose a left rule to apply and then iterate the process.

Right Active Propositions.

\begin{aligned}Δ; Γ ⟹ A; ·  Δ; Γ ⟹ B; · \\ & ∧R \\ Δ; Γ ⟹ A ∧ B; · \end{aligned}  \frac{⊤R}{Δ; Γ ⟹ ⊤}

\begin{aligned}Δ; Γ, A ⟹ B; · \\ & ⊃R \\ Δ; Γ ⟹ A ⊃ B; · \end{aligned}  \begin{aligned}Δ; Γ ⟹ [a/x]A; · \\ & ∀R^{a} \\ Δ; Γ ⟹ ∀x. A; · \end{aligned}

Left Active Propositions. In order to avoid duplicating the rules depending on a passive or active succedent, we write ρ to stand for either A; · or ·; R.

1[for the moment, we do not consider negation explicitly, but think of it as defined]

Draft of November 12, 1999

\begin{aligned}Δ; Γ, A, B ⟹ ρ \\ & ∧L \\ Δ; Γ, A ∧ B ⟹ ρ \end{aligned}  \begin{aligned}Δ; Γ ⟹ ρ \\ & ⊤L \\ Δ; Γ, ⊤ ⟹ ρ \end{aligned}

\begin{aligned}Δ; Γ, A ⟹ ρ  Δ; Γ, B ⟹ ρ \\ & ∨L \\ Δ; Γ, A ∨ B ⟹ ρ \end{aligned}  \frac{⊥L}{Δ; Γ, ⊤ ⟹ ρ}
Δ; Γ, [a/x]A ⟹ ρ

∃L^{a} Δ; Γ, ∃x. A ⟹ ρ

Transitions. These rules can be applied to move passive propositions which have been uncovered to their appropriate zones.

\begin{aligned}Δ; Γ ⟹ ·; R \\ & tR \\ Δ; Γ ⟹ R; · \end{aligned}  \begin{aligned}(Δ, L); Γ ⟹ ρ \\ & tL \\ Δ; (Γ, L) ⟹ ρ \end{aligned}

Right Passive Propositions. The active and transition rules always terminate when applied in a bottom-up fashion during proof search (see Lemma 4.7). Moverover, they can be applied in any order until sequents of the form Δ; · ⟹ ·; R are reached. Now a don’t-know non-deterministic choice arises: either we apply a right rule to infer R or a left rule to one of the passive assumptions in Δ. We also refer to don’t-know non-determinism as disjunctive non-determinism since we have to pick one of several possibilities, but one is sufficient.

\begin{aligned}Δ; · ⟹ A; · \\ & ∨R_{1} \\ Δ; · ⟹ ·; A ∨ B \end{aligned}  \begin{aligned}Δ; · ⟹ B; · \\ & ∨R_{2} \\ Δ; · ⟹ ·; A ∨ B \end{aligned}

no right rule for ⊥  \begin{aligned}Δ; · ⟹ [t/x]A; · \\ & ∃R \\ Δ; · ⟹ ·; ∃x. A \end{aligned}

Left Passive Propositions. Left passive propositions may be needed more than once, so they are duplicated in the application of the left rules.^{2}

\begin{aligned}Δ, A ⊃ B; · ⟹ A; · Δ, A ⊃ B; B ⟹ ·; R \\ & ⊃L \\ Δ, A ⊃ B; · ⟹ ·; R \end{aligned} ; \begin{aligned}Δ, ∀x. A; [t/x]A ⟹ ·; R \\ & ∀L \\ Δ, ∀x. A; · ⟹ ·; R \end{aligned}

2[some optimization may be possible here.]

Draft of November 12, 1999

Initial Sequents. This leaves the question of initial sequents, which is easily handled by allowing an left passive atomic proposition to match a right passive atomic proposition.

\frac{init}{Δ, P; · ⟹ ·; P}

The judgments Δ; Γ ⟹ ρ are hypothetical in Δ, but not hypothetical in Γ. This is because proposition in Γ do not persist, and because they have to be empty in the initial sequents. In other words, contraction and weakening are not available for Γ. However, it can be explained as a linear hypothetical judgment where each linear hypothesis must be used exactly once in a derivation. We do not formalize this notion any further, but just remark that appropriate versions of the substitution property can be devised to explain its meaning.

First, the soundness theorem is straightforward, since inversion proofs merely eliminate some disjunctive non-determinism.

Theorem 4.2 (Soundness of Inversion Proofs) If Δ; Γ ⟹ A; · or Δ; Γ ⟹ ·; A then Δ, Γ ⟹ A.

Proof: By a straightforward induction over the given derivation, applying weakening in some cases. □

Formulating appropriate theorems for the study of inversion proofs is somewhat difficult, because of the nature conjunctive and disjunctive non-determinism. To complement the soundness property, we first show the completeness theorem for the deductive system. Note, however, that this does not yet take into account the don’t care non-determinism we have in mind for the sequents with active propositions.

The completeness theorem requires a number of lemmas about inversion sequents. For a possible alternative path, see Exercise 4.2. The first set of results expresses the invertibility of the rules concerning the active propositions. That is, we can immediately apply any invertible rule witout losing completeness. The second set of results expresses the opposite: we can always postpone the non-invertible rules until all invertible rules have been applied.

To state inversion in the strongest form (which is needed in the completeness proof for the search procedure, Theorem 4.8) we define the depth of a derivation as one plus the maximum of the depth of the derivations of the premises of the last rule applied. The depth is defined as 1 if the last inference rule has no premises.

Lemma 4.3 (Inversion on Active Rules)

1. If Δ; Γ ⟹ A ∧ B; · then Δ; Γ ⟹ A; · and Δ; Γ ⟹ B; ·.

2. If Δ; Γ ⟹ A ⊃ B; · then Δ; Γ, A ⟹ B; ·.

3. If Δ; Γ ⟹ ∀x. A; · then Δ; Γ ⟹ [a/x]A; · for any new parameter a.

4. If Δ; Γ ⟹ R; · then Δ; Γ ⟹ ·; R.

5. If Δ; Γ, A ∧ B ⟹ ρ then Δ; Γ, A, B ⟹ ρ.

6. If Δ; Γ, ⊤ ⟹ ρ then Δ; Γ ⟹ ρ.

7. If Δ; Γ, A ∨ B ⟹ ρ then Δ; Γ, A ⟹ ρ and Δ; Γ, B ⟹ ρ.

8. If Δ; Γ, ∃x. A ⟹ ρ then Δ; Γ, [a/x]A ⟹ ρ for any new parameter a.

9. If Δ; Γ, L ⟹ ρ then Δ, L; Γ ⟹ ρ.

Moreover, in each case the derivations whose existence is asserted are of equal or smaller depth than the given derivations.

Proof: By straightforward induction on the structure of the given derivations. □

The dual lemma shows that passive rules can be postponed until after the active rules. We define the active size of a sequent Δ; Γ ⟹ A; · or Δ; Γ ⟹ ·; R as the number of logical quantifiers, connectives, constants, and atomic propositions in Γ and A. Note that the active size of a sequent is 0 if and only if it has the form Δ; · ⟹ ·; R.

Lemma 4.4 (Postponement of Passive Rules)

1. If Δ; Γ ⟹ A; · or Δ; Γ ⟹ ·; A then Δ; Γ ⟹ ·; A ∨ B.

2. If Δ; Γ ⟹ B; · or Δ; Γ ⟹ ·; B then Δ; Γ ⟹ ·; A ∨ B.

3. If Δ; Γ ⟹ [t/x]A; · or Δ; Γ ⟹ ·; [t/x]A then Δ; Γ ⟹ ·; ∃x. A.

4. If (Δ, A ⊃ B); Γ ⟹ A; · and (Δ, A ⊃ B); Γ, B ⟹ ρ then (Δ, A ⊃ B); Γ ⟹ ρ.

5. If (Δ, ∀x. A); Γ, [t/x]A ⟹ ρ then (Δ, ∀x. A); Γ ⟹ ρ.

Proof: By induction on the active size of the given sequent. In the base case, the result follows directly by an inference rule. In each other case we apply inversion to an element of Γ (Lemma 4.3) and appeal to the induction hypothesis. We show two cases in the proof of part (4).

Case: Γ = · and ρ = ·; R.

(Δ, A ⊃ B); B ⟹ ·; R  Assumption
(Δ, A ⊃ B); · ⟹ A; ·  Assumption
(Δ, A ⊃ B); · ⟹ ·; R  By rule ⊃L

Case: Γ = Γ′, C ∧ D.

(Δ, A ⊃ B); Γ′, C ∨ D, B ⟹ ρ  Assumption

(Δ, A ⊃ B); Γ′, C, B ⟹ ρ and

(Δ, A ⊃ B); Γ′, D, B ⟹ ρ  By inversion
(Δ, A ⊃ B); Γ′, C ∨ D ⟹ A; ·  Assumption

(Δ, A ⊃ B); Γ′, C ⟹ A; · and

(Δ, A ⊃ B); Γ′, D ⟹ A; ·  By inversion
(Δ, A ⊃ B); Γ′, C ⟹ ρ  By i.h. on Γ′, C
(Δ, A ⊃ B); Γ′, D ⟹ ρ  By i.h. on Γ′, D
(Δ, A ⊃ B); Γ′, C ∨ D ⟹ ρ  By rule ∨L

□

In sequent calculus, the main judgment Γ ⟹ A is hypothetical in Γ. This means Γ directly satisfies weakening and contraction (the additional substitution property is not relevant in this context). However, the inversion sequent Δ; Γ ⟹ ρ is not hypothetical in Γ. In particular, weakening is not obvious (since Γ must be empty for a passive rule to apply) and contraction is not obvious (since elements of Γ are not propagated from the conclusion to the premises of the rules).

For the proof of completeness, and also to permit some optimizations in the search procedure, we need to show that weakening and contraction for propositions in Γ are admissible, at the price of possibly lengthening the derivation. Note that weakening and contraction for Δ is trivial, since inversion sequents are hypothetical in Δ.

Lemma 4.5 (Structural Properties of Inversion Sequents)

1. If Δ; Γ ⟹ ρ then (Δ, A); Γ ⟹ ρ.

2. If (Δ, A, A); Γ ⟹ ρ then (Δ, A); Γ ⟹ ρ.

3. If Δ; Γ ⟹ ρ then Δ; (Γ, A) ⟹ ρ.

4. If Δ; (Γ, A, A) ⟹ ρ then Δ; (Γ, A) ⟹ ρ.

Proof: Parts (1) and (2) follow as usual by straightforward structural inductions over the given derivations. Parts (3) and (4) follow by induction on the structure of A, taking advantage of the inversion properties for active propositions (Lemma 4.3) and parts (1) and (2) for passive propositions. □

The first completeness theorem below does not express the conjunctive nondeterminism in the search for inversion proofs. This will be treated in a further refinement.

Theorem 4.6 (Completeness of Inversion Proofs) If Γ ⟹ A then ·; Γ ⟹ A; ·.

Proof: By induction on the structure of the given sequent derivation S, taking advantage of the inversion, postponement, and structural properties proven in this section. We consider in turn: invertible right rules, invertible left rules, initial sequents, non-invertible right rules and non-invertible left rules.

Case:

S = \begin{aligned}\begin{matrix}S_{1} \\ Γ ⟹ A_{1} \end{matrix} & \begin{matrix}S_{2} \\ Γ ⟹ A_{2} \end{matrix} \\ & ∧R \\ Γ ⟹ A_{1} ∧ A_{2} \end{aligned}

·; Γ ⟹ A_{1}; ·  By i.h. on S_{1}
·; Γ ⟹ A_{2}; ·  By i.h. on S_{2}
·; Γ ⟹ A_{1} ∧ A_{2}; ·  By rule ∧R

Cases: The right invertible rules ⊃R and ∀R and also the case for ⊤R are similar to the case for ∧R.

Case:

S = \begin{aligned}\begin{matrix}S_{1} \\ Γ, B_{1} ∨ B_{2}, B_{1} ⟹ A \end{matrix} & \begin{matrix}S_{2} \\ Γ, B_{1} ∨ B_{2}, B_{2} ⟹ A \end{matrix} \\ & ∨L \\ Γ, B_{1} ∨ B_{2} ⟹ A \end{aligned}

·; Γ, B_{1} ∨ B_{2}, B_{1} ⟹ A; ·  By i.h. on S_{1}
·; Γ, B_{1} ∨ B_{2}, B_{2} ⟹ A; ·  By i.h. on S_{2}
·; Γ, B_{1} ∨ B_{2}, B_{1} ∨ B_{2} ⟹ A; ·  By rule ∨L
·; Γ, B_{1} ∨ B_{2} ⟹ A; ·  By contraction (Lemma 4.5)

Cases: The left invertible rule ∃L and also the case for ⊥L are similar to the case for ∨L.

Case:

S = \begin{matrix}S_{1} \\ Γ, B_{1} ∧ B_{2}, B_{1} ⟹ A \end{matrix} ; ∧L_{1} ; Γ, B_{1} ∧ B_{2} ⟹ A

·; Γ, B_{1} ∧ B_{2}, B_{1} ⟹ A; ·  By i.h. on S_{1}
·; Γ, B_{1} ∧ B_{2}, B_{1}, B_{2} ⟹ A; ·  By weakening (Lemma 4.5)
·; Γ, B_{1} ∧ B_{2}, B_{1} ∧ B_{2} ⟹ A  By rule ∧L
·; Γ, B_{1} ∧ B_{2} ⟹ A  By contraction (Lemma 4.5)

Case: The case for ∧L_{2} is symmetric to ∧L_{1}. Note that there is no left rule for ⊤ in the sequent calculus, so the ⊤L rule on inversion sequents arises only from weakening (see the following case).

Case:

S = \frac{init}{Γ, P ⟹ P}

P; · ⟹ ·; P  By rule init
P; · ⟹ P; ·  By rule tR
·; P ⟹ P; ·  By rule tL
·; Γ, P ⟹ P; ·  By weakening (Lemma 4.5)

Case:

S = \begin{matrix}S_{1} \\ Γ ⟹ A_{1} \end{matrix} ; ∨R_{1} ; Γ ⟹ A_{1} ∨ A_{2}

·; Γ ⟹ A_{1}; ·  By i.h. on S_{1}
·; Γ ⟹ ·; A_{1} ∨ A_{2}  By postponement (Lemma 4.4)
·; Γ ⟹ A_{1} ∨ A_{2}; ·  By rule tR

Cases: The cases for the non-invertible right rules ∨R_{2} and ∃R are similar to ∨R_{1}.

Case:

S = \begin{aligned}\begin{matrix}S_{1} \\ Γ, B_{1} ⊃ B_{2} ⟹ B_{1} \end{matrix} & \begin{matrix}S_{2} \\ Γ, B_{1} ⊃ B_{2}, B_{2} ⟹ A \end{matrix} \\ & ⊃L \\ Γ, B_{1} ⊃ B_{2} ⟹ A \end{aligned}

·; Γ, B_{1} ⊃ B_{2} ⟹ B_{1}; ·  By i.h. on S_{1}
B_{1} ⊃ B_{2}; Γ ⟹ B_{1}; ·  By inversion (Lemma 4.3)
·; Γ, B_{1} ⊃ B_{2}, B_{2} ⟹ A; ·  By i.h. on S_{2}
B_{1} ⊃ B_{2}; Γ, B_{2} ⟹ A; ·  By inversion (Lemma 4.3)
B_{1} ⊃ B_{2}; Γ ⟹ A; ·  By postponement (Lemma 4.4)
·; Γ, B_{1} ⊃ B_{2} ⟹ A; ·  By rule tL

Case: The cases for the non-invertible left rule ∀L is similar to ⊃L.

□

To capture the conjunctive non-determinism we think of an unproven sequent as a goal and the unproven leaves of a partially constructed derivation as subgoals. From the inversion properties for active propositions we already know that we do not lose completeness when applying active rules. However, it is conceivable that the eager application of active rules does not terminate, which means that the search procedure we have in mind would be incomplete. Fortunately, this is not the case. While the following termination property is not directly needed in the completeness proof for the search procedure, it foreshadows the argument used there.

Lemma 4.7 (Termination of Active Rules) Given a goal Δ; Γ ⟹ ρ. Any sequence of applications of active rules terminates.

Proof: By induction on the active size of the given sequent. □

Next we describe a non-deterministic algorithm for proof search. There are a number of ways to eliminate the remaining disjunctive non-determinism. Typical is depth-first search, made complete by iterative deepening. The choice of the term t in the rules ∃R and ∀L is later solved by introducing free variables and equational constraints into the search procedures which are solved by unification (see Section 4.3). Many futher refinements and improvements are possible on this procedures, but not discussed here.

Given a goal Δ; Γ ⟹ ρ.

1. If Γ = · and ρ = ·; P succeed if P is in Δ.

2. If Γ = · and ρ = ·; R, but the previous case does not apply, guess an inference rule to reduce the goal. In the cases of ∃R and ∀L we also have to guess a term t. Solve each subgoal by recursively applying the procedure. This case represents a disjunctive choice (don’t know non-determinism). If no rule applies, we fail.

3. If Γ is non-empty or ρ = A; ·, choose any active rule which applies and solve each of the subgoals by recursively applying the procedure. This represents a conjunctive choice (don’t care non-determinism). Note that some active rule must always be applicable in this case.

This search procedure is clearly sound, because the inversion proof system is sound (Theorem 4.2). Furthermore, if there is a derivation the procedure will (in principle) always terminate and find some derivation if it guesses correctly in step (2).

Theorem 4.8 (Completeness of Inversion Search) Given a goal Δ; Γ ⟹ ρ. If there is a derivation of the goal, the inversion search procedures terminates and finds a derivation for any choices made in step (3) and some choices made in step (2).

Proof: By nested induction on depth of the given derivation I and the active size of the given sequent. That is, we can apply the induction hypothesis if

1. the depth of the derivation I strictly decreases, or

2. the depth of I remains the same and the active size of the goal strictly decreases.

Case: I is an initial sequent. Then we are in situation (1) and succeed.

Case: I ends in a passive rule. Then we are in situation (2). We “guess” the same rule instance to reduce our goal. Each of the resulting subgoals now has a proof of strictly smaller depth, and we can apply the induction hypothesis.

Case: I ends in an active rule. In that case we are in situation (3). Independent of the last rule used in I, we can apply any active rule to reduce our goal. By inversion (Lemma 4.3) each of the subgoals will have a proof of smaller or equal depth than I. Moreover, the active size of the goal strictly decreases and we can apply the induction hypothesis to each subgoal.

□

4.2 Focusing

The search procedure based on inversion developed in the previous section still has an unacceptable amount of don’t know non-determinism. The problem lies in the undisciplined use and proliferation of assumptions whose left rule is not invertible.

In a typical situation we have some universally quantified implications as assumptions. For example, Δ could be

\begin{matrix}∀x_{1}. ∀y_{1}. ∀z_{1}. P_{1}(x_{1}, y_{1}, z_{1}) ⊃ Q_{1}(x_{1}, y_{1}, z_{1}) ⊃ R_{1}(x_{1}, y_{1}, z_{1}), \\ ∀x_{2}. ∀y_{2}. ∀z_{2}. P_{2}(x_{2}, y_{2}, z_{2}) ⊃ Q_{2}(x_{2}, y_{2}, z_{2}) ⊃ R_{2}(x_{2}, y_{2}, z_{2}) \end{matrix}

If the right-hand side is passive, we now have to apply ∀L to one of the two assumptions. We assume we guess the first one and that we can guess an appropriate term t_{1}. After the ∀L rule and a left transition, we are left with

∀x_{1}. ∀y_{1}. ∀z_{1}. P_{1}(x_{1}, y_{1}, z_{1}) ⊃ Q_{1}(x_{1}, y_{1}, z_{1}) ⊃ R_{1}(x_{1}, y_{1}, z_{1}),
∀x_{2}. ∀y_{2}. ∀z_{2}. P_{2}(x_{2}, y_{2}, z_{2}) ⊃ Q_{2}(x_{2}, y_{2}, z_{2}) ⊃ R_{2}(x_{2}, y_{2}, z_{2}),
∀y_{1}. ∀z_{1}. P_{1}(t_{1}, y_{1}, z_{1}) ⊃ Q_{1}(t_{1}, y_{1}, z_{1}) ⊃ R_{1}(t_{1}, y_{1}, z_{1}).

Again, we are confronted with a don’t know non-deterministic choice, now between 3 possibilities. One can see that the number of possible choices quickly explodes. We can observe that the pattern above does not coincide with mathematical practice. Usually one applies an assumption or lemma of the form above by instantiating all the quantifiers and all preconditions at once. This strategy called focusing is a refinement of the inversion strategy presented in the previous section.

Roughly, when all propositions in a sequent are passive, we focus either on an assumption or the proposition we are trying to prove and then apply a sequence of non-invertible rules to the chosen proposition. This phase stops when either an invertible connective or an atomic proposition is reached.

As in the previous section, we capture this idea by a combination of a deductive system and a search strategy which distinguishes between conjunctive and disjunctive choices. We still use the sequents Δ; Γ ⟹ A; · and Δ; Γ ⟹ ·; R with the same notation for simplicity. All the active rules (but not the initial sequents) are copied verbatim to this system. In addition, we need two new forms of sequents to express the focusing phase of proof search. We write

Δ; A ≫ ·; R Focus on A on the left
Δ; · ≫ A; · Focus on A on the right

The initial and passive rules of the inversion derivation are replaced by the following set of rules.

Decision. These rules decide which formula to focus on and are treated in a don’t know non-deterministic manner. While we allow focusing on an atomic assumption, focusing on the succedent requires it to be non-atomic. The reason is our handling of initial sequents.

\begin{aligned}(Δ, L); L ≫ ·; R \\ & dL \\ (Δ, L); · ⟹ ·; R \end{aligned}  \begin{aligned}Δ; · ≫ R^{+}; · \\ & dR \\ Δ; · ⟹ ·; R^{+} \end{aligned}

Right Focus Propositions. The non-invertible rules on the right maintain the focus on principal formula of the inference. When we have reduced the right-hand side to a right-invertible or atomic proposition, we blur our focus and initiate decomposition with an active sequent. Here \overline{R} is either P, A ⊃ B, A ∧ B, ⊤, and ∀x. A.

\begin{aligned}Δ; · ≫ A; · \\ & ∨R_{1} \\ Δ; · ≫ A ∨ B; · \end{aligned}  \begin{aligned}Δ; · ≫ B; · \\ & ∨R_{2} \\ Δ; · ≫ A ∨ B; · \end{aligned}

no right focus rule for ⊥  \begin{aligned}Δ; · ≫ [t/x]A; · \\ & ∃R \\ Δ; · ≫ ∃x. A; · \end{aligned}

\begin{aligned}Δ; · ⟹ \overline{R}; · \\ & bR \\ Δ; · ≫ \overline{R}; · \end{aligned}

Left Focus Propositions. The non-invertible rules on the left also maintain their focus on the principal formula of the inference. When we have reached a non-atomic left-invertible proposition, we blur our focus and initiate decomposition with an active sequent. Here \overline{L}^{+} is either A ∨ B, ⊥, ∃x. A.

Δ; B ≫ ·; R Δ; · ⟹ A; ·
⊃L

Δ; A ⊃ B ≫ ·; R

\begin{aligned}Δ; A ≫ ·; R \\ & ∧L_{1} \\ Δ; A ∧ B ≫ ·; R \end{aligned}  \begin{aligned}Δ; B ≫ ·; R \\ & ∧L_{2} \\ Δ; A ∧ B ≫ ·; R \end{aligned}

no rule for ⊤L  \begin{aligned}Δ; \overline{L}^{+} ⟹ ·; R \\ & bL \\ Δ; \overline{L}^{+} ≫ ·; R \end{aligned}

Draft of November 12, 1999

Note that the second premise of the ⊃L rule is an unfocused sequent. From a practical point of view it is important to continue with the focusing steps in the first premise before attempting to prove the second premise, because the decomposition of B may ultimately fail when an atomic proposition is reached. Such a failure would render the possibly difficult proof of A useless.

It is possible to extend the definition of \overline{L}^{+} to include conjunction and ⊤ and remove the left focus rules for conjunction. In some situations this would clearly lead to shorter proofs, but the present version appears to have less disjunctive non-determinism.^{3}

Initial Sequents. There is a slight, but important asymmetry in the initial sequents: we require that we have focused on the left proposition.

\frac{init}{Δ; P ≫ ·; P}

Since this is the only rule which can be applied when the left focus formula is atomic, a proof attempt fails in a situation where Δ; P ≫ ·; Q for P ≠ Q. This is a very important property of the search, limiting non-determinism in focusing.

If one shows only applications of the decision rules in a derivation, the format is very close to assertion-level proofs as proposed by Huang [Hua94]. His motivation was the development of a formalism appropriate for the presentation of mathematical proofs in a human-readable form. This provides independent evidence for the value of focusing proofs. Focusing derivations themselves were developed by Andreoli [And92] in the context of classical linear logic. An adaptation to intuitionistic linear logic was given by Howe [How98] which is related the calculus LJT devised by Herbelin [Her95]. Herbelin’s goal was to devise a sequent calculus whose derivations are in bijective correspondence to normal natural deductions. Due to the ∨, ⊥ and ∃ elimination rules, this is not the case here.

The search procedure which works with focusing sequents is similar to the one for inversion: it mixes conjunctive non-determinism for active rules with disjunctive non-determinism for choice and focused rules. After the detailed development of inversion proofs, we will not repeat or extend the development here, but refer the interested reader to the literature. The techniques are very similar to the ones shown in Section 4.1.

4.3 Unification

When proving a proposition of the form ∃x. A by its right rule in the sequent or focusing calculus, we must supply a term t and then prove [t/x]A. The domain of quantification may include infinitely many terms (such as the natural numbers), so this choice cannot be resolved simply by trying all possible terms t. Similarly, when we use a hypothesis of the form ∀x. A we must supply a term t to substitute for x. We refer to this a existential non-determinism.

3[evaluate]

Draft of November 12, 1999

Fortunately, there is a technique called unification which is sound and complete for syntactic equality between terms. The basic idea is quite simple: we postpone the choice of t and instead substitute a new existential variable (often called meta-variable or logic variable) X for x and continue with the bottom-up construction of a derivation. When we reach initial sequents we check if there is a substitution for the existential variables such that the hypothesis matches the conclusion. If so, we apply this instantiation globally to the partial derivation and continue to search for proofs of other subgoals. Finding an instantiation for existential variables under which two propositions or terms match is called unification. It is decidable if a unifying substitution or unifier exists, and if so, we can effectively compute it in linear time. Moreover, we can do so with a minimal commitment and we do not need to choose between various possible unifiers.

Because of its central importance in both backward- and forward-directed search, unification has been thoroughly investigated. Herbrand [Her30] is given credit for the first description of a unification algorithm in a footnote of his thesis, but it was not until 1965 that it was introduced into automated deduction through the seminal work by Alan Robinson [Rob65, Rob71]. The first algorithms were exponential, and later almost linear [Hue76, MM82] and linear algorithms [MM76, PW78] were discovered. In the practice of theorem proving, generally variants of Robinson’s algorithm are still used, due to its low constant overhead on the kind of problems encountered in practice. For further discussion and a survey of unification, see [Kni89]. We describe a variant of Robinson’s algorithm.

Before we describe the unification algorithm itself, we relate it to the problem of proof search. We use here the sequent calculus with atomic initial sequents, but it should be clear that precisely the same technique of residuation applies to focused derivations. We enrich the judgment Γ ⟹^{−} A by a residual proposition F such that

1. if Γ ⟹^{−} A then Γ ⟹^{−} A \ F and F is true, and

2. if Γ ⟹^{−} A \ F and F is true then Γ ⟹^{−} A.

Generally, we cannot prove such properties directly by induction, but we need to generalize them, exhibiting the close relationship between the derivations of the sequents and residual formulas F.

Residual formulas F are amenable to specialized procedures such as unification, since they are drawn from a simpler logic or deductive system than the general propositions A. In practice they are often solved incrementally rather than collected throughout a derivation and only solved at the end. This is important for the early detection of failures during proof search. Incremental solution of residual formulas is the topic of Exercise ??.

What do we need in the residual propositions so that existential choices and equalities between atomic propositions can be expressed? The basic proposition is one of equality between atomic propositions, P_{1} ≐ P_{2}. We also have conjunction F_{1} ∧ F_{2}, since equalities may be collected from several subgoals, and ⊤ if there are no residual propositions to be proven. Finally, we need the existential quantifier ∃x. F to express the scope of existential variables, and ∀x. F to express the scope of parameters introduced in a derivation. We add equality between terms, since it is required to describe the unification algorithm itself. We refer to the logic with these connectives as unification logic, defined via a deductive system.

Formulas F ::= P_{1} ≐ P_{2} | t_{1} ≐ t_{2} | F_{1} ∧ F_{2} | ⊤ | ∃x. F | ∀x. F

The main judgment “F is valid”, written ⊧ F, is defined by the following rules, which are consistent with, but more specialized than the rules for these connectives in intuitionistic natural deduction (see Exercise ??).

\begin{matrix}\frac{≐ I}{⊧ P ≐ P} & \frac{≐ I′}{⊧ t ≐ t} \\ \begin{aligned}⊧ F_{1} ⊧ F_{2} \\ & ∧I \\ ⊧ F_{1} ∧ F_{2} \end{aligned} & \frac{⊤I}{⊧ ⊤} \\ \begin{aligned}⊧ [t/x]F \\ & ∃I \\ ⊧ ∃x. F \end{aligned} & \begin{aligned}⊧ [a/x]F \\ & ∀I^{a} \\ ⊧ ∀x. F \end{aligned} \end{matrix}

The ∀I^{a} rule is subject to the usual proviso that a is a new parameter not occurring in ∀x. F. There are no elimination rules, since we do not need to consider hypotheses about the validity of a formula F which is the primary reason for the simplicity of theorem proving in the unification logic.

We enrich the sequent calculus with residual formulas from the unification logic, postponing all existential choices. Recall that in practice we merge residuation and solution in order to discover unprovable residual formulas as soon as possible. This merging of the phases is not represented in our system.

Initial Sequents. Initial sequents residuate an equality between its principal propositions. Any solution to the equation will unify P′ and P, which means that this will translate to a correct application of the initial sequent rule in the original system.

\frac{init}{Γ, P′ ⟹^{−} P \ P′ ≐ P}

Propositional Connectives. We just give a few sample rules for the connectives which do not involve quantifiers, since all of them simply propagate or combine unification formulas, regardless whether they are additive, multiplicative, or exponential.

\begin{aligned}Γ, A ⟹^{−} B \ F \\ & ⊃R \\ Γ ⟹^{−} A ⊃ B \ F \end{aligned}  \frac{⊤R}{Γ ⟹^{−} ⊤ \ ⊤}

Γ, A ⊃ B ⟹^{−} A \ F_{1} Γ, A ⊃ B, B ⟹^{−} C \ F_{2}

⊃L

Γ, A ⊃ B ⟹^{−} C \ F_{1} ∧ F_{2}

Quantifiers. These are the critical rules. Since we residuate the existential choices entirely, the ∃R and ∀L rules instantiate a quantifier by a new parameter, which is existentially quantified in the residual formula in both cases. Similarly, the ∀R and ∃L rule introduce a parameter which is universally quantified in the residual formula.

\begin{aligned}Γ ⟹^{−} [a/x]A \ [a/x]F \\ & ∀R^{a} \\ Γ ⟹^{−} ∀x. A \ ∀x. F \end{aligned}  \begin{aligned}Γ, ∀x. A, [a/x]A ⟹^{−} C \ [a/x]F \\ & ∀L^{a} \\ Γ, ∀x. A ⟹^{−} C \ ∃x. F \end{aligned}

\begin{aligned}Γ ⟹^{−} [a/x]A \ [a/x]F \\ & ∃R^{a} \\ Γ ⟹^{−} ∃x. A \ ∃x. F \end{aligned}  \begin{aligned}Γ, ∃x. A, [a/x]A ⟹^{−} C \ [a/x]F \\ & ∃L^{a} \\ Γ, ∃x. A ⟹^{−} C \ ∀x. A \end{aligned}

The soundness of residuating equalities and existential choices in this manner is straightforward.

Theorem 4.9 (Soundness of Equality Residuation) If Γ ⟹^{−} A \ F and ⊧ F then Γ ⟹^{−} A.

Proof: By induction on the structure of the given derivation R. We show the critical cases. Note how in the case of the ∃R rule the derivation of ⊧ ∃x. F provides the essential witness term t. Case:

R = \frac{init}{Γ, P′ ⟹^{−} P \ P′ ≐ P}

⊧ P′ ≐ P  By assumption
P′ = P  By inversion
Γ, P′ ⟹^{−} P  By rule init

Case:

R = \begin{matrix}R_{1} \\ Γ ⟹^{−} [a/x]A_{1} \ [a/x]F_{1} \end{matrix} ; ∃R^{a} ; Γ ⟹^{−} ∃x. A_{1} \ ∃x. F_{1}

Draft of November 12, 1999

⊧ ∃x. F_{1}  By assumption
⊧ [t/x]F_{1} for some t  By inversion
Γ ⟹^{−} [t/x]A_{1} \ [t/x]F_{1}  By substitution for parameter a
Γ ⟹^{−} [t/x]A_{1}  By i.h.
Γ ⟹^{−} ∃x. A_{1}  By rule ∃R

Case:

R = \begin{matrix}R_{1} \\ Γ ⟹^{−} [a/x]A_{1} \ [a/x]F_{1} \end{matrix} ; ∀R^{a} ; Γ ⟹^{−} ∀x. A_{1} \ ∀x. F_{1}

⊧ ∀x. F_{1}  By assumption
⊧ [b/x]F_{1} for a new parameter b  By inversion
⊧ [a/x]F_{1}  By substititution of a for b
Γ ⟹^{−} [a/x]A_{1}  By i.h.
Γ ⟹^{−} ∀x. A_{1}  By rule ∀R
□

The opposite direction is more difficult. The desired theorem:

If Γ ⟹^{−} A then Γ ⟹^{−} A \ F for some F with ⊧ F

cannot be proved directly by induction, since the premisses of the two derivations are different in the ∃R and ∀L rules. However, one can be obtained from the other by substituting terms for parameters. Since this must be done simultaneously, we introduce a new notation.

Parameter Substitution ρ ::= · | ρ, t/a

We assume all the parameters a substituted for by ρ are distinct to avoid ambiguity. We write A[ρ], F [ρ], and Γ[ρ], for the result of applying the substitution ρ to a proposition, formula, or context, respectively.

Lemma 4.10 If Γ ⟹^{−} A where A = A′[ρ], Γ = Γ′[ρ] then Γ′ ⟹^{−} A′ \ F for some F such that ⊧ F [ρ].

Proof: The proof proceeds by induction on the structure of the given derivation D. We show only two cases, the second of which required the generalization of the induction hypothesis.

Case:

D = \frac{init}{Γ_{1}, P ⟹^{−} P}

Γ_{1} = Γ′_{1}[ρ], P = P′[ρ], and P = P′′[ρ]  Assumption
Γ′_{1}, P′ ⟹^{−} P′′ \ P′ ≐ P′′  By rule init
⊧ P′[ρ] ≐ P′′[ρ]  By rule ≐ I

Case:

D = \begin{matrix}D_{1} \\ Γ ⟹^{−} [t/x]A_{1} \end{matrix} ; ∃R ; Γ ⟹^{−} ∃x. A_{1}

∃x. A_{1} = A′[ρ]  Assumption

A′ = ∃x. A′_{1} for a new parameter a with

[a/x]A_{1} = ([a/x]A′_{1})[ρ, a/a]  By definition of substitution
[t/x]A_{1} = ([a/x]A′_{1})[ρ, t/a]  By substitution for parameter a
Γ = Γ′[ρ]  Assumption
Γ′[ρ] = Γ′[ρ, t/a]  Since a is new

Γ′ ⟹^{−} [a/x]A′_{1} \ [a/x]F_{1}, and

⊧ ([a/x]F_{1})[ρ, t/a]  By i.h.
Γ′ ⟹^{−} ∃x. A′_{1} \ ∃x. F_{1}  By rule ∃R
⊧ (∃x. F_{1})[ρ]  By rule ∃R and definition of substitution
□

Theorem 4.11 (Completeness of Equality Residuation) If Γ ⟹^{−} A then Γ ⟹^{−} A \ F for some F and ⊧ F.

Proof: From Lemma 4.10 with A′ = A, Γ′ = Γ, and ρ the identity substitution on the parameters in Γ and A. □

Next we describe an algorithm for proving residuated formulas, that is, an algorithm for unification. We do this in two steps: first we solve the problem in the fragment without parameters and universal quantifiers and then we extend the solution to the general case.

There are numerous ways for describing unification algorithms in the literature. We describe the computation of the algorithm as the bottom-up search for the derivation of a judgment. We restrict the inference rules such that they are essentially deterministic, and the inference rules themselves can be seen as describing an algorithm. This algorithm is in fact quite close to the implementation of it in ML which is available together with these notes.

In order to describe the algorithm in this manner, we need to introduce existential variables (often called meta-variables or logic variables) which are place-holders for the terms to be determined by unification. We use X and Y to stand for existential variables. Existential variables are different from parameters which are interpreted universally: all instances of a derivation with a parameter are valid. Existential variables in a derivation require only one instance to arrive at a valid derivation. While parameters are always local to a subderivation, we consider existential variables to be global in a derivation.^{4}

The second concept we need is that of a substitution for existential variables. We use a new notation, because this form of substitution is quite different from substitutions for bound variables x or parameters a.

Substitutions θ ::= · | θ, X ↦ t

We require that all variables X defined by a substitution are distinct. We write dom(θ) for the variables defined by a substitution and cod(θ) for all the variables occuring in the terms t. For a ground substitution cod(θ) is empty. For the technical development it is convenient to assume that the domain and co-domain of a substitution share no variables. This rules out “circular” substitutions such as X ↦ f(X) and it also disallows identity substitutions X ↦ X. The latter restriction can be dropped, but it does no harm and is closer to the implementation. As for contexts, we consider the order of the definitions in a substitution to be irrelevant.

We write t[θ], A[θ], and Γ[θ] for the application of a substitution to a term, proposition, or context. This is defined to be the identity on existential variables which are not explicitly defined in the substitution.

We also need an operation of composition, written as θ_{1} ∘ θ_{2} with the property that t[θ_{1} ∘ θ_{2}] = (t[θ_{1}])[θ_{2}] and similarly for propositions and contexts. Composition is defined by

\begin{matrix}(·) ∘ θ_{2} = θ_{2} \\ (θ_{1}, X ↦ t) ∘ θ_{2} = (θ_{1} ∘ θ_{2}), X ↦ t[θ_{2}] \end{matrix}

In order for composition to be well-defined and have the desired properties we require that dom(θ_{1}), dom(θ_{2}) and cod(θ_{2}) are disjoint, but of course variables in the co-domain of θ_{1} can be defined by θ_{2}.

Now we introduce the judgment which implicitly defines an algorithm for unification. We write

⊧ F / θ θ is a most general unifier for F.

The intent (to be proven later) is that if ⊧ F / θ then ⊧ F [θ], which means that θ is a unifier for F. Moreover, we show that whenever ⊧ F [θ′] then there exists a substitution θ′′ such that θ′ = θ ∘ θ′′, which means that θ is a most general unifier for F (any unifier is an instance of θ).

Conjunction and Truth. Algorithmically, we impose a left-to-right order on the solution of F_{1} and F_{2}, but this just fixes a don’t care non-deterministic choice.

\begin{aligned}⊧ F_{1} / θ_{1}  ⊧ F_{2}[θ_{1}] / θ_{2} \\ & ∧I \\ ⊧ F_{1} ∧ F_{2} / θ_{1} ∘ θ_{2} \end{aligned}  \frac{⊤I}{⊧ ⊤ / ·}

After all the rules have been shown, it will be easy to see that the side conditions on composition are satisfied and θ_{1} ∘ θ_{2} is well-defined.

4[example]

Draft of November 12, 1999

Existential Quantification. Existential variables are introduced for existential quantifiers. They must be “new” (even though the judgment is not parametric). Because of the way existential variables are global to a derivation, this freshness requirement is a global requirement: in a complete derivation, the existential variables chosen for all existential quantifiers must be distinct. To be completely formal about this condition would require to thread a list of existential variables or a counter through a derivation. We will dispense with this complication here. We define (θ′, X ↦ t) − X = θ′ and θ − X = θ if X is not in the domain of θ.

⊧ [X/x]F / θ X globally new

∃I ⊧ ∃x. F / θ − X

Despite the strong freshness requirement on X, the derivation of the premise is not parametric in X. That is, we cannot substitute an arbitrary term t for X in a derivation of the premiss and obtain a valid derivation, since the vr, rv, vv≠, and vv= rules below require one or both sides of the equation to be an existential variable. Substituting for such a variable invalidates the application of these rules. Moreover X can still appear in the co-domain of θ in the generated substitution.

Predicate and Function Constants. An equation between the same function constant applied to arguments is decomposed into equations between the arguments. Unification fails if different function symbols are compared, but this is only indirectly reflected by an absence of an appropriate rule. Failure can also be explicitly incorporated in the algorithm (see Exercise ??).

\begin{aligned}⊧ t_{1} ≐ s_{1} ∧ ⋯ ∧ t_{n} ≐ s_{n} / θ \\ & pp \\ ⊧ p(t_{1}, …, t_{n}) ≐ p(s_{1}, …, s_{n}) / θ \end{aligned} \begin{aligned}⊧ t_{1} ≐ s_{1} ∧ ⋯ ∧ t_{n} ≐ s_{n} / θ \\ & rr \\ ⊧ f(t_{1}, …, t_{n}) ≐ f(s_{1}, …, s_{n}) / θ \end{aligned}

These rules violate orthogonality by relying on conjunction in the premises for the sake of conciseness of the presentation. We could avoid this by introducing a separate judgment for the unification of lists of terms. When f or p have no arguments, the empty conjunction in the premise should be read as ⊤.

Existential Variables. There are four rules for variables. We write r for terms of the form f(t_{1}, …, t_{n}). Existential variables always range over terms (and not propositions), so we do not need rules for equations of the form X ≐ P or P ≐ X.

\begin{aligned}X not in r \\ & vr \\ ⊧ X ≐ r / (X ↦ r) \end{aligned} \begin{aligned}X not in r \\ & rv \\ ⊧ r ≐ X / (X ↦ r) \end{aligned}

These two rules come with the proviso that the existential variable X does not occur in the term r. This is necessary to ensure that the substitution X ↦ r is indeed a unifier. Otherwise unification fails and we can recognize formulas such as ∃x. x ≐ f(x) as false. This leaves equations of the form X ≐ Y between two existential variables.

\begin{matrix}Y ≠ X \\ vv & ≠ \\ ⊧ X ≐ Y / (X ↦ Y) \end{matrix}  \frac{vv=}{⊧ X ≐ X / ·}

We now explore the soundness and completeness of these rules, and then analyze the rules as the basis of an algorithm. In the statement of the properties below we take some care so that for a judgment ⊧ F, F never contains free existential variables which are seen only as part of the algorithm, not the definition of the logic. We write σ for ground substitutions. We say σ grounds a formula F if F [σ] contains no existential variables. We assume that there is a closed term to be substituted for each variable. This assumption is necessary, for example, to prove that ∃x. x ≐ x is valid.

Theorem 4.12 (Soundness of Unification) If ⊧ F / θ then for any substitution σ which grounds F [θ] we have ⊧ (F [θ])[σ].

Proof: By induction on the structure of the derivation U for ⊧ F / θ.

Case:

U = \frac{⊤I}{⊧ ⊤ / ·}

⊤[·][σ] = ⊤  By definition of substitution
⊧ ⊤  By rule ⊤I

Case:

U = \begin{aligned}\begin{matrix}U_{1} \\ ⊧ F_{1} / θ_{1} \end{matrix} & \begin{matrix}U_{2} \\ ⊧ F_{2}[θ_{1}] / θ_{2} \end{matrix} \\ & ∧I \\ ⊧ F_{1} ∧ F_{2} / θ_{1} ∘ θ_{2} \end{aligned}

σ grounds (F_{1} ∧ F_{2})[θ_{1} ∘ θ_{2}]  Assumption
θ_{2} ∘ σ grounds F_{1}[θ_{1}]  By properties of substitution
⊧ (F_{1}[θ_{1}])[θ_{2} ∘ σ]  By i.h. on U_{1}
σ grounds (F_{2}[θ_{1}])[θ_{2}]  By properties of substitution
⊧ (F_{2}[θ_{1}][θ_{2}])[σ]  By i.h. on U_{2}
⊧ (F_{1} ∧ F_{2})[θ_{1} ∘ θ_{2}][σ]  By rule ∧I and properties of substitution

Case:

U = \begin{matrix}U_{1} \\ ⊧ [X/x]F_{1} / θ′ \end{matrix} ; ∃I ; ⊧ ∃x. F_{1} / θ′ − X

In this case we distinguish subcases, depending on whether X is in the domain of θ′.

Draft of November 12, 1999

Subcase: θ′ = θ, X ↦ t. Recall that we assume that there are ground terms.

σ grounds (∃x. F_{1})[θ]  Assumption

σ ∘ σ′ grounds ([X/x]F_{1})[θ, X ↦ t]

for any appropriate σ′ which grounds t[σ]

⊧ ([X/x]F_{1})[θ, X ↦ t][σ ∘ σ′]  By i.h. on U_{∞}
⊧ [t[σ ∘ σ′]/x](F_{1}[θ][σ])  By properties of substitution
⊧ (∃x. F_{1})[θ][σ]  By rule ∃I and properties of substitution

Subcase: θ′ = θ and contains no binding for X. Then we proceed as in the previous subcase, using σ′ = X ↦ t′ for some arbitrary ground term t′.

Case:

U = \begin{aligned}X not in r \\ & vr \\ ⊧ X ≐ r / (X ↦ r) \end{aligned}

σ grounds (X ≐ r)[X ↦ r]  Assumption
(X ≐ r)[X ↦ r] = (r ≐ r)  By precondition for rule
⊧ (X ≐ r)[X ↦ r][σ]  By rule ≐ I

Case: Rule rv for r ≐ X is symmetric.

Case: Rule vv≠ for X ≐ X is similar.

Case: Rule vv= for X ≐ X and X ≐ Y for X ≠ Y is also similar.

Case:

U = \begin{matrix}U_{1} \\ ⊧ s_{1} = t_{1} ∧ … ∧ s_{n} = t_{n} / θ \end{matrix} ; rr ; ⊧ f(s_{1}, …, s_{n}) = f(t_{1}, …, t_{n}) / θ

σ grounds s_{1}[θ], …, s_{n}[θ] and t_{1}[θ], …, t_{n}[θ]  From assumption
⊧ (s_{1} ≐ t_{1} ∧ … ∧ s_{n} ≐ t_{n})[θ][σ]  By i.h. on U_{1}
s_{1}[θ][σ] = t_{1}[θ][σ], …, s_{n}[θ][σ] = t_{n}[θ][σ]  By inversion
⊧ f(s_{1}, …, s_{n}) ≐ f(t_{1}, …, t_{n})[θ][σ]  By rule ≐ I
□

For the completeness theorem, it is convenient to introduce an intermediate system in which equality is structural, rather than allowing general equality of the form t ≐ t as axioms. This is because there is a mismatch between the algorithm and the specification in that the algorithm analyzes and equality layer-by-layer, while the specification proves ⊧ t ≐ t all at once. We write ⊧^{−} F for a system which contains all the rules in ⊧ F, except that ≐ I is replaced by the following family of rules (one for each constant, function symbol, or predicate symbol h).

⊧^{−} s_{1} ≐ t_{1} ∧ … ∧ s_{n} ≐ t_{n}
≐ I_{h}
⊧^{−} h(s_{1}, …, s_{n}) ≐ h(t_{1}, …, t_{n})

Again, as in the case of the unification algorighm, we take the empty conjunction (for n = 0) to be ⊤. In the extension with parameters, we would have a separate rule for equality between parameters.

Lemma 4.13 (Structural Equality) ⊧ F if and only if ⊧^{−} F.

Proof: See Exercise 4.3. □

Using this property, we can show completeness for structural equality and easily lift it to the general system. In this completeness lemma we need to show that the solution found by the unification algorithm is minimally committed, that is, any actual ground solution is an instance of the solution found by the algorithm.

Lemma 4.14 (Completeness Lemma for Unification) If ⊧^{−} F [σ] for a substitution σ which grounds F, then ⊧ F / θ for some θ and σ = θ ∘ σ′ for some σ′.

Proof: By induction on the structure of derivation E of ⊧^{−} F [σ]. We show some of the cases. Case:

E = \frac{⊤I}{⊧^{−} ⊤[σ]}

⊧ ⊤ / ·  By rule ⊤I
σ = · ∘ σ  By definition of composition

θ = · and σ′ = σ satisfy the claim

Case:

E = \begin{aligned}\begin{matrix}E_{1} \\ ⊧^{−} F_{1}[σ] \end{matrix} & \begin{matrix}E_{2} \\ ⊧^{−} F_{2}[σ] \end{matrix} \\ & ∧I \\ ⊧^{−} (F_{1} ∧ F_{2})[σ] \end{aligned}

⊧ F_{1} / θ_{1} and σ = θ_{1} ∘ σ_{1} for some θ_{1} and σ_{1}  By i.h. on E_{1}
F_{2}[σ] = (F_{2}[θ_{1}])[σ_{1}] where σ_{1} grounds F_{2}[θ_{1}] By props. of substitution
⊧ F_{2}[θ_{1}] / θ_{2} and σ_{1} = θ_{2} ∘ σ_{2} for some θ_{2} and σ_{2}  By i.h. on E_{2}
⊧ (F_{1} ∧ F_{1}) / θ_{1} ∘ θ_{2}  By rule ∧I
σ = θ_{1} ∘ σ_{1} = θ_{1} ∘ (θ_{2} ∘ σ_{2}) = (θ_{1} ∘ θ_{2}) ∘ σ_{2}  By above
θ = θ_{1} ∘ θ_{2} and σ′ = σ_{2} satisfy the claim

Case:

E = \begin{matrix}E_{1} \\ ⊧^{−} [t/x]F_{1}[σ] \end{matrix} ; ∃I ; ⊧^{−} (∃x. f_{1})[σ]

[t/x]F_{1}[σ] = ([X/x]F_{1})[σ, X ↦ t] for a fresh X By definition of substitution

⊧ [X/x]F_{1} / θ_{1} and σ, X ↦ t = θ_{1} ∘ σ_{1}

for some θ_{1} and σ_{1}  By i.h. on E_{1}
⊧ ∃x. F_{1} / θ_{1} − X  By rule ∃I

Now we distinguish two subcases: X is in the domain of θ_{1} and X is not. Subcase: θ_{1} = θ′_{1}, X ↦ t′.

σ, X ↦ t = (θ′_{1}, X ↦ t′) ∘ σ_{1}

= (θ′_{1} ∘ σ_{1}), X ↦ t′[σ_{1}]  By definition of substitution

θ = θ′_{1} and σ′ = σ_{1} satisfy the claim Subcase: X is not in the domain of θ_{1}.

σ, X ↦ t = θ_{1} ∘ σ_{1}  By above
σ_{1} = σ′_{1}, X ↦ t  Since X ∉ dom(θ_{1})

θ = θ_{1} and σ′_{1} satisfy the claim

Case:

E = \begin{matrix}E_{1} \\ ⊧^{−} s′_{1} ≐ t′_{1} ∧ … ∧ s′_{n} ≐ t′_{n} \end{matrix} ; ≐ I_{f} ; ⊧^{−} (s ≐ t)[σ]

where s[σ] = f(s′_{1}, …, s′_{n}) and t[σ] = f(t′_{1}, …, t′_{n}). Here we distinguish several subcases, depending on the structure of s and t. Subcase: s = t = X for some existential variable X.

⊧ X ≐ X / ·  By rule vv=
σ = · ∘ σ  By definition of substitition

θ = · and σ′ = σ satisfy the claim Subcase: s = X and t = Y for X ≠ Y.

X[σ] = Y [σ]  By Lemma 4.13
σ = σ_{1}, X ↦ X[σ], Y ↦ Y [σ]  By definition of substitution
⊧ X ≐ Y / X ↦ Y  By rule vv≠
σ = (X ↦ Y) ∘ (σ_{1}, Y ↦ Y [σ])  By definition of composition

θ = X ↦ Y and σ′ = σ_{1}, Y ↦ Y [σ] satisfy claim Subcase: s = X and r = f(t_{1}, …, t_{n}).

Draft of November 12, 1999

X[σ] = r[σ]  By Lemma 4.13
X not in r  From above
⊧ X ≐ r / X ↦ r  By rule vr
σ = σ_{1}, X ↦ r[σ_{1}]  By properties of substitution
σ = (X ↦ r) ∘ σ_{1}  By definition of composition

θ = X ↦ r and σ = σ_{1} satisfy the claim

Subcase: s = f(s_{1}, …, s_{n}) and r = Y. Symmetric to previous case.
Subcase: s = f(s_{1}, …, s_{n}) and t = f(t_{1}, …, t_{n}).

⊧ s_{1} ≐ t_{1} ∧ … ∧ s_{n} ≐ t_{n} / θ and

σ = θ ∘ σ′ for some θ and σ′  By i.h. on E_{1}
⊧ f(s_{1}, …, s_{n}) ≐ f(t_{1}, …, t_{n}) / θ  By rule rr

θ and σ′ satisfy the claim

□

Theorem 4.15 (Completeness of Unification) If ⊧ F (where F contains no existential variables) then ⊧ F / ·.

Proof: By Lemma 4.13 we can reduce the problem to structural equality. On this, we apply Lemma 4.14 using the empty substitution for σ. □

Soundness and completeness of the deductive system for unification are not enough to yield all the desired properties of an implementation for unification. We also need to verify that, when given an F it always terminates, either failing or returning a substitution θ. By the properties above we know that failure will mean that there is no unifier, and that θ is indeed a most general unifier.

Termination is not a trivial property of the system for unification. This is because in the rule for conjunction of F_{1} ∧ F_{2} we apply unification to F_{2}[θ_{1}] where θ_{1} is a unifier for F_{1}. In general, F_{2}[θ_{1}] could be a much bigger than F_{2}, so a simple termination argument based on the structure of the formula F will fail. If no special measures are taken, an implementation would be exponential, since the textual size of the unifier of two terms may be exponential in the size of the inputs. Consider, for example,

∃x_{1}. ∃x_{2}. ∃x_{2}. f(x_{1}, x_{2}, x_{3}) ≐ f(g(x_{2}, x_{2}), g(x_{3}, x_{3}), g(x_{4}, x_{4}))

In practice, this rather unfortunate complexity bound does not seem to be much of a problem. Most implementations are straightforward, since the size of the terms in realistic theorem proving problems tends to remain relatively small. Moreover, the practically expensive part of unification (the occurs-check in the vr and rv rules) can largely be compiled away and does not need to be carried out very often.

For the proof of termination of unification, see Exercise 4.4.

4.4 Exercises

Exercise 4.1 Give an alternative proof of the inversion properties (Theorem 4.1) which does not use induction, but instead relies on admissibility of cut in the sequent calculus (Theorem 3.11).

Exercise 4.2 Formulate one or several cut rules directly on inversion sequents as presented in Section 4.1 and prove that they are admissible. Does this simplify the development of the completeness result for inversion proofs? Show how admissibility might be used, or illustrate why it is not much help.

Exercise 4.3 Prove Lemma 4.13.

Exercise 4.4 Prove that the rules for unification read as an algorithm for computing θ from F always terminate, either with failure to construct a derivation (in which case there is no unifier) or with a θ (in which case θ is a most general unifier).

The Inverse Method

After the definition of logic via natural deduction, we have developed a succession of techniques for theorem proving based on sequent calculi. We considered a sequent Γ ⟹ C as a goal, to be solved by backwards-directed search which was modeled by the bottom-up construction of a derivation. The critical choices were disjunctive non-determinism (resolved by guessing and backtracking) and existential non-determinism (resolved by introducing existential variables and unification). The limiting factor in more refined theorem provers based on this method is generally the number of disjunctive choices which have to be made. It is complicated by the fact that existential variables are global in a partial derivation, which means that choices in one conjunctive branch have effects in other branches. This effects redundancy elimination, since subgoals are not independent of each other.

The diametrically opposite approach would be to work forward from the initial sequents until the goal sequent is reached. If we guarantee a fair strategy in the selection of axioms and inference rules, every goal sequent can be derived this way. Without further improvements, this is clearly infeasible, since there are too many derivations for us to hope that we can find one for the goal sequent in this manner.

The inverse method is based on the property that in a cut-free derivation of a goal sequent, we only need to consider subformulas of the goal and their substitution instances. For example, when we have derived both A and B in the forward direction, we only derive their conjunction A ∧ B if A ∧ B is a subformula of the goal sequent.

The nature of forward search under these restrictions is quite different from the backward search. Since we always add new consequences to the sequents already derived, knowledge grows monotonically and no disjunctive non-determinism arises. Similarly for existential non-determinism, if we keep sequents in their maximally general form. On the other hand, there is a potentially very large amount of conjunctive non-determinism, since we have to apply all applicable rules to all sequents in a fair manner in order to guarantee completeness. The critical factor in forward search is to limit conjunctive non-determinism. We can view this as redundancy elimination: among the many ways that a given sequent may be derived, we try to actually consider a few as possible. The techniques developed in the preceding chapters, with some modifications, can be applied in this new setting.

Historically, the inverse method is due to Maslov [Mas64]. It has been adapted to intuitionistic and other non-classical logics by Voronkov [Vor92], Mints [Min94], and Tammet [Tam96, Tam97].

5.1 Forward Sequent Calculus

As a first step towards the inverse method, we write out a sequent calculus appropriate for forward search. This stems from a basic reinterpretation of a sequent during search. Previously, Γ ⟹ C expressed that we may use all hypotheses in Γ to prove that C is true. Now we will think of Γ ⟶ C to mean that we needed all the hypotheses in Γ in order to prove that C is true.

This means that weakening is no longer valid for sequents Γ ⟶ C and we have to take special care when we formulate correctness theorems. Secondly, we do not need to keep duplicate assumptions, so we view Γ in the sequent Γ ⟶ C as a set of assumptions. We write Γ_{1} ∪ Γ_{2} for the union of two sets of assumptions, and Γ, A stands for Γ ∪ {A}.^{1}

Initial Sequents. Previously, we allowed Γ, A ⟹ A, since the assumptions in Γ can be used, but are just not needed in this case. In the forward calculus, initial sequents

\frac{init}{A ⟶ A}

express that only the hypothesis A is needed to derive the truth of A and nothing else.

Conjunction. In the right rule for conjunction, we previously concluded Γ ⟹ A ∧ B from Γ ⟹ A and Γ ⟹ B. This expressed that all assumptions Γ are available in both branches. Now we need to take the union of the two sets of assumptions, expressing that both are needed to prove the conclusion.

Γ_{1} ⟶ A Γ_{2} ⟶ B

∧R Γ_{1} ∪ Γ_{2} ⟶ A ∧ B

On the left rules, so such considerations arise.

\begin{aligned}Γ, A ⟶ C \\ & ∧L_{1} \\ Γ, A ∧ B ⟶ C \end{aligned}  \begin{aligned}Γ, B ⟶ C \\ & ∧L_{2} \\ Γ, A ∧ B ⟶ C \end{aligned}

Note that if A ∧ B is already present in Γ in the two left rules, it will not be added again.

1In the language of judgments, Γ ⟶ A is a strict hypothetical judgment.

Draft of November 12, 1999

Truth. As in the backward sequent calculus, there is only a right rule. Unlike the backward sequent calculus, it does not permit any hypotheses.

\frac{⊤R}{· ⟶ ⊤}

Implication. In the backward sequent calculus, the right rule for implication has the form

\begin{aligned}Γ, A ⟹ B \\ & ⊃R. \\ Γ ⟹ A ⊃ B \end{aligned}

In the forward direction this would not be sufficient, because it would allow us to conclude A ⊃ B only if A is actually needed in the proof of B. To account for this case, we introduce two separate rules.

\begin{aligned}Γ, A ⟶ B \\ & ⊃R_{1} \\ Γ ⟶ A ⊃ B \end{aligned}  \begin{aligned}Γ ⟶ B \\ & ⊃R_{2} \\ Γ ⟶ A ⊃ B \end{aligned}

Another, more efficient possibility combines these rules into one which removes A from the context of the premise if it is there and otherwise leaves it unchanged (see Section ??). In the left rule we have to take a union as in the right rule for conjunction.

Γ_{1} ⟶ A Γ_{2}, B ⟶ C
⊃L
Γ_{1} ∪ Γ_{2}, A ⊃ B ⟶ C

Note that the principal proposition A ⊃ B does not occur in the premises. However, it might occur in Γ_{1} or Γ_{2}, in which case it is not added again in the conclusion.

Disjunction. This introduces no new considerations.

\begin{aligned}Γ ⟶ A \\ & ∨R_{1} \\ Γ ⟶ A ∨ B \end{aligned}  \begin{aligned}Γ ⟶ B \\ & ∨R_{2} \\ Γ ⟶ A ∨ B \end{aligned}
Γ_{1}, A ⟶ C Γ_{2}, B ⟶ C

∨L Γ_{1}, Γ_{2}, A ∨ B ⟶ C

Falsehood. There is only a left rule.

\frac{⊥L}{⊥ ⟶ C}

We postpone the consideration of negation and quantifiers.

The soundness of the forward sequent calculus is easy to establish.

Theorem 5.1 (Soundness of Forward Sequent Calculus) If Γ ⟶ C then Γ ⟹ C Proof: By induction on the structure of the derivation F of Γ ⟶ C. We show only some of the cases, since the patterns are very similar in the remaining ones. In order to avoid confusion, we write Γ, A and Γ ∪ {A} for forward sequents to be more explicit about possible contractions.

Case:

F = \frac{init}{C ⟶ C}

C ⟹ C  By rule init

Case:

F = \begin{aligned}\begin{matrix}F_{1} \\ Γ_{1} ⟶ C_{1} \end{matrix} & \begin{matrix}F_{2} \\ Γ_{2} ⟶ C_{2} \end{matrix} \\ & ∧R \\ Γ_{1} ∪ Γ_{2} ⟶ C_{1} ∧ C_{2} \end{aligned}

Γ_{1} ⟹ C_{1}  By i.h. on F_{1}
Γ_{1} ∪ Γ_{2} ⟹ C_{1}  By weakening
Γ_{2} ⟹ C_{2}  By i.h. on F_{2}
Γ_{1} ∪ Γ_{2} ⟹ C_{2}  By weakening
Γ_{1} ∪ Γ_{2} ⟹ C_{1} ∧ C_{2}  By rule ∧R

Case:

F = \begin{aligned}\begin{matrix}F_{1} \\ Γ_{1} ⟶ A \end{matrix} & \begin{matrix}F_{2} \\ Γ_{2}, B ⟶ C \end{matrix} \\ & ⊃L \\ Γ_{1} ∪ Γ_{2} ∪ \{A ⊃ B\} ⟶ C \end{aligned}

Γ_{1} ⟹ A  By i.h. on F_{1}
Γ_{1} ∪ Γ_{2}, A ⊃ B ⟹ A  By weakening
Γ_{2}, B ⟹ C  By i.h. on F_{2}
Γ_{1} ∪ Γ_{2}, A ⊃ B, B ⟹ C  By weakening
Γ_{1} ∪ Γ_{2}, A ⊃ B ⟹ C  By rule ⊃L
Γ_{1} ∪ Γ_{2} ∪ {A ⊃ B} ⟹ C  By contraction (if needed)
□

Completeness is more difficult. In fact, it is false! For example, for atomic propositions P and Q we can not derive P, Q ⟹ P. Fortunately, the absence of weakening is the only source of difficulty and can easily be taken into account.

Theorem 5.2 (Completeness of Forward Sequent Calculus) If Γ ⟹ C then Γ′ ⟶ C for some Γ′ ⊆ Γ.

Proof: By induction on the structure of S for Γ ⟹ C.

Case:

S = \frac{init}{Γ_{1}, C ⟹ C}

C ⟶ C  By rule init
{C} ⊆ Γ_{1}, C  By definition of ⊆

Case:

S = \begin{matrix}S_{1} \\ Γ, A ⟹ B \end{matrix} ; ⊃R ; Γ ⟹ A ⊃ B

Γ′′ ⟶ B for some Γ′′ ⊆ Γ, A  By i.h. on S_{1}
Γ′′ = Γ′, A and Γ′ ⊆ Γ  First subcase
Γ′ ⟶ A ⊃ B  By rule ⊃R_{1}
Γ′′ ⊆ Γ  Second subcase
Γ′′ ⟶ A ⊃ B  By rule ⊃R_{2}

Case:

S = \begin{aligned}\begin{matrix}S_{1} \\ Γ_{1}, A ⊃ B ⟹ A \end{matrix} & \begin{matrix}S_{2} \\ Γ_{1}, A ⊃ B, B ⟹ C \end{matrix} \\ & ⊃L \\ Γ_{1}, A ⊃ B ⟹ C \end{aligned}

Γ′_{1} ⟶ A for some Γ′_{1} ⊆ Γ_{1}, A ⊃ B  By i.h. on S_{1}
Γ′_{2} ⟶ C for some Γ′_{2} ⊆ Γ_{1}, A ⊃ B, B  By i.h. on S_{2}
Γ′_{2} = Γ′′_{2}, B and Γ′′_{2} ⊆ Γ_{1}, A ⊃ B  First subcase
Γ′_{1} ∪ Γ′′_{2} ∪ {A ⊃ B} ⟶ C  By rule ⊃L
Γ′_{1} ∪ Γ′′_{2} ∪ {A ⊃ B} ⊆ Γ_{1} ∪ {A ⊃ B}  By properties of ⊆
Γ′_{2} ⊆ Γ_{1}, A ⊃ B  Second subcase

Γ′ = Γ′_{2} satisfies claim

□

5.2 Negation and Empty Succedents

In the backward sequent calculus, the rules for negation

\begin{aligned}Γ, A ⟹ p \\ & ¬R^{p} \\ Γ ⟹ ¬A \end{aligned}  \begin{aligned}Γ, ¬A ⟹ A \\ & ¬L \\ Γ, ¬A ⟹ C \end{aligned}

require propositional parameters p. In Gentzen’s original formulation of the sequent calculus he avoided this complication by allowing an empty right-hand side. A sequent of the form

Γ ⟹ ·

can then be interpreted as

Γ ⟹ p for a parameter p not in Γ

As a result we can substitute an arbitrary proposition for the right-hand side (the defining property for parametric judgments) and obtain an evident judgment. In the sequent calculus with empty right-hand sides, this can be accomplished by weakening on the right:

If Γ ⟹ · then Γ ⟹ C for any proposition C.

When the right-hand side can be empty or a singleton we write Γ ⟹ γ, where γ = C or γ = ·.

In a forward sequent calculus we can take advantage of this in order to avoid overcommitment in the rules for negation and falsehood. We first show the forward rules for negation; then we reexamine all the previous rules.

Negation. We just take advantage of the new form of judgment, avoiding, for example, a commitment to a particular proposition C in the ¬L rule.

\begin{aligned}Γ, A ⟶ · \\ & ¬R \\ Γ ⟶ ¬A \end{aligned}  \begin{aligned}Γ ⟶ A \\ & ¬L \\ Γ, ¬A ⟶ · \end{aligned}

Interestingly, we do not need a second right rule for negation as for implication (see Exercise ??).

Falsehood. Falsehood can similarly benefit from avoiding commitment. Note that previously the rule stated ⊥ ⟶ C, although there are many possible choices for C. Now we just replace this by

\frac{⊥L}{⊥ ⟶ ·}

There still is no right rule.

Initial Sequents. They do not change.

\frac{init}{A ⟶ A}

Conjunction. The right rule requires no change.

Γ_{1} ⟶ A Γ_{2} ⟶ B

∧R Γ_{1} ∪ Γ_{2} ⟶ A ∧ B

On the left rules simply need to allow for an empty right-hand side.

\begin{aligned}Γ, A ⟶ γ \\ & ∧L_{1} \\ Γ, A ∧ B ⟶ γ \end{aligned}  \begin{aligned}Γ, B ⟶ γ \\ & ∧L_{2} \\ Γ, A ∧ B ⟶ γ \end{aligned}

Draft of November 12, 1999

Truth. Does not change.

\frac{⊤R}{· ⟶ ⊤}

Implication. The possibility of empty right-hand sides requires a third right rule for implication. Again, in an implementation the three rules might be combined into a more efficient one.

\begin{aligned}Γ, A ⟶ B \\ & ⊃R_{1} \\ Γ ⟶ A ⊃ B \end{aligned}  \begin{aligned}Γ ⟶ B \\ & ⊃R_{2} \\ Γ ⟶ A ⊃ B \end{aligned}  \begin{aligned}Γ, A ⟶ · \\ & ⊃R_{3} \\ Γ ⟶ A ⊃ B \end{aligned}
Γ_{1} ⟶ A Γ_{2}, B ⟶ γ
⊃L
Γ_{1} ∪ Γ_{2}, A ⊃ B ⟶ γ

Disjunction. The rule for disjunction on the right remains the same, but the left rule now has to account for several possibilities, depending on whether the right-hand sides of the premises are empty. Essentially, we take the union of the right-hand sides of the two premises, except that the result must be a singleton or empty for the sequent to be well-formed.

\begin{aligned}Γ ⟶ A \\ & ∨R_{1} \\ Γ ⟶ A ∨ B \end{aligned}  \begin{aligned}Γ ⟶ B \\ & ∨R_{2} \\ Γ ⟶ A ∨ B \end{aligned}
Γ_{1}, A ⟶ γ_{1} Γ_{2}, B ⟶ γ_{2}

∨L Γ_{1} ∪ Γ_{2}, A ∨ B ⟶ γ_{1} ∪ γ_{2}

In detail, either γ_{1} or γ_{2} is empty, or γ_{1} = γ_{2} = C = γ_{1} ∪ γ_{2}. The rule does not apply otherwise.

The statement of the soundness theorem does not change much with empty succedents.

Theorem 5.3 (Soundness of Forward Sequent Calculus)

1. If Γ ⟶ C then Γ ⟹ C, and

2. if Γ ⟶ · then Γ ⟹ C for all C.

Proof: By induction on the derivation F of Γ ⟶ γ. □

In the completeness theorem, we now need to allow possible weakening on the left or on the right.

Theorem 5.4 (Completeness of Forward Sequent Calculus)

1. If Γ ⟹ C then Γ′ ⟶ C or Γ′ ⟶ · for some Γ′ ⊆ Γ.

Proof: By induction on the derivation S of Γ ⟹ C. □

5.3 The Subformula Property

It is a general property of cut-free sequent calculi that all propositions occurring in a derivation are subformulas of the endsequent. In the forward direction we can therefore restrict the application of a rule to the case where the principal formula in the conclusion is a subformula of the goal sequent. We refine this property further by tracking positive and negative subformula occurrences. We then restrict left rule to introduce only negative subformulas of the goal sequent and right rules to positive subformulas of the goal sequent. To this end we introduce signed formulas.

Positive A^{+} ::= P^{+} | A_{1}^{+} ∧ A_{2}^{+} | A_{1}^{−} ⊃ A_{2}^{+} | A_{1}^{+} ∨ A_{2}^{+} | ⊤^{+} | ⊥^{+} | ¬A^{−}
Negative A^{−} ::= P^{−} | A_{1}^{−} ∧ A_{2}^{−} | A_{1}^{+} ⊃ A_{2}^{−} | A_{1}^{−} ∨ A_{2}^{−} | ⊤^{−} | ⊥^{−} | ¬A^{+}

It is obvious that every proposition can be annotated both positively and negatively, and that such an annotation is unique. We write Γ^{−} for a context A_{1}^{−}, …, A_{n}^{−} and γ^{+} for an empty succedent or C^{+}. All inference rules for the sequent calculus can be annotated so that for a goal sequent Γ^{−} ⟶ γ^{+}, each sequent arising in the derivation has the same form, with only negative propositions on the left and positive propositions on the right (see Exercise 5.1). We say that A is a subformula of Γ or γ if A is a subformula of an element of Γ or γ, respectively, and similarly for signed propositions.

Theorem 5.5 (Signed Subformula Property) Given a derivation S of Γ^{−} ⟶ γ^{+}. Then each sequent in S has the form A_{1}^{−}, …, A_{n}^{−} ⟶ B^{+} or A_{1}^{−}, …, A_{n}^{−} ⟶ · where all A_{i}^{−} and B^{+} are signed subformulas of Γ^{−} or γ^{+}.

Proof: By straightforward induction on the structure of S. □

Note that this is a very strong theorem, since it asserts not only that every provable goal sequent has a derivation consisting of subformulas, but that all derivations of a provable sequent consist only of subformulas. A sequent not consisting of subformulas cannot contribute to a derivation of a goal sequent in the (cut-free) forward sequent calculus.

The subformula property immediately gives rise to a procedure for forward theorem proving. We start with all initial sequents of the form A^{−} ⟶ A^{+} where both A^{−} and A^{+} are signed subformulas of the goal sequent. We also have to add · ⟶ ⊤^{+} and ⊥^{−} ⟶ · if ⊤^{+} or ⊥^{−} are subformulas of the goal sequent, respectively.

Then we apply all possible inference rules where the principal proposition in the conclusion is a subformula of the goal sequent. We stop with success when we have generated the goal sequent, or if the goal sequent can be obtained from a generated sequent by weakening. We fail if any possible way of applying inference rules yields only sequents already in the database. In that case the goal sequent cannot be derivable if we have not encountered it (or a strengthened form of it) already.

We now show an example derivation in a linearized format. The goal sequent is A ⊃ (B ⊃ C) ⟶ ((A ∧ B) ⊃ C). After signing each subformula we obtain

(A^{+} ⊃ (B^{+} ⊃ C^{−})^{−})^{−} ⟶ (((A^{−} ∧ B^{−})^{−}) ⊃ C^{+})^{+}

If show only the top-level sign, this leads to the following list of signed subformulas.

A^{+}, B^{+}, C^{−}, A^{−}, B^{−}, C^{+},
(B ⊃ C)^{−}, (A ∧ B)^{−},
(A ⊃ (B ⊃ C))^{−}, ((A ∧ B) ⊃ C)^{+}

This means we have both positive and negative occurrences of A, B, and C and we have to consider three initial sequents.

1 A^{−} ⟶ A^{+}  init
2 B^{−} ⟶ B^{+}  init
3 C^{−} ⟶ C^{+}  init
4 (A ∧ B)^{−} ⟶ A^{+}  ∧L_{1} 1
5 (A ∧ B)^{−} ⟶ B^{+}  ∧L_{1} 2
6 (A ∧ B)^{−}, (B ⊃ C)^{−} ⟶ C^{+}  ⊃L 5 3
7 (A ∧ B)^{−}, (A ⊃ (B ⊃ C))^{−} ⟶ C^{+} ⊃L 4 6
8 (A ⊃ (B ⊃ C))^{−} ⟶ ((A ∧ B) ⊃ C)^{+} ⊃R_{1} 7

We use the horizontal lines to indicate iterations of an algorithm which derives all possible new consequences from the sequents already established. We have elided those sequents that do not contribute to the final derivation. For example, in the first step we can use ⊃R_{2} to conclude C^{−} ⟶ ((A ∧ B) ⊃ C)^{+}, from C^{−} ⟶ C^{+}, since the succedent is a positive subformula of the goal sequent.

Note that the inference of line 7 contains an implicit contraction, since (A ∧ B)^{−} is an assumption in both premises (4 and 6).

5.4 Naming Subformulas

Without any further optimizations, the check if a given inference rule should be used in the forward direction is complicated, since we have to repeatedly scan the goal sequent for subformula occurrences. An integral part of the inverse method is to avoid this scan by introducing names for non-atomic subformulas and then specialize the inference rules to work only the names. We will not be formal about this optimization, since we view it as an implementation technique, but not an improvement of a logical nature. By expanding all newly defined names we obtain a derivation as in the previous section.

We return to the previous example to illustrate the technique. The goal sequent is A ⊃ (B ⊃ C) ⟶ (A ∧ B) ⊃ C). After naming each subformula we obtain the signed atomic propositions

A^{+}, B^{+}, C^{−}, A^{−}, B^{−}, C^{+}, and the new names

\begin{aligned}L_{1}^{−} & = & B^{+} ⊃ C^{−} \\ L_{2}^{−} & = & A^{−} ∧ B^{−} \\ L_{3}^{−} & = & A^{+} ⊃ L_{1}^{−} \\ L_{4}^{+} & = & L_{2}^{−} ⊃ C^{+} \end{aligned}

We can now write out the general sequent calculus inference rules, specialized to the above labels. Since the goal sequent contains no negative occurrence of negation or falsehood, we may restrict the right-hand sides of all rules to be non-empty. This means only two implication right rules are necessary instead of three for L_{4}^{+}.

Γ_{1} ⟶ B^{+} Γ_{2}, C^{−} ⟶ γ
⊃L (L_{1}^{−})
Γ_{1} ∪ Γ_{2}, L_{1}^{−} ⟶ γ

\begin{aligned}Γ, A^{−} ⟶ γ \\ & ∧L_{1} (L_{2}^{−}) \\ Γ, L_{2}^{−} ⟶ γ \end{aligned}  \begin{aligned}Γ, B^{−} ⟶ γ \\ & ∧L_{2} (L_{2}^{−}) \\ Γ, L_{2}^{−} ⟶ γ \end{aligned}
Γ_{1} ⟶ A^{+} Γ_{2}, L_{1}^{−} ⟶ γ
⊃L (L_{3}^{−})
Γ_{1} ∪ Γ_{2}, L_{3}^{−} ⟶ γ

\begin{aligned}Γ, L_{2}^{−} ⟶ C^{+} \\ & ⊃R_{1} (L_{4}^{+}) \\ Γ ⟶ L_{4}^{+} \end{aligned}  \begin{aligned}Γ ⟶ C^{+} \\ & ⊃R_{2} (L_{4}^{+}) \\ Γ ⟶ L_{4}^{+} \end{aligned}

In its labeled form, the derivation above looks as follows.

1 A^{−} ⟶ A^{+}  init
2 B^{−} ⟶ B^{+}  init
3 C^{−} ⟶ C^{+}  init
4 L_{2}^{−} ⟶ A^{+}  ∧L_{1} 1
5 L_{2}^{−} ⟶ B^{+}  ∧L_{1} 2
6 L_{2}^{−}, L_{1}^{−} ⟶ C^{+} ⊃L 5 3
7 L_{2}^{−}, L_{3}^{−} ⟶ C^{+} ⊃L 4 6
8 L_{3}^{−} ⟶ L_{4}^{+}  ⊃R_{1} 7

In the algorithm for labeling subterms we can avoid some redundancy if we give identical subterms the same label. However, this is not required for soundness and completeness, it only trims the search space.

Another choice arises for initial sequents. As in backwards search, we may restrict ourselves to atomic initial sequents or we may allow arbitrary labeled subformulas as long as they occur both negatively and positively. Tammet [Tam96] reports that allowing non-atomic initial sequents led to significant speed-up on a certain class of test problems. Of course, in their named form, even non-atomic sequents have the simple form L^{−} ⟶ L^{+} for a label L.

5.5 Forward Subsumption

For the propositional case, we can obtain a decision procedure from the inverse method. We stop with success if we have reached the goal sequent (or a strengthened form of it) and with failure if any possible application of an inference rule leads to a sequent that is already present. This means we should devise a data structure or algorithm which allows us to check easily if the conclusion of an inference rule application is already present in the database of derived sequents. This check for equality should allow for permutations of hypotheses.

We can improve this further by not just checking equality modulo permutations, but taking weakening into account. For example, if we have derived L_{1}^{−}, L_{2}^{−} ⟶ L_{4}^{+} then the sequent L_{1}^{−}, L_{2}^{−}, L_{3}^{−} ⟶ L_{4}^{+} is redundant and could simply be obtained from the previous sequent by weakening. Similarly, L_{1}^{−} ⟶ · has more information than L_{1}^{−} ⟶ L_{2}^{+}, so the latter clause does not need to be kept if we have the former clause. Note that we already need this form of weakening to determine success if the goal sequent has assumptions. We say the a sequent S subsumes a sequent S′ (written as S ≤ S′) if S′ can be obtains from S by weakening on the right and left.

In the propositional case, there is a relatively simple way to implement subsumption. We introduce a total ordering among all atomic propositions and also the new literals introduced during the naming process. Then we keep the antecedents of each sequent as an ordered list of atoms and literals. The union operation required in the implementation of inference rules with two premises, and the subset test required for subsumption can now both be implemented efficiently.

The reverse, called backward subsumption discards a previously derived sequent S if the new sequent S′ subsumes S. Generally, backward subsumption is considered less fundamentally important. For example, it is not necessary to obtain a decision procedure for the propositional case. Implementations generally appear to be optimized for efficient forward subsumption.

[ the remainder of this section is speculative ]

However, it seems possible to exploit backward subsumption in a stronger way. Instead of simply deleting the subsumed sequent, we could strengthen its consequences, essentially by replaying the rules applied to it on the stronger sequent.

5.6 Proof Terms for the Inverse Method

The simplicity of the proof for the completeness theorem (Theorem 5.4) indicates that a proof term assignment should be relatively straightforward. The implicit contraction necessary when taking the union of two sets of antecedents presents the only complication. A straightforward solution seems to be to label each antecedent not with just a single variable, but with a set of variables. When taking the union of two sets of antecedents, we also need to take the union of the corresponding label sets. But this would require globally different variables for labeling antecedents in order to avoid interference between the premises of two-premise rules. Another possibility would be to assign a unique label to each negative subformula of the goal sequent and simply use this label in the proof term. This strategy will have to be reexamined in the first-order case, since a given literal may appear with different arguments.

Note that proof term assignment in the forward sequent calculus can be done on-line or off-line. In the on-line method we construct an appropriate proof term for each sequent at each inference step in a partial derivation. In the off-line method we keep track of the minimal information so we can recover the actual sequence of inference steps to arrive a the final conclusion. From this we reconstruct a proof term only once a complete sequent derivation has been found.

The on-line method would be preferable if we could use the proof term information to guide further inferences or subsumption; otherwise the off-line method is preferable since the overhead is reduced to a a validation phase once a proof has been found.

5.7 Inverse Focusing

In the system presented so far the non-determinism in forward reasoning is still unacceptable, despite the use of subsumption. We can now analyze the rules in a way that is analogous to Chapter 4, taking advantage of inversion and focusing properties. This eliminates many derivations, significantly improving overall efficiency at a high level of abstraction. Similar optimizations have been proposed by Tammet [Tam96] and Mints [Min94], although the exact relationship between these system and the one presented below have yet to be investigated.

In focused derivations, we reason from the goal sequent upward, first applying invertible rules. This means that in the inverse method, invertible rules will be applied last, since we reason from the initial to the goal sequent. Conversely, in focused derivations we finish proofs in the focusing phase, which is therefore the first phase to be applied in the forward direction.

We first show the rules for focus sequents. These rules roughly correspond to the Tammet’s reduction strategy.

Δ; · > A; · Right focus on A
Δ; A > ·; R Left focus on A

We apply the following restrictions.

Left passive  L ::= P | A ∧ B | ⊤ | A ⊃ B | ∀x. A
Passive context Δ ::= · | Δ, L
Right passive R ::= P | A ∨ B | ⊥ | ∃x. A

These are slightly different from the previous definitions since conjunction and truth is treated in a different manner.

Left Focus Rules. As mentioned at the end of Section 5.4, we can restrict initial sequents to be atomic or literals which name compound formulas which appear both positively and negatively. As given below, however, the literals would have to stand for R-formulas for this rule to be applicable.

\frac{init}{Δ; P > ·; P}

\begin{aligned}Δ; A > ·; R \\ & ∧L_{1} \\ Δ; A ∧ B > ·; R \end{aligned}  \begin{aligned}Δ; B > ·; R \\ & ∧L_{2} \\ Δ; A ∧ B > ·; R \end{aligned}

\begin{aligned}Δ_{1}; B > ·; R  Δ_{2}; · ⟶ A; · \\ & ⊃L \\ Δ_{1} ∪ Δ_{2}; A ⊃ B > ·; R \end{aligned}  no rule ⊤L

Δ; [t/x]A > ·; R

∀L Δ; ∀x. A > ·; R

Right Focus Rules.

\begin{aligned}Δ; · > A; · \\ & ∨R_{1} \\ Δ; · > A ∨ B; · \end{aligned}  \begin{aligned}Δ; · > B; · \\ & ∨R_{2} \\ Δ; · > A ∨ B; · \end{aligned}

\begin{aligned}Δ; · > [t/x]A; · \\ & ∃R \\ Δ; · > ∃x. A; · \end{aligned}  no rule ⊥R

Transition Rules.

\frac{Δ; L > ·; R}{(Δ, L); · ⟶ ·; R}  \frac{Δ; · > R_{+}; ·}{Δ; · ⟶ ·; R_{+}}

Here, R_{+} is an non-atomic R-formula.

In the backwards directed focusing calculus we can choose between the active right rules in a don’t-care non-deterministic manner. This means the calculus admits many derivations; choosing any one of them is complete. For the forward directions we should eliminate this so that exactly one of the derivations will be generated. While the forward active rules below cut down some on the nondeterminism, they do not yet have this stronger property. For this will need to add some ordering properties^{2} (see Section ??). This roughly corresponds to Tammet’s inversion strategy.

Our partial solution is to force the right active rules to be applied first (in the downward direction) and the left active rules second. Moreover, we restrict ourselves to at most one active proposition on the left and right. Therefore we have the following three judgments (the first being an auxiliary one).

2[I speculate]

Draft of November 12, 1999

Δ; · ⟶ ·; R Neutral sequent
Δ; · ⟶ A; · Right active A
Δ; A ⟶ B; · Left active A and right active B

Right Active Rules.

\frac{Δ; · ⟶ ·; R}{Δ; · ⟶ R; ·}

\begin{aligned}Δ_{1}; · ⟶ A; ·  Δ_{2}; · ⟶ B; · \\ & ∧R \\ Δ_{1} ∪ Δ_{2}; · ⟶ A ∧ B; · \end{aligned}  \frac{⊤R}{·; · ⟶ ⊤; ·}

Δ; · ⟶ B; ·

⊃R_{2}

Δ; · ⟶ A ⊃ B; ·

Δ; · ⟶ [a/x]A; ·

∀R^{a} Δ; · ⟶ ∀x. A; ·

Left Active Rules.

\frac{(Δ, L); · ⟶ C; ·}{Δ; L ⟶ C; ·}

Δ; A ⟶ B; ·

⊃R_{1}

Δ; · ⟶ A ⊃ B; ·

\begin{aligned}Δ_{1}; A ⟶ C; ·  Δ_{2}; B ⟶ C; · \\ & ∨L \\ Δ_{1} ∪ Δ_{2}; A ∨ B ⟶ C; · \end{aligned}  \frac{⊥L}{·; ⊥ ⟶ C; ·}

Δ; [a/x]A ⟶ C; ·

∃L^{a} Δ; ∃x. A ⟶ C; ·

Note that the left rule for ⊥ is not satisfactory because of the unconstrained proposition C on the right. A satisfactory treatment can be given using empty right-hand sides (see Section 5.8) or by replacing C by a propositional parameter p. However, this latter solution has further consequences (see Exercise ??).

Transitions Rules.

\frac{Δ; \overline{L}_{+} ⟶ R; ·}{Δ; \overline{L}_{+} > ·; R}  \frac{Δ; · ⟶ \overline{R}; ·}{Δ; · > \overline{R}; ·}

We restrict these rules to

\begin{aligned}\overline{L}_{+} & ::= & A ∨ B | ⊥ | ∃x. A \\ \overline{R} & ::= & P | A ⊃ B | A ∧ B | ⊤ | ∀x. A \end{aligned}

Draft of November 12, 1999

Soudness of inverse focused derivations is relatively easy to see, since the rules are just specializations of the usual forward sequent rules. Completeness is more difficult to show, especially since it does not hold for arbitrary active sequents Δ; Γ ⟹ A; · or Δ; Γ ⟹ ·; A. This means that we have to take advantage of the don’t care non-determinism and choose (in the bottom-up direction) to always work on the left-hand side of the sequent first and then the right-hand side. One might proceed by first proving the completeness of this strategy with respect to the bottom-up focusing calculus, and then prove the completeness of the inverse focusing rules with respect to this intermediate calculus.

In practice, one might want to apply backwards rules in a don’t-care nondeterministic fashion if a given goal sequent does not have the form Δ; · ⟹ A; · and solve the remaining subgoals with the inverse method. Alternatively, one can “hide” left invertible connectives, for example, by discharging them and proving ·; · ⟶ A_{1} ⊃ … ⊃ A_{n} ⊃ A; · for Γ = A_{1}, …, A_{n}.

[ Fill in appropriate soundness and completeness theorem here. ]

5.8 Inverse Focusing with Negation

As in Section 5.2, negation is handled by allowing empty succedents. We apply the following restrictions.

Left passive  L ::= P | A ∧ B | ⊤ | A ⊃ B | ∀x. A | ¬A
Passive context Δ ::= · | Δ, L
Right passive R ::= P | A ∨ B | ⊥ | ∃x. A

We have the following judgments, where ρ is either empty or a singleton R and γ is either empty or a singleton A.

Δ; · > A; ·  Right focus on A
Δ; A > ·; ρ Left focus on A
Δ; · ⟶ ·; ρ Neutral sequent
Δ; · ⟶ A; · Right active A
Δ; A ⟶ γ; · Left active A, possible right active γ

Left Focus Rules.

\frac{init}{Δ; P > ·; P}

\begin{aligned}Δ; A > ·; ρ \\ & ∧L_{1} \\ Δ; A ∧ B > ·; ρ \end{aligned}  \begin{aligned}Δ; B > ·; ρ \\ & ∧L_{2} \\ Δ; A ∧ B > ·; ρ \end{aligned}

\begin{aligned}Δ_{1}; B > ·; ρ  Δ_{2}; · ⟶ A; · \\ & ⊃L \\ Δ_{1} ∪ Δ_{2}; A ⊃ B > ·; ρ \end{aligned}  no rule ⊤L

\begin{aligned}Δ; · ⟶ A; · \\ & ¬L \\ Δ; ¬A > ·; · \end{aligned}  \begin{aligned}Δ; [t/x]A > ·; ρ \\ & ∀L \\ Δ; ∀x. A > ·; ρ \end{aligned}

Draft of November 12, 1999

Right Focus Rules.

\begin{aligned}Δ; · > A; · \\ & ∨R_{1} \\ Δ; · > A ∨ B; · \end{aligned}  \begin{aligned}Δ; · > B; · \\ & ∨R_{2} \\ Δ; · > A ∨ B; · \end{aligned}
\begin{aligned}Δ; · > [t/x]A; · \\ & ∃R \\ Δ; · > ∃x. A; · \end{aligned}  no rule ⊥R

Transition Rules.

\frac{Δ; L > ·; ρ}{(Δ, L); · ⟶ ·; ρ}  \frac{Δ; · > R_{+}; ·}{Δ; · ⟶ ·; R_{+}}

Here, R_{+} is a non-atomic R-formula. Right Active Rules.

\frac{Δ; · ⟶ ·; R}{Δ; · ⟶ R; ·}

\begin{aligned}Δ_{1}; · ⟶ A; ·  Δ_{2}; · ⟶ B; · \\ & ∧R \\ Δ_{1} ∪ Δ_{2}; · ⟶ A ∧ B; · \end{aligned}  \frac{⊤R}{·; · ⟶ ⊤; ·}

Δ; · ⟶ B; ·

⊃R_{2}

Δ; · ⟶ A ⊃ B; ·
Δ; · ⟶ [a/x]A; ·

∀R^{a} Δ; · ⟶ ∀x. A; ·

Left Active Rules.

\frac{(Δ, L); · ⟶ γ; ·}{Δ; L ⟶ γ; ·}

\begin{aligned}Δ; A ⟶ B; · \\ & ⊃R_{1} \\ Δ; · ⟶ A ⊃ B; · \end{aligned}  \begin{aligned}Δ; A ⟶ ·; · \\ & ⊃R_{3} \\ Δ; · ⟶ A ⊃ B; · \end{aligned}

\begin{aligned}Δ; A ⟶ ·; · \\ & ¬R \\ Δ; · ⟶ ¬A; · \end{aligned}

\begin{aligned}Δ_{1}; A ⟶ γ_{1}; ·  Δ_{2}; B ⟶ γ_{2}; · \\ & ∨L \\ Δ_{1} ∪ Δ_{2}; A ∨ B ⟶ γ_{1} ∪ γ_{2}; · \end{aligned}  \frac{⊥L}{·; ⊥ ⟶ ·; ·}

Δ; [a/x]A ⟶ γ; ·

∃L^{a} Δ; ∃x. A ⟶ C; ·

Draft of November 12, 1999

Note that ∨L requires γ_{1} ∪ γ_{2} either to be a singleton C or empty.

Transitions Rules.

\frac{Δ; \overline{L}_{+} ⟶ ρ; ·}{Δ; \overline{L}_{+} > ·; ρ}  \frac{Δ; · ⟶ \overline{R}; ·}{Δ; · > \overline{R}; ·}

We restrict these rules to

\begin{aligned}\overline{L}_{+} & ::= & A ∨ B | ⊥ | ∃x. A \\ \overline{R} & ::= & P | A ⊃ B | A ∧ B | ⊤ | ∀x. A | ¬A \end{aligned}

[ Fill in appropriate soundness and completeness theorems here. The same remarks as in the previous sections apply. ]

5.9 Exercises

Exercise 5.1 Show the forward sequent calculus on signed propositions and prove that if Γ ⟶ A then Γ^{−} ⟶ A^{+}.

Exercise 5.2 In the exercise we explore add the connective A ≡ B as a primitive to inverse method.

1. Following Exercise 2.6, introduce appropriate left and right rules to the backward sequent calculus.

2. Transform the rules to be appropriate for the forward sequent calculus.

3. Extend the notion of positive and negative subformula.

4. Extend the technique of subformula naming and inference rule specialization.

5. Show inverse derivations for each of the following.

(a) Reflexivity: ⟶ A ≡ A.

(b) Symmetry: A ≡ B ⟶ B ≡ A.

(c) Transitivity: A ≡ B, B ≡ C ⟶ A ≡ C.

6. Compare your technique with thinking of A ≡ B as a syntactic abbreviation for (A ⊃ B) ∧ (B ⊃ A). Do you see significant advantages or disadvantages of your method?

98  The Inverse Method

Resolution

Generalizing the basic ideas of the inverse method as introduced in the preceding chapter requires unification (see Section 4.3), although it is employed in a different way than in backward search. The underlying method can be traced directly to Robinson’s original work on resolution [Rob65], and precise connections to classical resolution have been established in the literature [Tam97].

Following the blue-print of the propositional inverse method, this chapter develops resolution for first-order intuitionistic logic.

6.1 Forward Sequent Calculus

The extension of the forward sequent calculus to the first-order case is straightforward.

\begin{aligned}Γ, [t/x]A ⟶ γ \\ & ∀L \\ Γ, ∀x. A ⟶ γ \end{aligned}  \begin{aligned}Γ ⟶ [a/x]A \\ & ∀R^{a} \\ Γ ⟶ ∀x. A \end{aligned}

\begin{aligned}Γ, [a/x]A ⟶ γ \\ & ∃L^{a} \\ Γ, ∃x. A ⟶ γ \end{aligned}  \begin{aligned}Γ ⟶ [t/x]A \\ & ∃R \\ Γ ⟶ ∃x. A \end{aligned}

Recall the restriction on the ∀R and ∃L rules: the derivation of premise must be parametric in a. That is, a may not occur in Γ or A. Soundness and completeness of this calculus with respect to the backward sequent calculus extends in a straightforward way.

These rules suggest an extension of the subformula property. We write A < B for A is an immediate subformula of B, ^{±} for an arbitrary sign (^{+} or ^{−}) and ∓ for its complement.

A^{±} < (A ∧ B)^{±}  B^{±} < (A ∧ B)^{±}
A^{±} < (A ∨ B)^{±}  B^{±} < (A ∨ B)^{±}
A^{∓} < (A ⊃ B)^{±}  B^{±} < (A ⊃ B)^{±}
[a/x]A^{+} < (∀x. A)^{+} for all parameters a
[t/x]A^{−} < (∀x. A)^{−} for all terms t
[t/x]A^{+} < (∃x. A)^{+} for all terms t
[a/x]A^{−} < (∃x. A)^{−} for all parameters a

We write A <^{∗} B for the reflexive and transitive closure of the immediate subformula relation. Also, we write A <^{∗} Γ if there is a formula B in Γ such that A <^{∗} B, and Δ <^{∗} Γ if for every A in Δ, A <^{∗} Γ.

The signed subformula property (Theorem 5.5) directly extends to the firstorder case, using the definitions above:

For all sequents Δ^{−} ⟶ A^{+} or Δ^{−} ⟶ · in a derivation of Γ^{−} ⟶ C^{+} or Γ^{−} ⟶ · we have Δ^{−}, A^{+} <^{∗} Γ^{−}, C^{+}.

Before formalizing resolution, we now go through several examples which show how to take advantage of this extended subformula property in order to construct a search algorithm.

The first example is

(∀x. P (x) ⊃ P (g(x))) ⟶ P (c) ⊃ P (g(g(c)))

for a unary predicate P, function f and constant c. We begin by enumerating and naming subformulas. First, the atomic subformulas, from left to right.

(i) P (\underline{t})^{+}  for all terms \underline{t}
(ii) P (g(\underline{s}))^{−}  for all terms \underline{s}
(iii) P (c)^{−}
(iv) P (g(g(c)))^{+}

Now, we have to consider all initial sequents Q ⟶ Q where Q is a subformula of the goal sequent above. To this end we unify positive and negative atomic propositions, treating \underline{t} and \underline{s} as variables, since they stand for arbitrary terms. We obtain:

1. P (g(\underline{s}))^{−} ⟶ P (g(\underline{s}))^{+}  for all term \underline{s}, from (ii) and (i)
2. P (g(g(c)))^{−} ⟶ P (g(g(c)))^{+} from (ii) and (iv)
3. P (c)^{−} ⟶ P (c)^{+}  from (iii) and (i)

Note that the sequent (1) above represents a schematic judgment in the same way that inferences rules are schematic, where \underline{s} is a schematic variable ranging over arbitrary terms. This will be true not only of the initial sequents, but of the sequents we derive. This is one of the major generalizations from the propositional case of the inverse method to resolution.

We can see that the initial sequents described in line (1) includes those in line (2), since we can use g(c) for \underline{s}. This is an extended form of subsumption: not only do we check is one sequent can be weakened to another, but we also have to allow for instantiation of variables (\underline{s}, in this case).

Next, we introduce names for compound subformulas.

L_{1}(\underline{t})^{−} = P (\underline{t})^{+} ⊃ P (g(\underline{t}))^{−}  for terms \underline{t}
L_{2}^{−}  = ∀x. L_{1}(x)^{−}
L_{3}^{+}  = P (c)^{−} ⊃ P (g(g(c)))^{+}

From the general forward sequent rules, we can now construct versions of the inference rules specialized to subformulas of the goal sequent.

Γ_{1} ⟶ P (\underline{t})^{+} Γ_{2}, P (g(\underline{t}))^{−} ⟶ γ
⊃L
Γ_{1} ∪ Γ_{2}, L_{1}(\underline{t})^{−} ⟶ γ
Γ, L_{1}(t)^{−} ⟶ γ
∀L
Γ, L_{2}^{−} ⟶ γ
Γ, P (c)^{−} ⟶ P (g(g(c)))^{+}
⊃R_{1}
Γ ⟶ L_{3}^{+}

\begin{aligned}Γ ⟶ P (g(g(c)))^{+} \\ & ⊃R_{2} \\ Γ ⟶ L_{3}^{+} \end{aligned}  \begin{aligned}Γ, P (c)^{−} ⟶ · \\ & ⊃R_{3} \\ Γ ⟶ L_{3}^{+} \end{aligned}

The notation distinguishes the cases where an arbitrary term t is involved in the rule because of the principal connective (in the ∀L rule) and where an arbitrary term \underline{t} is involved because of subformula considerations (in the ⊃L rule).

We can now use these rules, starting from the remaining two initial sequents to derive the goal sequent L_{2}^{−} ⟶ L_{3}^{+}. We omit some, but not all sequents that could be generated, but do not contribute to the final derivation.

1. P (g(\underline{s}))^{−} ⟶ P (g(\underline{s}))^{+}  init, for all terms \underline{s}
3. P (c)^{−} ⟶ P (c)^{+}  init
4. P (c)^{−}, L_{1}(c)^{−} ⟶ P (g(c))^{+}  ⊃L 3 1[c/\underline{s}]
5. P (g(\underline{t}))^{−}, L_{1}(g(\underline{t}))^{−} ⟶ P (g(g(\underline{t})))^{−} ⊃L 1[\underline{t}/\underline{s}] 1[g(\underline{t})/\underline{s}], for all \underline{t}
6. P (g(g(c)))^{−} ⟶ L_{3}^{+}  ⊃R_{2} 1[g(c)/\underline{s}]
7. P (g(\underline{t}))^{−}, L_{2}^{−} ⟶ P (g(g(\underline{t})))^{+}  ∀L 5, for all \underline{t}
8. P (c)^{−}, L_{2}^{−}, L_{1}(c)^{−} ⟶ P (g(g(c)))^{+} ⊃L 3 7[c/\underline{t}]
9. P (c)^{−}, L_{2}^{−} ⟶ P (g(g(c)))^{+}  ∀L 8, with contraction
10. L_{2}^{−} ⟶ L_{3}^{+}  ⊃R_{1} 9

Inference previously involved matching a sequents against the premises of an inference rule. As this example shows, we now have to unify derived sequents with the premises of the inference rules. The schematic variables in the sequent as well as in the inference rule may be instantiated in this process, thereby determining the most general conclusion. It is important in this process to note that the scope of each schematic variable includes only a particular sequent or inference rule. Schematic variables called \underline{t} in different sequents are different— usually this is accounted for by systematically renaming variables before starting unification.

The example above does not involve any parameters, only schematic variables. We now consider another example involving parameters,

∃y. ∀x. P (x, y) ⟶ ∀x. ∃y. P (x, y)

for a binary predicate P. Clearly, this judgment should be derivable. Again, we first generate positive and negative atomic subformulas.

(i) P (\underline{t}, \underline{a})^{−} for all terms \underline{t} and parameters \underline{a}
(ii) P (\underline{b}, \underline{s})^{+} for all parameters \underline{b} and terms \underline{s}

Because of the negative existential and positive universal quantification the allowed instances of the atomic subformulas are restricted to parameters in certain places. However, it should be understood that \underline{a} in line (i) is only a schematic variable ranging over parameters and may be instantiated to different parameters for different uses of a negative formula P ( , )^{−}.

Next we generate all possible atomic initial sequents. This means we have to look for common instances of the positive and negative atomic formulas schemas listed above. The only possible instances have the form

1. P (\underline{b}, \underline{a})^{−} ⟶ P (\underline{b}, \underline{a})^{+} for all parameters \underline{b} and terms \underline{s}

Now we list the possible compound subformulas.

L_{1}(\underline{a})^{−} = ∀x. P (x, \underline{a})^{−} for parameters \underline{a}
L_{2}^{−}  = ∃y. L_{1}(y)^{−}
L_{3}(\underline{b})^{+} = ∃y. P (\underline{b}, y)^{+} for parameters \underline{b}
L_{4}^{+}  = ∀x. L_{3}(x)^{+}

The specialized inference rules read:

\begin{aligned}Γ, P (t, \underline{a})^{−} ⟶ γ \\ & ∀L \\ Γ, L_{1}(\underline{a})^{−} ⟶ γ \end{aligned}  \begin{aligned}Γ, L_{1}(a)^{−} ⟶ γ \\ & ∃L^{a} \\ Γ, L_{2}^{−} ⟶ γ \end{aligned}

\begin{aligned}Γ ⟶ P (\underline{b}, s)^{+} \\ & ∃R \\ Γ ⟶ L_{3}(\underline{b})^{+} \end{aligned}  \begin{aligned}Γ ⟶ L_{3}(b)^{+} \\ & ∀R^{b} \\ Γ ⟶ L_{4}^{+} \end{aligned}

Note that the ∃L and ∀R rules have parametric premises, which means we have to enforce the side condition that parameter a or b do not occur elsewhere in the premises of these two rules, respectively. The derivation takes the following simple form. We omit signs for brevity, and it should be understood that \underline{b} and \underline{a} are quantified locally in each sequent.

1. P (\underline{b}, \underline{a}) ⟶ P (\underline{b}, \underline{a}) init
2. L_{1}(\underline{a}) ⟶ P (\underline{b}, \underline{a}) ∀L 1
3. P (\underline{b}, \underline{a}) ⟶ L_{3}(\underline{b}) ∃R 1
4. L_{1}(\underline{a}) ⟶ L_{3}(\underline{b})  ∃R 2
5. L_{1}(\underline{a}) ⟶ L_{3}(\underline{b})  ∀L 3 (subsumed by 4)
6. L_{2} ⟶ L_{3}(\underline{b})  ∃L^{a} 4
7. L_{1}(\underline{a}) ⟶ L_{4}  ∀R^{b} 4
8. L_{2} ⟶ L_{4}  ∀R^{b} 6 or ∃L^{a} 7

Note that the ∃L and ∀R rule are not applicable to sequents (2) or (3), because the side conditions on the parameters would be violated.

Next we consider the converse, which should not be derivable.

∀x. ∃y. P (x, y) ⟶ ∃y. ∀x. P (x, y)

Again, we first generate the atomic subformulas.

(i) P (\underline{t}, \underline{a})^{−} for all terms \underline{t} and parameters \underline{a}
(ii) P (\underline{b}, \underline{s})^{+} for all parameters \underline{b} and terms \underline{s}

Then the possible initial sequents.

1. P (\underline{b}, \underline{a})^{−} ⟶ P (\underline{b}, \underline{a})^{+} for all parameters \underline{b} and terms \underline{a}

Then, the compound subformulas.

L_{1}(\underline{t})^{−} = ∃y. P (\underline{t}, y)^{−} for terms \underline{t}
L_{2}^{−}  = ∀x. L_{1}(x)^{−}
L_{3}(\underline{s})^{+} = ∀x. P (x, \underline{s})^{+} for terms \underline{s}
L_{4}^{+}  = ∃y. L_{3}(y)^{+}

From this we derive the specialized rules of inference.

\begin{aligned}Γ, P (\underline{t}, a)^{−} ⟶ γ \\ & ∃L^{a} \\ Γ, L_{1}(\underline{t})^{−} ⟶ γ \end{aligned}  \begin{aligned}Γ, L_{1}(t)^{−} ⟶ γ \\ & ∀L \\ Γ, L_{2}^{−} ⟶ γ \end{aligned}

\begin{aligned}Γ ⟶ P (b, \underline{s})^{+} \\ & ∀R \\ Γ ⟶ L_{3}(\underline{s})^{+} \end{aligned}  \begin{aligned}Γ ⟶ L_{3}(s)^{+} \\ & ∃R \\ Γ ⟶ L_{4}^{+} \end{aligned}

Given an initial sequent

1. P (\underline{b}, \underline{a})^{−} ⟶ P (\underline{b}, \underline{a})^{+} for all parameters \underline{b} and terms \underline{a}

we see that no inference rules are applicable, because the side condition on parameter occurrences would be violated. Therefore the goal sequent cannot be derivable.

6.2 Factoring

The examples in the previous section suggest the following algorithm:

1. Determine all signed schematic atomic subformulas of the given goal sequent.

2. Unify positive and negative atomic subformulas after renaming variables so they have none in common. This yields a set of initial sequents from which subsumed copies should be eliminated.

3. Name all signed compound subformulas as new predicates on their free variables.

4. Specialize the inference rules to these subformulas.

5. Starting from the initial sequents, apply the specialized inference rules in a fair way by unifying (freshly renamed) copies of sequents derived so far with premises of the inference rules, generating most general conclusions as a new schematic sequents.

6. Stop with success when the goal sequent has been derived.

Perhaps somewhat surprisingly, this method is incomplete using only the rules given so far. As a counterexample, consider

· ⟶ ∃x. P (x) ⊃ P (x) ∧ P (c)

for a unary predicate P and constant c. Initial sequents:

1. P (\underline{t}) ⟶ P (\underline{t}) for all terms t
2. P (c) ⟶ P (c) (subsumed by (1))

Signed subformulas:

\begin{aligned}L_{1}^{+}(\underline{s}) & = & P (\underline{s})^{+} ∧ P (c)^{+} \\ L_{2}^{+}(\underline{s}) & = & P (\underline{s})^{−} ⊃ L_{1}(\underline{s})^{+} \\ L_{3}^{+} & = & ∃x. L_{2}^{+}(x) \end{aligned}

Specialized rules (omitting polarities and the irrelevant ⊃R_{3}):

Γ_{1} ⟶ P (\underline{s}) Γ_{2} ⟶ P (c)

∧I Γ_{1} ∪ Γ_{2} ⟶ L_{1}

\begin{aligned}Γ, P (\underline{s}) ⟶ L_{1}(\underline{s}) \\ & ⊃R_{1} \\ Γ ⟶ L_{2}(\underline{s}) \end{aligned}  \begin{aligned}Γ ⟶ L_{1}(\underline{s}) \\ & ⊃R_{2} \\ Γ ⟶ L_{2}(\underline{s}) \end{aligned}

\begin{aligned}Γ ⟶ L_{2}(t) \\ & ∃R \\ Γ ⟶ L_{3} \end{aligned}

Draft of November 12, 1999

Initially, we can only apply ∧I, after renaming a copy of (1).

1. P (\underline{t}) ⟶ P (\underline{t})  init, for all terms \underline{t}
3. P (\underline{t}), P (c) ⟶ L_{1}(\underline{t}) ∧R 1[\underline{t}/\underline{t}] 1[c/\underline{t}], for all terms \underline{t}

Now there are two ways to apply the ⊃R_{1} rule, but either P (\underline{t}) or P (c) is left behind as an assumption, and the goal sequent cannot be derived.

The problem is that even though the sequent

P (c) ⟶ L_{1}(c)

should be derivable, it is only the contraction of an instance of sequent (3). We therefore extend the system with an explicit rule which permits contraction after instantiation, called factoring. That is, after we derive a new sequent, we consider possible most general unifiers among antecedents of the sequent and add the results (while continuing to check for subsumption).

In the example above, we proceed as follows:

1. P (\underline{t}) ⟶ P (\underline{t})  init, for all terms \underline{t}
3. P (\underline{t}), P (c) ⟶ L_{1}(\underline{t}) ∧R 1[\underline{t}/\underline{t}] 1[c/\underline{t}], for all terms \underline{t}
4. P (c) ⟶ L_{1}(c)  factor 3[c/\underline{t}]
5. · ⟶ L_{2}(c)  ⊃R_{1} 4
6. · ⟶ L_{3}  ∃R

Usually, this is done eagerly for each rule which unions assumptions and therefore might allow new factors to be derived. It is also possible to delay this until the rules which require factoring (such as ⊃R), but this might require factoring to be done repeatedly and may prohibit some subsumption.

In our inference rule notation, where unification of sequents with premises of rules is implicit, this factoring rule would simply look like a contraction.

Γ, A, A ⟶ C ; contract ; Γ, A ⟶ C

Previously, this was implicit, since we maintained assumptions as sets.

Draft of November 12, 1999

106  Resolution

Equality

Reasoning with equality in first order logic can be accomplished axiomatically. That is, we can simply add reflexivity, symmetry, transitivity, and congruence rules for each predicate and function symbol and use the standard theorem proving technology developed in the previous chapters. This approach, however, does not take strong advantage of inherent properties of equality and leads to a very large and inefficent search space.

While there has been a deep investigation of equality reasoning in classical logic, much less is known for intuitionistic logic. Some recent references are [Vor96, DV99].

In this chapter we develop some of the techniques of equational reasoning, starting again from first principles in the definition of logic. We therefore recapitulate some of the material in earlier chapters, now adding equality as a new primitive predicate symbol.

7.1 Natural Deduction

We characterize equality by its introduction rule, which simply states that s ≐ s for any term s.

\frac{≐ I}{⊢ s ≐ s}

We have already seen this introduction rule in unification logic in Section 4.3. In the context of unification logic, however, we did not consider hypothetical judgments, so we did not need or specify elimination rules for equality.

If we know s ≐ t we can replace any number of occurrences of s in a true proposition and obtain another true proposition.

⊢ s ≐ t ⊢ [s/x]A

≐ E_{1}
⊢ [t/x]A

Symmetrically, we can also replace occurrences of t by s.

⊢ s ≐ t ⊢ [t/x]A
≐ E_{2}
⊢ [s/x]A

It might seem that this second rule is redundant, and in some sense it is. In particular, it is a derivable rule of the calculus with only ≐ E_{1}:

\begin{matrix}⊢ s ≐ t \frac{≐ I}{⊢ s ≐ s} \\ ≐ E_{1} \\ ⊢ t ≐ s \end{matrix} ⊢ [t/x]A

≐ E_{1}
⊢ [s/x]A

However, this deduction is not normal (as defined below), and without the second elimination rule the normalization theorem would not hold and cut elimination in the sequent calculus would fail. We continue this discussion below, after introducing normal derivations.

Next, we check the local soundness and completeness of the rules. First, local soundness:

\begin{aligned}\frac{≐ I}{⊢ s ≐ s} & \begin{matrix}D \\ ⊢ [s/x]A \end{matrix} \\ & ≐ E_{1} \\ ⊢ [s/x]A \end{aligned} ⟹_{R} \begin{matrix}D \\ ⊢ [s/x]A \end{matrix}

and the reduction for ≐ E_{2} is identical.

Second, we have to verify local completeness. There are two symmetric expansions

\begin{matrix}D \\ ⊢ s ≐ t \end{matrix}  ⟹_{E}  \begin{aligned}\begin{matrix}D \\ ⊢ s ≐ t \end{matrix} & & \frac{≐ I}{⊢ s ≐ s} \\ & & ≐ E_{1} \\ & ⊢ s ≐ t \end{aligned}

and

\begin{matrix}D \\ ⊢ s ≐ t \end{matrix}  ⟹_{E}  \begin{aligned}\begin{matrix}D \\ ⊢ s ≐ t \end{matrix} & & \frac{≐ I}{⊢ t ≐ t} \\ & & ≐ E_{2} \\ & ⊢ s ≐ t \end{aligned}

witnessing local completeness.

Note that the second is redundant in the sense that for local completeness we only need to show that there is some way to apply elimination rules so that we can reconstitute the connective by introduction rules. This is an interesting example where local completeness (in the absence of the ≐ E_{2} rule) does not imply global completeness.

Next we define normal and extraction derivations. These properties are given by the inherent role of introduction and elimination rules.

\frac{≐ I}{⊢ s ≐ s ⇑} ; \begin{aligned}⊢ s ≐ t ↓  ⊢ [s/x]A ⇑ \\ & ≐ E_{1} \\ ⊢ [t/x]A ⇑ \end{aligned}  \begin{aligned}⊢ s ≐ t ↓  ⊢ [t/x]A ⇑ \\ & ≐ E_{2} \\ ⊢ [s/x]A ⇑ \end{aligned}

The elimination rule is similar to the rules for disjunction in the sense that there is a side derivation whose conclusion is copied from the premise to the conclusion of the elimination rule. In the case of disjunction, the copy is identical; here, some copies of s are replaced by t or vice versa.

Now we can see, why the derivation of ≐ E_{2} is not normal:

\begin{matrix}⊢ s ≐ t ↓ \frac{≐ I}{⊢ s ≐ s ⇑} \\ ≐ E_{1} \\ ⊢ t ≐ s? \end{matrix} ⊢ [t/x]A ⇑

≐ E_{1}
⊢ [s/x]A ⇑

The judgment marked with ? should be t ≐ s ⇑ considering it is the conclusion of an equality elimination inference, and it should be t ≐ s ↓ considering it is the left premise of an equality elimination. Since no coercion from ⇑ to ↓ is available for normal derivations the deduction above cannot be annotated.

We assign proof terms only in their compact form (see Section 3.2). This means we have to analyse how much information is needed in the proof term to allow bi-directional type checking. Recall that we have introduction terms I and elimination terms E and that introduction terms are checked against a given type, while elimination term must carry enough information so that their type is unique. Following these considerations leads to the following new terms.

Intro Terms I ::= … | refl  for ≐ I
Elim Terms E ::= … | subst_{1}^{λx.A} E I for ≐ E_{1}
| subst_{2}^{λx.A} E I  for ≐ E_{2}

The typing rules are straightforward. Recall that we localize the hypothesize to make the rules more explicit.

\frac{≐ I}{Γ^{↓} ⊢ refl : s ≐ s ⇑}

Γ^{↓} ⊢ E : s ≐ t ↓ Γ^{↓} ⊢ I : [s/x]A ⇑

≐ E_{1}

Γ^{↓} ⊢ subst_{1}^{λx.A} E I : [t/x]A ⇑

Γ^{↓} ⊢ E : s ≐ t ↓ Γ^{↓} ⊢ I : [t/x]A ⇑

≐ E_{2}

Γ^{↓} ⊢ subst_{2}^{λx.A} E I : [s/x]A ⇑ We record the proposition A and an indication of the bound variable x in order to provide enough information for bi-direction type checking. Recall the desired property (Theorem 3.4):

1. Given Γ^{↓}, I, and A. Then either Γ^{↓} ⊢ I : A ⇑ or not.

2. Given Γ^{↓} and E. Then either there is a unique A such that Γ^{↓} ⊢ E : A ↓ or there is no such A.

First, it is clear that the constant refl for equality introduction does not need to carry any terms, since s ≐ s is given.

Second, to check subst_{1}^{λx.A} E I against A′ we first synthesize the type of E obtaining s ≐ t and thereby s and t. Knowing t and A′ does not determine A (consider, for example, [t/x]A = q(t, t) which allows A = q(x, x), A = q(x, t), A = q(t, x) and A = q(t, t)). However, A is recorded explicitly in the proof term, together with the variable x. Therefore we can now check whether the given type [t/x]A is equal to A′. If that succeeds we have to check the introduction term I against [s/x]A to verify the correctness of the whole term.

7.2 Sequent Calculus

The rules for the sequent calculus are determined by the definition of normal deduction as in Chapter 3. Introduction rules are turned into right rules; elimination rules into left rules.

\frac{≐ R}{Γ ⟹ s ≐ s}

\begin{aligned}Γ, s ≐ t ⟹ [s/x]A \\ & ≐ L_{1} \\ Γ, s ≐ t ⟹ [t/x]A \end{aligned}  \begin{aligned}Γ, s ≐ t ⟹ [t/x]A \\ & ≐ L_{2} \\ Γ, s ≐ t ⟹ [s/x]A \end{aligned}

The proof for admissibility of cut in this calculus runs into difficulties when the cut formula was changed in the application of the ≐ L_{1} or ≐ L_{2} rules. Consider, for example, the cut between

D = \begin{matrix}D_{1} \\ Γ, s ≐ t ⟹ [s/x]A \end{matrix} ; ≐ L_{1} ; Γ, s ≐ t ⟹ [t/x]A  and  \begin{matrix}E \\ Γ, s ≐ t, [t/x]A ⟹ C \end{matrix}

If [t/x]A is the principal formula of the last inference in E, we would normally apply the induction hypothesis to D_{1} and E, in effect pushing the cut past the last inference in D. We cannot do this here, since [s/x]A and [t/x]A do not match. None of the rules in the sequent calculus without equality changed the conclusion in a left rule, so this situation did not arise before.

The simplest remedy seems to be to restrict the equality rules so they must be applied last in the bottom-up construction of a proof, and only to atomic formulas or other equalities. In this way, they cannot interfere with other inferences— they have been pushed up to the leaves of the derivation. This restriction is interesting for other purposes as well, since it allows us to separate equality reasoning from logical reasoning during the proof search process.

We introduce one new syntactice category and two new judgments. E stands for a basic proposition, which is either an atomic proposition P or an equation s ≐ t.

Γ ⟹^{E} E E has an equational derivation from Γ
Γ ⟹^{−} A A has a regular derivation from Γ

Equational derivations are defined as follows.

\frac{init}{Γ, P ⟹^{E} P}  \frac{≐ R}{Γ ⟹^{E} s ≐ s}

\begin{aligned}Γ, s ≐ t ⟹^{E} [s/x]E \\ & ≐ L_{1} \\ Γ, s ≐ t ⟹^{E} [t/x]E \end{aligned}  \begin{aligned}Γ, s ≐ t ⟹^{E} [s/x]E \\ & ≐ L_{1} \\ Γ, s ≐ t ⟹^{E} [t/x]E \end{aligned}

Regular derivations have all the inference rules of sequent derivations without equality (except for initial sequents) plus the following coercion.

\begin{aligned}Γ ⟹^{E} E \\ & eq \\ Γ ⟹^{−} E \end{aligned}

Regular derivations are sound and complete with respect to the unrestricted calculus. Soundness is direct.

Theorem 7.1 (Soudness of Regular Derivations)

1. If Γ ⟹^{E} E then Γ ⟹ E

2. If Γ ⟹^{−} A then Γ ⟹ A

Proof: By straightforward induction over the given derivations. □

In order to prove completeness we need a lemma which states that the unrestricted left equality rules are admissible in the restricted calculus. Because new assumptions are made, the statment of the lemma must actually be slightly more general by allowing substitution into hypotheses.

Lemma 7.2 (Admissibility of Generalized Equality Rules)

1. If [s/x]Γ, s ≐ t ⟹^{−} [s/x]A then [t/x]Γ, s ≐ t ⟹^{−} [t/x]A.

2. If [t/x]Γ, s ≐ t ⟹^{−} [t/x]A then [s/x]Γ, s ≐ t ⟹^{−} [s/x]A.

3. If [s/x]Γ, s ≐ t ⟹^{E} [s/x]A then [t/x]Γ, s ≐ t ⟹^{E} [t/x]A.

4. If [s/x]Γ, s ≐ t ⟹^{E} [s/x]A then [t/x]Γ, s ≐ t ⟹^{E} [t/x]A.

Proof: By induction on the structure of the given derivations S or E, where the second and fourth parts are completely symmetric to the first and third part. In most cases this follows directly from the induction hypothesis. We show a few characteristic cases. Case:

S = \begin{matrix}S_{1} \\ [s/x]Γ, s ≐ t, [s/x]A_{1} ⟹^{−} [s/x]A_{2} \end{matrix} ; ⊃R ; [s/x]Γ, s ≐ t ⟹^{−} [s/x]A_{1} ⊃ [s/x]A_{2}

[t/x]Γ, s ≐ t, [t/x]A_{1} ⟹^{−} [t/x]A_{2}  By i.h. on S_{1}
[t/x]Γ, s ≐ t ⟹^{−} [t/x]A_{1} ⊃ [t/x]A_{2}  By rule ⊃R

Case:

S = \begin{matrix}E \\ [s/x]Γ, s ≐ t ⟹^{E} [s/x]E \end{matrix} ; eq ; [s/x]Γ, s ≐ t ⟹^{−} [s/x]E

[t/x]Γ, s ≐ t ⟹^{E} [t/x]E  By i.h. (3) on E
[t/x]Γ, s ≐ t ⟹^{−} [t/x]E  By rule eq

Case:

E = \frac{init}{[s/x]Γ′, [s/x]P_{1}, s ≐ t ⟹^{E} [s/x]P_{2}}

We obtain the first equation below from the assumption that E is an initial sequent.

[s/x]P_{1} = [s/x]P_{2}  Given
[t/x]Γ′, [t/x]P_{1}, s ≐ t ⟹^{E} [t/x]P_{1}  By rule init
[t/x]Γ′, [t/x]P_{1}, s ≐ t ⟹^{E} [s/x]P_{1}  By rule ≐ L_{2}
[t/x]Γ′, [t/x]P_{1}, s ≐ t ⟹^{E} [s/x]P_{2}  Same, by given equality
[t/x]Γ′, [t/x]P_{1}, s ≐ t ⟹^{E} [t/x]P_{2}  By rule ≐ L_{1}

Case:

E = \begin{matrix}E′ \\ [s/x]Γ′, [s/x]q ≐ [s/x]r, s ≐ t ⟹^{E} [[s/x]q/y]E′ \end{matrix} ; ≐ L_{1} ; [s/x]Γ′, [s/x]q ≐ [s/x]r, s ≐ t ⟹^{E} [s/x]E

Note that we wrote the premise so that E′ does contain an occurrence of x. We obtain the first equation below from the form of the inference rule ≐ L_{1}.

[s/x]E = [[s/x]r/y]E′  Given
[s/x]Γ′, [s/x]q ≐ [s/x]r, s ≐ t ⟹^{E} [s/x][q/y]E′ Same as E′ (x not in E′)
[t/x]Γ′, [t/x]q ≐ [t/x]r, s ≐ t ⟹^{E} [t/x][q/y]E′  By i.h. on E′
[t/x]Γ′, [t/x]q ≐ [t/x]r, s ≐ t ⟹^{E} [[t/x]q/y]E′  Same, since x not in E′
[t/x]Γ′, [t/x]q ≐ [t/x]r, s ≐ t ⟹^{E} [[t/x]r/y]E′  By rule ≐ L_{1}
[t/x]Γ′, [t/x]q ≐ [t/x]r, s ≐ t ⟹^{E} [t/x][r/y]E′  Same, since x not in E′
[t/x]Γ′, [t/x]q ≐ [t/x]r, s ≐ t ⟹^{E} [s/x][r/y]E′  By rule ≐ L_{2}
[t/x]Γ′, [t/x]q ≐ [t/x]r, s ≐ t ⟹^{E} [[s/x]r/y]E′  Same, since x not in E′
[t/x]Γ′, [t/x]q ≐ [t/x]r, s ≐ t ⟹^{E} [s/x]E  Same, by given equality
[t/x]Γ′, [t/x]q ≐ [t/x]r, s ≐ t ⟹^{E} [t/x]E  By rule ≐ L_{1}

Case:

E = \begin{matrix}E′ \\ [s/x]Γ, s ≐ t ⟹^{E} [s/x]E′ \end{matrix} ; ≐ L_{1} ; [s/x]Γ, s ≐ t ⟹^{E} [s/x]E

Note that we wrote the premise so that E′ does contain an occurrence of x. We obtain the first line below from the shape of the conclusion in the inference rule ≐ L_{1} with the principal formula s ≐ t.

[s/x]E = [t/x]E′  Given
[t/x]Γ, s ≐ t ⟹^{E} [t/x]E′  By i.h. on E′
[t/x]Γ, s ≐ t ⟹^{E} [s/x]E  Same, by given equality
[t/x]Γ, s ≐ t ⟹^{E} [t/x]E  By rule ≐ L_{1}
□

A second lemma is helpful to streamline the completeness proof.

Lemma 7.3 (Atomic Initial Sequents) Γ, A ⟹^{−} A.

Proof: By induction on the structure of A. This is related to repeated local expansion. We show a few of cases.

Case: A = P.

Γ, P ⟹^{E} P  By rule init
Γ, P ⟹^{−} P  By rule eq

Case: A = (s ≐ t).

Γ, s ≐ t ⟹^{E} s ≐ s  By rule ≐ R
Γ, s ≐ t ⟹^{E} s ≐ t  By rule ≐ L_{1}

114  Equality

Case: A = A_{1} ∧ A_{2}.

Γ, A_{1} ⟹^{−} A_{1}  By i.h. on A_{1}
Γ, A_{1} ∧ A_{2} ⟹^{−} A_{1}  By rule ∧L_{1}
Γ, A_{2} ⟹^{−} A_{2}  By i.h. on A_{2}
Γ, A_{1} ∧ A_{2} ⟹^{−} A_{2}  By rule ∧L_{2}
Γ, A_{1} ∧ A_{2} ⟹^{−} A_{1} ∧ A_{2}  By rule ∧R
□

With these two lemmas, completeness is relatively simple. Theorem 7.4 (Completeness of Regular Derivations) If Γ ⟹ A then Γ ⟹^{−} A. Proof: By induction on the structure of the given derivation S. We show some cases; most are straightforward. Case:

S = \begin{matrix}S_{2} \\ Γ, A_{1} ⟹ A_{2} \end{matrix} ; ⊃R ; Γ ⟹ A_{1} ⊃ A_{2}

Γ, A_{1} ⟹^{−} A_{2}  By i.h. on S_{2}
Γ ⟹^{−} A_{1} ⊃ A_{2}  By rule ⊃R

Case:

S = \frac{init}{Γ′, A ⟹ A}

Γ′, A ⟹^{−} A  By Lemma 7.3

Case:

S = \begin{matrix}S_{1} \\ Γ′, s ≐ t ⟹ [s/x]A \end{matrix} ; ≐ L_{1} ; Γ′, s ≐ t ⟹ [t/x]A

Γ′, s ≐ t ⟹^{−} [s/x]A  By i.h. on S_{1}
Γ′, s ≐ t ⟹^{−} [t/x]A  By Lemma 7.2
□

Draft of November 12, 1999

Regular derivations are the basis for proof search procedures. Furthermore, we can prove admissibility of cut, essentially following the same argument as in the system without equality for regular derivations. On equality derivations, we have to employ a new argument.

Theorem 7.5 (Admissibility of Cut with Equality)

1. If Γ ⟹^{E} E and Γ, E ⟹^{E} F then Γ ⟹^{E} F.

2. If Γ ⟹^{E} E and Γ, E ⟹^{−} C then Γ ⟹^{−} C.

3. If Γ ⟹^{−} A and Γ, A ⟹^{E} F then Γ ⟹^{−} F.

4. If Γ ⟹^{−} A and Γ, A ⟹^{−} C then Γ ⟹^{−} C.

Proof: We prove the properties in sequence, using earlier ones to in the proofs of later ones.

Part (1): Given

\begin{matrix}E \\ Γ ⟹^{E} E \end{matrix}  and  \begin{matrix}F \\ Γ, E ⟹^{E} F \end{matrix}

we construct a derivation for Γ ⟹^{E} F by nested induction on the structure of E and F. That is, in appeals to the induction hypothesis, E may be smaller (in which case F may be arbitrary), or E stays the same and F gets smaller.

Cases: If E is a side formula of the last inference in F we appeal to the induction hypothesis on the premise and reapply the inference on the result. If F is an initial sequent we can directly construct the desired derivation. In the remaining cases, we assume E is the principal formula of the last inference in F.

Case:

E = \frac{≐ R}{Γ ⟹^{E} s ≐ s}  and  F = \begin{matrix}F_{1} \\ Γ, s ≐ s ⟹^{E} [s/x]F_{1} \end{matrix} ; ≐ L_{1} ; Γ, s ≐ s ⟹^{E} [s/x]F_{1}
Γ ⟹ [s/x]F_{1}  By i.h. on E and F_{1}

Case:

E = \begin{matrix}E_{1} \\ Γ′, q ≐ r ⟹^{E} [q/x]s′ = [q/x]t′ \end{matrix} ; ≐ L_{1} ; Γ′, q ≐ r ⟹^{E} [r/x]s′ ≐ [r/x]t′

Γ′, q ≐ r, [r/x]s′ ≐ [r/x]t′ ⟹^{E} F  F, in this case
Γ′, q ≐ r, [q/x]s′ ≐ [q/x]t′ ⟹^{E} F  By Lemma 7.2
Γ′, q ≐ r ⟹^{E} F  By i.h. on E_{1} and above

Draft of November 12, 1999

Part (2): Given

\begin{matrix}E \\ Γ ⟹^{E} E \end{matrix}  and  \begin{matrix}S \\ Γ, E ⟹^{−} C \end{matrix}

we construct a derivation for Γ ⟹^{−} C by induction over the structure of S. Since E is either atomic or an equality, it cannot be the principal formula of an inference in S. When we reach a coercion from ⟹^{E} to ⟹^{−} in S we appeal to Part (1).

Part (3): Given

\begin{matrix}S \\ Γ ⟹^{−} A \end{matrix}  and  \begin{matrix}F \\ Γ, A ⟹^{E} F \end{matrix}

we construct a derivation for Γ ⟹^{E} F by nested induction on the structure of F and S. If A is the principal formula of an inference in F then A must be atomic or an equality. In the former case we can derive the desired conclusion directly; in the latter case we proceed by induction over S. Since A is an equality, it cannot be the principal formula of an inference in S. When we reach a coercion for ⟹^{E} to ⟹^{−} in S we appeal to Part (1).

Part (4): Given

\begin{matrix}S \\ Γ ⟹^{−} A \end{matrix}  and  \begin{matrix}T \\ Γ, A ⟹^{−} C \end{matrix}

we construct a derivation for Γ ⟹^{−} C by nested induction on the structure of A, and the derivations S and T as in the proof of admissibility of cut without equality (Theorem 3.11). When we reach coercions from equality derivations we appeal to Parts 3 or 2. □

Bibliography

[And92] Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):197–347, 1992.

[Byr99] John Byrnes. Proof Search and Normal Forms in Natural Deduction. PhD thesis, Department of Philosophy, Carnegie Mellon University, May 1999.

[Cur30] H.B. Curry. Grundlagen der kombinatorischen Logik. American Journal of Mathematics, 52:509–536, 789–834, 1930.

[DV99] Anatoli Degtyarev and Andrei Voronkov. Equality reasoning in sequent-based calculi. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science Publishers, 1999. In preparation.

[Gen35] Gerhard Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:176–210, 405–431, 1935. Translated under the title Investigations into Logical Deductions in [Sza69].

[Her30] Jacques Herbrand. Recherches sur la théorie de la démonstration. Travaux de la Société des Sciences et de Lettres de Varsovic, 33, 1930.

[Her95] Hugo Herbelin. Séquents qu’on calcule. PhD thesis, Universite Paris 7, January 1995.

[Hil22] David Hilbert. Neubegründung der Mathematik (erste Mitteilung). In Abhandlungen aus dem mathematischen Seminar der Hamburgischen Universität, pages 157–177, 1922. Reprinted in [Hil35].

[Hil35] David Hilbert. Gesammelte Abhandlungen, volume 3. Springer-Verlag, Berlin, 1935.

[How69] W. A. Howard. The formulae-as-types notion of construction. Unpublished manuscript, 1969. Reprinted in To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 1980.

[How98] Jacob M. Howe. Proof Search Issues in Some Non-Classical Logics. PhD thesis, University of St. Andrews, Scotland, 1998.

[Hua94] Xiarong Huang. Human Oriented Proof Presentation: A Reconstructive Approach. PhD thesis, Universität des Saarlandes, 1994.

[Hue76] Gérard Huet. Résolution d’équations dans des langages d’ordre 1, 2, …, ω. PhD thesis, Université Paris VII, September 1976.

[Kle52] Stephen Cole Kleene. Introduction to Metamathematics. North-Holland, 1952.

[Kni89] Kevin Knight. Unification: A multi-disciplinary survey. ACM Computing Surveys, 2(1):93–124, March 1989.

[LS86] Joachim Lambek and Philip J. Scott. Introduction to Higher Order Categorical Logic. Cambridge University Press, Cambridge, England, 1986.

[Mas64] S. Maslov. The inverse method of establishing deducibility in the classical predicate calculus. Soviet Mathematical Doklady, 5:1420–1424, 1964.

[Min94] G. Mints. Resolution strategies for the intuitionistic logic. In Constraint Programming, pages 289–311. NATO ASI Series F, Springer-Verlag, 1994.

[ML85a] Per Martin-Löf. On the meanings of the logical constants and the justifications of the logical laws. Technical Report 2, Scuola di Specializzazione in Logica Matematica, Dipartimento di Matematica, Università di Siena, 1985.

[ML85b] Per Martin-Löf. Truth of a proposition, evidence of a judgement, validity of a proof. Notes to a talk given at the workshop Theory of Meaning, Centro Fiorentino di Storia e Filosofia della Scienza, June 1985.

[ML94] Per Martin-Löf. Analytic and synthetic judgements in type theory. In Paolo Parrini, editor, Kant and Contemporary Epistemology, pages 87–99. Kluwer Academic Publishers, 1994.

[MM76] Alberto Martelli and Ugo Montanari. Unification in linear time and space: A structured presentation. Internal Report B76-16, Ist. di Elaborazione delle Informazione, Consiglio Nazionale delle Ricerche, Pisa, Italy, July 1976.

[MM82] Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258–282, April 1982.

[Par92] Michel Parigot. λμ-calculus: An algorithmic interpretation of classical natural deduction. In A. Voronkov, editor, Proceedings of the International Conference on Logic Programming and Automated Reasoning, pages 190–201, St. Petersburg, Russia, July 1992. Springer-Verlag LNCS 624.

[Pfe95] Frank Pfenning. Structural cut elimination. In D. Kozen, editor, Proceedings of the Tenth Annual Symposium on Logic in Computer Science, pages 156–166, San Diego, California, June 1995. IEEE Computer Society Press.

[Pra65] Dag Prawitz. Natural Deduction. Almquist & Wiksell, Stockholm, 1965.

[PW78] M. S. Paterson and M. N. Wegman. Linear unification. Journal of Computer and System Sciences, 16(2):158–167, April 1978.

[Rob65] J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–41, January 1965.

[Rob71] J. A. Robinson. Computational logic: The unification computation. Machine Intelligence, 6:63–72, 1971.

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

[Tam96] T. Tammet. A resolution theorem prover for intuitionistic logic. In M. McRobbie and J. Slaney, editors, Proceedings of the 13th International Conference on Automated Deduction (CADE-13), pages 2–16, New Brunswick, New Jersey, 1996. Springer-Verlag LNCS 1104.

[Tam97] T. Tammet. Resolution, inverse method and the sequent calculus. In A. Leitsch G. Gottlog and D. Mundici, editors, Proceedings of the 5th Kurt Gödel Colloquium on Computational Logic and Proof Theory (KGC’97), pages 65–83, Vienna, Austria, 1997. Springer-Verlag LNCS 1289.

[Vor92] Andrei Voronkov. Theorem proving in non-standard logics based on the inverse method. In D. Kapur, editor, Proceedings of the 11th International Conference on Automated Deduction, pages 648–662, Saratoga Springs, New York, 1992. Springer-Verlag LNCS 607.

[Vor96] Andrei Voronkov. Proof-search in intuitionistic logic with equality, or back to simultaneous rigid e-unification. In M.A. McRobbie and J.K. Slaney, editors, Proceedings of the 13th International Conference on Automated Deduction, pages 32–46, New Brunswick, New Jersey, July/August 1996. Springer-Verlag LNAI 1104.