Formalised Cut-elimination for the Display

Calculus of Relation Algebras

Jeremy E. Dawson and Rajeev Goré

Automated Reasoning Group  Formal Methods Group
Computer Sciences Laboratory  Dept. of Computer Science
Res. Sch. of Inf. Sci. and Eng.  Fac. of Eng. and Inf. Tech.
Institute of Advanced Studies  The Faculties

Australian National University

jeremy@discus.anu.edu.au           rpg@discus.anu.edu.au
discus.anu.edu/∼jeremy             discus.anu.edu.au/∼rpg

Goré supported by an Australian Research Council Queen Elizabeth II Fellowship. Dawson supported by an Australian Research Council Large Research Grant.

Semantics and Syntax of Logic of Relation Algebras

RA: Algebra of binary relations (sets of ordered pairs) over underlying set U Atomic constants: c ::= ⊥ | ⊤ | 1 | 0 (∅ | U × U | identity | diversity) Atomic formulae: p ::= p_{0} | p_{1} | p_{2} | ⋯ (relation symbols) Formulae: A ::= c | p | ¬A | A ∧ A | A ∨ A | ⌣ A | A ∘ A | A + A ¬ is complement ∧, ∨ are ∩, ∪ A + B is ¬(¬A ∘ ¬B) converse ⌣ A := {(y, x)|(x, y) ∈ A} composition A ∘ B := {(x, z)|∃y ∈ U. (x, y) ∈ A & (y, z) ∈ B}

Australian National University  2003  2

Display Calculus δRA for Relation Algebra

RA: Algebra of binary relations (sets of ordered pairs) over underlying set U Atomic constants: c ::= ⊥ | ⊤ | 1 | 0 (∅ | U × U | identity | diversity) Atomic formulae: p ::= p_{0} | p_{1} | p_{2} | ⋯ (relation symbols) Formulae: A ::= c | p | ¬A | A ∧ A | A ∨ A | ⌣ A | A ∘ A | A + A Structure: X ::= A | I | ∗X | X , X | E | •X | X ; X

Sequent:  X ⊢ Y  where X is the antecedent and Y is the succedent
Sequent rule:  (name) \frac{X_{1} ⊢ Y_{1} ⋯ X_{n} ⊢ X_{n}}{X ⊢ Y}  \frac{premisses}{conclusion}

Display Calculus δRA: Display Postulates

\begin{matrix}∗X ⊢ Y \\ ∗Y ⊢ X \end{matrix} \begin{matrix}X ⊢ ∗Y \\ Y ⊢ ∗X \end{matrix} \begin{matrix}∗ ∗ X ⊢ Y \\ X ⊢ Y \end{matrix}  \begin{matrix}•X ⊢ Y \\ X ⊢ •Y \end{matrix}  \begin{matrix}• • X ⊢ Y \\ X ⊢ Y \end{matrix} \begin{matrix}X ⊢ Z ; ∗ •Y \\ X ; Y ⊢ Z \\ Y ⊢ ∗ • X ; Z \end{matrix} \begin{matrix}Z ; ∗ •Y ⊢ X \\ Z ⊢ X ; Y \\ ∗ • X ; Z ⊢ Y \end{matrix}  \begin{matrix}X ⊢ Z , ∗ Y \\ X , Y ⊢ Z \\ Y ⊢ ∗X , Z \end{matrix} \begin{matrix}Z , ∗ Y ⊢ X \\ Z ⊢ X , Y \\ ∗X , Z ⊢ Y \end{matrix}

Intuition: Allow us to unravel complex structures: think of high school algebra where we solved x^{2} − 4 = 0 by “making x the subject”

Invertible rules: Reversible, merely bookkeeping device

\begin{matrix}∗X ⊢ Y \\ ∗Y ⊢ X \end{matrix} \begin{matrix}X ⊢ ∗Y \\ Y ⊢ ∗X \end{matrix} \begin{matrix}∗ ∗ X ⊢ Y \\ X ⊢ Y \end{matrix}  \begin{matrix}•X ⊢ Y \\ X ⊢ •Y \end{matrix}  \begin{matrix}• • X ⊢ Y \\ X ⊢ Y \end{matrix} \begin{matrix}X ⊢ Z ; ∗ •Y \\ X ; Y ⊢ Z \\ Y ⊢ ∗ • X ; Z \end{matrix} \begin{matrix}Z ; ∗ •Y ⊢ X \\ Z ⊢ X ; Y \\ ∗ • X ; Z ⊢ Y \end{matrix}  \begin{matrix}X ⊢ Z , ∗ Y \\ X , Y ⊢ Z \\ Y ⊢ ∗X , Z \end{matrix} \begin{matrix}Z , ∗ Y ⊢ X \\ Z ⊢ X , Y \\ ∗X , Z ⊢ Y \end{matrix}

