A New Machine-checked Proof of Strong Normalisation for Display Logic

Jeremy E. Dawson and Rajeev Goré^{∗}

Department of Computer Science and Automated Reasoning Group Australian National University Canberra ACT 0200, Australia

         jeremy@arp.anu.edu.au  rpg@arp.anu.edu.au

Tel: +61-2-6125-8603 Fax: +61-2-6125-8651

Abstract

We use a deep embedding of the display calculus for relation algebras δRA in the logical framework Isabelle/HOL to formalise a new, machine-checked proof of strong normalisation and cut-elimination for δRA which does not use measures on the size of derivations. Our formalisation generalises easily to other display calculi and can serve as a basis for formalised proofs of strong normalisation for the classical and intuitionistic versions of a vast range of substructural logics like the Lambek calculus, linear logic, relevant logic, BCK-logic, and their modal extensions. As far as we are aware, this is the first full formalisation of a strong normalisation result using a logical framework.

1 Introduction

Sequent calculi provide a rigorous basis for meta-theoretic studies of various logics. The central theorem is cut-elimination which states that detours through lemmata can be avoided: it can be used to show many important logical properties like consistency, interpolation, and Beth definability. In computer science, cut-free sequent calculi can be used for automated deduction [11], for nonclassical extensions of logic programming [18], and for studying the deep connection between cut-elimination, lambda calculi and functional programming. Sequent calculi, and their extensions, therefore play an important role in theoretical computer science.

Display Logic [2] is a generalised sequent framework for non-classical logics, based on Gentzen’s sequent calculus [19]. Since it is not really a logic, we prefer the term display calculi and use it from now on. Display calculi extend Gentzen’s language of sequents with extra, complex, n-ary structural connectives, in addition to Gentzen’s sole structural connective, the “comma”. Properties such as associativity are explicitly stated as structural rules. Display calculi provide an extremely general sequent framework encompassing a vast range of substructural logic like the bi-intuitionistic and bi-classical versions of the Lambek calculus, linear logic, relevant logic, BCK-logic, and their modal and tense logical extensions, in a uniform way [20, 10]. The most remarkable property of display calculi is a generic cut-elimination theorem, which applies whenever the rules for the display calculus satisfy certain, easily checked, conditions [2]. Display calculi therefore provide an important generalisation of sequent calculi.

∗Contact Author WordCount = delatex cutelimlics.tex | wc = 6592

Traditional proofs of cut-elimination in sequent calculi do not eliminate the cut rule directly due to problems in eliminating applications of contraction above cut. Gentzen [19] himself first replaced the cut rule with the mix rule, showed that cut was derivable from mix, and then eliminated the mix rule. Borisavljevic et al [3] have shown that the direct elimination of the cut rule is by no means trivial, requiring a further detour through a special normal form for derivations. The problems caused by contraction can also be avoided by proving a lemma that contraction itself is an admissible rule, as done by Pfenning [17]. We cannot follow this last strategy since explicit structural rules like contraction are what give display calculi their generality.

In [2], Nuel Belnap gives a direct proof that the cut rule is admissible in display calculi. In [20], Heinrich Wansing gives a direct proof of strongnormalisation for the cut-elimination procedure for a particular display calculus. Wansings’s proof of termination uses a complex measure on the size of derivations. When we tried to mechanise Wansing’s proof using a logical framework, we were unable to proceed beyond a point in the proof where Wansing states that “This construction generalises easily to the case where A is introduced … at more than one point … ”.

We therefore developed and mechanised a new direct proof of strong normalisation for the display calculus δRA using four complex orderings, which we proved to be well-founded. Our orderings do not depend upon the size of derivations. As far as we are aware, this is the first full formalisation of a strong normalisation result using a logical framework. The work required approximately 9 man-months, approximately 1600 lines of Isabelle/HOL theory files and 8500 lines of ML proof files, and takes approximately 35 minutes to fully type-check on a 300MHz Pentium machine.

We are aware of only three other attempts to formalise proof theory, cut elimination or strong normalisation.

The first is the work of Pfenning where he formalises the admissibility of cut for classical, intuitionistic and linear logic using the logical framework Elf [17]. In previous work [6], we found that the Elf implementation reports success even when certain transformations, essential to cut-elimination, are deleted from the encoding! Our conclusion was that the Elf implementation was not a full formalisation of cut-elimination. Pfenning essentially says the same thing in the conclusion of [17]:“Once the structural proof of admissibility has been found and implemented, it is natural to ask if it can also be encoded in stronger frameworks such as Coq [DFH+93] so that structural inductions are made explicit and the proof is fully formally verified.”. In separate work, we have answered this question in the affirmative using Isabelle/HOL instead of Coq.

The second is the work of Matthews et al [12, 1, 13] which implements Feferman’s FS_{0} in Isabelle, and uses it to formalise and extend various metatheoretical systems. It should be possible to formalise cut-elimination in this implementation, but it does not appear to have been done.

The third is the work of Mikhajlova and von Wright [14], giving a formalisation of a sequent calculus for first-order logic in the system HOL. This work makes no attempt to prove a cut-elimination or strong normalisation result, and as we point out later, actually contains an unfortunate bug.

The paper is set out as follows. In Section 2 we describe the display calculus δRA for the logic of relation algebras, the logical framework Isabelle and its subtheory HOL, and our encoding of δRA into Isabelle/HOL. In Section 3 we describe essential functions for reasoning about derivations. In Section 4 we describe Isabelle/HOL functions that allow us to reason about cuts, and discuss the problems we had in formalising Wansing’s proof of strong normalisation. In Section 5 we describe our new proof of strong normalisation for the display calculus δRA. Section 6 presents further work.

A longer version of this paper can be found at http://arp.anu.edu.au/

~rpg/CutElim/ and the actual Isabelle code at http://discus.anu.edu.

au/~jeremy/deep-files/ via your favourite web browser. Enjoy!

