Machine Checking Proof Theory: an application of logic to logic

Rajeev Goré

Computer Sciences Laboratory The Australian National University Canberra

                          rajeev.gore@anu.edu.au

Abstract. Modern proof-assistants are now mature enough to formalise many aspects of mathematics. I outline some work we have done using the proof-assistant Isabelle to machine-check aspects of proof theory in general, and specifically the proof theory of provability logic GL.

1 Motivation

Proof theory, broadly construed, is the study of derivations as first-class objects. Typically, we study a proof-calculus which captures the notion that a particular formula A is deducible from a given finite collection Γ of assumption formulae in some given logic L: usually written as Γ ⊢_{L} A. Typical such calculi are Gentzen’s Sequent Calculi, Natural Deduction Calculi or Hilbert Calculi.

But proof theory is error prone. There are numerous examples of published “proofs” in proof theory which have turned out to be incorrect at a later date. These errors often lie undiscovered for years, usually until some diligent Phd student actually tries to work through the proofs in detail and discovers a bug. I give a concrete example later.

Part of the problem is that conferences and journal typically enforce page limits, so that authors are forced to elide full details. Another cause is that proof-theoretical proofs typically contain many similar cases, and humans are notoriously bad at carrying out repetitive tasks with precision. Thus authors often resort to words like “the other cases are similar”. But sometimes the errors are very subtle, and are not just a matter of routine checking.

Proof-theoretic proofs often proceed by induction since derivations are usually structured objects like lists, trees or graphs.

Proof assistants are computer programs which allow a user to encode and check proofs written using a special syntax and interface. They have a long history going back to the early 1970s, are usually based upon an encoding of higher-order logic into some extension of Church’s typed λ-calculus, and are now an exciting and mature area of research. Indeed, there is now a strong movement to “formalise mathematics” using computers as exemplified by Tom Hales’ project to formally verify his “proof” of the Kepler Conjecture http:

//code.google.com/p/flyspeck/.

Most modern proof-assistants allow us to define infinite sets using inductive definitions. Most also automatically generate powerful induction principles for proving arbitrary properties of such sets.

Given that proof-theory is error-prone and that it typically utilises proofs by induction, can we use modern proof-assistants to help us machine-check proof theory?

An Oath: I have only a limited amount of time and I need to cover a lot of background material. I also want to show you some actual code that we have developed, but I wish to simplify it to hide unimportant details. So here is an oath: I will tell the truth, I may not tell the whole truth, but I won’t lie. So complain immediately if you see something blatantly incorrect!

Acknowledgements: Most of the work reported here has been done in collaboration with Jeremy E Dawson. He is a perfect example of a serious mathematician who checks all of his proofs in Isabelle ... just to be sure.

2 Proof Theory: Purely Syntactic Calculi for L-Deduction

To begin with the basics, I just want to talk briefly about the proof-calculi we typically study.

We typically work with judgements of the form Γ ⊢_{L} Δ where Γ and Δ are “collections” of formulae. I deliberately want to leave vague the exact definition of “collection” for now: think of it as some sort of data-structure for storing information.

From these judgements, we usually define rules, and form a calculus by assembling a finite collection of such rules.

A rule typically has a rule name, a (finite) number of premises, a sidecondition and a conclusion as shown below:

Γ_{1} ⊢_{L} Δ_{1}  ⋯  Γ_{n} ⊢_{L} Δ_{n}
RuleName  Condition
Γ_{0} ⊢_{L} Δ_{0}

We read the rules top-down as statements of the form “if premises hold then conclusion holds”, again deliberately using the imprecision of “holds” rather than something more exact.

A derivation of the judgement Γ ⊢_{L} Δ is typically a finite tree of judgements with root Γ ⊢_{L} Δ where parents are obtained from children by “applying a rule”. From now on, I will usually omit L to reduce clutter.

Figure 1 shows some typical rules from the literature:

Gentzen’s LK: in some formulations uses rules built from multisets, but it can also be easily turned into a calculus which uses sets. LK has a particularly pleasing property in that in all its rules, the components of the premises like A and B are subformulae of the components of the conclusion like A → B;

Calculus  Example Rule  Collection
LK  \begin{aligned}Γ, B ⊢ Δ & Γ ⊢ A, Δ \\ (→ L) \\ & Γ, A → B ⊢ Δ \end{aligned}  sets of formulae

LJ  \begin{aligned}Γ, A → B ⊢ A & Γ, B ⊢ C \\ (→ L) \\ & Γ, A → B ⊢ C \end{aligned} multisets + SOR

ND  \begin{aligned}Γ ⊢ K & Γ, K ⊢ M \\ (\{.\}_{.}I) \\ & Γ ⊢ \{M\}_{K} \end{aligned}  multisets + SOR

NL  \begin{aligned}Δ ⊢ A & Γ [B] ⊢ C \\ (\L) \\ & Γ [(Δ, A \ B)] ⊢ C \end{aligned}  trees with holes

DL  \begin{aligned}X ⊢ A & B ⊢ Y \\ (→ L) \\ & A → B ⊢ (∗X) ∘ Y \end{aligned}  complex trees

Fig. 1. Example of Rules of Some Existing Calculi

Gentzen’s LJ: uses sequents built from multisets, with an added condition that the right hand side must consist of at most one formula. The particular formulation shown also carries its principal formula A → B from the conclusion into one of its premises, which can be used to show that the contraction rule is redundant;

ND for Security Protocols: Natural deduction calculi have been used to reason about security protocols. This rule captures the idea that the ability to decode the key K and the ability to decode a message M using that key, allows us to decode M even when it is encrypted with key K;

NL: The non-associative Lambek calculus uses sequents built from trees containing “holes”. The rule allows us to replace the formula B in a hole inside the tree Γ, with a more complex subtree built from the tree Δ and the formula A \ B;

Display Logic: Belnap’s display logic uses sequents built from complex structural connectives like ∗ and ∘ so that its sequents are akin to complex trees.