Theorem (Belnap82): For every sequent X ⊢ Y and every substructure Z of X ⊢ Y, there is a structurally equivalent sequent Z ⊢ Y′ or X′ ⊢ Z that has Z displayed as the whole of its antecedent or succedent.

\begin{matrix}∗X ⊢ Y \\ ∗Y ⊢ X \end{matrix} \begin{matrix}X ⊢ ∗Y \\ Y ⊢ ∗X \end{matrix} \begin{matrix}∗ ∗ X ⊢ Y \\ X ⊢ Y \end{matrix}  \begin{matrix}•X ⊢ Y \\ X ⊢ •Y \end{matrix}  \begin{matrix}• • X ⊢ Y \\ X ⊢ Y \end{matrix} \begin{matrix}X ⊢ Z ; ∗ •Y \\ X ; Y ⊢ Z \\ Y ⊢ ∗ • X ; Z \end{matrix} \begin{matrix}Z ; ∗ •Y ⊢ X \\ Z ⊢ X ; Y \\ ∗ • X ; Z ⊢ Y \end{matrix}  \begin{matrix}X ⊢ Z , ∗ Y \\ X , Y ⊢ Z \\ Y ⊢ ∗X , Z \end{matrix} \begin{matrix}Z , ∗ Y ⊢ X \\ Z ⊢ X , Y \\ ∗X , Z ⊢ Y \end{matrix}

Theorem (Belnap82): For every sequent X ⊢ Y and every substructure Z of X ⊢ Y, there is a structurally equivalent sequent Z ⊢ Y′ or X′ ⊢ Z that has Z displayed as the whole of its antecedent or succedent.

e.g. \frac{∗p_{3} ⊢ p_{0} ; (p_{0} ∘ p_{1})}{∗(p_{0} ; (p_{0} ∘ p_{1})) ⊢ p_{3}}  \frac{∗p_{3} ; ∗ •(p_{0} ∘ p_{1}) ⊢ p_{0}}{∗p_{3} ⊢ p_{0} ; (p_{0} ∘ p_{1})} \frac{∗ • p_{0} ; p_{3} ⊢ p_{0} ∘ p_{1}}{∗p_{3} ⊢ p_{0} ; (p_{0} ∘ p_{1})}

Display Calculus δRA: Logical Rules

Left and right introduction rules for every logical connective

(id) p ⊢ p  (cut) \frac{X ⊢ A A ⊢ Y}{X ⊢ Y}
(+ ⊢) \frac{A ⊢ X B ⊢ Y}{A + B ⊢ X ; Y}  decoding/rewrite  (⊢ +) \frac{Z ⊢ A ; B}{Z ⊢ A + B}

(∧ ⊢) \frac{A , B ⊢ Z}{A ∧ B ⊢ Z} rewrite/decoding (⊢ ∧) \frac{X ⊢ A Y ⊢ B}{X , Y ⊢ A ∧ B}

Introduced formula is always displayed Gentzen overloading: Antecedent Part ⊤ ¬ ∧ 1 ⌣ ∘ Connective I ∗ , E • ; Succedent Part ⊥ ¬ ∨ 0 ⌣ +

Example: ∗(p_{0} ; p_{1}) ⊢ ∗ • (p_{1} , p_{3}) means ¬(p_{0} + p_{1}) ⊢ ¬ ⌣ (p_{1} ∧ p_{3})

Australian National University  2003  7

Display Logic δRA: Structural Rules

A structural rule contains no logical connectives and no formula variables.

(A ; ⊢) \begin{matrix}X ; (Y ; Z) ⊢ W \\ (X ; Y) ; Z ⊢ W \end{matrix}  ^{(⊢ A) \begin{matrix}W ⊢ X , (Y , Z) \\ W ⊢ (X , Y) , Z \end{matrix}}  (⊢ P) \frac{Z ⊢ Y , X}{Z ⊢ X , Y}^{(I_{−}^{+} ⊢) \begin{matrix}X , I ⊢ Y \\ X ⊢ Y \\ I , X ⊢ Y \end{matrix}} ^{(⊢ E_{−}^{+} ) \begin{matrix}X ⊢ E ; Y \\ X ⊢ Y \\ X ⊢ Y ; E \end{matrix}} ^{(⊢ •E) \begin{matrix}X ⊢ E \\ X ⊢ •E \end{matrix}} ^{(•I ⊢) \begin{matrix}I ⊢ X \\ •I ⊢ X \end{matrix}} (M ⊢) \frac{X ⊢ Z}{X , Y ⊢ Z}  (⊢ C) \frac{Z ⊢ X , X}{Z ⊢ X}  (tag) \frac{X ; Y ⊢ Z}{•Y ; • X ⊢ •Z}