2 A Deep Embedding of δRA in Isabelle/HOL

The following grammar defines the syntax of relation algebras where the elements of the top line are Boolean and the elements of the bottom line are their relational analogues:

A B ::= p_{i} | ⊤ | ⊥ | ¬A | A ∧ B | A ∨ B | A ⊃ B
| 1 | 0 |∼ A |⌣ A | A + B | A ∘ B | A → B

A display calculus for relation algebras called δRA can be found in [8]. Sequents of δRA are expressions of the form X ⊢ Y where X and Y are built from the nullary structural constants E and I and formulae, using the structural connectives in the grammar below:

X Y ::= A | I | E | ∗X | •X | X ; Y | X , Y

The defining feature of display calculi is that in all logical introduction rules, the principal formula is always “displayed” as the whole of the right-hand or

datatype formula = Btimes formula formula ("_&& _" [68,68] 67)
                 | Rtimes formula formula ("_oo _" [68,68] 67)
                 | Bplus formula formula ("_v _" [64,64] 63)
                 | Rplus formula formula ("_++ _" [64,64] 63)
                 | Bneg formula ("--_" [70] 70)
                 | Rneg formula ("_^" [75] 75)
                 | Btrue ("T")
                 | Bfalse("F")
                 | Rtrue ("r1")
                 | Rfalse("r0")
                 | FV string
                 | PP string

Figure 1: Isabelle/HOL Representation of Formulae of δRA.

left-hand side. For example, the rule (LK- ⊢ ∨), shown below left, is typical of Gentzen’s sequent calculi like LK, while the rule (δRA- ⊢ ∨) shown on the right is typical of display calculi; see [8] for details:

\frac{Γ ⊢ Δ, P , Q}{Γ ⊢ Δ, P ∨ Q}(LK- ⊢ ∨) \frac{X ⊢ P , Q}{X ⊢ P ∨ Q}(δRA- ⊢ ∨)

Isabelle is an automated proof assistant [16]. Its meta-logic is an intuitionistic typed higher-order logic, sufficient to support the built-in inference steps of higher-order unification and term rewriting. Isabelle accepts inference rules of the form “from α_{1}, α_{2}, …, α_{n}, infer β” where the α_{i} and β are expressions of the Isabelle meta-logic, or are expressions using a new syntax, defined by the user, for some “object logic”. Most users build on one of the comprehensive “object logics” already supplied, like Isabelle/HOL [15], which is an Isabelle theory based on the higher-order logic of Church [4] and the HOL system of Gordon [7]. In [6], we describe our initial attempts to formalise display calculi in various logical frameworks, describe why we selected Isabelle/HOL, and give an explanation of this deep embedding. We assume the reader is familiar with ML and logical frameworks in general.

Formulae of δRA are represented by the datatype shown in Figure 1. The constructors FV and SV represent formula and structure variables which appear in the statement of a rule or theorem, and which are instantiated to actual formulae of δRA when constructing derivations. The constructor PP represents a primitive proposition p_{i}, which is not amenable to substitution.

Structures of δRA are represented by the datatype shown in Figure 2. The operator Structform causes a formula to be “cast” into a structure. We say that a structure expression is formula-free if it does not contain any formula as a sub-structure: that is, if it contains no occurrences of Structform. A formula-free sequent is defined similarly.

datatype structr = Comma structr structr
                 | SemiC structr structr
                 | Star structr
                 | Blob structr
                 | I
                 | E
                 | Structform formula
                 | SV string

Figure 2: Isabelle/HOL Representation of Structures of δRA.

The notation in parentheses in Figures 1 describe an alternative infix syntax which is closer to the actual syntax of δRA. For technical reasons, a different method is used to specify the alternative infix syntax for structures and sequents: details omitted. Sequents of δRA are represented by the Isabelle/HOL datatype below:

datatype sequent = Sequent structr structr
datatype rule = Rule (sequent list) sequent
              | Bidi sequent sequent
              | InvBidi sequent sequent

The premisses of a rule are represented using a list of sequents while the conclusion is a single sequent. Thus Rule prems concl means a rule with premisses prems and conclusion concl. Many single-premiss rules of display calculi are defined to be usable from top to bottom as well as from bottom to top: the two constants Bidi and InvBidi allow us to cater for these. A sequent (Sequent X Y) can also be represented as $X |- $Y. Thus the

term Sequent (SV ''X'') (Structform (FV ''A'')) is printed, and may
be entered, as ($''X'' |- ''A'').

In contrast to the formula and structure variables modelled explicitly by FV and SV, Isabelle has “scheme variables”, identified by a preceding ‘?’. When a scheme variable appears in an Isabelle theorem, the theorem is true when anything, of the appropriate type, is substituted for that variable.

The constant rls represents the set of rules of δRA and cutr is the name of the cut rule, encoded using the datatypes just described: we omit the details of this code. We handle substitutions for structure and formula variables explicitly via various functions: details omitted. We use the term “derivation” to refer to a proof within the sequent calculus, reserving the term “proof” for a meta-theoretic proof of a theorem about the sequent calculus. We model a derivation tree using the following datatype:

datatype pftree = Pr sequent rule (pftree list)
                | Unf sequent

In a term Pr seq rule pts the subterm seq is the sequent at the root (bottom) of the tree, and rule is the rule used in the last (bottom) inference. Thus, if the tree represents a real derivation, then sequent seq will be an instantiation of the conclusion of rule, and the corresponding instantiations of the premisses of rule will be the roots of the trees in the list pts. The trees in pts are called the immediate subtrees of Pr seq rule pts.

The leaves of a derivation tree are either axioms with no premisses, or “Unfinished” sequents whose derivations are currently unfinished.