Thus there are many different notions of “sequent”. Our hope is to encode the proofs about such sequents in a modern proof-assistant, specifically Isabelle.

3 Applying A Rule: Example Derivation In Gentzen’s LK

In almost all cases, we build derivations in a top-down manner, starting from leaves which are instances of Γ, p ⊢ p, Δ by “applying” a rule. Rule application typically proceeds using pattern-matching as exemplified by the following derivation from Gentzen’s LK.

Example 1. Here, Γ, A means “Γ multiset-union A”.

\begin{aligned}& Γ, A, B ⊢ Δ \\ (∧ ⊢) \\ & Γ, A ∧ B ⊢ Δ \end{aligned}  \begin{aligned}Γ ⊢ A, Δ & Γ, B ⊢ Δ \\ (→⊢) \\ & Γ, A → B ⊢ Δ \end{aligned}
p_{0} ⊢ p_{0}, q_{0}  p_{0}, q_{0} ⊢ q_{0} (→⊢) p_{0}, (p_{0} → q_{0}) ⊢ q_{0} (∧ ⊢) p_{0} ∧ (p_{0} → q_{0}) ⊢ q_{0}

The first rule instance (→⊢) utilises the substitutions Γ := {p_{0}}, A := p_{0}, B := q_{0} and Δ := {q_{0}}.

The second rule instance (∧ ⊢) utilises the substitutions Γ := ∅, A := p_{0}, B := p_{0} → q_{0} and Δ := {q_{0}}.

The example also illustrates the use of sequent calculi as “backward chaining” decision procedures where we can find a derivation starting from p_{0}∧(p_{0} → q_{0}) ⊢ q_{0} and applying the rules in a systematic way “backwards” towards the leaves.

For propositional LK, decidability follows almost immediately by observing that in every such “backward” rule application, at least one formula disappears from the sequents, and is replaced by strictly smaller formulae only. Thus, every branch of rule applications must terminate.

More generally, we typically find some numerical measure which strictly decreases when “reducing” a conclusions to its premises. Indeed, the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, to be held next in Oslo, is dedicated to research aimed at automating reasoning in various non-classical logics using this technique. Some of us have even made a career out of this endeavour!

Notice that the structure of “collections” is significant. For example, the structural rule of contraction shown below at left using multisets is well-defined, with a typical instance shown below at right:

\begin{aligned}& Γ, A, A ⊢ Δ \\ (Ctr) \\ & Γ, A ⊢ Δ \end{aligned}  \begin{aligned}p_{0}, p_{0} ⊢ q_{0} \\ & (Ctr) \\ p_{0} ⊢ q_{0} \end{aligned}

Similarly, the following contraction lemma is well-defined:

If Γ, A, A ⊢ Δ is derivable then so is Γ, A ⊢ Δ.

But neither makes sense in a setting where sequents are built from sets since the rule instance shown below at left collapses to identity.

\begin{aligned}p_{0}, p_{0} ⊢ q_{0} \\ & (Ctr) \\ p_{0} ⊢ q_{0} \end{aligned}  \{p_{0}\} ⊢ \{q_{0}\} ; identity ; \{p_{0}\} ⊢ \{q_{0}\}

Similarly, the contraction lemma is meaningless since Γ ∪ {A} ∪ {A} ⊢ Δ is the same as Γ ∪ {A} ⊢ Δ.

Although automated reasoning is an important application of sequent calculi, most uses of proof theory are meta-theoretic. For example, proof theory is typically used to answer questions like the following:

Consistency: ∅ ⊢_{L} A and ∅ ⊢_{L} ¬A are not both derivable; Disjunction Property: If ∅ ⊢_{Int} A ∨ B then ∅ ⊢_{Int} A or ∅ ⊢_{Int} B; Craig Interpolation: If Γ ⊢_{L} Δ holds then so do Γ ⊢_{L} A and A ⊢_{L} Δ for some

formula A with Vars(A) ⊆ Vars(Γ) ∩ Vars(Δ); Normal Forms: Is there a (unique) normal form for derivations ? Curry-Howard: Do normal derivations correspond to well-typed terms of some

λ-calculus ? Equality: When are two derivations of Γ ⊢_{L} A equivalent ? Relative Strengths: Every derivation in ⊢_{1} can be simulated polynomially by a

derivation in ⊢_{2}

The methods used usually involve reasoning about derivations rather than finding derivations, as exemplified by the following lemmas:

Identity: The judgement A ⊢ A is derivable for all A. Monotonicity: If Γ ⊢ Δ is derivable then so is Γ, Σ ⊢ Δ. Exchange: If Γ, A, B ⊢ Δ is derivable then so is Γ, B, A ⊢ Δ. Contraction: If Γ, A, A ⊢ Δ is derivable then so is Γ, A ⊢ Δ. Inversion: If the conclusion of a rule instance is derivable then so are the corre-

sponding premise instances. Cut-elimination/-admissibility: If Γ ⊢ A, Δ is (cut-free) derivable and Γ, A ⊢ Δ

is (cut-free) derivable then so is Γ ⊢ Δ, where the cut rule is:

Γ ⊢ A, Δ  Γ, A ⊢ Δ (cut) Γ ⊢ Δ

Weak/Strong Normalisation: Algorithm to transform a derivation into a normal

form by eliminating topmost/nested cuts ? Cost: How much bigger is the transformed derivation?

4 Proof Theory Is Error-Prone: Provability Logic GL

To illustrate the fact that proof-theory is error-prone, I would like to describe the history of the cut-elimination theorem for a propositional modal logic called GL, after Gödel-Löb.