Note: no (M) (P) or (C) rules for ; since ∘/+ are not classical connectives

Logical Variation Via Structural Rules (modularity)

An equation A ≤ B is primitive iff A and B are built from relational variables and the constants ⊤ and 1 with the help of ⌣, ∧, ∨ and ∘ only, and if no relational variable appears in A more than once (Kracht96).

Logical Variation Via Structural Rules (modularity)

Purely syntactic class of formulae An equation A ≤ B is primitive iff A and B are built from relational

variables and the constants ⊤ and 1 with the help of ⌣, ∧, ∨ and ∘ only, and if no relational variable appears in A more than once (Kracht96).

Examples: from modal logic

reflexivity  seriality  symmetry  transitivity (T) 1 ≤ A  (D) A ∘ ⊤ = ⊤ (B) A = ⌣A  (4) A ∘ B ≤ A ∨ B

An equation A ≤ B is primitive iff A and B are built from relational variables and the constants ⊤ and 1 with the help of ⌣, ∧, ∨ and ∘ only, and if no relational variable appears in A more than once (Kracht96).

reflexivity  seriality  symmetry  transitivity (T) 1 ≤ A  (D) A ∘ ⊤ = ⊤ (B) A = ⌣A  (4) A ∘ B ≤ A ∨ B (T) \frac{X ⊢ Z}{E ⊢ Z}  (D) \begin{matrix}I ⊢ Z \\ X ; I ⊢ Z \end{matrix} (B) \begin{matrix}•X ⊢ Z \\ X ⊢ Z \end{matrix} (4) \frac{X_{1} ⊢ Z X_{2} ⊢ Z}{X_{1} ; X_{2} ⊢ Z}

Kracht shows how to convert each primitive equation into a purely structural rule An equation A ≤ B is primitive iff A and B are built from relational

variables and the constants ⊤ and 1 with the help of ⌣, ∧, ∨ and ∘ only, and if no relational variable appears in A more than once (Kracht96).

reflexivity  seriality  symmetry  transitivity (T) 1 ≤ A  (D) A ∘ ⊤ = ⊤ (B) A = ⌣A  (4) A ∘ B ≤ A ∨ B (T) \frac{X ⊢ Z}{E ⊢ Z}  (D) \begin{matrix}I ⊢ Z \\ X ; I ⊢ Z \end{matrix} (B) \begin{matrix}•X ⊢ Z \\ X ⊢ Z \end{matrix} (4) \frac{X_{1} ⊢ Z X_{2} ⊢ Z}{X_{1} ; X_{2} ⊢ Z}

Theorem [Belnap 82]: Any display calculus whose rules obey eight conditions given by Belnap enjoys cut-elimination. If X ⊢ Y is derivable, then it is derivable without the cut rule.

Theorem: Using results of Kracht 96 we can construct a cut-free display calculus which is sound and complete for any primitive extension of RA.

Formalising δRA in Isabelle/HOL

Formulae: A ::= c | p | ¬A | A ∧ A | A ∨ A | ⌣ A | A ∘ A | A + A

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")
| PP string
| FV string

Formalising δRA in Isabelle/HOL

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

datatype structr = Comma structr structr                  '
| SemiC structr structr                  ;
| Star structr                             *
| Blob structr                             @
| I                                         $I
| E                                         $E
| Structform formula
| SV string                                $''X''
datatype sequent = Sequent structr structr                |-

$''X'' |- ''A'' is syntactic sugar for

Sequent (SV ''X'') (Structform (FV ''A''))

A Deep Embedding of Rules

(name) \frac{X_{1} ⊢ Y_{1} ⋯ X_{n} ⊢ X_{n}}{X ⊢ Y}  \begin{matrix}X ⊢ Y ; Z \\ ∗ • Y ; X ⊢ Z \end{matrix}

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

     ss1   "ss1 == Bidi ($''X'' |- $''Y''; $''Z'')
                          ( *@$''Y''; $''X'' |- $''Z'')"

Deep embedding because of the ''X''. Shallow embedding would use ?X.

This means we must handle substitutions explicitly.

rls is the set of rules of δRA