Display calculi use the initial sequent p ⊢ p, using primitive propositions only. It is then proved that the sequent A ⊢ A is derivable for all formulae A by induction on the size of A, where A stands for a formula composed of primitive propositions and logical connectives. We proved this, as the theorem idfpp. We also need to reason about the derivation trees of derived rules which may use the (derived) rule A ⊢ A, for arbitrary formula A. Therefore we let the derivation tree Pr (''A'' |- ''A'') idf [] stand for a complete derivation, which uses the lemma that A ⊢ A is derivable, and let the derivation tree Unf (''A'' |- ''A'') stand for an incomplete derivation with unfinished premiss A ⊢ A.

For example, the incomplete derivation tree shown below at left is represented as the Isabelle/HOL term shown below at right where ''A'' |- PP p && ''A'' stands for A ⊢ p ∧ A and cA and ands are the contraction and (⊢ ∧) rules, and idf is the derived rule A ⊢ A:

\begin{matrix}A ⊢ p & A ⊢ A & (⊢ ∧) & A, A ⊢ p ∧ A \\ (ctr) \\ A ⊢ p ∧ A \end{matrix}

                      Pr (''A'' |- PP p && ''A'') cA
                       [Pr (''A'', ''A'' |- PP p && ''A'') ands
                       [Unf (''A'' |- PP p),
                        Pr (''A'' |- ''A'') idf []]]

3 Reasoning About Derivations and Derivability

We now describe various functions which allow us to reason about derivations in δRA and theorems we have proved about derivability in δRA.

allPT f pt holds if property f holds for every sub-tree in the derivation tree pt.

allNextPTs f pt holds if property f holds for every proper sub-tree of pt.

wfb (Pr concl rule pts) holds if sequent rule rule has an instantiation with conclusion instance concl and premiss instances which are the conclusions of the derivation trees in the list pts. Such a node is said to be well-formed.

allPT wfb pt holds if every sub-tree of the derivation tree pt is wellformed. That is, if every node in pt is well-formed. Such a derivation is said to be well-formed.

frb rules (Pr concl rule pts) holds when the lowest rule rule used in

a derivation tree Pr concl rule pts belongs to the set rules.

allPT (frb rules) pt holds when every rule used in a derivation tree pt belongs to the set rules.

premsPT pt returns a list of all “premisses” (unfinished leaves) of the derivation tree pt. That is, the sequents found in nodes of pt of the form

     Unf seq.

conclPT pt returns the end-sequent of the derivation tree pt. That is, the conclusion of the bottom-most rule instance.

Definition 3.1 A derivation tree pt is valid if it is well-formed, uses rules in the set of rules rules of the calculus, and has no unfinished leaves.

valid_def = "valid ?rules ?pt ==
   allPT wfb ?pt & allPT (frb ?rules) ?pt & premsPT ?pt = []"

The question marks in front of rules and pt flag that they are Isabelle scheme variables, even though the question marks would be absent in the Isabelle/HOL theory file itself: we do this throughout this paper.

Definition 3.2 (IsDerivableR) IsDerivableR rules prems' concl holds

iff there exists a derivation tree pftr which uses only rules from set rules, is well-formed, has conclusion concl, and has premisses from set prems'.

"IsDerivableR ?rules ?prems' ?concl == (EX pftr.
      allPT (frb ?rules) pftr & allPT wfb pftr &
      conclPT pftr = ?concl & set (premsPT pftr) <= ?prems')"

Here, set is a function that allows us to treat its argument as a set rather than a list, and <= is the subset relation ⊆. Our main result about derivability is a recursive characterisation of derivability.

Theorem 3.1 (IsDerivableR recur) A conclusion concl is derivable from premisses prems using rules rules if and only if either concl is one of prems, or there exists an instantiated rule obtained from rules and the conclusion of rule is concl and the premisses of rule are themselves derivable from prems using rules.

IsDerivableR_recur = "IsDerivableR ?rules ?prems ?concl = (
 ?concl : ?prems | (EX rule. ruleFromSet rule ?rules &
 conclRule rule = ?concl & (ALL p : set (premsRule rule).
 IsDerivableR ?rules ?prems p)) )" : thm

The appellation “: thm” indicates a statement that has been proved in Isabelle/HOL using previous Isabelle/HOL definitions and theorems: we follow this practice for theorems and lemmata throughout this paper.

In the third clause for IsDerivable on [14, page 302], which deals with the case of a result being provable using derived rules, an incorrect use of an existential quantifier gives that P → Q could be used as a derived rule on the grounds that one instance of it, say True → True, is provable.

4 Reasoning About Cuts and Wansing’s Proof

We assume familiarity with notions like “parametric ancestors” of a cut formula from [2], “principal moves” and “parametric moves” from the literature on strong normalisation: details can be found in the Appendix (Section 7).

Definition 4.1 A cut rule application is left- [ right-] principal if the cutformula is the principal formula of the left [right] premiss of the cut rule.

Each of the following functions requires the bottom node of the derivation tree to be of the form Pr seq rule pts, and that if rule is (cut), then for: cutOnFmls s the cut is on a formula in the set s; cutIsLP A the cut is on formula A and is left-principal; cutIsLRP A the cut is on formula A and is (left- and right-)principal. It follows from the definitions that a

derivation tree satisfying any of allPT (cutOnFmls s), allPT (cutIsLP

A) and allPT (cutIsLRP A) has no unfinished leaves. We omit details.

The ideas inherent in principal and parametric moves are well-known, but they were first applied to prove strong normalisation for a display calculus by Wansing to show that any (sufficiently long) sequence of steps in the process of cut-elimination terminates. This paper is reproduced in [20].