The logic GL has an Hilbert axiomatisation which extends the standard axiomatisation for modal logic K by adding Löb’s axiom □(□A → A) → □A. It rose to prominence when Solovay showed that □A could be interpreted as “A is provable in Peano Arithmetic” [7]. An initial proof-theoretic account was given by Leivant in 1981 when he “proved” cut-elimination for a set-based sequent calculus for GL [3]. But Valentini in 1983 found a simple counter-example and gave a new cut-elimination proof [8]. The issue seemed to have been settled, but in 2001, Moen [5] claimed that Valentini’s transformations don’t terminate if the sequents Γ ⊢ Δ are based on multisets. There is of course no a priori reason why a proof based on sets should not carry over with some modification to a proof based on multisets, so this set the cat amongst the pigeons.

In response, Negri [6] in 2005 gave a new cut-elimination proof using sequents built from labelled formulae w : A, which captures that the traditional formula

\begin{matrix}[β_{1} ; β_{2} ; ⋯; β_{n}] ⟹ α & β \\ θ = match(β, α) & β_{1}θ ; β_{2}θ ; ⋯; β_{n}θ \end{matrix}

Fig. 2. Backward Chaining in Logical Frameworks

A is true at the possible world w. But this is not satisfactory as it brings the underlying (Kripke) semantics of modal logic into the proof theory. Mints in 2005 announced a new proof using traditional methods [4].

But the question of Moen versus Valentini remained unresolved. Finally, Goré and Ramanayake [2] in 2008 showed that Moen is incorrect, and that Valentini’s proof using multisets is mostly okay.

Many such examples exist in the literature.

5 Interactive Proof Assistants

Interactive proof-assistants are now a mature technology for “formalising mathematics”. They come in many different flavours as indicated by the names

of some of the most popular ones Mizar, HOL, Coq, LEGO, NuPrl, NqThm,
Isabelle, λ-Prolog, HOL-Lite, LF, ELF, Twelf · · · with apologies to those

whose favourite proof-assistant I have omitted.

Most of the modern proof-assistants are implemented using a modern functional programming language like ML, which was specifically designed for the implementation of such proof-assistants.

The lowest levels typically implement a typed lambda-calculus with hooks provided to allow the encoding of further logical notions like equality of terms on top of this base implementation. The base implementation is usually very small, comprising of a few hundred lines of code, so that this code can be scrutinised by experts to ensure its correctness.

Almost all aspects of proof-checking eventually compile down to a typechecking problem using this small core, so that trust rests on strong typing and a well-scrutinised small core of (ML) code.

Most proof-assistants also allow the user to create a proof-transcript which can be cross-checked using other proof-assistants to guarantee correctness.

I don’t want to go into details, but one type of proof-assistant, called a logical framework, allows the user to manage a proof using the “backward chaining” idea which we saw in use earlier to find derivations using sequent calculi.

Figure 5 shows how these logical frameworks typically work. Thus given some goal β and an inference step which claims that α is implied by β_{1} up to β_{n}, we pattern-match α and β to find their most general unifier θ, and then reduce the original goal β to the n subgoals β_{1}θ ⋯ β_{n}θ.

The pattern matching required is usually (associative-commutative) higher order unification.

The important point is that the logical framework keeps track of sub-goals and the current proof state.

The syntax of the “basic propositions” like α, β is defined via an “object logic”, which is a parameter. Different “object logics” can be invoked using the same logical-framework for the task at hand.

The logical properties of “;” like associativity or commutativity, and properties of the “⟹” like classicality or linearity are determined by the “meta-logic”, which is usually fixed for the logical framework in question.

For example, the meta-logic of Isabelle is higher-order intuitionistic logic. Higher order simply means that functions can accept other functions as arguments and can produce functions as results.

6 Isabelle’s LK Object Logic: a shallow embedding of sequent calculus

We begin with what is called a “shallow embedding” of sequents. The meaning of this term will become apparent as we proceed.

The “propositions” of Isabelle’s sequent object logic are sequents built from sequences of formulae as defined in the grammar below:

\begin{aligned}prop & = & sequence |- sequence \\ sequence & = & elem (, elem)^{∗} | empty \\ elem & = & $id | $var | formula \\ formula & = & ∼ formula | formula & formula | ⋯ \end{aligned}

Thus sequents are built from “collections” which are sequences of formulae. A sequent rule built from premise sequents β_{1}, ⋯, β_{n} with conclusion sequent α is encoded directly as the meta-logical expression:

[β_{1} ; ⋯; β_{n}] ⟹ α

Example 2. For example, the (cut) rule shown below is encoded as the metalogical expression shown below it:

Γ ⊢ Δ, P  Γ, P ⊢ Δ (cut) Γ ⊢ Δ

           [| $G |- $D,P  ;  $G,P |- $D |] ==> $G |- $D

Thus we encode the horizontal bar separating the premises from the conclusion directly using the meta-logical implication ⟹.

The advantage is that we can immediately create and check derivations using the proof assistant to manage the backward chaining involved. That is, we use the proof-assistant to find derivations by applying the rules in a backward way. There is thus a perfect match between the backward chaining involved in finding derivations and the backward chaining involved in the subgoaling provided by the proof-assistant.

The disadvantage is that there is no explicit encoding of a derivation. The derivation is kept implicitly by the proof-assistant and we cannot manipulate its structure. Nor is it possible to encode statements like the identity lemma: the sequent A ⊢ A is derivable for all formulae A. It is possible to show that particular instances of this sequent like P &Q ⊢ P &Q are derivable, but we cannot actually encode the inductive nature of the proof which would require us to show that it held for A being atomic, and that an inductive step would take us from the case for formulae of length n to formulae of length n + 1. In particular, there is no way to state the final step of the induction which allows us to state that the lemma holds for all finite formulae.

7 A Deeper Embedding: Change Object Logic

Recall that the meta-logic provides us with a method for backward chaining via expressions of the form:

β_{1} ; ⋯; β_{n} ⟹ α

The usual method for obtaining the power for reasoning about sequent derivations is to use the full power of higher-order classical logic (HOL) to build the basic propositions β_{i}.