A shallow embedding would provide, not model, the set of rules.

Formalising Derivations

datatype dertree = Der sequent rule (dertree list)
                  | Unf sequent
True derivation has leaves Der (PP ''p'' |- PP ''p'') id []

A derived rule will have some Unfinished leaf sequents Example:

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

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

idf is the admissible rule A ⊢ A

Reasoning About Derivations

datatype dertree = Der sequent rule (dertree list)
                  | Unf sequent

wfb :: "dertree => bool" returns true if the end-sequent of dertree and the end-sequents of its immediate children in dertree list are a well-formed instance of rule

allDT ::  "(dertree => bool) => dertree => bool" returns true if

every node of dertree satisfies the given boolean valued function allDT wfb returns true if every rule application in dertree is well formed allDT (frb rules) returns true if every rule application in dertree is a member of set rules

Formalising Derivability

IsDerivableR ::"rule set => [sequent set,sequent] => bool"

Definition 1 IsDerivableR rules prems concl holds iff there exists a derivation tree dt which uses only rules from set rules, is well-formed, has conclusion concl, and has premisses from set prems.

 "IsDerivableR rules prems concl == (EX dt.
     allDT (frb rules) dt & allDT wfb dt &
     conclDT dt = concl & set (premsDT dt) <= prems)"

Lemma 1 The sequent PP ''p'' |- PP ''p'' is derivable for all atoms p

Proof: Let dt be Der (PP ''p'' |- PP ''p'') id [] in
  IsDerivableR rls {} (PP ''p'' |- PP ''p'')

Results About Derivability

Our main result about derivability is a recursive characterisation of derivability.

Theorem 1 A conclusion concl is derivable from premisses prems using rules rules iff 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

Formalising Derivable Rules

"IsDerivable rules (Rule prems concl) =
         IsDerivableR rules (set prems) concl"

Lemma 2 (idf ) The sequent ''A'' |- ''A'' is derivable for all formulae A that contain no formula variables Add the rule idf to rls :

  idf == Rule [] (''A'' |- ''A'')

Der (''A'' |- ''A'') idf [] stands for a complete derivation which uses the (proven) admissible rule idf that A ⊢ A is derivable Unf (''A'' |- ''A'') stands for an incomplete derivation with unfinished premiss A ⊢ A

Reducing a Left-and-Right Principal Cut

A cut on A is left- [right-] principal if the left [right] inference immediately above the cut introduces A via a logical rule, written (⊢ A) [(A ⊢)]

Π_{L} (⊢ A) X ⊢ A ^{Π_{R} (A ⊢) A ⊢ Y} X ⊢ Y

C8: All left-and-right principal cuts can be replaced by cuts on strictly smaller subformulae of A

Base Case: (cut) \frac{p ⊢ p p ⊢ p}{p ⊢ p}reduced to just p ⊢ p

Similar cases for ⊤, 1, ⊥, 0

Example of a Principal reduction (C8 condition)

\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

Principal cut on formula A ∨ B

\begin{matrix}Π_{ZAB} \\ Z ⊢ A, B \end{matrix} (dp) ∗A, Z ⊢ B \begin{matrix}Π_{BY} \\ B ⊢ Y \end{matrix} (cut) ∗A, Z ⊢ Y

(dp) Z ⊢ A, Y

(dp) Z, ∗Y ⊢ A

\begin{matrix}Π_{AX} \\ A ⊢ X \end{matrix}

(cut)
Z, ∗Y ⊢ X

(dp) Z ⊢ X, Y

Transformed derivation uses cuts only on A and B

Must exhibit and hard-wire such transformations for every logical connective

So if cut is not left-and-right principal then we try to make it so ...

Australian National University  2003  22

Making a cut left-principal

Given a derivation ending in a non left-and-right principal cut on formula A, we trace the ancestor occurrences of this A up Π_{L}:

\begin{matrix}Π_{L} \\ X ⊢ A \end{matrix} \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} X ⊢ Y

an ancestor of A is principal if introduced by logical rule (⊢ A) all other ancestors of A are parametric ancestors (including those

“introduced” by weakening there must be at least one introduction of A in every branch not all occurrences of A need be ancestors of this occurrence of A

Australian National University  2003  23

Making a cut left-principal

Given a derivation ending in a non left-and-right principal cut on formula A,

we trace all ancestor occurrences of this A up Π_{L}: Let Π[A? = Y] mean “in Π, replace all parametric ancestors of A with Y ” Suppose Π_{L} does not branch at all for simplicity

\begin{aligned}Π_{L}^{1} & (⊢ A) & V ⊢ A \\ & (π) \\ Π_{L}^{2} \end{aligned} ; (ρ) ; X ⊢ A \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} (cut) X ⊢ Y  \begin{aligned}^{Π_{L}^{′1} (⊢ A) V ⊢ A} & \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} & (cut) & V ⊢ Y \\ & (π) \\ Π_{L}^{2}[A? = Y] \end{aligned} ; (ρ) ; X ⊢ Y