We have implemented large parts of Wansing’s strong normalisation proof. In fact we completed it, subject to assertions (which we had intended to prove) about the effect of primitive and parametric reductions. These assertions are too complex to include and explain here, but they implied (inter alia) that the subtree Π′[Y] and its conclusion Z[Y] ⊢ A in the right (transformed) tree of Figure 5 is the same as the tree Π[A] and its conclusion Z[A] ⊢ A in the left (original) tree: that is, the transformation process does not alter Π but leaves it intact. In fact, this is true only if Z contains no parametric ancestors of A, and examples can be constructed using contraction where this fails. Thus our assertion failed, and so we could not prove Wansing’s result. We attempted to repair this defect by reference to the relevant part of Wansing’s proof [20, page 54] in which he states that the extension to situations more complex than that of Figure 5 is to be shown “analogously”. Unfortunately it is based on a diagram much like Figure 5 and appears to rely on the fact that the subtree Π in Figure 5 appears unchanged in the transformed tree.

5 A New Proof of Strong Normalisation

We now give a new direct proof of strong normalisation which does not rely on the size of derivation trees. Given a derivation tree with (cut) at its root, the tree can be changed to deal with that particular cut; we call these “cutreductions”. Following Wansing [20, §4.2], we classify these cut-reductions as principal or parametric. More generally, we can change a tree by performing a cut-reduction on any subtree; we call such changes reductions.

5.1 Defining Strongly Normalisable Derivations

Definition 5.1 (reduces) Assuming a relation cutReduces (defined later), derivation tree Π_{0} reduces to derivation tree Π_{1} if either (a) Π_{0} cutReduces to Π_{1}, or (b) Π_{0} and Π_{1} are identical except that exactly one of the immediate subtrees of Π_{0} reduces to the corresponding immediate subtree of Π_{1}.

  reduces_Unf = "reduces (Unf ?seq) ?ptn = False"
  reduces_Pr  = "reduces (Pr ?seq ?rule ?ptl) ?ptn =
   ( (EX ptl'. onereduces ?ptl ptl' & ?ptn = Pr ?seq ?rule ptl')
     | cutReduces (Pr ?seq ?rule ?ptl) ?ptn )"
  onereduces_Nil  = "onereduces [] ?ptl' = False"
  onereduces_Cons = "onereduces (?h # ?t) ?ptl' = ( ?ptl' ~= []
    & (reduces ?h (hd ?ptl') & ?t = (tl ?ptl')
       | ?h = (hd ?ptl') & onereduces ?t (tl ?ptl')) )"

Wansing [20, p. 52] defines a strongly normalisable derivation tree as a tree from which every sequence of reductions is finite. We define inductively the set of strongly normalisable derivation trees using Isabelle’s inductive definition feature, which defines the minimal set closed under the given rules. For example, the rules {0 ∈ S, n ∈ S ⟹ n + 2 ∈ S} define S to be the set of even naturals, although the set of all naturals also satisfies the rules. For more details, see [15, § 2.10].

Definition 5.2 (sn set) The set sn set is the smallest set of derivation trees such that: (a) if Π_{0} cannot be reduced then Π_{0} ∈ sn set (b) if every tree Π_{1} to which Π_{0} reduces is in sn set then Π_{0} ∈ sn set.

inductive "sn_set"
  intrs
    snI "(ALL ptn.
    reduces ?pt ptn --> ptn : sn_set) ==> ?pt : sn_set"

Note that Definition 5.2.(b) subsumes Definition 5.2.(a), which is why there is only one clause in the corresponding Isabelle code.

Definition 5.3 (strongly normalisable) A derivation tree is strongly normalisable iff it is a member of sn set.

5.2 Various Well-Founded Orderings

To prove that every derivation tree is strongly normalisable, we use a binary relation dtorder on derivation trees, and show that it is well-founded. First we need an auxiliary definition.

Definition 5.4 (sn1red) For two lists ptl1 and ptl2 of derivation trees, sn1red ptl1 ptl2 holds iff the lists ptl1 and ptl2 are non-empty and differ at only one position where ptl1 contains tree pt1 and ptl2 contains tree pt2, and pt1 reduces to pt2, and pt1 is strongly normalisable.

sn1red_Nil  = "sn1red [] ?ptl2 = False"
sn1red_Cons = "sn1red (?h # ?t) ?ptl2 = (?ptl2 ~= [] &
       (reduces ?h (hd ?ptl2) & ?h : sn_set & ?t = (tl ?ptl2)
       | ?h = (hd ?ptl2) & sn1red ?t (tl ?ptl2)) )"
Definition 5.5 (LRPorder, cutorder, sn1order, dtorder) We define four

binary relations, LRPorder, cutorder, sn1order and dtorder on derivation trees as sets of ordered pairs:

(a) Π_{1} <_{LRP} Π_{0} if the bottom inferences of derivations Π_{1} and Π_{0} are both ( cut), and either

(i) the cut in Π_{1} is left-principal or right-principal, and the cut in Π_{0} is neither, or

(ii) the cut in Π_{1} is (left- and right-)principal, and the cut in Π_{0} is not (left- and right-)principal.

(b) Π_{1} <_{cut} Π_{0} if the bottom inferences of derivations Π_{1} and Π_{0} are both ( cut), and if either

(i) the size of the cut-formula of Π_{1} is smaller than that of Π_{0}, or (ii) each derivation has the same cut-formula, and Π_{1} <_{LRP} Π_{0}.

(c) Π_{1} <_{sn1} Π_{0} if Π_{0} and Π_{1} are the same except that one of the immediate subtrees of Π_{0} is strongly normalisable and reduces to the corresponding immediate subtree of Π_{1}.

(d) Π_{1} <_{dt} Π_{0} iff any of the following hold:

(i) the bottom inference of Π_{1} is not ( cut), but that of Π_{0} is (ii) Π_{1} <_{cut} Π_{0} (iii) Π_{1} <_{sn1} Π_{0}.

The definitions use Isabelle’s inductive definitions but we give only dtorder.

inductive "dtorder"
 intrs
  cnc "?rule ~= cutr ==>
       (Pr ?seq1 ?rule ?ptl1, Pr ?seq2 cutr ?ptl2) : dtorder"
  dtc "?pts : cutorder ==> ?pts : dtorder"
  snr "?pts : sn1order ==> ?pts : dtorder"