Isabelle’s incarnation of HOL provides the usual connectives of logic like conjunction, disjunction, implication, negation and the higher order quantifiers. But it also provides many powerful facilities allowing us to define new types, define functions which accept and return other functions as arguments, and even define infinite sets using inductive definitions.

For example, the following HOL expressions capture the usual inductive definition of the natural numbers by encoding the facts that “zero is a natural number, and if n is a natural number then so is its successor s(n)”:

                       0 ∈ nat
                       n ∈ nat ⟹ s(n) ∈ nat

Most proof-assistants will automatically generate an induction principle from a given inductive definition. For example, Isabelle will automatically generate the usual induction principle which states that we can prove a property P holds of all natural numbers if we can show that P (0) holds and we can show that P (n) implies P (s(n)). An implicit assumption which facilitates such induction principles is that the inductive definitions are the only way to construct its members. Thus, if n is a natural number, then it is either 0, or is of the form s(m) for some natural number m.

To encode sequent calculus into HOL we first encode the grammar for recognising formulae as below:

   datatype fml = FC string (fml list)    (* fml connective *)
                | FV string               (* fml variable   *)
                | PP string               (* prim prop      *)

There are three type constructors FC, FV and PP which encode formula connectives, formula variables, and atomic formulae (primitive propositions). Each of them takes one string argument which is simply the string we want to use for that construction. The formula connective constructor also accepts a list of formulae, which constitute its subformulae.

For example, FC "&" [FV "A", PP "q"] encodes A & q. Since we want to encode modal provability logic GL, we require only the classical connectives, plus two unary modalities FC "Box" [.] for □. and FC "Dia" [.] for ♢..

Isabelle’s HOL allows us to form sets and multisets of objects of an arbitrary type, so the HOL expressions fml set and fml multiset capture the types of formula sets and formula multisets.

Using these types we can build a sequent type using an infix constructor ⊢ via:

           datatype seq = fml multiset ⊢ fml multiset

Isabelle’s HOL allows us to form lists of objects of an arbitrary but fixed type, so we define the type of a rule as a pair with the first component being a list of sequent premises and the second component being the conclusion sequent:

                  datatype inf = (seq list , seq)

Finally, we use the HOL type declaration rli :: inf set to declare that rli is a set of inferences, each a pair of the form mechanism (seq list , seq), and inductively define the set rli by giving a finite collection of rule instances which belong to this set. For example, the traditional rule (& ⊢) for introducing a conjunction into the left hand side of a sequent as shown below is given by the encoding below it:

Γ ⊢ A, Δ  Γ ⊢ B, Δ (⊢ &) Γ ⊢ A&B, Δ
( [ G ⊢ {A} + D , G ⊢ {B} + D ], G ⊢ {A&B} + D ) ∈ rli

The encoding uses HOL’s notation “+” for multiset union, and a slightly inaccurate description of encoding singleton multisets as {A}. Thus each element of rli is a pair whose first component is a list of its premises, and whose second component is its conclusion.

We are now in a position to encode the set derrec of “recursively derivable sequents” given an initial set pms of premise sequents and an initial set rli of inference rules. The set derrec is defined inductively as shown below:

   1  derrec :: (seq list, seq) set ⇒ seq set ⇒ seq set
   2  c ∈ pms ⟹ c ∈ derrec rli pms

3  [ (ps, c) ∈ rli ;

   4  ∀ p. p ∈ (set ps) ⟹ p ∈ derrec rli pms ]
   5  ⟹ c ∈ derrec rli pms

The explanation is as below:

1: A type declaration which tells the proof-assistant that derrec accepts a set

of inference rules and a set of sequents, and produces a set of sequents; 2 The base case of the inductive definition of derrec captures that “each premise

is itself (vacuously) derivable from the premises using the rules”. Note that there is an implicit outermost universal quantifier which is not shown explicitly, but which binds free variables like c, ps, rli, pms.

3 The first conjunct of an inductive clause stating that ps/c is a rule instance; 4: The second conjunct of the inductive clause which captures that “each premise

p in the set obtained from sequent list ps is derivable from the premises pms using the rules rli”. Here we use a function set to convert a list into the set of its members;

5: The “then” part of the inductive clause which concludes that sequent “c is derivable from pms using rli”.

8 Inductive Proofs via Automated Inductive Principles

Induction principles are generated automatically by Isabelle from the inductive definition of derrec. A heavily simplified version for proving an arbitrary property P is shown below:

1  ∀x.∀P.

   2  [ x ∈ derrec rli pms ;

3  ∀c.c ∈ pms ⟹ P(c) ;
4  ∀c.∀ps.[ (ps, c) ∈ rli ; ∀y ∈ (set ps). P(y) ⟹ P(c) ]
5  ] ⟹ P(x)

An explanation is:

1: for all sequents x and all properties P 2 : if x is derivable from premises pms using rules rli, and 3 : P holds for every premise c in pms, and 4 : for each rule, if P of its premises implies P of its conclusion, 5 : then P holds of x

If you look closely, you will see that this is an induction principle which we use often in proof-theory: prove that some property holds of the leaves of a derivation, and prove that the property is preserved from the premises to the conclusion of each rule. For example, consider the standard translation from sequents of LK to formulae given by τ(A_{1}, ⋯, A_{n} ⊢ B_{1}, ⋯, B_{m}) = A_{1} ∧ ⋯ ∧ A_{n} → B_{1} ∨ ⋯ ∨ B_{m}. We typically use this translation to argue that all derivable sequents are valid in the semantics of first-order logic. The proof proceeds by showing that the translation of the leaves of a derivation are all valid, and showing that if the translations of the premises are valid then the translations of the conclusion are valid, for every rule.

Using these inductive principles we proved the following lemma about derivability using Isabelle, where the question marks indicate free-variables which are implicitly universally quantified:

Lemma 1.

?ps ⊆ derrec ?rli ?pms ; ?c ∈ derrec ?rli ?ps ⟹ ?c ∈ derrec ?rli ?pms