New cut is left-principal (similarly make it also right principal)

Australian National University  2003  24

Making a cut left-principal – simpler cases

Π_{L}^{1} is empty, A introduced by A ⊢ A. No new cuts needed

\begin{aligned}A ⊢ A & (π) & Π_{L}^{2} \\ & (ρ) \\ X ⊢ A \end{aligned} \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} (cut) X ⊢ Y  \begin{aligned}\begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} & (π) & Π_{L}^{2}[A? = Y] \\ & (ρ) \\ X ⊢ Y \end{aligned}

Case for “introduction” by weakening, no new cuts needed

\begin{aligned}\begin{matrix}Π_{L}^{1} \\ V ⊢ W \end{matrix} & (Wk Z(A)) & V ⊢ W , Z(A) \\ & (π) \\ Π_{L}^{2} \end{aligned} ; (ρ) ; X ⊢ A \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} (cut) X ⊢ Y  \begin{aligned}\begin{matrix}Π_{L}^{1} \\ V ⊢ W \end{matrix} & (Wk Z(A? = Y)) & V ⊢ W , Z(Y) \\ & (π) \\ Π_{L}^{2}[A? = Y] \end{aligned} ; (ρ) ; X ⊢ Y
Australian National University  2003  25

Making a cut (left-and-right-)principal

Similarly to make a left-principal cut also right principal But note, one cut ⇝ several cuts (in general) Summing up:

single non-principal cut ⇝ several left-principal cuts
single left-principal cut ⇝ several principal cuts
single principal cut ⇝ several cuts on sub-formulae

To deal with several left-and-right-principal/left-principal/arbitrary cuts, deal

with a top-most one first (sub-tree containing single cut) Procedurally, this is a deeply nested recursion. Is an equally deeply nested inductive proof necessary?

Australian National University  2003  26

Cut-Admissibility (Weak Normalisation)

Show that the cut rule (cut) \frac{X ⊢ A A ⊢ Y}{X ⊢ Y} is admissible Assume: we have cut-free derivations of X ⊢ A and A ⊢ Y Show: that there is a cut-free derivation of X ⊢ Y In general, cut-elimination proceeds by repeatedly eliminating an arbitrary top-most cut Must show that this procedure terminates Usual argument is a double induction on the size (degree) of the cut formula and the heights of the given derivations (grade)

Cut-Admissibility By Structural Induction

elim eliminates a single arbitrary top-most cut, by turning it into several

left-principal cuts and using elimAllLP to eliminate them … Our initial derivation contains only one bottom-most cut which is not left and

right principal and we know how to turn it into multiple left principal cuts

Cut-Admissibility By Structural Induction

elim eliminates a single arbitrary top-most cut, by turning it into several

left-principal cuts and using elimAllLP to eliminate them … all new cuts are left principal elimAllLP eliminates several left-principal cuts, by repeatedly using elimLP

to eliminate the top-most remaining one …

Cut-Admissibility By Structural Induction

elim eliminates a single arbitrary top-most cut, by turning it into several

left-principal cuts and using elimAllLP to eliminate them … elimAllLP eliminates several left-principal cuts, by repeatedly using elimLP

to eliminate the top-most remaining one … elimLP eliminates a top-most left-principal cut, by turning it into several

principal cuts and using elimAllLRP to eliminate them … all new cuts are left-and-right principal

Cut-Admissibility By Structural Induction

elim eliminates a single arbitrary top-most cut, by turning it into several

left-principal cuts and using elimAllLP to eliminate them … elimAllLP eliminates several left-principal cuts, by repeatedly using elimLP

to eliminate the top-most remaining one … elimLP eliminates a top-most left-principal cut, by turning it into several

principal cuts and using elimAllLRP to eliminate them … elimAllLRP eliminates several principal cuts, by repeatedly using elimLRP

to eliminate the top-most remaining one … elimLRP eliminates a top-most principal cut, by turning it into several cuts on

smaller cut-formulae, and using elimAll to eliminate them … all new cuts are on strictly smaller cut-formulae

Australian National University  2003  31

Cut-Admissibility By Structural Induction