Theorem 5.1 (wf LRPorder, wf cutorder, wf sn1order) The relations

LRPorder, cutorder and sn1order are well-founded. Only one shown.

   wf_LRPorder = "wf LRPorder" : thm

Despite the notation, these relations are not reflexive, and some are not transitive. Intuitively, (Π_{1}, Π_{0}) ∈ dtorder means that Π_{1} is closer to being cut-free (in some sense) than is Π_{0}. To prove that dtorder is well-founded, we first need a result on the interaction between cutorder and sn1order.

Lemma 5.1 (sntr') If Π_{2} <_{cut} Π_{1} and Π_{1} <_{sn1} Π_{0} then Π_{2} <_{cut} Π_{0}.

sntr' = "[| (?pty, ?ptza) : cutorder; (?ptza, ?ptz) : sn1order |]
         ==> (?pty, ?ptz) : cutorder" : thm

Theorem 5.2 (wf dtorder) dtorder is well-founded. Not shown.

5.3 Inheriting Strong Normalisation

We next define snHered, a property of derivation trees which indicates that a tree inherits strong normalisation from its immediate subtrees.

Definition 5.6 (snHered) Π satisfies snHered iff: if all the immediate subtrees of Π are strongly normalisable then Π is strongly normalisable.

   snHered_def = "snHered ?pt ==
     set (nextUp ?pt) <= sn_set --> ?pt : sn_set"

Lemma 5.2 (hereds sn) A derivation tree Π is strongly normalisable iff every subtree of Π has the property snHered.

hereds_sn = "(ALL pts.
  isSubt ?pt pts --> snHered pts) = (?pt : sn_set)" : thm

Proof: The “only if” part uses the theorem sn set.induct below which is generated automatically by Isabelle from the inductive definition of sn set.

sn_set.induct = "[| ?xa : sn_set ; (!!pt. (ALL ptn.
    reduces pt ptn --> ptn : sn_set & ?P ptn) ==> ?P pt ) |]
 ==> ?P ?xa" : thm

The “if” part uses induction on the height of Π using the assumption that every subtree of Π, including itself, has the property snHered. Q.E.D.

5.4 Reasoning About Cut-Reductions

We intend to define cut-reduction in a way that enables us to make some assertions about cut-reductions. We first define properties nparRedP and c8redP of reductions (which in fact apply to parametric and principal reductions respectively). The definitions do not require that the bottom inference of the derivation be (cut), but they are used only where this is so.

Definition 5.7 (nparRedP) The relation nparRedP holds between two derivation trees Π_{0} and Π_{1} if every subtree Π_{1}^{s} of Π_{1} with a bottom inference ( cut) satisfies either (a) Π_{1}^{s} is a proper subtree of Π_{0}, or (b) Π_{1}^{s} and Π_{0} have the same cut-formula and Π_{1}^{s} <_{LRP} Π_{0}.

nparRedP_Unf = nparRedP "(Unf ?seq) ?ptn = False"
nparRedP_Pr  = "nparRedP (Pr ?seq ?rule ?ptl) ?ptn = (ALL pts.
 isSubt ?ptn pts & isCut pts -->
    isSubt (Pr ?seq ?rule ?ptl) pts & Pr ?seq ?rule ?ptl ~= pts
  | cutForm (Pr ?seq ?rule ?ptl) = cutForm pts &
    (pts, Pr ?seq ?rule ?ptl) : LRPorder)"

Definition 5.8 (c8redP) A reduction from Π_{0} to Π_{1} satisfies c8redP if the lowest rule of Π_{0} is ( cut), and for each subtree Π_{1}^{s} of Π_{1} whose lowest rule is ( cut), either (a) Π_{1}^{s} is a proper subtree of Π_{0}, or (b) the cut-formula of Π_{1}^{s} is smaller than the cut-formula of the lowest rule of Π_{0}.

   c8redP = "c8redP ?pt ?ptn == ALL pts.
     isSubt ?ptn pts & botRule pts = cutr -->
       isSubt ?pt pts & ?pt ~= pts |
       size (cutForm pts) < size (cutForm ?pt)"

Note that both Definition 5.8(b) and Definition 5.7(b) imply (Π_{1}^{s}, Π_{0}) ∈ dtorder. We now define a cut-reduction (being either parametric or principal) as satisfying one of the properties nparRedP and c8redP, as well as some further simple conditions which help the proof.

Definition 5.9 (cutReduces) The derivation tree Π_{0} cut-reduces to Π_{1} if the following hold simultaneously: Π_{0} and Π_{1} satisfy either nparRedP (for a parametric reduction) or c8redP (for a principal reduction); Π_{0} and Π_{1} have the same conclusion; the bottom rule of Π_{0} is ( cut); Π_{0} and Π_{1} are not identical; Π_{1} does not consist solely of an unfinished leaf; and Π_{0} has at least one immediate subtree.

cutReduces_Pr = "cutReduces (Pr ?seq ?rule ?ptl) ?ptn = (
 (nparRedP (Pr ?seq ?rule ?ptl) ?ptn
   | c8redP (Pr ?seq ?rule ?ptl) ?ptn)
  & conclPT ?ptn = ?seq & ?rule = cutr
  & (Pr ?seq ?rule ?ptl) ~= ?ptn & ~ isUnf ?ptn & ?ptl ~= [] )"

Note that for the purposes of the proof of strong normalisation, we have defined cut-reduction weakly in that, for example, we do not require that the new derivation tree ptn be well-formed (via allPT wfb ptn) or require that it use rules which belong to the calculus (via allPT (frb rls) ptn). However the definition is also strong in that it requires that either nparRedP or c8redP holds. Later we will show that the reductions in which we are interested do satisfy nparRedP or c8redP. The result of this is that we prove strong normalisation for a larger class of reductions than we are really interested in. The requirement that Π_{0} and Π_{1} be distinct is necessary to ensure that null reductions are excluded.