If each premise in ps is derivable from premises pms using rules rli, and c is derivable from ps using rli, then c is derivable from pms using rli.

9 An Even Deeper Embedding: Derivation Trees As Objects

The main advantage of the method outlined in the previous section was that there was no concrete representation of a derivation. That is, we relied on the proof-assistant to perform pattern-matching and rule instantiations in an appropriate way, so that all we needed was to capture the idea that derivations began with premises and ended with a single sequent.

If we are to reason about cut-elimination, then we are required to perform transformations on explicit derivations. We therefore need a representation of such trees inside our encoding.

In previous work [1], we described such an encoding using the following datatype:

   datatype seq dertree = Der seq (seq dertree list)
                        | Unf seq

The declaration states that a derivation tree can either be an Unfinished leaf sequent built using the constructor Unf, or it can be a pair consisting of a conclusion sequent and a list of sub-derivation-trees bound together using the constructor Der.

In that work, we described how we maintained substitutions as lists of pairs of the form (x, t) representing the substitution x := t. We also described how we manipulated substitutions and instantiation directly to obtain rule instances.

We required such low-level aspects to be made explicit so that we could reason about display logic which required us to check conditions on rules like “a rule is closed under substitution of arbitrary structures for variables”.

Our use of dertee can be seen as an even deeper embedding of proof-theory into Isabelle/HOL since we utilise the proof-assistant only to maintain the current and further goals.

Omitting details now, suppose we define valid rli dt to hold when derivation tree dt uses rules from rli only and has no Unfinished leaves. We proved:

Lemma 2.

          valid ?rli ?dt ⟹ (conclDT ?dt) ∈ derrec ?rls {}

If derivation tree dt is valid wrt the rules rli then its conclusion is derivable from the empty set of premises using rli.

Lemma 3.

    ?c ∈ derrec ?rli {} ⟹ EX dt. valid ?rli dt & conclDT dt = ?c

If the sequent c is derivable from the empty set of premises using rules rli then there exists a derivation tree dt which is valid wrt rli and whose conclusion is exactly c.

Thus we now know that our “deep embedding” of derivability using derrec can be faithfully captured using the “even deeper” embedding using explicit derivation trees. Indeed, the lemmas allow us to move freely between the two embeddings at will to omit or include details as required by the lemma we wish to prove.

10 Mix Admissibility for Provability Logic

We finally come to the crux of our work. Below is the traditional formulation of the mix-rule for sequents built from multisets where Π_{A} is formed from Π by deleting all occurrences of A:

\begin{aligned}Γ ⊢ Δ & Π ⊢ Σ \\ (mix) \\ & Γ, Π_{A} ⊢ Δ_{A}, Σ \end{aligned} A ∈ Δ & A ∈ Π

The rule can be expressed as a lemma rather than a rule using the embeddings we have developed so far as shown below where we now explicitly use the name glss for the fixed but inductively defined set of rule instances for provability logic GL:

   (?G ⊢ ?D) ∈ derrec glss {} ; (?P ⊢ ?S) ∈ derrec glss {}

⟹

   ((?G + (ms delete {?A} ?P) ⊢ (ms delete {?A} ?D) + ?S))
                                        ∈ derrec glss {}

Here we defined a function ms_delete which deletes all occurrences of its first argument from its second argument. Our main result, which we intend to report in a proper paper, is that this lemma can be proved using our embeddings and Isabelle.

11 Proofs of Cut-Elimination in Classical Propositional Logic

The Isabelle proof described in §10 took the form of a proof of admissibility of the mix (or multicut) rule, in which multiple occurrences of the cut-formula are removed at once. We note that this proof was based on that in [2] which does prove cut- (rather than mix-) elimination. Of course, given contraction rules (or contraction admissibility), cut- and mix-admissibility are equivalent.

However the proof is different — in proving mix-admissibility directly, the inductive hypothesis has the form that when two sequents S′ and S′′ are derivable, then the result S of applying the mix rule to them is derivable. But if we have an inductive hypothesis of cut-admissibility, when the pattern of the inductive proof means that we can apply an inductive hypothesis to S′ and S′′, it does not follow that we can apply contraction to S′ and S′′ and then expect the inductive hypothesis to apply to the results of those contractions. This makes a proof of mix-admissibility easier than a proof of cut-admissibility.

However we now describe a formalised proof of cut-admissibility for classical propositional logic.

We model a sequent as a pair of multisets of formulae, written X |- Y. Thus the order of formulae within X and Y is not significant, but the number of occurrences of a formula is.

Although some of our results are parameterised over an arbitrary “subformula” relation, and assume this to be well-founded, we consistently use the “immediate” subformula relation (eg, (A, A ∧ B)).

We use a system where the rules for the binary connectives are invertible, so for example, we have

\frac{X ⊢ Y, A X ⊢ Y, B}{X ⊢ Y, A ∧ B}  \frac{X, A, B ⊢ Y}{X, A ∧ B ⊢ Y}

Thus approach had the convenient feature that all rules could be considered as a “base rule” extended by an arbitrary context, where the extension applies to the conclusion and all premises (as shown below, for the ⊢ ∧ and axiom rules).

\frac{⊢ A ⊢ B}{⊢ A ∧ B}  \frac{X ⊢ Y, A X ⊢ Y, B}{X ⊢ Y, A ∧ B}  A ⊢ A X, A ⊢ Y, A

We defined systems with and without explicit weakening and contraction rules.

First, the system lksss = extrs lksne, which is just the logical introduction rules and the axiom. We showed weakening admissibility lksss wk adm, and then contraction admissibility lksss ctr adm. This required proving invertibility of the rules lks inv rl.

Next, we add the weakening rules to get the system lkxss {} = extrs lkxne. For this we showed contraction admissibility lkxss ctr adm. Similarly to the above, this required proving an invertibility result, lkx inv rl. It does not require all the rules to be invertible — clearly, weakening rules are not invertible.