elim eliminates a single arbitrary top-most cut, by turning it into several

left-principal cuts and using elimAllLP to eliminate them … elimAllLP eliminates several left-principal cuts, by repeatedly using elimLP

to eliminate the top-most remaining one … elimLP eliminates a top-most left-principal cut, by turning it into several

principal cuts and using elimAllLRP to eliminate them … elimAllLRP eliminates several principal cuts, by repeatedly using elimLRP

to eliminate the top-most remaining one … elimLRP eliminates a top-most principal cut, by turning it into several cuts on

smaller cut-formulae, and using elimAll to eliminate them … elimAll eliminates several arbitrary cuts, by repeatedly using elim to

eliminate the top-most remaining one … termination

Australian National University  2003  32

Putting It All Together

  canElim       :: "(dertree => bool) => bool"
  canElimAll   :: "(dertree => bool) => bool"

canElim f means that if a derivation tree pt has no cuts other than at the bottom, and satisfies f, then there is an equivalent cut-free derivation tree.

canElimAll f means that if every subtree of a given tree pt satisfies f, then there is a cut-free derivation tree pt' equivalent to pt (we also require that if the bottom rule of pt is not (cut), then the bottom rule of pt' is the same).

allLP' = "canElimAll (cutIsLP ?A) ==> canElim (cutOnFmls {?A})"

Here f is (cutIsLP ?A) [(cutOnFmls {?A})] which means that if the lowest rule application is cut then it is a left-principal cut with cut formula ?A [if the lowest rule application is cut then the cut formula is from set {?A}]

allLP' means “if you can eliminate several cuts, all left-principal on A, then you can eliminate a single cut, at the bottom, on A” (its backwards!)

Australian National University  2003  33

Putting It All Together ...

allLP' = "canElimAll (cutIsLP ?A) ==> canElim (cutOnFmls {?A})"
allLRP' = "canElimAll (cutIsLRP ?A) ==> canElim (cutIsLP ?A)"
elimLRP = "canElim (cutIsLRP ?A) ==> canElimAll (cutIsLRP ?A)"
elimLP = "canElim (cutIsLP ?A) ==> canElimAll (cutIsLP ?A)"

Chaining these implications gives

canElim (cutIsLRP ?A) ==> canElim (cutOnFmls ?A)

Dealing with left-right-principal cuts gives

canElimAll (cutOnFmls {?A, ?B}) ==>
    canElim (cutIsLRP (?A v ?B))
elimFmls = "canElim (cutOnFmls ?s) ==> canElimAll (cutOnFmls ?s)"
"[| canElim (cutOnFmls {?A}); canElim (cutOnFmls {?B}) |]
     ==> canElim (cutOnFmls {?A v ?B})"

Finally ...

A proof by induction on the structure of a formula then gives

canElimFml = "canElim (cutOnFmls {?fml})"

(“you can eliminate one cut on any given formula fml”),

canElimAny = "canElim (cutOnFmls UNIV)",

(“you can eliminate one cut whatever the cut-formula”), and, using elimFmls,

canElimAll = "canElimAll (cutOnFmls UNIV)"

Finally we convert canElimAll into

cutElim = "IsProvableR rls {} ?concl  ==>
             IsProvableR (rls - {cut}) {} ?concl"

Strong Normalisation

Cut-admissibility proceeds by eliminating the top-most cut Strong normalisation: define reduction steps, eliminate any cut that can be reduced, and prove that this cut-elimination procedure terminates: Π_{n} < Π_{n−1} < ⋯ < Π_{2} < Π_{0} Π_{n} is cut-free n is finite weak-normalisation (attacking top most cut) is an instance of this method Usually define reductions as either a parametric or principal move, with proviso that we must not cross a cut in a parametric move

Australian National University  2003  36

Why Formalise (in Isabelle) ?

Strong-normalisation proofs are notoriously difficult involving many cases We tried to formalise Heinrich Wansing’s proof of strong-normalisation for display logic, but got stuck at one particular case

Why Formalise (in Isabelle) ?

Strong-normalisation proofs are notoriously difficult involving many cases We tried to formalise Heinrich Wansing’s proof of strong-normalisation for display logic, but got stuck at one particular case Found a problem ... Wansing assumes that Π_{L}^{1} is unchanged!

V_{A} is (∗A , X) V_{Y} is (∗Y , X)