5.5 Strong-Normalisation

Lemma 5.3 (dth) For a given derivation Π_{0}, if all derivation trees Π′ <_{dt} Π_{0} have the property snHered, then so does Π_{0}.

dth = "ALL pt'. (pt', ?pt) : dtorder --> snHered pt'
       ==> snHered ?pt" : thm

Proof: The machine-proof is quite complicated, and a careful examination of it highlights why the definition of dtorder needs to be so complex. Q.E.D.

Theorem 5.3 (all sn) Every derivation tree is strongly normalisable.

   all_snH = "snHered ?pt"    : thm
   all_sn  = "strongNorm ?pt" : thm

Proof: By well-founded induction, it follows from Lemma 5.3 that every derivation tree satisfies snHered; the result follows from Lemma 5.2. Q.E.D.

At this point we have actually shown using Isabelle that a class of reductions which we have defined is strongly normalising. We need to show that this class of reductions contains the ones we are interested in.

5.6 Making A Cut (Left) Principal

The following are the main theorems used to develop the mechanised proof based on making cuts (left and right) principal.

We use a functional definition mLP ptAY seqY ptA of the transformation used to make a cut left-principal. The arguments to mLP are: a derivation tree ptAY with root A ⊢ Y such as the right subtree Π_{R} of the left tree given in Figure 5; a sequent seqY; and a derivation tree ptA with root seqA such as the tree with root X ⊢ A which forms the left subtree of the left tree given in Figure 5. Sequent seqA will usually contain occurrences of A in one or more succedent position(s), and sequent seqY is seqA with zero, one or more of these occurrences of A changed to Y. The result of mLP is a new derivation tree, with root seqY whose new cuts (on A) are left-principal, such as the right tree given in Figure 5. The definition of mRP is similar. We also defined a function ncLP seqY ptA which returns true iff calculating the tree mLP ptAY seqY ptA does not involve traversing another cut; ncRP has analogous meaning.

We need to show that the transformation performed by mLP are in the class of reductions that are strongly normalising. We assume an initial cut as in Figure 5: that is, with conclusion X ⊢ Y and cut-formula A.

Theorem 5.4 (pRedLP2) Consider a parametric reduction of a cut which proceeds by transforming the left subtree (to change its conclusion from X[A] ⊢ A to X[Y] ⊢ Y), using the function mLP. Assume that the subtree satisfies the condition ncLP (in effect, that the transformation can be performed without traversing another cut). Also assume the cut is not already left-principal. Then the reduction satisfies the condition nparRedP.

pRedLP2 = "[| ?ptY = mLP ?ptAY ?seqY ?ptA;
      ?pt = Pr ?seqY cutr [?ptA, ?ptAY];
      ~ rootIsSucP ?ptA; valid rls ?pt;
      ncLP ?seqY ?ptA |]
   ==> nparRedP ?pt ?ptY & valid rls ?ptY &
       conclPT ?ptY = conclPT ?pt" : thm

The condition ~rootIsSucP?ptA means that the cut is not already leftprincipal. It is required to avoid null reductions: if the cut is already leftprincipal, then ?pt and mLP ?ptAY ?seqY ?ptA are equal. The following result is similar, but says that the parametric reduction is a cut-reduction.

Theorem 5.5 (pRedLP3) The same as Theorem 5.4, except with conclusion

cutReduces ?pt ?ptY & valid rls ?ptY"

There are analogous theorems pRedRP2, pRedRP3, which guarantee that we can make a cut right-principal, and consequently another theorem which guarantees that we can make a cut (left and right) principal. The associated functions also produce derivations that satisfy cutReduces. Thus every parametric move corresponds to a reduction which is in the class of strongly normalising reductions.

5.7 Dealing With Principal Cuts

For each logical connective and constant in the calculus, we prove a result like the following one for ∨.

Theorem 5.6 (orC8) Assume we are given a valid derivation tree pt. Assume that if the bottom rule of pt is ( cut), then the cut is principal and its cut-formula is A ∨ B. Also assume that any cuts above the root of pt have either A or B as cut-formula. Then then there is a valid derivation tree ptn with the same conclusion as pt, such that all cuts in ptn have either A or B as cut-formula.

orC8 = "[| allPT wfb ?pt; allPT (frb rls) ?pt;
  cutIsLRP (?A v ?B) ?pt; allNextPTs (cutOnFmls {?B, ?A}) ?pt |]
 ==> EX ptn. conclPT ptn = conclPT ?pt & allPT wfb ptn &
    allPT (frb rls) ptn & allPT (cutOnFmls {?B, ?A}) ptn" : thm

We have also shown that the principal reductions described above satisfy c8redP, and are in fact cut-reductions: for each logical connective. These results (one for each logical connective) were combined to give Theorem 5.7.

Theorem 5.7 (vformC8W') If the bottom-most rule of a valid derivation tree Π_{0} is a (left and right) principal cut, then there exists a valid derivation tree Π_{1} with the same conclusion as Π_{0}, such that Π_{0} cutReduces to Π_{1}.

vformC8W' = "[| ?pt = Pr ?seq cutr ?ptl;  valid rls ?pt ;
       cutIsLRP ?form ?pt |]
   ==> EX ptn. cutReduces ?pt ptn & valid rls ptn" : thm

Thus every principal move gives a reduction which is in the class of strongly normalising reductions.

5.8 Cut-Elimination Via Strong Normalisation

Recall that a valid derivation tree is one which is well-formed, uses rules from rls, and has no unfinished leaves.

Definition 5.10 (validRed) A valid reduction is a reduction of tree Π_{0} to tree Π_{1}, where Π_{1} is a valid tree which has the same conclusion as Π_{0}.

validRed_def "validRed == {(ptn, pt).
    conclPT ptn = conclPT pt & valid rls ptn & reduces pt ptn}"

Lemma 5.4 A valid reduction of a subtree is a valid reduction of the whole tree.