These invertibility results were obtained from “generalised” invertibility results gen inv and gen inv wk. To describe the general results we need some definitions.

Definition 1 (id decomp). A rule set rls has the identity decomposition property, id decomp rls, iff whenever \frac{ps}{A ⊢ A} ∈ rls, the sequents in the list ps are derivable.

Definition 2 (unique concl). A rule set rls has the unique conclusion property, unique concl rls, iff no two distinct rules in rls have the same conclusion.

Definition 3 (iscrls). Identity or single conclusion rules, iscrls are rules which are A ⊢ A, ⊢ A or A ⊢, for some A

Lemma 4 (gen inv, gen inv wk). When a set rls of identity or single conclusion rules satisfies the unique conclusion property, and the set of their extensions satisfies the identity decomposition property, then the set extrs rls of their extensions are invertible (with respect to the derivation system consisting of those rules).

They are also invertible with respect to the derivation system consisting of those rules and the (extended) weakening rules.

id_decomp_def : "id_decomp ?rls ==
   ALL A ps. (ps, {#A#} |- {#A#}) : ?rls --> set ps <= derrec ?rls {}"
unique_concl_def : "unique_concl ?rls ==
     ALL qs qs' d. (qs, d) : ?rls & (qs', d) : ?rls --> qs = qs'"
gen_inv : "[| ?rls <= iscrls; unique_concl ?rls; id_decomp (extrs ?rls);
  ?x : extrs ?rls |] ==> inv_rl (extrs ?rls) ?x"
gen_inv_wk : "[| ?rls <= iscrls; ?rlsw = ?rls Un wkrls;
  unique_concl ?rls; id_decomp (extrs ?rls); ?x : extrs ?rls |] ==>
  inv_rl (extrs ?rlsw) ?x"

For contraction admissibility we have similar generalised results.

Definition 4 (subfml cp prop). A rule (ps, c) has the subformula property, subfml cp prop (ps, c), iff, for every p in ps, either p >= c or, every formula in p has a sub-formula in c. Here p >= c means that the antecedent of c is a sub-multiset of the antecedent of p, and similarly for their succedents.

Lemma 5 (gen ctr adm, gen ctr adm wk). When a set rls of identity or single conclusion rules satisfies the subformula property, and the set of their extensions are invertible, then contraction is admissible (with respect to the derivation system consisting of extensions of rls).

Similarly if the weakening rules are included (they need not be invertible or satisfy the subformula property).

subfml_cp_prop.simps : "subfml_cp_prop ?sub (?ps, ?c) =
   (ALL p:set ?ps.  ?c <= p |
     (ALL fp. ms_mem fp p --> (EX fc. ms_mem fc ?c & (fp, fc) : ?sub)))"
gen_ctr_adm : "[| ?A : wfp ?sub; ?rls <= iscrls;
  Ball ?rls (subfml_cp_prop ?sub);
  Ball (extrs ?rls) (inv_rl (extrs ?rls)) |] ==> ctr_adm (extrs ?rls) ?A"
gen_ctr_adm_wk : "[| ?A : wfp ?sub; ?rls <= iscrls; ?rlsw = ?rls Un wkrls;
            Ball ?rls (subfml_cp_prop ?sub);
     Ball (extrs ?rls) (inv_rl (extrs ?rlsw)) |] ==> ctr_adm (extrs ?rlsw) ?A"

The results mentioned above follow as corollaries.

Corollary 1. For the systems lksss and lkxss {},

– the logical introduction rules are invertible

– contraction is admissible

lks_inv_rl : "Ball (extrs lksne) (inv_rl (extrs lksne))"
lkx_inv_rl : "Ball (extrs lksne) (inv_rl (extrs lkxne))"
lksss_ctr_adm : "ctr_adm lksss ?A"
lkxss_ctr_adm : "ctr_adm (lkxss {}) ?A"

We now look at cut-admissibility for these systems. We obtained a general cut-admissibility result, which depends on a further definition.

Definition 5 (cas, car). A pair of sequents ((X_{l} ⊢ Y_{l}), (X_{r} ⊢ Y_{r})) is in the set cas rls A if cut on A is admissible, that is: if (X_{l} ⊢ Y_{l}) and (X_{r} ⊢ Y_{r}) are derivable (using rules rls), then (X_{l}, (X_{r} − A) ⊢ (Y_{l} − A), Y_{r}) is derivable.

A pair of sequents ((X_{l} ⊢ Y_{l}), (X_{r} ⊢ Y_{r})) is in the set car rls A iff (X_{l}, (X_{r} − A) ⊢ (Y_{l} − A), Y_{r}) is derivable.

Definition 6 (c8s prop). A set of rules satisfies the C8 property (so-called following its use in Display Logic) if, whenever a formula is introduced on both sides (as shown by way of an example where A = A′ ∨ A′′), and assuming cutadmissibility for smaller cut-formulae, we have admissibility of the cut shown.

\begin{aligned}X_{l} ⊢ Y_{l}, A′, A′′ \\ & (⊢ ∨) \\ X_{l} ⊢ Y_{l}, A′ ∨ A′′ \end{aligned}  \begin{aligned}A′, X_{r} ⊢ Y_{r} & A′′, X_{r} ⊢ Y_{r} \\ & (∨ ⊢) \\ A′ ∨ A′′, X_{r} ⊢ Y_{r} \end{aligned} cut? X_{l}, X_{r} ⊢ Y_{l}, Y_{r}