\begin{matrix}Π_{L}^{1} & (⊢ A) & V_{A} ⊢ A \\ (dp) \\ X ⊢ A, A \end{matrix} ; (ctr) ; X ⊢ A \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} (cut) X ⊢ Y  \begin{aligned}^{Π_{L}^{′1} (⊢ A) V_{Y} ⊢ A} & \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} & (cut) & V_{Y} ⊢ Y \\ & (dp) \\ X ⊢ Y, Y \end{aligned} ; (ctr) ; X ⊢ Y

Branch in left subtree — before and after

Π′ (intro-A) X′ ⊢ A ^{Π′′ (intro-A) X′′ ⊢ A} (π) Π_{L}

(ρ) X ⊢ A

\begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix}

(cut)
X ⊢ Y

\begin{matrix}Π′ \\ X′ ⊢ A \end{matrix} \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} (cut) X′ ⊢ Y ^{\begin{matrix}Π′′ \\ X′′ ⊢ A \end{matrix} \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} (cut) X′′ ⊢ Y} (π) Π_{L}[A?= Y]

(ρ) X ⊢ Y

Two successive introductions – before

Π  (ρ) X, B ⊢ ∗B

(⊢ ¬) X, B ⊢ ¬B

(dp) ∗¬B, X ⊢ ∗B

(⊢ ¬) ∗¬B, X ⊢ ¬B

(dp) X ⊢ ¬B, ¬B

(⊢ cont) X ⊢ ¬B

\begin{matrix}Π_{R} \\ ¬B ⊢ Y \end{matrix}

(cut)

X ⊢ Y

Two successive introductions – after

\begin{aligned}\begin{aligned}Π & (ρ) & X, B ⊢ ∗B \\ & (⊢ ¬) \\ X, B ⊢ ¬B \end{aligned} & \begin{matrix}Π_{R} \\ ¬B ⊢ Y \end{matrix} & (cut) & X, B ⊢ Y \\ & (dp) \\ ∗Y, X ⊢ ∗B \end{aligned} ; (⊢ ¬) ; ∗Y, X ⊢ ¬B\begin{matrix}Π_{R} \\ ¬B ⊢ Y \end{matrix} (cut) ∗Y, X ⊢ Y

(dp) X ⊢ Y, Y

(⊢ cont) X ⊢ Y

Defining Reductions

Definition 2 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) ?dtn = False"
reduces_Der  = "reduces (Der ?seq ?rule ?dtl) ?dtn =
 ( (EX dtl'. onereduces ?dtl dtl' & ?dtn = Der ?seq ?rule dtl')
   | cutReduces (Der ?seq ?rule ?dtl) ?dtn )"
onereduces_Nil  = "onereduces [] ?dtl' = False"
onereduces_Cons = "onereduces (?h # ?t) ?dtl' = ( ?dtl' ~= []
  & (reduces ?h (hd ?dtl') & ?t = (tl ?dtl')
      | ?h = (hd ?dtl') & onereduces ?t (tl ?dtl')) )"

Defining Strongly Normalising Derivation Trees

Definition 3 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 .

A derivation tree is strongly normalisable iff it is a member of sn set.

inductive "sn_set"
  intrs
     snI "(ALL dtn.
     reduces ?dt dtn --> dtn : sn_set) ==> ?dt : sn_set"

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.

Various Binary Orderings

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

a. the cut in Π_{1} is left-principal or right-principal, and the cut in Π_{0} is neither, or

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

2. Π_{1} <_{cut} Π_{0} if the bottom inferences of derivations Π_{1} and Π_{0} are both cut, and if either

a. the size of the cut-formula of Π_{1} is smaller than that of Π_{0}, or

b. each derivation has the same cut-formula, and Π_{1} <_{LRP} Π_{0}.

Various Binary Orderings

1. Π_{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}.

2. Π_{1} <_{dt} Π_{0} iff any of the following hold:

a. the bottom inference of Π_{1} is not cut, but that of Π_{0} is

b. Π_{1} <_{cut} Π_{0}

c. Π_{1} <_{sn1} Π_{0}.

Theorem 2 The relations LRPorder, cutorder, sn1order, and dtorder

are well-founded

Despite 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}.

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 4 Π satisfies snHered iff: if all the immediate subtrees of Π are strongly normalisable then Π is strongly normalisable.

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

Lemma 3 A derivation tree Π is strongly normalisable iff every subtree of Π has the property snHered. Proof: The “only if” part uses a clever instantiation of a theorem generated automatically by Isabelle from the inductive definition of sn set. The “if” part uses induction on the height of Π using the assumption that every subtree of Π, including itself, has the property snHered.

Australian National University  2003  46

Defining Cut-Reductions