Theorem 5.8 Parametric and principal moves give valid reductions.

Proof: Using pRedLP3, pRedRP3 and vformC8W'. Q.E.D.

Theorem 5.9 (cutExRed) For any valid tree with a single cut at the bottom there exists a cut-reduction to another valid tree with the same conclusion, using only parametric and principal moves.

cutExRed = "[| isCut ?pt; valid rls ?pt;
       allNextPTs (cutOnFmls {}) ?pt |]
   ==> EX ptn. cutReduces ?pt ptn & valid rls ptn" : thm

Proof: We use only pRedLP3 and pRedRP3 and vformC8W', so that the reductions are restricted to parametric and principal moves. Note that

conclPT ptn = conclPT pt is implied by cutReduces pt ptn. Q.E.D.

Theorem 5.10 (ExRed) For any valid tree which contains a cut, there is available at least one valid reduction (apply Theorem 5.9 to a top-most cut).

 ExRed = "[| valid rls ?pt ; ~ allPT (Not o isCut) ?pt |]
    ==> EX ptn. (ptn, ?pt) : validRed" : thm

Below, the notation ^* denotes transitive closure.

Theorem 5.11 (validRed min) For any derivation tree Π there exists a tree Π^{r} obtained from Π such that Π^{r} cannot be further validly reduced.

validRed_min = "EX ptn. (ptn, ?pt1) : validRed^* &
                ~ (EX pts. (pts, ptn) : validRed)" : thm

Proof: Every tree with a cut admits at least one valid reduction, and parametric and principal moves give valid reductions, and there is no infinite sequence of valid reductions. So repeatedly perform any sequence of principal and parametric reductions until no reduction is possible. Q.E.D.

Below, allPT (Not o isCut) ptn means that ptn is cut-free since o stands for composition of functions in Isabelle/HOL.

Theorem 5.12 (redNoCut) For any valid tree Π, there exists a cut-free valid tree Π^{r}, obtained from Π by repeated valid reductions, such that Π^{r} has the same conclusion as Π.

redNoCut = "valid rls ?pt ==> EX ptn.
   allPT (Not o isCut) ptn & valid rls ptn &
   (ptn, ?pt) : validRed^* & conclPT ptn = conclPT ?pt" : thm

Corollary 5.1 Any sequence of principal and parametric moves starting from some derivation Π containing cuts, eventually terminates with a cutfree derivation Π^{r} that has the same conclusion as Π.

Proof: In Theorem 5.12, starting from Π, choose a sequence of parametric and principal reductions only. Since valid reductions are reductions, they are strongly normalising by Theorem 5.3, hence this sequence must terminate with some valid derivation Π^{r}, to which no reduction is applicable. This is only possible if Π^{r} is cut-free. Q.E.D.

We therefore have cut-elimination via strong normalisation.

Theorem 5.13 (cutElim SN) If a sequent can be derived using rules rls, then it can be derived from those rules omitting ( cut).

cutElim_SN = "IsDerivableR rls {} ?concl ==>
              IsDerivableR (rls - {cutr}) {} ?concl" : thm

6 Further Work

Belnap’s theorem is expressed to apply to any Display Calculus satisfying his conditions. To prove his theorem in that form would require modelling an arbitrary Display Calculus, with generalised rules for arbitrary sets of structural and logical connectives. A theoretical framework for such generalised rules can be found in [9]. This would require a “deeper” embedding still. For, in our first implementation [5], we set up the specific connectives and rules of δRA in Isabelle, and used Isabelle proofs as the δRA-derivations. In the present implementation, we again set up the specific connectives and rules of δRA, although we set up data structures to model arbitrary derivations. To prove the generic Belnap theorem, we need to set up the necessary structures to model arbitrary sets of connectives and rules from [9].

References

[1] D A. Basin and S Matthews. Structuring metatheory on inductive definitions. Information and Computation, 162(1-2):80–95, 2000.

[2] N D Belnap. Display logic. J. of Philosophical Logic, 11:375–417, 1982.

[3] M Borisavljevic, K Dosen, and Z Petric. On permuting cut with contraction. Mathematical Structures in Computer Science, 10:99–136, 2000.

[4] A Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.

[5] J Dawson and R Goré. A mechanised proof system for relation algebra using display logic. In JELIA98: Proceedings of the European Workshop on Logic in Artificial Intelligence, LNAI 1489:264-278. Springer, 1998.

    http://discus.anu.edu.au/~jeremy/dra/dra-files/.

[6] J E Dawson and R Goré. Embedding display calculi into logical frameworks: Comparing Twelf and Isabelle. In C Fidge (Ed), Proc. CATS

    2001, ENTCS, 42:89–103, http://www.elsevier.nl/gej-ng/31/29/
    23/68/show/Products/notes/cover.htt, 2001. Elsevier.

[7] M J C Gordon and T F Melham. Introduction to HOL: a Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.

[8] R Goré. Cut-free display calculi for relation algebras. In D van Dalen and M Bezem (Eds), CSL96: Selected Papers of the Annual Conference of the European Association for Computer Science Logic, volume LNCS 1258, pages 198–210. Springer, 1997.

[9] R Goré. Gaggles, Gentzen and Galois: How to display your favourite substructural logic. Logic Journal of the Interest Group in Pure and Applied Logic, 6(5):669–694, 1998.

[10] R Goré. Substructural logics on display. Logic Journal of the Interest Group in Pure and Applied Logic, 6(3):451–504, 1998.

[11] A Heuerding. Sequent Calculi for Proof Search in some Modal Logics. PhD thesis, Institute for Applied Mathematics and Computer Science, University of Berne, Switzerland, 1998.

[12] S. Matthews, A. Smaill, and D. Basin. Experience with FS_{0} as a framework theory. In G Huet and G Plotkin (Eds), Logical Environments, pages 61–82. Cambridge University Press, 1993.