car_eq : "((?Xl |- ?Yl, ?Xr |- ?Yr) : car ?rls ?A) =
    ((?Xl + (?Xr - {#?A#}) |- ?Yl - {#?A#} + ?Yr) : derrec ?rls {})"
car_eq' : "((?X |- mins ?A ?Y, mins ?A ?U |- ?V) : car ?rls ?A) =
      ((?X + ?U |- ?Y + ?V) : derrec ?rls {})"

cas_eq : "((?seql, ?seqr) : cas ?rls ?A) =
      (?seql : derrec ?rls {} & ?seqr : derrec ?rls {} -->
       (?seql, ?seqr) : car ?rls ?A)"
c8s_prop_def :
 "c8s_prop ?isubfml ?rls ?A == ALL ps qs pse qse Xl Yl Xr Yr.
   (ps, 0 |- {#?A#}) : ?rls --> (qs, {#?A#} |- 0) : ?rls -->
   pse = map (extend (Xl |- Yl)) ps --> qse = map (extend (Xr |- Yr)) qs -->
   set pse Un set qse <= derrec (extrs ?rls) {} -->
   (ALL sfa. (sfa, ?A) : ?isubfml --> (ALL Xl Yl Xr Yr.
      (Xl |- mins sfa Yl, mins sfa Xr |- Yr) : cas (extrs ?rls) sfa)) -->
   (Xl |- mins ?A Yl, mins ?A Xr |- Yr) : car (extrs ?rls) ?A"

Then we have the general cut-admissibility theorem:

Theorem 1. If the basic rules in set rls are single-conclusion or identity rules, and rls also contains the identity rules, and if rls satisfies the C8 property, then for the system extrs rls, if contraction is admissible, then cut is admissible.

Corollary 2. Cut is admissible for the systems lksss and lkxss {}.

gen_scas_all : "[| wf ?psubfml; All (c8s_prop ?psubfml ?rls);
  All (ctr_adm (extrs ?rls)); ?rls <= iscrls;
  ALL A. ([], {#A#} |- {#A#}) : ?rls |] ==>
  (?Xl |- mins ?A ?Yl, mins ?A ?Xr |- ?Yr) : cas (extrs ?rls) ?A"
lks_scas_all : "(?Xl |- mins ?A ?Yl, mins ?A ?Xr |- ?Yr) : cas lksss ?A"
lkx_scas_all : "(?Xl |- mins ?A ?Yl, mins ?A ?Xr |- ?Yr) : cas (extrs lkxne) ?A"

To prove the cut-admissibility result, we used an induction scheme which permits inductive proof of any predicate which depends on two derivable sequents. The inductive step in such a proof is defined by gen step2sr.

gen_step2sr_def' : "gen_step2sr ?P ?A ?sub ?rls ((?psl, ?cl), ?psr, ?cr) =
    ((ALL A'.  (A', ?A) : ?sub --> (ALL dl:derrec ?rls {}.
       ALL dr:derrec ?rls {}. ?P A' (dl, dr))) -->
     (ALL pl:set ?psl. pl : derrec ?rls {} & ?P ?A (pl, ?cr)) -->
     (ALL pr:set ?psr. pr : derrec ?rls {} & ?P ?A (?cl, pr)) -->
     ?cl : derrec ?rls {} --> ?cr : derrec ?rls {} --> ?P ?A (?cl, ?cr))"
gen_step2sr_lem : "[| ?A : wfp ?sub;
    ALL A. ALL (psa, ca):?rls. ALL (psb, cb):?rls.
      gen_step2sr ?P A ?sub ?rls ((psa, ca), psb, cb);
    ?seqa : derrec ?rls {}; ?seqb : derrec ?rls {} |] ==>
  ?P ?A (?seqa, ?seqb)"

It is this which we need to prove for every possible last derivation steps on either side of the desired cut. Let the last derivation step on the left be (psl, cl), and, on the right, (psr, cr). It concerns a property P which depends on a formula A (typically, that cut-admissibility holds for A). We assume that cut-admissibility holds for sub-formulae A′ of A. We also assume that for each premise pl in psl, P A (pl, cr) holds, and that for each premise pr in psr, P A (cl, pr) holds, and prove that these imply that P A (cl, cr) holds.

If we can do this for all then this is sufficient to prove that P A (seql, seqr) holds for any pair of derivable sequents (gen step2sr lem).

This approach had the advantage that we could prove separate lemmas stating that gen step2sr holds for various rules in the last position on either side of the cut, rather than having to prove this as part of one single huge result.

The same approach was taken in the inductive proofs of logical introduction rule invertibility and contraction admissibility, although these cases are simpler because there is one preceding derivation to deal with, not two.

Note that this induction scheme is “induction on the fact of derivation” of the premises of the cut, where we assume the desired result holds for the preceding step of the derivation.

A proof of these results might instead use “induction on the size of the derivation”, assuming the desired result holds for any smaller derivation. As we see below, this approach would be more general. But so far our formalisation of these results has not required a derivation whose size can be measured or compared (although this is described in §9).

Finally, we add the contraction rules to get the system lkxcss {} = extrs lkxcne. We now consider proving cut-admissibility of this system.

The easiest way is to simply omit the contraction rules and use the previous results (for lkxss {} = extrs lkxne), since both contraction and cut are admissible in that system.

One could also use an inductive argument similar to that described above to prove mix-admissibility (ie, where the property P is that the mix, or multicut, rule, rather than the cut rule, is admissible).

TODO - try this - how different/difficult is it?

But we want to explore what is involved in proving cut-admissibility directly, by induction: ie, admissibility of a single cut is the property which we prove by assuming it as an inductive hypothesis.

Now where the last step on both sides is contraction of the cut-formula, preceded by introduction of that formula, it can be seen that we need invertibility of the logical introduction rules (whereas in the work described above, we needed invertibility to prove contraction admissibility). Further, to prove this in the presence of explicit contraction rules we need an inductive hypothesis of “multiinvertibility” (which means, for example, that if X, (A ∧ B)^{n} ⊢ Y is derivable then X, A^{n} ⊢ Y and X, B^{n} ⊢ Y are derivable). So we proved multi-invertibility

as lkxc inv rl.

Then, in the scenario where the last n steps are contraction of the cutformula, preceded by some other rule ρ, we typically need to perform first the n contractions, then the cut (by induction), then the rule ρ. This means that the inductively justified cut is performed on a sequent which does not appear in the original derivation. Thus the inductive scheme described above will not work: instead we can use induction on the height of the derivation tree which leads to the premises of the cut. See the diagram below. So we need to use explicit derivation trees as described in §9.

Analogous to gen step2sr we define a predicate height step2 tr which expresses the key step of a proof of a property of two sequents by induction on height of their derivations. (In the case of height step2 tr, though, we need to put the condition that the sequents be derivable into P). Then the result height step2 tr lem expresses the result that if we can prove this step for all derivation trees then P A holds for all derivation trees.

height_step2_tr_eq : "height_step2_tr ?P ?A ?sub (?dta, ?dtb) =
  ((ALL A'. (A', ?A) : ?sub --> (ALL a b. ?P A' (a, b))) -->
    (ALL dtp. (dtp, ?dta) : measure heightDT --> ?P ?A (dtp, ?dtb)) -->
    (ALL dtq. (dtq, ?dtb) : measure heightDT --> ?P ?A (?dta, dtq)) -->
       ?P ?A (?dta, ?dtb))"
height_step2_tr_lem : "[| ?A : wfp ?sub;
  ALL A dta dtb. height_step2_tr ?P A ?sub (dta, dtb) |] ==>
    ?P ?A (?dta, ?dtb)"

The proof of cut-admissibility then goes like this:

First, consider the case where the cut-formula is compound (eg A′∧A′′). Since we have invertibility of the logical introduction rules, we can use this fact and the inductive assumption that cuts on A′ or A′′ are admissible, to get admissibility of the cut on A′ ∧ A′′. The significant part of the proof in this case is reused from the cut-admissibility of lksss.

Then we have to consider the case where the cut-formula is atomic. We need to trace up contractions on that cut-formula on either side and see what the next rule above that is. Note that the number of consecutive contractions on either side may be zero — it turns out that there is no need to treat this case differently from the case where there is one or more contractions. There was one exception to this — the case of a weakening on the cut-formula is slightly different depending on whether there are zero or more contractions below the weakening. ^{1}.

Here is the case of a parametric derivation step immediately above the topmost contraction on the cut-formula. The rule ρ which changes X′_{l} and Y′_{l} to X_{l} and Y_{l} has to allow arbitrary context, so that it can be applied after the cut.

\begin{aligned}X′_{l} ⊢ Y′_{l}, A^{n} \\ & (ρ) \\ X_{l} ⊢ Y_{l}, A^{n+1} \end{aligned} ; (ctr^{n}) ; X_{l} ⊢ Y_{l}, A A, X_{r} ⊢ Y_{r} cut? X_{l}, X_{r} ⊢ Y_{l}, Y_{r}

1 We wasted considerable time and effort before discovering this fact, in that we dealt

with various cases for the rule immediately above the cut being weakening, a para-

metric case of contraction, etc

X′_{l} ⊢ Y′_{l}, A^{n} ; (ctr^{n}) ; X′_{l} ⊢ Y′_{l}, A A, X_{r} ⊢ Y_{r}

cut? X′_{l}, X_{r} ⊢ Y′_{l}, Y_{r} (ρ) X_{l}, X_{r} ⊢ Y_{l}, Y_{r}

The remaining cases are where the cut-formula A is atomic (otherwise we we have the case where invertibility applies, as mentioned above). These cases are the axiom A ⊢ A or weakening on A, and are easy: in the case of A ⊢ A, we have that A is in X_{l} or Y_{r}, and in the case of weakening, it either reverses the last contraction (if any), or, if there were no contractions, is a trivial case.

STILL TO DO - get a generalised form of this theorem, as gen scas all

lkxc_inv_rl : "Ball (extrs (multiples lksne)) (inv_rl (extrs lkxcne))"
lkxc_scas_all :
   "(?Xl |- mins ?A ?Yl, mins ?A ?Xr |- ?Yr) : cas (extrs lkxcne) ?A"

12 Objections and Impediments

A frequent objection to the idea of machine-checking anything is that the errors could also have been found by a good Phd student working with pencil and paper. But even diligent Phd students are apt to fall for errors which lie within sentences marked by “clearly ...” or the “other cases are similar”. The beauty of proof-assistants lies in their absolutely pedantic insistence that nothing is proved until it passes through the type-checking procedure of the proof-assistant.

Another objection is that this is not research but is just high level programming since you have to have the proof first. To some extent this is true since the current prototypical example is usually the verification of a given proof from a paper or a book. But many researchers now build the proof interactively. Indeed, better user-interfaces make this very possible.

The main impediment in my opinion is the sheer effort required to become familiar with proof-assistants before productive work can be started. It takes at least three months of full-time work to learn how to use an interactive proof assistant well. But as I hope I have shown you, it is worth it!

References

1. J E Dawson and R Goré. Formalised Cut Admissibility for Display Logic. In Proc. 15th International Conference on Theorem Proving in Higher Order Logic, LNCS 2410:131-147, 2002.

2. R Goré and R Ramanayake. Valentini’s Cut Elimination for Provability Logic Resolved. in Advances in Modal Logic, Volume 7, pp 67–86, College Publications, London, 1981. NOTE 1981 MUST BE WRONG

3. D. Leivant. On the Proof Theory of the Modal Logic for Arithmetic Provability. Journal of Symbolic Logic, 46:531–538, 1981.

4. G. Mints. Cut elimination for provability logic. Collegium Logicum 2005.

5. A. Moen. The proposed algorithms for eliminating cuts in the provability calculus GLS do not terminate. NWPT 2001, Norwegian Computing Center, 2001-12-10. http://publ.nr.no/3411

6. S. Negri. Proof Analysis in Modal Logic. Journal of Philosophical Logic, 34:507– 544, 2005.

7. R.M. Solovay. Provability Interpretations of Modal Logic. Israel Journal of Mathematics, 25:287–304, 1976.

8. S. Valentini. The Modal Logic of Provability: Cut-elimination. Journal of Philosophical Logic, 12:471–476, 1983.