Definition 5 Two derivation trees Π_{0} and Π_{1} satisfy nparRedP 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}. Definition 6 Two derivation trees Π_{0} and Π_{1} satisfy 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 that of the lowest rule of Π_{0}.

Defining Cut-Reduction and Hence Reduction

Definition 7 The derivation tree Π_{0} cut-reduces to Π_{1} if the following hold simultaneously:

(a) Π_{0} and Π_{1} satisfy either nparRedP (for a parametric reduction) or c8redP (for a principal reduction)

(b) Π_{0} and Π_{1} have the same conclusion

(c) the bottom rule of Π_{0} is cut

(d) Π_{0} and Π_{1} are not identical

(e) Π_{1} does not consist solely of an unfinished leaf

(f) and Π_{0} has at least one immediate subtree

Australian National University  2003  48

Strong-Normalisation

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

dth = "ALL dt'. (dt', ?dt) : dtorder --> snHered dt'
        ==> snHered ?dt" : 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. Theorem 3 Every derivation tree is strongly normalisable.

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

Proof: By well-founded induction, it follows from Lemma 4 that every derivation tree satisfies snHered; the result follows from Lemma 3.

Australian National University  2003  49

Where are we?

We have actually shown using Isabelle that a class of reductions which we have defined (in terms of cutReduces, and hence of nparRedP and c8redP) is strongly normalising. We would like to show that this class of reductions contains the ones to which Wansing’s theorem refers.

We can’t do that, but we can at least show that this class contains enough reductions to eliminate any cuts.

Dealing With Parametric Cuts

Theorem 4 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 transformation can be performed without traversing another cut. Also assume the cut is not already left-principal. Then the reduction satisfies the condition nparRedP.

Theorem 5 The same as Theorem 4, except with conclusion “Then the reduction satisfies the condition cutReduces”.

Analogous theorems pRedRP2, pRedRP3 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 in the class of strongly normalising reductions.

Australian National University  2003  51

Dealing With Principal Cuts

Theorem 6 Case for ∨: Given a valid derivation tree dt, assume that if the bottom rule of dt is cut, then the cut is principal and its cut-formula is A ∨ B. Then then there is a valid derivation tree dtn with the same conclusion as dt such that dt and dtn satisfy c8redsfP (since the original cut on A ∨ B is replaced with new cuts on its proper subformulae A and B).

These principal reductions satisfy c8redsfP and hence c8redP, and are in fact cut-reductions. These results (one for each logical connective) give

Theorem 7 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}.

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

Cut-Elimination Via Strong Normalisation

Definition 8 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}. Theorem 8 Parametric and principal moves give valid reductions. Theorem 9 For any valid tree which contains a cut, there is available at least one valid reduction (reduce a top-most cut). Corollary: Any sequence of principal and parametric moves starting from some derivation Π containing cuts, eventually terminates with a cut-free derivation Π^{r} that has the same conclusion as Π. Theorem 10 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

Australian National University  2003  53

Belnap’s Conditions and New C8

Appendix: Belnap’s Conditions.

For every sequent rule Belnap82, page 388 first defines the following notions: in an application Inf of a sequent rule (ρ), “constituents occurring as part of occurrences of structures assigned to structure-variables are defined to be parameters of Inf ; all other constituents are defined as nonparametric, including those assigned to formula-variables. Constituents occupying similar positions in occurrences of structures assigned to the same structure-variable are defined as congruent in Inf ”. The eight (actually seven) conditions shown below are from [Kracht96]:

(C1) Each formula which is a constituent of some premiss of a rule ρ is a subformula of some formula in the conclusion of ρ.

(C2) Congruent parameters are occurrences of the same structure.

(C3) Each parameter is congruent to at most one constituent in the conclusion. Equivalently, no two constituents of the conclusion are congruent.

(C4) Congruent parameters are either all antecedent parts or all succedent parts of their respective sequent.

(C5) If a formula is non-parametric in the conclusion of a rule ρ, it is either the entire antecedent, or the entire succedent (called a principal formula).

(C6/7) Each rule is closed under simultaneous substitution of arbitrary structures for congruent parameters.

(C8) If there are inference rules ρ_{1} and ρ_{2} with respective conclusions X ⊢ φ and φ ⊢ Y with φ principal in both inferences (in the sense of C5), and if (cut) is applied to yield X ⊢ Y then, either X ⊢ Y is identical to X ⊢ φ or to φ ⊢ Y; or it is possible to pass from the premisses of ρ_{1} and ρ_{2} to X ⊢ Y by means of inferences falling under (cut) where the cut-formula is always a proper subformula of φ.