[13] S Matthews. Implementing FS_{0} in isabelle: adding structure at the metalevel. In J Calmet and C Limongelli (Eds), Proc. Disco’96. Springer, 1996.

[14] A Mikhajlova and J von Wright. Proving isomorphism of first-order proof systems in HOL. In J Grundy and M Newey (Eds), Theorem Proving in Higher-Order Logics, LNCS 1479, pages 295–314. Springer, 1998.

[15] T Nipkow, L C. Paulson, and M Wenzel. Isabelle’s logics: HOL. Technical report. 15 February 2001, doc/logics-HOL.dvi in the Isabelle distribution.

[16] L C. Paulson. The Isabelle reference manual. Technical report. 15 February 2001, doc/ref.dvi in the Isabelle distribution.

[17] F Pfenning. Structural cut elimination. In Proc. LICS 94, 1994.

[18] D. Pym and J. Harland. A Uniform Proof-theoretic Investigation of Linear Logic Programming. J. of Logic and Computation 4:2:175-207, 1994.

[19] M. E. Szabo, editor. The collected papers of Gerhard Gentzen, pages 68–131. North-Holland, Amsterdam, 1969.

[20] H Wansing. Displaying Modal Logic, volume 3 of Trends in Logic. Kluwer Academic Publishers, Dordrecht, August 1998.

\begin{matrix}Π_{ZAB} \\ Z ⊢ A, B \end{matrix} (⊢ ∨) Z ⊢ A ∨ B  ^{\begin{matrix}Π_{AX} \\ A ⊢ X \end{matrix} \begin{matrix}Π_{BY} \\ B ⊢ Y \end{matrix} (∨ ⊢) A ∨ B ⊢ X, Y} (cut) Z ⊢ X, Y

Figure 3: Principal cut on formula A ∨ B

\begin{aligned}^{\begin{matrix}Π_{ZAB} \\ Z ⊢ A, B \end{matrix} (cs1) ∗A, Z ⊢ B} & \begin{matrix}Π_{BY} \\ B ⊢ Y \end{matrix} & (cut) & ∗A, Z ⊢ Y \\ & (\overline{cs1}) \\ Z ⊢ A, Y \end{aligned} ; (cs2) ; Z, ∗Y ⊢ A  \begin{matrix}Π_{AX} \\ A ⊢ X \end{matrix} (cut) Z, ∗Y ⊢ X

(\overline{cs2}) Z ⊢ X, Y

Figure 4: Transformed principal cut on formula A ∨ B

7 Appendix: An Operational View of Cut-Elimination

In this section we give an operational view of cut-elimination, to give some intuition of what is involved in the overall cut-elimination procedure a là Belnap [2]. We assume familiarity with notions like “parametric ancestors” of a cut formula from [2].

Definition 7.1 An application of the cut rule is left-principal [ right-principal] if the cut-formula is the principal formula of the left [right] premiss of the cut rule.

Belnap’s condition C8 guarantees that all principal cuts can be replaced by cuts on strictly smaller formulae. For example, the principal cut on A∨B shown in Figure 3 can be replaced by the derivation shown in Figure 4. The replacement derivation contains cuts only on A and B, which are smaller formulae than A ∨ B. Where the cut-formula is a single formula variable, it is necessarily introduced by the identity axiom: such cuts can be removed trivially.

The transformation of a pricipal cut on A into one or more cuts on strict subformulae of A is known as a “principal move”. We now need a way to turn arbitrary cuts into principal ones.

\begin{aligned}Π[A] & (intro-A) & Z[A] ⊢ A \\ & (π) \\ Π_{L}[A] \end{aligned} ; (ρ) ; X ⊢ A \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} (cut) X ⊢ Y

Π′[Y] (intro-A) Z[Y] ⊢ A  \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} (cut) Z[Y] ⊢ Y

(π) Π_{L}[Y]

(ρ) X ⊢ Y

Figure 5: Making a cut left-principal

In the case of a cut that is not left-principal, say we have a tree like the one on the left in Figure 5. Then we transform the subtree rooted at X ⊢ A by simply changing its root sequent to X ⊢ Y, and proceeding upwards, changing all ancestor occurrences of A to Y. In doing this we run into difficulty at each point where A is introduced: at such points we insert an instance of the cut rule. The diagram on the right hand side of Figure 5 shows this in the case where A is introduced at just one point.

In Figure 5, the notation Π_{L}[A] and Z[A] means that the sub-derivation Π_{L} and structure Z may contain occurrences of A which are parametric ancestors of the cut-formula A: thus (intro-A) is the lowest rule where A is the principal formula on the right of ⊢. The notation Π_{L}[Y] and Z[Y] means that all such “appropriate” instances of A are changed to Y: that is, instances of A which can be traced to the instance displayed on the right in X ⊢ A. The rules contained in the new sub-derivation Π_{L}[Y] are the same as the rules used in Π_{L}; thus it remains to be proved that Π_{L}[Y] is well-formed. The resulting cut in the diagram on the right of Figure 5 is left-principal. Notice that the original sub-derivation Π may be transformed into a different sub-derivation Π′ during this process since the parametric ancestors of A occurring in Π[A] will in turn need to be “cut away” below where they are introduced, and replaced by Y.

There is one condition: for a parametric move, the portion of the derivation tree that is changed must not contain a cut: that is, there must be no cuts in the parts of the trees in Figure 5 shown below:

\begin{matrix}Z[A] ⊢ A & (π) & Π_{L}[A] \\ (ρ) \\ X ⊢ A \end{matrix}  \begin{matrix}Z[Y] ⊢ Y & (π) & Π_{L}[Y] \\ (ρ) \\ X ⊢ Y \end{matrix}

Subsequently, the “mirror-image” procedure is followed, to convert a left-principal cut into one or more (left- and right-)principal cuts.

The process of making a cut left-principal, or of making a left-principal cut (left and right) principal is called a “parametric move”.