The Foundation of a Generic Theorem Prover

Lawrence C Paulson Computer Laboratory University of Cambridge

Abstract

Isabelle [28, 30] is an interactive theorem prover that supports a variety of logics. It represents rules as propositions (not as functions) and builds proofs by combining rules. These operations constitute a meta-logic (or ‘logical framework’) in which the object-logics are formalized. Isabelle is now based on higher-order logic — a precise and well-understood foundation.

Examples illustrate use of this meta-logic to formalize logics and proofs. Axioms for first-order logic are shown sound and complete. Backwards proof is formalized by meta-reasoning about object-level entailment.

Higher-order logic has several practical advantages over other meta-logics. Many proof techniques are known, such as Huet’s higher-order unification procedure.

Key words: higher-order logic, higher-order unification, Isabelle, LCF, logical frameworks, meta-reasoning, natural deduction

Contents

1 History and overview 2

2 The meta-logic M 4 2.1 Syntax of the meta-logic . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2 Syntactic conventions . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3 Semantics of the meta-logic . . . . . . . . . . . . . . . . . . . . . . . 5 2.4 Inference rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

3 Representing intuitionistic propositional logic 7

4 Backwards proof construction 11 4.1 Proof states as derived rules . . . . . . . . . . . . . . . . . . . . . . . 12 4.2 Proof construction by resolution . . . . . . . . . . . . . . . . . . . . . 13 4.3 Lifting a rule over assumptions . . . . . . . . . . . . . . . . . . . . . 14 4.4 Deriving object-level rules . . . . . . . . . . . . . . . . . . . . . . . . 16

5 Quantification 18

6 Backwards proof with quantifiers 20 6.1 Lifting over universal quantifiers . . . . . . . . . . . . . . . . . . . . . 20 6.2 Unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

7 Other representations of eigenvariables 25 7.1 Hilbert’s ϵ-operator . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 7.2 Replacing Hilbert’s ϵ by special constants . . . . . . . . . . . . . . . . 26 7.3 Lifting versus special constants . . . . . . . . . . . . . . . . . . . . . 27

8 An implementation 29

9 Related work 31

1 History and overview

The dominance of classical first-order logic is challenged every year by something new. Scott’s Logic of Computable Functions appeared in 1969 and attracted the interest of Robin Milner. Milner built a proof checker but found it impossibly tedious for proofs of any length. He later developed Edinburgh lcf, a proof checker that was programmable [26].

Edinburgh lcf’s meta-language (ml) does not merely execute obvious command sequences. ml gives a general representation of logic. Terms and formulae are computable data, as are theorems. Each inference rule is a function from theorems to theorems. A theorem can be built only by applying rules to existing theorems.

While forwards proof is fundamental, it is often preferable to work backwards from a goal. Each inference rule maps premises to conclusion; its ‘inverse’ is a function (called a tactic) mapping a goal to subgoals. A tactic also returns a validation: a function from theorems to a theorem. When the backwards proof is finished, applying the validation functions performs the forwards proof, and yields the desired theorem. Tacticals operate on tactics, expressing control structures such as sequential or repetitive application of a tactic.

ml’s secure type checking ensures soundness: theorems are constructed only by rules. Exceptions signal when a rule or tactic is wrongly applied. Still, a tactic can be invalid: promising more than it can deliver. If its validation function is wrong then the final forwards proof will not yield the theorem that was expected. Tactics should be built using tactics and tacticals known to be valid. The lcf environment grows with use: rules can be composed as functions; tactics can be combined by tacticals.

By 1986, Edinburgh lcf’s techniques had spread to several systems [29], Standard ml had become a language in its own right, and Isabelle reached a usable form. Isabelle was intended to allow lcf-style proofs in various logics, using a representation of logic that did not require writing a function for each rule. In Isabelle-86, a rule was represented by a Horn clause; rules could be combined to build proofs [28]. (See also de Groote [14].) Since forwards and backwards proof were simply styles of proof construction, there was little difference between rules and tactics. Each state of a backwards proof was a derived rule:

\frac{subgoal ⋯ subgoal}{original goal}

Isabelle’s tactics and tacticals could be used like lcf ones though they were based on totally different principles.

The initial concern was with implementation problems. Quantifiers required a syntax involving the typed λ-calculus, while the joining of rules required unification; these together required higher-order unification [19]. I experimented with many different ways of enforcing the variable conditions of quantifier rules. Eventually Isabelle-86 supported many logics: Martin-Löf’s Type Theory, intuitionistic and classical sequent calculi, Zermelo-Fraenkel set theory. It was implemented in Standard ml.

Isabelle-86 was based on a naïve calculus of rules. It left many questions open, such as whether the following rules should be regarded as distinct:

\frac{A B}{C}  \frac{B A}{C}  \frac{A B A}{C}

The treatment of quantifiers seemed particularly unclear.

Many people have developed calculi for mathematical reasoning [7, 9, 15, 25]. A calculus of logics is often called a logical framework; I prefer to speak of a meta-logic and its object-logics. Isabelle-86 required a precise meta-logic suited to its aims and methods. A fragment of higher-order logic (called M here for ‘meta’) now serves this purpose. Implication expresses entailment; universal quantification expresses schematic rules and general premises; equality expresses definitions. The meta-logic extends that of Isabelle-86: it can express things like ‘adding the double negation rule to intuitionistic logic entails the excluded middle.’

Isabelle constructs proofs through deductions in M. The paper presents these methods formally in order to clarify theoretical issues such as soundness. Here is an outline of the paper:

Section 2 presents the meta-logic M: intuitionistic higher-order logic.

Section 3 formalizes the natural deduction rules for intuitionistic propositional logic in M. The formalization is shown sound and complete by induction on normalized proofs.

Section 4 describes how meta-level reasoning expresses object-level backwards proof, with examples from propositional logic.

Section 5 considers object-logics with quantifiers. The natural deduction system is extended to intuitionistic first-order logic and again shown sound and complete.

Section 6 extends the backwards proof methods to handle quantifiers and unification, with examples from first-order logic. The representation of eigenvariables differs from Isabelle-86.

Using Hilbert’s ϵ-operator, Section 7 recovers the Isabelle-86 representation and compares it with its alternative.

Section 8 describes how an implementation (the latest is called Isabelle-

88) was obtained from Isabelle-86.

Section 9 concludes with a discussion of related work.

Isabelle’s treatment of backwards proof has unique advantages over lcf’s. An Isabelle proof state is formalized by a meta-theorem; there are no validations. The subgoals are guaranteed sufficient to obtain the final goal. Unification is naturally accommodated. The techniques are presented within M, but resemble those of Isabelle-86 and may apply to other meta-logics.

Most of the examples below have been tested using Isabelle. They cover only propositional and first-order logic, but illustrate general techniques. Besides, the point is not to handle every esoteric logic. It is that mathematics requires a living language. Definitions extend its syntax; theorems extend its primitive modes of reasoning. In Zermelo-Fraenkel set theory the Cartesian product is defined by the power set, union, pairing, and separation axioms. ‘Obvious’ properties like

\frac{a ∈ A b ∈ B}{⟨a, b⟩ ∈ A × B}

require tedious proofs. A mathematician, having performed the proofs, would treat Cartesian product like a primitive with the obvious properties as new rules of inference. Isabelle is an attempt to support this style.

2 The meta-logic M

Alonzo Church developed higher-order logic, also called hol or simple type theory. It is based on the typed λ-calculus [16]. Gordon [13] built his hol theorem prover from lcf; another theorem prover is tps [2].

Andrews [1] has written a book covering higher-order logic. Here is a brief sketch of a fragment called M, which will be our meta-logic.

2.1 Syntax of the meta-logic

The types^{1} consist of basic types and function types of the form σ → τ. Let the Greek letters σ, τ, and υ stand for types.

The terms are those of the typed λ-calculus — constants, variables, abstractions, combinations — with the usual type constraints. Let a, b, and c stand for terms, using f, g, and h for terms of function type. Typical bound variables will be x, y, and z. Write a : σ to mean ‘a has type σ.’

The basic types and constants depend on the logic being represented. But they always include the type of propositions, prop, and the logical constants of M. A formula is a term of type prop. Let ϕ, ψ, and θ stand for formulae. The implication ϕ ⇒ ψ means ‘ϕ implies ψ.’ The universally quantified formula ⋀ x.ϕ means ‘for all x, ϕ is true,’ where x ranges over some type σ. The equality a ≡ b means ‘a equals b.’

The symbols ⇒, ⋀, and ≡ have been chosen to differ from symbols of objectlogics: those to be represented in M. In an object-logic presented below the corresponding symbols are ⊃, ∀, and =. The words ‘meta-implication,’ ‘meta-equality,’ ‘meta-formula,’ ‘meta-theorem,’ ‘meta-rule,’ etc., refer to expressions of M.

Quantification involves λ-abstraction. For every type σ, there is a constant ⋀_{σ} of type (σ → prop) → prop. The formula ⋀ x.ϕ, where x has type σ, abbreviates ⋀_{σ}(λx.ϕ). Using λ-conversions every quantification can be put into the form ⋀_{σ}(f), more readably ⋀ x.f(x), where f is a term of type σ → prop. Abstraction also expresses quantifiers in object-logics, as we shall see in Section 5.

1Sometimes called arities, following Martin-Löf, to avoid confusion with ml types or object-level types.

2.2 Syntactic conventions

The application of a to the successive arguments b_{1}, …, b_{m} is written a(b_{1}, …, b_{m}):

a(b_{1}, …, b_{m}) abbreviates (⋯ (ab_{1}) ⋯ b_{m})

In the absence of parentheses, implication (⇒) groups to the right. Let Φ, Ψ, and Θ stand for lists of formulae. Implication can also be written for such lists: if Φ is the list [ϕ_{1}, …, ϕ_{m}], then

\begin{matrix}ϕ_{1} ⇒ ⋯ ⇒ ϕ_{m} ⇒ ψ \\ [ϕ_{1}, …, ϕ_{m}] ⇒ ψ \\ Φ ⇒ ψ \end{matrix} \} each abbreviate ϕ_{1} ⇒ (⋯ ⇒ (ϕ_{m} ⇒ ψ) ⋯)

One λ or quantifier does the work of many:

λx_{1} … x_{m} . a ; ⋀ x_{1} … x_{m} . ϕ} abbreviates { λx_{1} …. λx_{m}.a ; ⋀ x_{1} …. ⋀ x_{m}.ϕ

The scope of a λ or quantifier extends far to the right:

λx . f(x, g(x)) ; ⋀ x . ϕ ⇒ b ≡ c} abbreviates { λx . (f(x, g(x))) ; ⋀ x . (ϕ ⇒ (b ≡ c))

A substitution has the form [a_{1}/x_{1}, …, a_{k}/x_{k}], where x_{1}, …, x_{k} are distinct variables and a_{1}, …, a_{k} are terms. If b is an expression and s is the substitution above then bs is the expression that results from simultaneously replacing every free occurrence of x_{i} by a_{i} in b, for i = 1, …, k (of course a_{i} must have the same type as x_{i}). Substitution must be carefully defined to avoid capture of free variables.

Substitutions are not part of M itself. The term f(a) indicates function application, not substitution. The β-reduction law, namely ((λx.b)(a)) ≡ b[a/x], expresses substitution at the object-level.

2.3 Semantics of the meta-logic

Higher-order logic is a language for writing formal mathematics. It can be justified on intuitive grounds, or else we can demonstrate its consistency by constructing a standard model in set theory.

Every type denotes a non-empty set. Given sets for each basic type, the interpretation of σ → τ is the set of functions from σ to τ. A closed term of type σ denotes a value of the corresponding set. Given a value for each constant, λ-abstractions denote functions.

The type prop denotes a set of truth values. Classical logic uses {T, F}; topos theory provides various intuitionistic interpretations [22]. The logical constants (⋀_{σ}, ⇒, and ≡_{σ}) denote appropriate truth-valued functions.

Remark. Requiring all types to be non-empty permits this simple inference system, where

(⋀ x . ⋀ θ . θ) ⇒ (⋀ θ . θ)

is a theorem. (Here θ is a bound variable of type prop!) If the type of x were empty then ⋀ θ . θ would be true; every formula would be true; the logic would be inconsistent.

Lambek and Scott [22, pages 128–132] present an inference system for higherorder logic allowing empty types.

2.4 Inference rules

The constant symbols include, for every type σ,

⇒ : prop → (prop → prop)
⋀σ : (σ → prop) → prop
≡_{σ} : σ → (σ → prop)

The implication rules are ⇒-introduction and ⇒-elimination:

\frac{{[ϕ] \atop ψ}}{ϕ ⇒ ψ}  \frac{ϕ ⇒ ψ ϕ}{ψ}

These are natural deduction rules; ⇒-introduction discharges the assumption ϕ. In most other rules, the conclusion depends on all assumptions of the premises.

The universal quantification rules are ⋀-introduction and ⋀-elimination:

\frac{ϕ}{⋀ x.ϕ}  \frac{⋀ x.ϕ}{ϕ[b/x]}

These are also called generalization and specialization. The generalization rule is subject to the eigenvariable condition that x is not free in the assumptions.

The equality rules are reflexivity, symmetry, and transitivity:

a ≡ a  \frac{a ≡ b}{b ≡ a}  \frac{a ≡ b b ≡ c}{a ≡ c}

The λ-conversions are α-conversion (bound variable renaming), β-conversion, and extensionality:

(λx.a) ≡ (λy.a[y/x])  ((λx.a)(b)) ≡ a[b/x]  \frac{f(x) ≡ g(x)}{f ≡ g}

The α-conversion axiom holds provided y is not free in a. Extensionality holds provided x is not free in the assumptions, f, or g. Extensionality is equivalent to η-conversion, namely (λx.f(x)) ≡ f where x is not free in f (see Hindley and Seldin [16, pages 72–74]).

The abstraction and combination rules are

\frac{a ≡ b}{(λx.a) ≡ (λx.b)}  \frac{f ≡ g a ≡ b}{f(a) ≡ g(b)}

Abstraction holds provided x is not free in the assumptions.

Logical equivalence means equality of truth values:

\frac{{[ϕ] \atop ψ}  {[ψ] \atop ϕ}}{ϕ ≡ ψ}  \frac{ϕ ≡ ψ ϕ}{ψ}

The typed λ-calculus satisfies the strong normalization and Church-Rosser properties [16]. Thus repeatedly applying β and η-reductions always terminates. The reductions can take place in any order; the resulting normal form will be the same up to α-conversion. To summarize:

Theorem 1 Every term can be reduced to a normal form that is unique up to αconversion.

Remark. Because of normal forms, equality is decidable in the typed λ-calculus — but not in higher-order logic. The normal form does not take account of the logical rules. No effective procedure can reduce every theorem to some unique true formula.

There is also a normalization procedure for hol proofs. This plays a crucial role in demonstrating that an object-logic is faithfully expressed.

3 Representing intuitionistic propositional logic

To represent an object-logic in Isabelle we extend the meta-logic with types, constants, and axioms. A simple example is intuitionistic propositional logic (ipl).

To represent the syntax of ipl, introduce the basic type form for denotations of formulae. Introduce the constant symbols

⊥ : form
&, ∨, ⊃ : form → (form → form)
true : form → prop

Variables of type form include A, B, and C.

Object-sentences are enclosed in double brackets [[]]. The meta-formula [[A]] abbreviates true(A) and means that A is true. Keeping the types form and prop distinct avoids presuming that truth-values of the object-logic are identical to those of the meta-logic. To avoid confusing these logics, let us use distinctive terminology. There is a meta-rule called ⇒-elimination. The similar object-rule is called the ⊃E rule, while the corresponding meta-axiom is called the ⊃E axiom.

The natural deduction rules (Figure 1) of intuitionistic logic are represented by meta-level axioms (Figure 2). The resulting extension of M is called Mipl. The outer quantifiers of meta-axioms will often be dropped.

The new symbols have the usual interpretations. Let the type form denote a set of truth values such that &, ∨, ⊃, and ⊥ have their intuitionistic meanings [11, Chapter 5]. The axioms are true under this semantics: for example, if A is true and B is true then A & B is true. Meta-implication (⇒) expresses the discharge of assumptions. The ⊃I axiom says that if the truth of A implies the truth of B, then the formula A ⊃ B is true.

The resemblance between the meta-level axioms and the rules should be regarded as a happy coincidence. An axiom formalizes not the syntax of a rule but its semantic justification. The resemblance diminishes in first-order logic (Section 5). The formalization of modal logic by Avron et al. [3] (in their meta-logic) reflects Kripke semantics rather than the syntax of the rules.

An obvious question is whether the object-logic is faithfully represented. The definition below is oriented towards natural deduction: it concerns entailments rather than theorems.

Definition 1 Let L be a logic and A_{1}, …, A_{m}, B be formulae of L. Let M_{L} be a meta-logic obtained from M by adding types, constants, and axioms. Suppose that [[−]] is a function mapping each formula A of L to a meta-formula [[A]] of M_{L}. Then say

• M_{L} is sound for L if, for every M_{L}-proof of [[B]] from [[A_{1}]], …, [[A_{m}]], there is an L-proof of B from A_{1}, …, A_{m}.

• M_{L} is complete for L if, for every L-proof of B from A_{1}, …, A_{m}, there is an M_{L}-proof of [[B]] from [[A_{1}]], …, [[A_{m}]].

• M_{L} is faithful for L if M_{L} is sound and complete for L.

Informally, Mipl is sound for ipl because the additional axioms are true and the rules of M are sound. A better argument is by induction on normal proofs in M. Here is a summary of the proof-theoretic concepts of Prawitz [31, 32]. For simplicity, let us ignore equality rules, identifying terms that are equivalent up to λ-conversions.

A branch in a proof traces the construction and destruction of a formula. Each branch is obtained by repeatedly walking downwards from a premise of a rule to its conclusion, but terminates at the second premise of ⇒-elimination. Thus in

\frac{ϕ ⇒ ψ ϕ}{ψ}

a branch may connect ϕ ⇒ ψ with ψ but not ϕ with ψ since these formulae may be syntactically unrelated. (This discussion is for M. For logics having other connectives, most elimination rules are special cases.)

Every proof in M can be normalized such that, in every branch, no elimination rule immediately follows an introduction rule. In a normal proof, every branch

introduction (I)  elimination (E)
Conjunction  \frac{A B}{A & B}  \frac{A & B}{A}  \frac{A & B}{B}
Disjunction \frac{A}{A ∨ B}  \frac{B}{A ∨ B}  \frac{A ∨ B  {[A] \atop C}  {[B] \atop C}}{C}
Implication  \frac{{[A] \atop B}}{A ⊃ B}  \frac{A ⊃ B  A}{B}
Contradiction  \frac{⊥}{A}

Figure 1: The rules of intuitionistic propositional logic

⋀ AB . [[A]] ⇒ ([[B]] ⇒ [[A & B]])  (&I)
⋀ AB . [[A & B]] ⇒ [[A]]  ⋀ AB . [[A & B]] ⇒ [[B]]  (&E)
⋀ AB . [[A]] ⇒ [[A ∨ B]]  ⋀ AB . [[B]] ⇒ [[A ∨ B]]  (∨I)
⋀ ABC . [[A ∨ B]] ⇒ ([[A]] ⇒ [[C]]) ⇒ ([[B]] ⇒ [[C]]) ⇒ [[C]]  (∨E)
⋀ AB . ([[A]] ⇒ [[B]]) ⇒ [[A ⊃ B]]  (⊃ I)
⋀ AB . [[A ⊃ B]] ⇒ [[A]] ⇒ [[B]]  (⊃ E)
⋀ A . [[⊥]] ⇒ [[A]]  (⊥E)

Figure 2: Meta-level axioms for intuitionistic propositional logic

\frac{\frac{\frac{\frac{⋀ AB . [[A]] ⇒ ([[B]] ⇒ [[A & B]])}{⋀ B . [[C]] ⇒ ([[B]] ⇒ [[C & B]])}}{[[C]] ⇒ ([[D]] ⇒ [[C & D]])}  ⋮ ; [[C]]}{[[D]] ⇒ [[C & D]]}  ⋮ ; [[D]]}{[[C & D]]}

Figure 3: The meta-proof formalizing a &I inference

\frac{\frac{\frac{⋀ AB . ([[A]] ⇒ [[B]]) ⇒ [[A ⊃ B]]}{⋀ B . ([[C]] ⇒ [[B]]) ⇒ [[C ⊃ B]]}}{([[C]] ⇒ [[D]]) ⇒ [[C ⊃ D]]} \frac{[ [[C]] ] ; ⋮ ; [[D]]}{[[C]] ⇒ [[D]]}}{[[C ⊃ D]]}

Figure 4: The meta-proof formalizing an ⊃I inference

begins with an assumption or axiom, then has a series of eliminations, then a series of introductions. During the eliminations the formulae shrink to a minimum; during the introductions they grow again.

Observe that [[B]] is an atomic Mipl-formula. A normal proof can be put into expanded normal form, where every minimum formula is atomic [32, page 254]. For example, if a minimum formula is ϕ ⇒ ψ, then the following can be spliced into the proof, reducing the minimum formula to ψ:

\frac{ϕ ⇒ ψ [ϕ]}{\frac{ψ}{ϕ ⇒ ψ}}

Completeness holds because to each object-level inference there corresponds a meta-proof involving an Mipl axiom. Soundness holds because to each occurrence of an Mipl axiom in a meta-proof there corresponds an object-level inference. Figures 3 and 4 illustrate the correspondence.

Theorem 2 Mipl is sound for ipl. Proof : By induction on the size of the expanded normal proof in Mipl of [[B]] from [[A_{1}]], …, [[A_{m}]], construct an ipl proof of B from A_{1}, …, A_{m}.

Since [[B]] is atomic, the branch terminating with [[B]] cannot contain introduction rules, and thus cannot discharge assumptions. The branch must consist entirely of elimination rules. If it is just [[B]] then B is an assumption, one of A_{1}, …, A_{m}. Otherwise the branch contains elimination rules, so its first formula cannot be atomic. It must consist of an axiom followed by elimination rules. There is one case for each axiom.

For the &I axiom, B is C &D for some formulae C and D. The meta-proof must have the structure of Figure 3. It has two ⋀-eliminations involving C and D, and two ⇒-eliminations, involving proofs of [[C]] and [[D]] from [[A_{1}]], …, [[A_{m}]]. By the induction hypothesis, construct ipl proofs of C and D from A_{1}, …, A_{m}. Applying &I gives an ipl proof of C & D.

For the ⊃I axiom, B is C ⊃ D. The meta-proof must have the structure of Figure 4. It contains a proof of [[C]] ⇒ [[D]] from [[A_{1}]], …, [[A_{m}]]. By expanded normal form this consists of a proof of [[D]] from [[A_{1}]], …, [[A_{m}]], [[C]], followed by ⇒-introduction, discharging the assumption [[C]]. By the induction hypothesis, construct an ipl proof of D from A_{1}, …, A_{m}, C, and ⊃I gives an ipl proof of C ⊃ D from A_{1}, …, A_{m}.

The cases for the other axioms are similar. □

Theorem 3 Mipl is complete for ipl. Proof : By induction on the size of the ipl proof of B from A_{1}, …, A_{m}, construct a proof of [[B]] from [[A_{1}]], …, [[A_{m}]] in Mipl.

Suppose the last inference of the ipl proof is ⊃I, and the conclusion is C ⊃ D. Then the rule is applied to an ipl proof of D from A_{1}, …, A_{m}, C. By the induction hypothesis, construct an Mipl-proof of [[D]] from [[A_{1}]], …, [[A_{m}]], [[C]]. Now it is easy to construct a meta-proof like that in Figure 4.

The cases for the other axioms are similar. □

Remark. The heavy use of meta-implication (⇒) may suggest that the meta-logic ought to involve sequents. Then the &I axiom would be

[[A]], [[B]] |− [[A & B]]

and the resolution rule (Section 4.2) would resemble the cut rule. However, this amounts to using the sequent symbol as a logical connective. In typical usage, an axiom is a formula — not a sequent [36]. Such a use of sequents would also complicate the use of hypothetical rules (illustrated in Section 4.4).

4 Backwards proof construction

The reduction of the goal ϕ to the subgoals ϕ_{1}, …, ϕ_{m} amounts to deriving the rule ϕ_{1}, …, ϕ_{m}/ϕ. The meta-logic represents this object-level rule as the implication [ϕ_{1}, …, ϕ_{m}] ⇒ ϕ. Such Horn clauses are combined by a derived meta-rule: resolution.

Let us begin by looking at backwards proof as a style of proof construction. Then we can formalize backwards proof in M, obtaining the methods implemented in Isabelle.

\begin{aligned}& \frac{A & B ⊃ C ⊃ A & C}{A & B ⊃ C ⊃ A & C} & ⟼_{1}^{⊃I} & \frac{A & B ; ⋮ ; C ⊃ A & C}{A & B ⊃ C ⊃ A & C} & ⟼_{2}^{⊃I} & \frac{A & B ; C ; ⋮ ; A & C}{A & B ⊃ C ⊃ A & C} \\ ⟼_{3}^{&I} & \frac{A & B ; C ; ⋮ ; A  A & B ; C ; ⋮ ; C}{A & B ⊃ C ⊃ A & C} & ⟼_{4}^{asm} & \frac{A & B ; C ; ⋮ ; A}{A & B ⊃ C ⊃ A & C} & ⟼_{5}^{&E} & A & B ⊃ C ⊃ A & C \end{aligned}

Figure 5: The steps of the backwards proof

4.1 Proof states as derived rules

In this section, ‘rule,’ ‘proof,’ etc., refer to object-level rules and proofs. The method is illustrated by a sample proof in intuitionistic propositional logic:

\frac{\frac{\frac{\frac{[A & B]}{A} [C]}{A & C}}{C ⊃ A & C}}{A & B ⊃ (C ⊃ A & C)}

A backwards proof grows from the root upwards, rather than from the leaves downwards. Every state of the proof can be represented by a derived rule whose conclusion is the main goal, here A & B ⊃ (C ⊃ A & C), and whose premises are the current subgoals. The proof of the derived rule — namely, the internal structure — has no further role and is suppressed. The initial state is represented by the trivial rule whose premise and conclusion are identical.

Figure 5 shows the sequence of proof states, represented as derived rules. Each step is written as an arrow (like ⟼_{2}^{⊃I}) giving the inference rule and step number. The initial rule is combined with ⊃I, to derive a rule involving the discharge of the assumption A & B. Combining this rule again with ⊃I adds C to the assumptions. Combining the resulting rule with &I derives a rule that has two premises. This splits the goal A & C in two. The full proof at this point is

\frac{\frac{A & B ; C ; ⋮ ; A  A & B ; C ; ⋮ ; C}{A & C}}{\frac{C ⊃ A & C}{A & B ⊃ (C ⊃ A & C)}}

The second subgoal, C, holds trivially by assumption. The first subgoal is proved using &E to prove A from A&B. The final state is the theorem A&B ⊃ (C ⊃ A&C).

4.2 Proof construction by resolution

To formalize this kind of proof construction in M requires a change in notation. An object-inference like \frac{A&B}{A} will now be written [[A & B]] ⇒ [[A]]. The meta-inference ϕ ⟼ ψ will now be written \frac{ϕ}{ψ}.

The initial state in a proof of C is formalized by the trivial meta-theorem [[C]] ⇒ [[C]]. A state of the proof having n subgoals is represented by a derived object-rule having n premises, formalized by the meta-theorem

[ψ_{1}, …, ψ_{n}] ⇒ [[C]]

The state with zero subgoals is the meta-theorem [[C]], which represents the objecttheorem C. Outer quantifiers are dropped, so the meta-theorems may contain free variables.

Most Isabelle proof steps use resolution, a derived meta-rule. Resolution instantiates free variables of an object-rule by unification against a subgoal in the proof state. In a simple case, the substitution s must match ϕ against ψ, namely ϕs ≡ ψ:

\frac{Φ ⇒ ϕ Ψ ⇒ ψ ⇒ θ}{Ψ ⇒ Φs ⇒ θ}  (1)

The list notation for nested implication eliminates subscripts; Φ and Ψ are lists of formulae. Here is the meta-rule again, writing out the lists in full.

Let i be given; if ϕs ≡ ψ_{i} then

\frac{[ϕ_{1}, …, ϕ_{m}] ⇒ ϕ [ψ_{1}, …, ψ_{i}, …, ψ_{n}] ⇒ θ}{[ψ_{1}, …, ϕ_{1}s, …, ϕ_{m}s, …, ψ_{n}] ⇒ θ}

Resolution replaces the subgoal ψ_{i} by ϕ_{1}s, …, ϕ_{m}s in the proof state. The first premise is an object-level rule and the second is a proof state; the conclusion is a new proof state:

\frac{object-level rule proof state}{new proof state}

Full resolution involves unification. The free variables of the object-level rule should be distinct from those of the proof state. In the examples, variables are renamed by subscripting. Isabelle variables contain an index to facilitate renaming.

Resolution is easily derived in M. Using both quantifier rules k times derives an instantiation rule,

\frac{ϕ}{ϕ[a_{1}/x_{1}, …, a_{k}/x_{k}]}

provided that x_{1}, …, x_{k} are not free in the assumptions. Resolution consists of instantiation followed by reasoning about implication.

Remark. Isabelle resolution [28] is ordinary resolution restricted to Horn clauses. Many Isabelle proof procedures use techniques of logic programming. Completeness of resolution is not a central issue in Isabelle, for a proof may use any meta-rules.

4.3 Lifting a rule over assumptions

The resolution rule (1) represents lcf-style backwards proof, which does not recognize natural deduction. In lcf (and early versions of Isabelle) natural deduction must be expressed through a sequent calculus. Our formalization of ipl expresses natural deduction by meta-implication. We now supplement resolution with a method (called lifting) of making assumptions at the meta-level.

Suppose we want to formalize the sample proof, Figure 5. Resolving the ⊃I axiom against the goal [[A & B ⊃ (C ⊃ A & C)]] will produce the subgoal

[[A & B]] ⇒ [[C ⊃ A & C]]  (2)

which contains the assumption A & B. The next backwards step should use ⊃I again. We can prepare the axiom by replacing its bound variables A and B by new free variables A_{2} and B_{2},

([[A_{2}]] ⇒ [[B_{2}]]) ⇒ [[A_{2} ⊃ B_{2}]]

and then lift it over the assumption A & B, to obtain the meta-theorem

([[A & B]] ⇒ ([[A_{2}]] ⇒ [[B_{2}]])) ⇒ ([[A & B]] ⇒ [[A_{2} ⊃ B_{2}]])  (3)

Resolution with this instantiates A_{2} and B_{2}, replacing the subgoal (2) by

[[A & B]] ⇒ ([[C]] ⇒ [[A & C]])

This subgoal contains the assumptions A & B and C.

The lifting rule. The general case is lifting the object-rule [ϕ_{1}, …, ϕ_{m}] ⇒ ϕ over the list of assumptions Θ:

\frac{[ϕ_{1}, …, ϕ_{m}] ⇒ ϕ}{[Θ ⇒ ϕ_{1}, …, Θ ⇒ ϕ_{m}] ⇒ (Θ ⇒ ϕ)}

This meta-rule, called lifting or ⇒-lifting, is derivable in M.

Suppose first that Θ = [θ]. Clearly ⇒-introduction gives

\frac{ψ}{θ ⇒ ψ}

If ψ represents an object-rule then it must be an implication, say ϕ ⇒ ψ′. To push θ to the right, assume θ ⇒ ϕ and apply the following meta-rule, whose derivation is simple:

\frac{θ ⇒ (ϕ ⇒ ψ′) θ ⇒ ϕ}{θ ⇒ ψ′}

If ψ′ is also an implication then repeating this step pushes θ fully to the right; finally, an equal number of ⇒-introductions discharges the assumptions like θ ⇒ ϕ. If ψ′ is not an implication then the result would be

(θ ⇒ ϕ) ⇒ (θ ⇒ ψ′)

Now if Θ = [θ_{1}, …, θ_{k}] then repeatedly apply the process above to θ_{k}, …, θ_{1}.

A sample proof. Now we can formalize the proof of A & B ⊃ (C ⊃ A & C). The first step is the resolution of the ⊃I axiom with the initial proof state:

\frac{([[A_{1}]] ⇒ [[B_{1}]]) ⇒ [[A_{1} ⊃ B_{1}]] [[A & B ⊃ C ⊃ A & C]] ⇒ [[A & B ⊃ C ⊃ A & C]]}{([[A & B]] ⇒ [[C ⊃ A & C]]) ⇒ [[A & B ⊃ C ⊃ A & C]]}

The ⊃I axiom was prepared for resolution by dropping outer quantifiers, introducing new free variables A_{1} and B_{1}. Resolution instantiated A_{1} to A & B and B_{1} to C ⊃ A & C. The new state has one subgoal: to prove C ⊃ A & C from the assumption A & B.

Recall that lifting the ⊃I axiom over A & B produces the meta-theorem (3). Resolving (3) with the proof state instantiates A_{2} to C and B_{2} to A & C:

\frac{(3) ([[A & B]] ⇒ [[C ⊃ A & C]]) ⇒ [[A & B ⊃ (C ⊃ A & C)]]}{([[A & B]] ⇒ [[C]] ⇒ [[A & C]]) ⇒ [[A & B ⊃ (C ⊃ A & C)]]}

To save space, define abbreviations for the main goal and the assumption list:

ψ = [[A & B ⊃ (C ⊃ A & C)]]
Θ = [ [[A & B]], [[C]] ]

Thus the current proof state is (Θ ⇒ [[A & C]]) ⇒ ψ.

The next step is resolution with the &I axiom, after lifting it over the assumptions:

\frac{(Θ ⇒ [[A_{3}]]) ⇒ (Θ ⇒ [[B_{3}]]) ⇒ (Θ ⇒ [[A_{3} & B_{3}]]) (Θ ⇒ [[A & C]]) ⇒ ψ}{(Θ ⇒ [[A]]) ⇒ (Θ ⇒ [[C]]) ⇒ ψ}

The variable instantiations are A_{3} to A and B_{3} to C. Observe how the assumptions, Θ, are copied to both subgoals.

The next step solves the second goal by assumption. It is formalized by resolution with the meta-tautology Θ ⇒ [[C]], without lifting:

\frac{Θ ⇒ [[C]] (Θ ⇒ [[A]]) ⇒ (Θ ⇒ [[C]]) ⇒ ψ}{(Θ ⇒ [[A]]) ⇒ ψ}

Next, resolution with the &E axiom reduces the goal A to the subgoal A & B. Since the goal cannot instantiate the variable B of the &E axiom, let us take the correct instance of the axiom, lifted over Θ:

\frac{(Θ ⇒ [[A & B]]) ⇒ (Θ ⇒ [[A]]) (Θ ⇒ [[A]]) ⇒ ψ}{(Θ ⇒ [[A & B]]) ⇒ ψ}

Full resolution (with unification) can instantiate variables in the proof state. But Section 4.4 gives a better treatment of &E.

We solve the last subgoal by assumption — resolution with another meta-tautology:

\frac{Θ ⇒ [[A & B]] (Θ ⇒ [[A & B]]) ⇒ ψ}{ψ}

This concludes the proof of A & B ⊃ (C ⊃ A & C), representing each step of the object-level proof by a meta-level resolution. The proof is valid for arbitrary object-formulae A, B, and C. To emphasize this we may generalize ψ over its free variables, obtaining the final meta-theorem

⋀ ABC . [[A & B ⊃ (C ⊃ A & C)]]

4.4 Deriving object-level rules

Gordon [13] prefers higher-order logic because it can express many of its derived rules as theorems. Isabelle expresses derived rules as meta-theorems, allowing us to work in first-order logic or even weaker systems.

A new conjunction rule. The &E rules typically work in the forwards direction: from A&B conclude A. Another version of conjunction elimination, resembling ∨E, is better suited to backwards proof:

\frac{A & B \begin{matrix}[A, B] \\ C \end{matrix}}{C}

This conjunction rule discharges the assumptions A and B in its second premise; we can also say [33] that its second premise is the rule \frac{A B}{C}.

The formalization in Mipl is

⋀ ABC . [[A & B]] ⇒ ([[A]] ⇒ [[B]] ⇒ [[C]]) ⇒ [[C]]

To prove it, start with the goal [[C]]. For fixed A, B, C we may assume [[A & B]] and [[A]] ⇒ [[B]] ⇒ [[C]]. Once [[C]] has been proved, discharging the meta-assumptions and generalizing produces the correct meta-theorem.

The first step is resolution with the meta-assumption [[A]] ⇒ [[B]] ⇒ [[C]]:

\frac{[[A]] ⇒ [[B]] ⇒ [[C]] [[C]] ⇒ [[C]]}{[[A]] ⇒ [[B]] ⇒ [[C]]}

The subgoals are [[A]] and [[B]]. We resolve &E against the first subgoal:

\frac{[[A & B]] ⇒ [[A]] [[A]] ⇒ [[B]] ⇒ [[C]]}{[[A & B]] ⇒ [[B]] ⇒ [[C]]}

Next, resolve with the meta-assumption [[A & B]]:

\frac{[[A & B]] [[A & B]] ⇒ [[B]] ⇒ [[C]]}{[[B]] ⇒ [[C]]}

Next, use the other &E axiom:

\frac{[[A & B]] ⇒ [[B]] [[B]] ⇒ [[C]]}{[[A & B]] ⇒ [[C]]}

Finally, resolve with [[A & B]] again:

\frac{[[A & B]] [[A & B]] ⇒ [[C]]}{[[C]]}

Hypothetical rules. Adding the double negation rule to intuitionistic propositional logic gives classical logic. More precisely, if every formula A satisfies the double negation rule,

\frac{(A ⊃ ⊥) ⊃ ⊥}{A}

then every formula B satisfies the excluded middle, B ∨ (B ⊃ ⊥).^{2} The formalization of this entailment is

(⋀ A . [[(A ⊃ ⊥) ⊃ ⊥]] ⇒ [[A]]) ⇒ (⋀ B . [[B ∨ (B ⊃ ⊥)]])

Here the premise is a schematic rule. We must make, and finally discharge, the quantified meta-assumption

⋀ A . [[(A ⊃ ⊥) ⊃ ⊥]] ⇒ [[A]]

Conversely, any formula that satisfies the excluded middle also satisfies double negation [11, page 27]:

\frac{A ∨ (A ⊃ ⊥) (A ⊃ ⊥) ⊃ ⊥}{A}

The formalization of this derived rule is

⋀ A . [[A ∨ (A ⊃ ⊥)]] ⇒ [[(A ⊃ ⊥) ⊃ ⊥]] ⇒ [[A]]

Contrast the use of quantifiers in these examples.

2The proof is tricky. From (B ∨ (B ⊃ ⊥)) ⊃ ⊥ prove both B ⊃ ⊥ and (B ⊃ ⊥) ⊃ ⊥.

5 Quantification

Many logical constants introduce bound variables: universal and existential quantifiers (∀ and ∃), description operators (λ, ι and ϵ), general product and sum (Π and Σ), union and intersection of families (as in ⋃_{i∈I} A_{i}), and so on. Isabelle implements logics comprising most of these.

Adding quantifiers to the previous object-logic gives intuitionistic first-order logic (ifol). Formally, extend Mipl to become Mifol. Add the type term for denotations of terms. The quantifiers are the constant symbols

∀, ∃ : (term → form) → form

If A, A(x), and A(x, y) each have type form then the three variables named A must have different types, and so are different variables. Rather than declaring a fixed list of variables with their types, let the context determine the types — avoiding things like A & A(x). For emphasis, F, G, and H will stand for formulavalued functions.

Write ∀x.A for ∀(λx.A) and ∃x.A for ∃(λx.A). By λ-conversion every quantified formula is equivalent to one of the form ∀(F) or ∃(F), where F has type term → form.

The rules (Figure 6) and their meta-level axioms (Figure 7) do not have the close resemblance that we saw for propositional logic. The eigenvariable conditions of ∀I and ∃E are not formalized literally. Note that the two conditions differ in form but not in effect. Both ensure that x serves only to specify a truth-valued function, through its occurrences in A.

In the axioms, F denotes not the text of the quantification but its meaning: a truth-valued function. The axiom ∀I states that if F is an everywhere-true function then ∀x.F (x) is true. Similarly, B denotes not the text of a formula but a truthvalue. The ∃E axiom states that if ∃x.F (x) is true and F (x) implies B for all x, then B is true. The axioms reflect the meanings of the corresponding rules.

Although the justification of each axiom is semantic, they behave as expected in syntax. Substitution for the variables F and B avoids capture of the variable x. In particular, B may not be replaced by a formula containing x. Assumptions also obey the eigenvariable conditions, as we shall see below.

The demonstration that these axioms faithfully represent first-order logic is similar to that for propositional logic (Section 3).

Theorem 4 Mifol is sound for ifol. Proof : By induction over the expanded normal proof in Mifol of [[B]] from [[A_{1}]], …, [[A_{m}]], construct an ifol proof of B from A_{1}, …, A_{m}. The branch terminating with [[B]], unless it is trivial, consists of an axiom followed by elimination rules.

For the ∃I axiom, B is ∃x.G(x). The normalized proof must have the form shown in Figure 8. Two ⋀-eliminations introduce G and u; then ⇒-elimination is applied to a proof of [[G(u)]] from [[A_{1}]], …, [[A_{m}]]. By the induction hypothesis construct an ifol proof of G(u) from A_{1}, …, A_{m}, and use the ∃I rule to prove ∃x.G(x). The

introduction (I)  elimination (E)

Universal quantifier  \frac{A}{∀x.A}∗  \frac{∀x.A}{A[t/x]}

Existential quantifier  \frac{A[t/x]}{∃x.A}  \frac{∃x.A  {[A] \atop B}}{B} ∗

*Eigenvariable conditions: ∀I: provided x not free in the assumptions

∃E: provided x not free in B or in any assumption save A

Figure 6: Quantifier rules

⋀ F . (⋀ x . [[F (x)]]) ⇒ [[∀x.F (x)]]  (∀I)
⋀ F y . [[∀x.F (x)]] ⇒ [[F (y)]]  (∀E)

⋀ F y . [[F (y)]] ⇒ [[∃x.F (x)]]  (∃I)
⋀ F B . [[∃x.F (x)]] ⇒ (⋀ x . [[F (x)]] ⇒ [[B]]) ⇒ [[B]]  (∃E)

Figure 7: Meta-level axioms for the quantifier rules

\frac{\frac{\frac{⋀ F y . [[F (y)]] ⇒ [[∃x.F (x)]]}{⋀ y . [[G(y)]] ⇒ [[∃x.G(x)]]}}{[[G(u)]] ⇒ [[∃x.G(x)]]}  ⋮ ; [[G(u)]]}{[[∃x.G(x)]]}

Figure 8: The meta-proof formalizing an ∃I inference

\frac{\frac{\frac{\frac{⋀ F B . [[∃x.F (x)]] ⇒ (⋀ x . [[F (x)]] ⇒ [[B]]) ⇒ [[B]]}{⋀ B . [[∃x.G(x)]] ⇒ (⋀ x . [[G(x)]] ⇒ [[B]]) ⇒ [[B]]}}{[[∃x.G(x)]] ⇒ (⋀ x . [[G(x)]] ⇒ [[C]]) ⇒ [[C]]} ⋮ ; [[∃x.G(x)]]}{(⋀ x . [[G(x)]] ⇒ [[C]]) ⇒ [[C]]} \frac{\frac{[ [[G(y)]] ] ; ⋮ ; [[C]]}{[[G(y)]] ⇒ [[C]]}}{⋀ y . [[G(y)]] ⇒ [[C]]}}{[[C]]}

Figure 9: The meta-proof formalizing an ∃E inference Mifol proof is shown without β-conversions, identifying terms that have the same normal form. If G is λx.A then G(u) ≡ A[u/x], and [[∃x.G(x)]] ≡ [[∃x.A]].

For ∃E, the proof (Figure 9) contains a proof of ⋀ y . [[G(y)]] ⇒ [[C]] from [[A_{1}]], …, [[A_{m}]]. Assuming expanded normal form, it consists of a proof of [[C]] followed by ⇒-introduction, discharging [[G(y)]], followed by ⋀-introduction. (The bound variable y can be chosen so that it is not free in [[A_{1}]], …, [[A_{m}]].) By the induction hypothesis, there are ifol proofs of C from A_{1}, …, A_{m}, G(y) and of ∃x.G(x) from A_{1}, …, A_{m}. The ∃E rule gives an ifol proof of C from A_{1}, …, A_{m}.

The cases for the other axioms are similar. □

Theorem 5 Mifol is complete for ifol. Proof : By induction over the ifol proof of B from A_{1}, …, A_{m}, construct a proof of [[B]] from [[A_{1}]], …, [[A_{m}]] in Mifol.

The hardest case is when the last inference is ∃E. Then the rule is applied to an ifol proof of ∃x.A, and to a proof of B from A. By the axiom for ∃E, it is enough to prove the theorems [[∃x.A]] and ⋀ x . [[A]] ⇒ [[B]]. By the induction hypothesis, there is an Mifol-proof of [[∃x.A]], and also a proof of [[B]] from [[A]]. The meta-proof resembles that in Figure 9, where G is λx.A. Again, terms having the same normal form are identified. □

Remark. Perhaps the type names term and form are overly syntactic; term denotes a set of individuals while form denotes a set of truth-values. The meaning of A ⊃ B should depend on the meanings of A and B, not on their syntactic structure.

Still, types play an important syntactic role. An expression of type term represents an ifol term, and similarly form represents formulae. By assigning a type to each syntactic category of the object-logic, type-checking in M enforces syntactic constraints.

6 Backwards proof with quantifiers

Quantifiers complicate backwards proof: goals may contain unknowns and parameters. An unknown takes the form of a free variable in the proof state, and can be replaced by any term. Unification is a standard technique for solving unknowns. A parameter comes from an eigenvariable of a rule. Parameters have two possible representations, ⋀-bound variables and Hilbert ϵ-terms.

6.1 Lifting over universal quantifiers

The universal quantifier ⋀ is the obvious way to express a goal involving parameters. Recall the axioms ∀I and ∃E. If we use ∀I to prove ∀z.G(z) ∨ H(z) then the subgoal will be ⋀ z . [[G(z) ∨ H(z)]]. Resolution against a quantified goal requires a new derived meta-rule: lifting an object-rule over a quantified variable. This ⋀-lifting resembles ⇒-lifting, introduced earlier to handle assumptions.

Suppose we want to apply ∨I to the goal ⋀ z . [[G(z) ∨ H(z)]]. The ∨I axiom has quantified variables A and B:

⋀ AB . [[A]] ⇒ [[A ∨ B]]

(Lifting seems easier to explain if quantifiers are shown explicitly. In the sample proofs below, outer quantifiers are dropped after lifting.) Lifting the axiom over z produces a meta-theorem with new quantified variables G and H, functions of z:

⋀ GH . (⋀ z . [[G(z)]]) ⇒ (⋀ z . [[G(z) ∨ H(z)]])  (4)

Why is this a theorem? By the ∨I axiom, [[G(z)]] implies [[G(z) ∨ H(z)]] for all G, H, and z. Thus we may reduce ⋀ z . [[G(z) ∨ H(z)]] to the subgoal ⋀ z . [[G(z)]].

The ∃I axiom has quantified variables F and y:

⋀ F y . [[F (y)]] ⇒ [[∃x.F (x)]]

Lifting over z produces quantified variables G and f:

⋀ Gf . (⋀ z . [[G(z, f(z))]]) ⇒ (⋀ z . [[∃x.G(z, x)]])  (5)

By the ∃I axiom, [[G(z, f(z))]] implies [[∃x.G(z, x)]] for all G, f, and z. Thus we may reduce ⋀ z . [[∃x.G(z, x)]] to the subgoal ⋀ z . [[G(z, f(z))]]. The pattern may become clearer if we recall that ∃x.F (x) means ∃(F) and ∃x.G(z, x) means ∃(G(z)); we have replaced F by G(z).

The lifting rule. Given an object-rule, lifting replaces all the outer quantified variables by new ones of function type. Its formal derivation consists of several steps. Consider the M-proof

\frac{\frac{⋀ y . ψ}{ψ[f(z)/y]}}{⋀ z . ψ[f(z)/y]}

Here f is a variable (of function type), and the final step will involve generalization over f. For k quantified variables we can similarly derive the rule

\frac{⋀ y_{1} … y_{k} . ψ}{⋀ z . ψ[f_{1}(z)/y_{1}, …, f_{k}(z)/y_{k}]}

where the f_{i} are free variables. If z has type σ then lifting replaces y_{i} (of type τ_{i}) by a different variable f_{i} (of type σ → τ_{i}).

Typically ψ is an implication ϕ ⇒ ψ′. To push the ⋀ z into the implication, assume ⋀ z . ϕ and apply this derived meta-rule:

\frac{⋀ z . ϕ ⇒ ψ′ ⋀ z . ϕ}{⋀ z . ψ′}

If the object-rule has several premises then ψ′ will also be an implication; continue pushing the ⋀ z into the right. Then use ⇒-introduction to discharge the assumptions like ⋀ z . ϕ, and use ⋀-introduction to generalize over the variables f_{1}, …, f_{k}. This yields general forms of lifting.

Repeated lifting over the variables z_{n}, …, z_{1} allows resolution with the goal ⋀ z_{1} … z_{n}.θ.

A sample proof. Consider a proof of ∀z.G(z) ∨ H(z) from ∀z.G(z):

\frac{\frac{\frac{∀z.G(z)}{G(z)}}{G(z) ∨ H(z)}}{∀z.G(z) ∨ H(z)}

In the meta-proof, G and H are function variables. We may afterwards substitute ∀z.A for G and ∀z.B for H, where A and B are any formulae.

Working backwards, the first inference is ∀I. The first resolution instantiates F_{1} to λz.G(z) ∨ H(z):

\frac{(⋀ z . [[F_{1}(z)]]) ⇒ [[∀z.F_{1}(z)]] [[∀z.G(z) ∨ H(z)]] ⇒ [[∀z.G(z) ∨ H(z)]]}{(⋀ z . [[G(z) ∨ H(z)]]) ⇒ [[∀z.G(z) ∨ H(z)]]}

Here resolution must cope with function variables like F_{1}, determining the correct λabstraction and identifying terms that have the same normal form. For this Isabelle uses higher-order unification [19, 28]. The conclusion is normalized to eliminate β-redexes.

Observe that the goal G(z) ∨ H(z) must be proved for arbitrary z, a parameter. The next step uses the ∨I axiom, which becomes the meta-theorem (4) after lifting over z. Resolution with this produces the subgoal G(z):

\frac{(⋀ z.[[G_{2}(z)]]) ⇒ ⋀ z.[[G_{2}(z) ∨ H_{2}(z)]] (⋀ z.[[G(z) ∨ H(z)]]) ⇒ [[∀z.G(z) ∨ H(z)]]}{(⋀ z . [[G(z)]]) ⇒ [[∀z.G(z) ∨ H(z)]]}

The instantiations are G_{2} to G and H_{2} to H.

The next inference, ∀E, cannot easily be used backwards. Its conclusion, A[t/x], can match a goal in numerous ways. Higher-order unification of a term with F (y), where F and y are variables, yields many unifiers.^{3} Instead, work forwards. Making the assumption [[∀z.G(z)]], the ∀E axiom proves ⋀ y.[[G(y)]]. (Recall that we are deriving a rule, and therefore may assume its premise.) Lifting this theorem over z gives ⋀ f. ⋀ z . [[G(f(z))]].

\frac{⋀ z . [[G(f_{3}(z))]] (⋀ z . [[G(z)]]) ⇒ [[∀z.G(z) ∨ H(z)]]}{[[∀z.G(z) ∨ H(z)]]}

The final resolution replaces f_{3} by λz.z, and so

G(f_{3}(z)) ≡ G((λz.z)(z)) ≡ G(z)

This use of function variables is typical: the term f_{3}(z) states precisely its dependence on the context. The following sections give more examples.

3When this example was run, Isabelle did actually make the correct unifier its first choice.

Both kinds of lifting together. The goal ∀z . P (z) ⊃ P (z) ∨ Q(z) leads to the proof state

(⋀ z . [[P (z)]] ⇒ [[P (z) ∨ Q(z)]]) ⇒ [[∀z . P (z) ⊃ P (z) ∨ Q(z)]]

The next step requires both kinds of lifting: to lift the ∨I axiom over the assumption P (z) and then the variable z. The result after lifting is

⋀ GH . (⋀ z . P (z) ⇒ [[G(z)]]) ⇒ (⋀ z . P (z) ⇒ [[G(z) ∨ H(z)]])

The methods of this section and 4.3 work together to derive this sort of lifting.

6.2 Unification

Unification is a powerful aid for reasoning about quantification. We can prove a < b by proving a < c and c < b for some c. A procedure runs in linear time provided that, for some constant K, if the input has size n then the run time is Kn. Given ∀x.P (x) ∨ Q(x) we may argue by cases on whether P (a) or Q(a) holds, leaving a unspecified. Each of these cases involve unknowns: terms that must eventually be stated to complete the proof. Unification instantiates unknowns in goals.

Certain examples in first-order logic are especially helpful. Construct a proof of ∃xy.P (f(x), y) from ∀z.P (z, g(z)), considering how unification can determine the instantiations of x, y, and z. To exercise all the quantifier rules, prove ∀x.∃y.P (x, y) from ∃y.∀x.P (x, y) and try to prove the converse. Here we will work two simpler examples: a proof of ∀x.∃y . x = y, and an attempted proof of ∃y.∀x . x = y. These illustrate eigenvariable conditions.

The examples involve a reflexive equality relation, with the axiom ⋀ y . [[y = y]].

Resolution using unification. Resolution easily handles goals containing unknowns. Simply extend the meta-rule (1) of Section 4.2 to instantiate both premises, the object-rule and the proof state. If the substitution s satisfies ϕs ≡ ψs then

\frac{Φ ⇒ ϕ Ψ ⇒ ψ ⇒ θ}{Ψs ⇒ Φs ⇒ θs}

This resolution rule applies if s unifies ϕ and ψ. Resolution can affect variables throughout the proof state: Ψ becomes Ψs and θ becomes θs.

A successful proof. A first-order proof of ∀x.∃y . x = y is

\frac{\frac{x = x}{∃y . x = y}}{∀x.∃y . x = y}

The first resolution in the backwards proof of ∀x.∃y.x = y involves the ∀I axiom, instantiating F_{1} to λx.∃y . x = y:

\frac{(⋀ x . [[F_{1}(x)]]) ⇒ [[∀x.F_{1}(x)]] [[∀x.∃y . x = y]] ⇒ [[∀x.∃y . x = y]]}{(⋀ x . [[∃y . x = y]]) ⇒ [[∀x.∃y . x = y]]}

The meta-theorem (5) is the result of lifting the ∃I axiom over a variable. We use the lifted axiom here with different variable names. Resolution yields

\frac{(⋀ x . [[G_{2}(x, f_{2}(x))]]) ⇒ ⋀ x . [[∃y.G_{2}(x, y)]] (⋀ x . [[∃y.x = y]]) ⇒ [[∀x.∃y.x = y]]}{(⋀ x . [[x = f_{2}(x)]]) ⇒ [[∀x.∃y.x = y]]}

The variable G_{2} is instantiated to λxy . x = y, so the normal form of G_{2}(x, f_{2}(x)) is x = f_{2}(x).

Putting λx.x for f_{2} solves the subgoal, ⋀ x . [[x = f_{2}(x)]], by reflexivity. In the formal proof, this happens by lifting the reflexivity axiom over x and then resolving:

\frac{⋀ x . [[g_{3}(x) = g_{3}(x)]] (⋀ x . [[x = f_{2}(x)]]) ⇒ [[∀x.∃y . x = y]]}{[[∀x.∃y . x = y]]}

Consider the steps of higher-order unification [19, 28]. The initial disagreement pair is

⟨⋀ x . [[g_{3}(x) = g_{3}(x)]], ⋀ x . [[x = f_{2}(x)]]⟩

It reduces to the pairs ⟨λx.g_{3}(x), λx.x⟩ and ⟨λx.g_{3}(x), λx.f_{2}(x)⟩. The first pair forces g_{3}(x) to be λx.x; the second forces f_{2}(x) to be λx.x. This is a unifier: the common instance is ⋀ x . [[x = x]].

An unsuccessful proof. An attempt to prove ∃y.∀x . x = y is

\frac{\frac{x = t}{∀x . x = t}}{∃y.∀x . x = y}

Here t can be any term not containing x free. No such term satisfies x = t, so the top formula is false.

The first resolution in the attempted proof of ∃y.∀x.x = y involves the ∃I axiom:

\frac{[[F_{1}(y_{1})]] ⇒ [[∃x.F_{1}(x)]] [[∃y.∀x . x = y]] ⇒ [[∃y.∀x . x = y]]}{[[∀x . x = y_{1}]] ⇒ [[∃y.∀x . x = y]]}

The subgoal contains a new variable, y_{1}.

Resolution with the ∀I axiom gives

\frac{(⋀ x . [[F_{2}(x)]]) ⇒ [[∀x.F_{2}(x)]] [[∀x . x = y_{1}]] ⇒ [[∃y.∀x . x = y]]}{(⋀ x . [[ x = y_{1}]]) ⇒ [[∃y.∀x . x = y]]}

We are stuck. The subgoal ⋀ x . [[ x = y_{1}]] is false; no fixed y_{1} can equal every x. Resolution with the reflexivity axiom fails. The initial disagreement pair

⟨⋀ x . [[g_{3}(x) = g_{3}(x)]], ⋀ x . [[x = y_{1}]]⟩

reduces to the pairs ⟨λx.g_{3}(x), λx.x⟩ and ⟨λx.g_{3}(x), λx.y_{1}⟩. The first pair forces g_{3}(x) to be λx.x, reducing the second to ⟨λx.x, λx.y_{1}⟩, which has no unifier.

7 Other representations of eigenvariables

We have seen how to express most forms of Isabelle-86 proof construction as formal inference in a meta-logic. What about the Isabelle-86 treatment of eigenvariables?

Isabelle-86 does not use ⋀-lifting; it enforces eigenvariable conditions literally. The quantifier rule

\frac{Γ |− A(y)}{Γ |− ∀x.A(x)}

holds provided y is not free in Γ or A. (Isabelle-86 cannot handle natural deduction, so its object-logics are typically sequent calculi.) Isabelle-86 reduces Γ |− ∀x.A(x) to the subgoal Γ |− A(y), where y is a variable not previously used in the proof. Since two proofs must not be combined if they have eigenvariables in common, resolution renames all eigenvariables in its first premise. Isabelle-86 maintains the eigenvariable conditions — it accounts for assignments to variables in Γ and A, forbidding those that would introduce y into Γ or A.

The meta-logic M represents each inference rule as an implication. This fails if a premise has free variables. Subject to the usual conditions, the following inference is valid:

\frac{ϕ[y/x]}{⋀ x.ϕ}

The following implication is invalid:

ϕ[y/x] ⇒ ⋀ x.ϕ  (6)

Both cases involve implicit quantification over y, but with different scopes.

Replacing y by a special term can transform the implication (6) into a valid formula. For this, M is too weak a meta-logic, so let us temporarily adopt full higher-order logic.

7.1 Hilbert’s ϵ-operator

Church’s formulation of higher-order logic includes the Hilbert ϵ-operator: ϵx.ψ is a term for any formula ψ. It embodies a strong Axiom of Choice. If ψ is true for some value of x then ϵx.ψ denotes some such value; otherwise ϵx.ψ has an arbitrary value of the same type as x. (Recall that no type may denote the empty set.) An axiom scheme for the ϵ-operator is

⋀ x . ψ ⇒ ψ[(ϵx.ψ) / x]

Full higher-order logic has classical negation. Putting ¬ϕ for ψ, taking the contrapositive, and pushing the ⋀ x inwards, gives

ϕ[(ϵx.¬ϕ) / x] ⇒ ⋀ x.ϕ

So the special term to plug into the implication (6) is ϵx.¬ϕ: a value chosen to falsify ϕ, if such exists.

The term ϵx.¬ϕ contains the same free variables as ⋀ x.ϕ. For example, a theorem representing ∀I in first-order logic is

⋀ F . [[ F (ϵx . ¬[[F (x)]]) ]] ⇒ [[∀x.F (x)]]

where the variable F is free in ϵx . ¬[[F (x)]] but bound in the surrounding term. Specializing F to λx . g(x) = 0 yields the theorem

[[g(ϵx . ¬[[g(x) = 0]]) = 0]] ⇒ [[∀x . g(x) = 0]]

Specializing F to λx . G(x) ⊃ H(x) yields the theorem

[[G(ϵx . ¬[[G(x) ⊃ H(x)]]) ⊃ H(ϵx . ¬[[G(x) ⊃ H(x)]])]] ⇒ [[∀x . G(x) ⊃ H(x)]]

The term ϵx . ¬[[F (x)]] produces two different terms

ϵx . ¬[[g(x) = 0]] and ϵx . ¬[[G(x) ⊃ H(x)]]

Each eigenvariable is represented by a giant term: ϵx . ¬[[F (x)]] contains the formula F, which may contain other ϵ-terms. I tried this cumbersome representation in early versions of Isabelle, but no method of structure sharing would control the exponential growth.

7.2 Replacing Hilbert’s ϵ by special constants

Here is something similar to ϵ-terms but more practical. Extend higher-order logic with the axiom scheme

ϕ[y{ϕ} / x] ⇒ ⋀ x.ϕ  (7)

We simply postulate constants to satisfy the implication (6). For each ϕ there is a unique constant y{ϕ} not free in ϕ. This is Henkin’s technique for reducing first-order logic to propositional logic [5, page 30]. Its main application is the Completeness Theorem; here it extends our propositional proof methods to first-order logic.

The simplest representation of y{ϕ} is to regard ϕ as part of the name, but this is as cumbersome as ϵ-terms. Enumerating names like y{609} (Lisp’s gensym) does not work if ⋀ x.ϕ contains free variables: substitution could create distinct instances of (7), and even introduce occurrences of y{609} in ⋀ x.ϕ. We must make certain that one constant is not used for different instances of (7) in a proof.

Taking the free variables of ⋀ x.ϕ as part of the name, and updating them, provides an automatic renaming mechanism — precisely that of Isabelle-86. Thus y{ϕ} should be written y{z_{1}, …, z_{n}}, where z_{1},…,z_{n} are the free variables of ⋀ x.ϕ. The only way to introduce occurrences of y{ϕ} into ⋀ x.ϕ is to instantiate some free variable z_{i} with y{z_{1}, …, z_{n}}. This is prevented by the occurs check in unification.

The ϵ-terms can express functions like λx . ϵy . ψ, which maps x to some y such that ψ holds. But y{z_{1}, …, z_{n}} is a constant — so z_{1}, …, z_{n} must not be bound in the surrounding term. This restricts the generalization rule (⋀-introduction) to variables not mentioned by special constants. Instead we can use the instantiation rule,

\frac{ϕ}{ϕ[a_{1}/x_{1}, …, a_{k}/x_{k}]}

where the variables x_{1}, …, x_{k} must not be free in the assumptions. In M the rule follows by generalization and specialization, but here it must be taken as primitive. In each special constant, x_{i} is replaced by all free variables of a_{i}.

The ∀I axiom becomes

[[F (y{F })]] ⇒ [[∀x.F (x)]]

Note that there is no ⋀ F: since the variable F is mentioned by the constant y{F }, it must be free in the axiom. However, we may replace F by a term, creating a new special constant. Replacing F by λx . g(x) = 0 yields the theorem

[[g(y{g}) = 0]] ⇒ [[∀x . g(x) = 0]]

Replacing F by λx.G(x) ⊃ H(x) yields the theorem

[[G(y{G, H}) ⊃ H(y{G, H})]] ⇒ [[∀x.G(x) ⊃ H(x)]]

The theorems contain different constants y{g} and y{G, H}: thus y{F } is automatically renamed.

Compare these with the ϵ-term examples. Keeping just the free variables of F, rather than F itself, prevents the exponential growth.

7.3 Lifting versus special constants

Redoing the examples from Section 6.2 illustrates how special constants work.

A successful proof. The first resolution in the backwards proof of ∀x.∃y . x = y involves the ∀I axiom:

\frac{[[F_{1}(x\{F_{1}\})]] ⇒ [[∀x.F_{1}(x)]] [[∀x.∃y . x = y]] ⇒ [[∀x.∃y . x = y]]}{[[∃y . x\{\} = y]] ⇒ [[∀x.∃y . x = y]]}

Here F_{1} is assigned λx.∃y . x = y, which has no free variables. Thus the special constant x{} in the conclusion has no variables.

Next we resolve with the ∃I axiom:

\frac{[[F_{2}(y_{2})]] ⇒ [[∃x.F_{2}(x)]] [[∃y . x\{\} = y]] ⇒ [[∀x.∃y . x = y]]}{[[ x\{\} = y_{2}]] ⇒ [[∀x.∃y . x = y]]}

The function variable F_{2} is instantiated to λy .x{} = y, so the normal form of F_{2}(y_{2}) is x{} = y_{2}.

Resolving the proof state with the reflexivity axiom sets y_{2} to x{}, completing the proof:

\frac{[[x_{3} = x_{3}]] [[ x\{\} = y_{2}]] ⇒ [[∀x.∃y . x = y]]}{[[∀x.∃y . x = y]]}

A unsuccessful proof. The first step in the attempted proof of ∃y.∀x . x = y is the same as before:

\frac{[[F_{1}(y_{1})]] ⇒ [[∃x.F_{1}(x)]] [[∃y.∀x . x = y]] ⇒ [[∃y.∀x . x = y]]}{[[∀x . x = y_{1}]] ⇒ [[∃y.∀x . x = y]]}

Resolution with the ∀I axiom gives

\frac{[[F_{2}(x\{F_{2}\})]] ⇒ [[∀x.F_{2}(x)]] [[∀x . x = y_{1}]] ⇒ [[∃y.∀x . x = y]]}{[[x\{y_{1}\} = y_{1}]] ⇒ [[∃y.∀x . x = y]]}

The instantiation of F_{2} is λx . x = y_{1}, which contains free variable y_{1}: hence the special constant x{y_{1}} in the conclusion. The subgoal [[x{y_{1}} = y_{1}]] cannot be solved because the instantiation of y_{1} to x{y_{1}} would be circular. These terms are not unifiable.

Parallel derivations. A final example will compare ⋀-lifting with special constants. The main goal, ψ, is

[[∃u.∀x.∃v.∀y.∃w.P (u, x, v, y, w)]]

Each state in the backwards proof has one subgoal. Here are the derivations for both styles, in parallel:

lifting  special constants
[[∀x.∃v.∀y.∃w.P (a, x, v, y, w)]] ⇒ ψ  [[∀x.∃v.∀y.∃w.P (a, x, v, y, w)]] ⇒ ψ
(⋀ x.[[∃v.∀y.∃w.P (a, x, v, y, w)]]) ⇒ ψ  [[∃v.∀y.∃w.P (a, x{a}, v, y, w)]] ⇒ ψ
(⋀ x.[[∀y.∃w.P (a, x, f(x), y, w)]]) ⇒ ψ  [[∀y.∃w.P (a, x{a}, b, y, w)]] ⇒ ψ
(⋀ xy.[[∃w.P (a, x, f(x), y, w)]]) ⇒ ψ  [[∃w.P (a, x{a}, b, y{a, b}, w)]] ⇒ ψ
(⋀ xy.[[P (a, x, f(x), y, g(x, y))]]) ⇒ ψ  [[P (a, x{a}, b, y{a, b}, c)]] ⇒ ψ

In the sequence of states new symbols appear one by one: the free variable a, the parameter x, the free variable f or b, the parameter y, and the free variable g or c. Consider the final meta-theorem (the last line above):

lifting  special constants

The variable a cannot be assigned a term containing x or y free because x and y are bound variables.

The variable a cannot be assigned a term containing x{a} or y{a, b} because a is free in these constants.

Assigning λx.b to f replaces the term f(x) by b, which may contain x free but not y.

The variable b cannot be assigned a term containing y{a, b}, for this constant contains b.

Assigning λxy.c to g replaces the term g(x, y) by c, which may contain x and y free.

The variable c can be assigned a term containing x{a} or y{a, b}, for c is free in neither constant.

Special constants raise many questions. When is the name of a special constant significant, and what is its scope? Does the axiom scheme (7) entail classical logic or the Axiom of Choice? With lifting, the status of parameters is clear. They can be renamed by α-conversion. The scope of a parameter is its goal. Here is a proof state with two subgoals:

(⋀ x.ϕ) ⇒ (⋀ y.θ) ⇒ ψ

The scope of x is the first goal and that of y is the second.

Lifting is clearly preferable — especially because it works in the simple metalogic M. Higher-order unification easily copes with the additional function variables like f and g above.

8 An implementation

This research has always been concerned with implementation issues, of which the main one is how to represent a logic. I have criticized lcf for representing inference rules as functions, preferring visible structures [28]. But colleagues have pointed out that such structures are essentially the theorems of a (meta) logic, and the functions that manipulate them are (meta) rules. Thus Isabelle adopts lcf’s representation at the meta-level.

Object-rules in Isabelle-86 are expressed in the typed λ-calculus and have the familiar pattern of premises over conclusion. Free variables and special constants give the effect of weak quantification. Written in M, the general form of an Isabelle-86 rule is something like

(⋀ y_{1}.ϕ_{1}) ⇒ ⋯ ⇒ (⋀ y_{m}.ϕ_{m}) ⇒ ϕ

Below the level of rules, Isabelle operates on terms: substitution, normalization, higher-order unification, parsing and printing. Above, Isabelle is concerned with backwards proof: tactics and tacticals. Above pure Isabelle come the object-logics with their special tactics.

M. J. C. Gordon uses higher-order logic as a specification language for hardware. His hol theorem prover [13] has supported several large proofs about circuit designs [6]. Since hol is based on lcf, it may seem to be the obvious starting point for a version of Isabelle based on M. However hol and Isabelle support distinct methods of use, giving conflicting design requirements. I obtained the current version of Isabelle by modifying Isabelle-86. Only the level of rules needed substantial change; the lower levels were slightly modified and the higher levels hardly at all.

The natural deduction rules of M are represented by the corresponding sequent calculus. A meta-theorem has the form Ψ |− ϕ, where ϕ depends on the assumptions Ψ, and expresses object-rules using ⋀ and ⇒. Lifting and resolution are coded directly; implementing them by execution of primitive rules would be painfully slow.

Isabelle now uses ⋀-lifting instead of special constants. Despite having quantifiers, Isabelle provides a separate class of schematic variables^{4} — free variables intended for substitution. Why have two kinds of free variables? Consider trying to prove

4‘Logical variables’ in prolog jargon.

[[(∃z.F (z)) & B]] ⇒ [[∃z.F (z) & B]]

which expresses a derived rule about ∃ and &. In the proof, the free variables F and B are fixed while the rightmost existential quantifier produces a schematic variable that must eventually be replaced by a term. The meta-rules ensure that every theorem Ψ |− ϕ has no schematic variables in Ψ; instantiation only affects schematic variables.

Object-logics include intuitionistic first-order logic, Martin-Löf’s Constructive Type Theory (ctt) [23] and a first-order sequent calculus similar to lk [36]. The Isabelle-86 logics were easily adapted to the new Isabelle. The most drastic change in the representation of proofs, ⋀-lifting, was the main source of problems. But many things worked immediately, including the object-logics’ specialized proof procedures. The Isabelle-86 logics were sequent calculi, but most now have a simpler formulation using natural deduction. Sequent calculi are mainly suitable for classical logic [32, page 245].

All proofs in this paper are in single steps. But Isabelle provides tacticals (resembling lcf’s) for joining simple proof procedures into complex ones. Constructive Type Theory has a rewriting tactic that works by executing a ‘logic program’ derived from ctt rules. This tactic is heavily used in the largest ctt example, which develops elementary number theory up to the theorem

a mod b + (a/b) × b = a

The first-order sequent calculus has an automatic proof procedure that performs associative unification using higher-order unification [20, page 37]. The procedure is not complete but it saves many steps in interactive proof and works with any convenient mixture of primitive and derived rules. Using derived rules about set theory, Isabelle can prove theorems like

c ≠ ∅ |− ⋂_{x∈c}(f(x) ∩ g(x)) = ( ⋂_{x∈c} f(x)) ∩ ( ⋂_{x∈c} g(x))

Huet’s unification procedure [19] may return, with a unifier, unsolved disagreement pairs ⟨a_{1}, b_{1}⟩, …, ⟨a_{m}, b_{m}⟩. When this happens, the pairs have at least one and perhaps infinitely many unifiers. To avoid enumerating these unifiers the disagreement pairs can be kept to constrain future unifications. (This is Huet’s key observation, which makes his procedure practical.) Isabelle-86 stores with each derived rule ϕ its unsolved disagreement pairs. Isabelle now expresses these using equality:

a_{1} ≡ b_{1} ⇒ ⋯ ⇒ a_{m} ≡ b_{m} ⇒ ϕ

Equality also replaces the Isabelle-86 definition mechanism. The meta-axiom K ≡ a defines the constant K. We can then unfold K to a, or fold a back to K. This is more sensible than automatically unfolding all constants.

See the User’s Manual for more detailed information about Isabelle [30].

9 Related work

De Bruijn’s automath is an early attempt (begun in 1966) to develop a formal language of mathematics [7]. The automath languages are meant to appear natural to mathematicians while allowing the computer checking of proofs. Coquand and Huet’s Calculus of Constructions [9] is similar but has a different treatment of abbreviations and context. Both are extended typed λ-calculi providing the Cartesian product of a family of types.^{5}

Many pieces of mathematics have been computer checked in automath [21] and the Constructions [10]. The mathematician specifies all items of discourse — including the logical constants — by writing axioms and definitions. The calculi can express classical reasoning, constructive reasoning, and various shades in between. But the properties of the logical constants may be unclear, for their definitions are technical.

Is there a clear, uniform formalization of logic? Martin-Löf’s theory of expressions represents the syntax of his Constructive Type Theory. It is essentially Church’s typed λ-calculus, which represents the syntax of higher-order logic. So Isabelle has always represented object-theorems in the typed λ-calculus. But what about the representation of rules? Initially I adopted an obvious form of inference rule, without fully developing the concept. As it happened, Schroeder-Heister had already done so.

With Schroeder-Heister’s rules of higher levels, a rule may be the premise of another rule. This extends natural deduction: assumptions may be (higher level) rules, not just formulae [33]. Schematic variables in a rule express quantification [34]. Unfortunately, propositional logic requires a complicated treatment of assumption discharge, while the full conception is extremely complex. The meta-logic M is perhaps a rendering of Schroeder-Heister’s work into a more convenient and familiar notation.

Martin-Löf has formulated a general concept of rule [24]. In a notation resembling automath’s he has produced succinct descriptions of first-order logic and Constructive Type Theory [25]. Most recently, people at the University of Edinburgh have elaborated Martin-Löf’s ideas into the Edinburgh Logical Framework [15], and formalized diverse logics [3].

automath and its descendants exploit the interpretation of propositions-as-types. Each proposition A is interpreted as the type (or set) Ã of proof objects, and A is true if it has a proof object, namely if there exists a : Ã. Here is a summary of propositions-as-types [18, 27]:

• Absurdity (⊥) is interpreted as the empty type.

• A proof object of A & B consists of a pair ⟨a, b⟩, where a is a proof object of A and b is a proof object of B — namely where a : Ã and b : B̃. Thus A & B is interpreted as the Cartesian product Ã × B̃.

5The so-called ‘dependent product’ or ‘dependent function space’

• A proof object of A ∨ B contains either a proof object of A or else a proof object of B, and an indication of which. Thus A ∨ B is interpreted as the disjoint union Ã + B̃.

• A proof object of A ⊃ B consists of a function f such that if a is a proof object of A then f(a) is a proof object of B — namely if a : Ã then f(a) : B̃. Thus A ⊃ B is interpreted as the function type Ã → B̃.

• A proof object of ∀x:A . B(x) consists of a function f such that if a belongs to A then f(a) is a proof object of B(a), namely if a : A then f(a) : B̃(a). Thus ∀x:A . B(x) is interpreted as the type Πx:A . B̃(x), the product of the family of types {B̃(x)}_{x:A}.

Observe that if the type B does not involve x then {B}_{x:A} is the constant family, and the product Πx:A . B is the function type A → B. But the A in A ⊃ B is a set Ã of proof objects, while the A in ∀x:A . B(x) typically is an ordinary set, like the natural numbers. Calculi like automath are expressive and yet compact, for Π encompasses function types, implication, and universal quantification.

The meta-logic M, based on higher-order logic, is strikingly different. Its function types σ → τ, implications ϕ ⇒ ψ, and universal quantifications ⋀ x.ϕ are independent. Recall how each is used to formalize propositional logic. The type of the constant & indicates that it is a function on truth values. The axioms about & express properties of that function.

& : form → (form → form) ⋀ AB . [[A]] ⇒ ([[B]] ⇒ [[A & B]])

Propositions-as-types seems to offer advantages. Observe that ⋀-lifting and ⇒- lifting would become simply Π-lifting. The richer type system allows a neat formalization of typed object-logics: the type term(T) might represent the set of terms of object-type T. The formalization of a typed logic in M involves a type of all object-terms, including those of no legal object-type; object-level type checking requires additional rules for type inference. My choice of an old-fashioned calculus for Isabelle reflects practical considerations.

Under propositions-as-types, the formal proof of the proposition A consists of a proof of a : Ã, where a is a proof object. A proof object is smaller than a standard proof tree (which contains repeated subformulae) yet still can grow large. Following the lcf tradition, Isabelle has never stored the steps of proofs. Milner’s representation of logic makes stored proofs unnecessary, a vital space savings. Now some people regard this as a mistake. Martin-Löf’s Type Theory exploits propositions-as-types; its proof objects constitute a functional programming language; the theorem prover Nuprl can execute them [8]. The proof objects of ordinary logics may be useful in proof editors.

Isabelle is intended for verifications involving hundreds of proofs, each involving hundreds of steps. Isabelle must support a degree of automation, and this requires unification. Propositions-as-types could consume excessive space; and what would take the place of Huet’s unification procedure for higher-order logic [19]?

\begin{matrix}\frac{\frac{∀x.A}{A}}{∃x.A} & \frac{\frac{∀x.A}{A[0/x]}}{∃x.A} \\ (a) & (b) \end{matrix}

Figure 10: Two proofs of ∃x.A from ∀x.A

The choice of meta-logic can have subtle consequences stemming from the semantics. In M every type denotes a non-empty set; under propositions-as-types there must be an empty type. Standard first-order logic assumes a non-empty universe, and so ∀x.A implies ∃x.A. The meta-logic M can represent the standard proof, Figure 10(a). Avron et al. [3] suggest that deriving this in their formalization of first-order logic requires a constant, say 0. Their proof presumably represents that of Figure 10(b).

A logic for the formalization of mathematics must presuppose the very minimum. Philosophers have debated whether a logic must be predicative — free of ‘vicious circles’ [37, page 37]:

The vicious circles in question arise from supposing that a collection of objects may contain members which can only be defined by means of the collection as a whole. Thus, for example, the collection of propositions will be supposed to contain a proposition stating that “all propositions are either true or false.” It would seem, however, that such a statement could not be legitimate unless “all propositions” referred to some already definite collection, which it cannot do if new propositions are created by statements about “all propositions.” We shall, therefore, have to say that statements about “all propositions” are meaningless.

Whitehead and Russell’s ramified type theory is the ancestor of Church’s simple type theory (higher-order logic), which is impredicative. The simplest impredicative formula is ⋀ θ.θ, a definition of absurdity: all propositions are true. The disjunction ϕ ∨ ψ is equivalent to

⋀ θ . (ϕ ⇒ θ) ⇒ (ψ ⇒ θ) ⇒ θ

Leibniz’s definition of equality, x = y if y has every property of x, involves quantification over propositional functions: ⋀ ϕ . ϕ(x) ⇒ ϕ(y).

Most of the other calculi are predicative and intuitionistic. To make M predicative, we can forbid bound variables whose type involves prop. The resulting system is much weaker but can still serve as a meta-logic, which requires only quantification over object-formulae. Its proof theory is as simple as that of first-order logic.

Amy Felty and Dale Miller [12] have formalized several logics in a logic programming language based on hol. Logically their formalizations resemble those in Sections 3 and 5, but also express search procedures involving tactics and tacticals. Felty and Miller compare these with the usual approach of programming tactics in ml. They claim that the Edinburgh Logical Framework can be easily translated into higher-order logic.

Higher-order logic makes an adequate meta-logic from the theoretical perspective. We can draw on established proof theory to demonstrate soundness and completeness of the formalization of first-order logic: compare with the argument in Harper et al. [15]. The implementation, Isabelle, demonstrates its practical strengths. Basing Isabelle’s reasoning methods on a precise calculus has already lead to extensions such as hypothetical rules. It is shedding light on issues such as theory structure.

Acknowledgements. Thierry Coquand contributed greatly to this research, which owes much to Michael Gordon’s work on higher-order logic. David Matthews has continued to support his ml compiler. Philippe de Groote wrote the Isabelle-86 version of lk. Brian Monahan, David Wolfram and the referee commented on the paper. Thanks also to Peter Dybjer, Furio Honsell, Martin Hyland, Philippe Noël, and the editor. The serc provided funding under grant GR/E0355.7.

References

[1] P. B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof (Academic Press, 1986).

[2] P. B. Andrews, D. A. Miller, E. L. Cohen, and F. Pfenning, Automating higherorder logic, in: W. W. Bledsoe and D. W. Loveland, editors, Automated Theorem Proving: After 25 Years (American Mathematical Society, 1984), pages 169–192.

[3] A. Avron, F. A. Honsell, and I. A. Mason, Using typed lambda calculus to implement formal systems on a machine, Report ecs-lfcs-87-31, Computer Science Department, University of Edinburgh (1987).

[4] J. Barwise, editor, Handbook of Mathematical Logic (North-Holland, 1977).

[5] J. Barwise, An introduction to first-order logic, in: Barwise [4], pages 5–46.

[6] G. Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis (Kluwer Academic Publishers, 1988).

[7] N. G. de Bruijn, A survey of the project automath, in: Seldin and Hindley [35], pages 579–606.

[8] R. L. Constable et al., Implementing Mathematics with the Nuprl Proof Development System (Prentice-Hall, 1986).

[9] Th. Coquand and G. Huet, The calculus of constructions, Information and Computation 76 (1988), pages 95–120.

[10] Th. Coquand and G. Huet, Constructions: a higher order proof system for mechanizing mathematics, in: B. Buchberger, editor, eurocal ’85: European Conference on Computer Algebra, Volume 1: Invited lectures (Springer, 1985), pages 151–184.

[11] M. Dummett, Elements of Intuitionism (Oxford University Press, 1977).

[12] A. Felty and D. Miller, Specifying theorem provers in a higher-order logic programming language, in: E. Lusk and R. Overbeek, editors, Ninth International Conference on Automated Deduction (Springer Lecture Notes in Computer Science 310, 1988), pages 61–80.

[13] M. J. C. Gordon, hol: A proof generating system for higher-order logic, in: Birtwistle and Subrahmanyam [6], pages 79–128.

[14] Ph. de Groote, How I spent my time in Cambridge with Isabelle, Report RR 87-1, Unité d’informatique, Université Catholique de Louvain, Belgium (1987).

[15] R. Harper, F. Honsell and G. Plotkin, A Framework for Defining Logics, Symposium on Logic in Computer Science (ieee Computer Society Press, 1987), pages 194–204.

[16] J. R. Hindley and J. P. Seldin, Introduction to Combinators and λ-Calculus (Cambridge University Press, 1986).

[17] C. A. R. Hoare and J. C. Shepherdson, editors, Mathematical Logic and Programming Languages (Prentice-Hall, 1985).

[18] W. A. Howard, The formulae-as-types notion of construction, in: Seldin and Hindley [35], pages 479–490.

[19] G. P. Huet, A unification algorithm for typed λ-calculus, Theoretical Computer Science 1 (1975), pages 27–57.

[20] G. P. Huet and B. Lang, Proving and applying program transformations expressed with second-order patterns, Acta Informatica 11 (1978), pages 31–55.

[21] L. S. Jutting, Checking Landau’s ‘Grundlagen’ in the automath system (PhD Thesis, Technische Hogeschool, Eindhoven, 1977).

[22] J. Lambek and P. J. Scott, Introduction to Higher Order Categorical Logic (Cambridge University Press, 1986).

[23] P. Martin-Löf, Constructive mathematics and computer programming, in: Hoare and Shepherdson [17], pages 167–184.

[24] P. Martin-Löf, On the meanings of the logical constants and the justifications of the logical laws, Report, Department of Mathematics, University of Stockholm (1986).

[25] P. Martin-Löf, Amendment to intuitionistic type theory, Lecture notes obtained from P. Dybjer, Computer Science Department, Chalmers University, Gothenburg (1986).

[26] R. Milner, The use of machines to assist in rigorous proof, in: Hoare and Shepherdson [17], pages 77–88.

[27] B. Nordström and J. M. Smith, Propositions and specifications of programs in Martin-Löf’s type theory, BIT 24 (1984), pages 288–301.

[28] L. C. Paulson, Natural deduction as higher-order resolution, Journal of Logic Programming 3 (1986), pages 237–258.

[29] L. C. Paulson, Logic and Computation: Interactive Proof with Cambridge LCF (Cambridge University Press, 1987).

[30] L. C. Paulson, A preliminary user’s manual for Isabelle, Report 133, Computer Laboratory, University of Cambridge (1988).

[31] D. Prawitz, Natural Deduction: A Proof-theoretical Study (Almquist and Wiksell, 1965).

[32] D. Prawitz, Ideas and results in proof theory, in: J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium (North-Holland, 1971), pages 235–308.

[33] P. Schroeder-Heister, A natural extension of natural deduction, Journal of Symbolic Logic 49 (1984), pages 1284–1300.

[34] P. Schroeder-Heister, Generalized rules for quantifiers and the completeness of the intuitionistic operators &, ∨, ⊃, ⊥, ∀, ∃, in: M. M. Richter et al., editors, Logic Colloquium ’83 (Springer Lecture Notes in Mathematics 1104, 1984).

[35] J. P. Seldin and J. R. Hindley, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (Academic Press, 1980).

[36] G. Takeuti, Proof Theory (second edition) (North Holland, 1987).

[37] A. N. Whitehead and B. Russell, Principia Mathematica (Paperback edition to *56, Cambridge University Press, 1962).