Introduction Sequents, Multisets, Sets and Provability Logic Reasoning About Derivations and Derivability Capturing the Core of Cut-Admissibility Proofs The Proof of Cut-Admissibility for GLS Conclusion

Generic Methods for Formalising Sequent Calculi Applied to Provability Logic

Jeremy Dawson and Rajeev Goré

Logic and Computation Group School of Computer Science

College of Engineering and Computer Science Australian National University Canberra ACT 0200, Australia

http://users.rsise.anu.edu.au/~jeremy/
  http://users.rsise.anu.edu.au/~rpg/

October 5, 2010

Outline

1 Introduction
2 Sequents, Multisets, Sets and Provability Logic
3 Reasoning About Derivations and Derivability

Derivability Predicates and their Induction Principles

4 Capturing the Core of Cut-Admissibility Proofs
5 The Proof of Cut-Admissibility for GLS

Deep and Shallow Embeddings

6 Conclusion

Introduction

Formalisation of cut-admissibility for the GLS sequent system cut-admissibility applies for many sequent systems proofs can be tedious — details omitted (“other cases are similar”) we try to get common elements of the proofs for re-use provability logic has unusual features (GL rule has formula on both sides of ⊢), proof more complex previous proofs wrong, or allegedly so but actually OK formalised proof in Isabelle/HOL confirms the result, omits no details, and uses many lemmas applicable for other logics

Sequents and Multisets, Sets and Provability Logic

sequents Γ ⊢ Δ where Γ and Δ are “collections” of formulae Our “collections” are multisets (unordered, but repetitions counted) Tree-shaped derivations, conclusion at the bottom Tree branches where rule has > 1 premise, leaf where rule has no premises

Provability Logic

explicit weakening and contraction rules usual (additive) rules for ¬, ∧, ∨, → additional rule GLR which characterises GL:

□X , X , □B ⊢ B

GLR or GLR(B) or GLR(X , B)

□X ⊢ □B

in our formalisation, cut or multicut rules not part of GLS

Γ ⊢ A, Δ  Γ, A ⊢ Δ

(cut)

Γ ⊢ Δ
Γ′ ⊢ A^{n}, Δ′  Γ′′, A^{m} ⊢ Δ′′

(multicut)

Γ′, Γ′′ ⊢ Δ′, Δ′′

Derivability Predicates and their Induction Principles

An inference rule is a list of premises and a conclusion. Then derrec rls prems is the set of sequents derivable using rules rls from the set prems of premises.

The induction principle (simplified) from the definition of derrec :

\frac{x ∈ derrec rls prems ∀c ∈ prems. P c ∀(ps, c) ∈ rls. (∀p in ps. P p) ⇒ P c}{P x}

Induction on two derivations

Induction for a property of two derivations (eg cut-admissibility!)

cl ∈ derrec rlsl {} cr ∈ derrec rlsr {}

∀(lps, lc) ∈ rlsl. ∀(rps, rc) ∈ rlsr.

(∀lp ∈ lps. P lp rc) ∧ (∀rp ∈ rps. P lc rp) ⇒ P lc rc P cl cr

to prove P(C_{l}, C_{r}), the induction hypothesis is that P(P_{li}, C_{r}) and P(C_{l}, P_{rj}) hold for all i and j:

P_{l1} … P_{ln} ; ρ_{l} ; C_{l}  P_{r1} … P_{rm} ; ρ_{r} ; C_{r}
......................... (cut ?)

?

The Induction Pattern in Cut-Admissibility Proofs

Definition of gen step2ssr

In the diagram below, to prove P(C_{l}, C_{r}), the induction hypothesis is that P(P_{li}, C_{r}) and P(C_{l}, P_{rj}) hold for all i and j:

P_{l1} … P_{ln} ; R_{l} ; C_{l}  P_{r1} … P_{rm} ; R_{r} ; C_{r}
......................... (cut ?)

?

gen step2ssr expresses that property P holds, given appropriate inductive hypotheses, for last rules on each side R_{l} and R_{r}. P might be that cut-admissibility holds for cut-formula A, rule set rls, assuming it holds for smaller (subformula relation sub)

The Induction Pattern in Cut-Admissibility Proofs

We defined a predicate gen step2ssr (see the paper, Defnition 1), which says that you can prove the inductive step at a point in the derivation We proved a lemma which says that if this property holds throughout a tree for a property P, then P holds (Theorem 1) Then we proved that this predicate gen step2ssr holds for the case where the cut-formula A is parametric on the left, subject to certain conditions: a result applicable to many cut-elimination proofs (Theorem 2)

The proof of Goré & Ramanayake, and our proof

The proof of Goré & Ramanayake Proves admissibity of (cut) (we prove admissibity of (multicut)) Induction on height of derivation and on “width” Induction on size of cut-formula.

In contrast, in our proof we prove admissibity of (multicut) Induction on “fact of” derivation and on del0 (approximates to ∂^{0}, related to width) Well-founded induction on immediate subformula relation

Deep and Shallow Embeddings — Derivations

Deep or shallow embeddings of derivations, rules and variables. shallow means that a feature in the logic is identified with the same feature of Isabelle/HOL

Derivations:

Deep: the actual derivation tree is a data structure in HOL

   datatype 'a dertree = Der 'a ('a dertree list)
       | Unf 'a (* unfinished leaf not proved *)

there is a predicate which tests whether each node of an derivation tree is an instance of a rule Shallow: no derivation tree data structure, but an inductive definition in HOL saying what formulae are derivable; (the course of a proof, in HOL, of a formula, could be described by a derivation tree)

Using a deep embedding — explicit derivation trees

To define del0 on a derivation we need an explicit derivation tree

A valid tree is one whose inferences are in the set of rules and which as a whole has no premises.

Lemma

Sequent X ⊢ Y is derivable, shallowly, from the empty set of premises using rules rls (ie, is in derrec rls {}) iff some explicit derivation tree dt is valid wrt. rls and has a conclusion X ⊢ Y .

"(?a : derrec ?rls {}) =
   (EX dt. valid ?rls dt & conclDT dt = ?a)"

“mix and match” a deep embedding (derivation trees) with a shallow embedding (inductively defined sets of derivable sequents)

Defining del0

Definition (del0)

For derivation tree dt and formula B, define del0 B dt: if the bottom rule of dt is GLR(Y , A) (for any Y , A), then del0 B dt is 1 (0) if □B is (is not) in the antecedent of the conclusion of dt if the bottom rule of dt is not GLR, then del0 B dt is obtained by summing del0 B dt' over all premise subtrees

dt' of dt.

ie, you go up each branch of an explicit derivation tree until you find an instance of the GLR rule, and count 1 where B is in Y

\frac{□Y , Y , □A ⊢ A}{□Y ⊢ □A}

The Proof

Lemma

If μ is a valid derivation tree with conclusion □X , X , □B ⊢ B, and del0 B μ = 0, then □X , X ⊢ B is derivable.

Proof. Applying the GLR rule to the □X , X , □B ⊢ B gives □X ⊢ □B. Tracing upwards, change each □B to □X in the usual way. Contraction is not problematic since we use, as the inductive hypothesis, that all occurrences of □B can be replaced by □X .

Introduction Sequents, Multisets, Sets and Provability Logic Reasoning About Derivations and Derivability Capturing the Core of Cut-Admissibility Proofs The Proof of Cut-Admissibility for GLS Conclusion

Defining muxbn

μ \{ \frac{Π_{l}}{□X , X , □B ⊢ B}

GLR(B)

□X ⊢ □B

Π_{r} ρ □B^{k}, Y ⊢ Z
.................................................. (multicut ?)

□X , Y ⊢ Z

Figure: A multicut on cut formula □B where □B is left-principal via GLR

Definition (muxbn) muxbn B n holds iff: for all instances of Figure 1 (for fixed B) such that del0 B μ ≤ n, the multicut in Figure 1 is admissible.

Proofs of muxbn

Lemma

If μ is a valid derivation tree with conclusion □X , X , □B ⊢ B, and del0 B μ = 0, and multicut on B is admissible, and □B^{k}, Y ⊢ Z is derivable, then □X , Y ⊢ Z is derivable. That is, if multicut on B is admissible, then muxbn B 0 holds.

Proof. □X ⊢ □B is derivable from □X , X , □B ⊢ B via GLR(X , B). By Lemma 3, □X , X ⊢ B is derivable. The rest of the proof is by induction on the derivation of □B^{k}, Y ⊢ Z, in effect, by tracing relevant occurrences of □B up that derivation. Suppose an inference GLR(Y , C) is encountered, with B in Y . (see next slide)

□B^{k}, B^{k}, □Z, Z, □C ⊢ C
GLR(Y , C)
□B^{k}, □Z ⊢ □C

Z is Y with B deleted. By induction, □X , B^{k}, □Z, Z, □C ⊢ C is derivable. From there we have the derivation shown below.

Lemma 3 ; □X , X ⊢ B  □X , B^{k}, □Z, Z, □C ⊢ C

mcut(B)

□X , □X , X , □Z, Z, □C ⊢ C

ctr

□X , X , □Z, Z, □C ⊢ C

GLR(C)

□X , □Z ⊢ □C

Additional weakening steps necessary if □B in Z or if B in □Z (shown by machine-checking!)

From muxbn B n to muxbn B (n + 1)

μ \{ \frac{Π_{l}}{□X , X , □B ⊢ B}

GLR(B) □X ⊢ □B

Suppose del0 B μ = n + 1. Since del0 B μ > 0, the tree μ/□X ⊢ □B contains one or more branches with a GLR rule, with □B in the antecedent. (one such branch shown).

□G, G, □B^{k}, B^{k}, □A ⊢ A

GLR(A)

□G, □B^{k} ⊢ □A

⋮
□X , X , □B ⊢ B

GLR(X , B)

□X ⊢ □B

From muxbn B n to muxbn B (n + 1)

□G, G, □B^{k}, B^{k}, □A ⊢ A

GLR(A) (delete this)

□G, □B^{k} ⊢ □A

⋮
□X , X , □B ⊢ B
GLR(X , B)
□X ⊢ □B

Delete top step, adjoin □A on the left, extra weakening step:

□A, □G, □B^{k} ⊢ □A ; ⋮

□A, □X , X , □B ⊢ B

(weakening) (extra step)

□A, A, □X , X , □B ⊢ B

GLR(B)

□A, □X ⊢ □B

Call this μ^{A}/□A, □X ⊢ □B, then del0 B μ > del0 B μ^{A}, so μ^{A}/□A, □X ⊢ □B can be left branch of an admissible multicut.

Multicutting with □A, □X ⊢ □B

□A, □X ⊢ □B  □X , X , □B ⊢ B
.......................................... (multicut + ctr)
□A, □X , X ⊢ B

□A, □X ⊢ □B  □G, G, □B^{k}, B^{k}, □A ⊢ A
..................................................... (multicut + ctr)
□G, G, □X , B^{k}, □A ⊢ A

Now, multicut on B (smaller cut-formula), and contraction, gives

□G, G, □A, □X , X ⊢ A

GLR

□G, □X ⊢ □A

(weakening)

□G, □X , □B^{k} ⊢ □A

Introduction Sequents, Multisets, Sets and Provability Logic Reasoning About Derivations and Derivability Capturing the Core of Cut-Admissibility Proofs The Proof of Cut-Admissibility for GLS Conclusion

From del0 B μ = n + 1 to del0 B μ′ = n

□G, □B^{k} ⊢ □A ; ⋮

□X , X , □B ⊢ B

We use this proof again, now adjoin □X on the left, to get

previous slide □X , □G, □B^{k} ⊢ □A

⋮
□X , □X , X , □B ⊢ B

(contraction)

□X , X , □B ⊢ B

That is, given a derivation μ of □X , X , □B ⊢ B with del0 B μ = n + 1, we have a derivation μ′ with del0 B μ′ = n.

Wrapping it up

Lemma

Assume that multicut-admissibility holds for cut-formula B, and that muxbn B n holds. Then muxbn B (n + 1) holds.

Proof. See the Figure: given μ, where del0 B μ = n + 1, we can replace it by by μ′, where del0 B μ′ = n. Since muxbn B n holds, the multicut in the Figure is admissible, as required.

Now, since muxbn B 0 holds, repeated use of this Lemma gives that muxbn B n for all n.

The cut-admissibility theorem

Theorem

Multicut is admissible in GLS.

Proof. Most of the proof is as usual for cut-elimination proofs, using induction on the size (or structure) of the cut-formula. The difficult case is with a multicut as in the Figure, which is handled by the previous lemma.

Conclusion : value of the formalisation

proofs usually tedious, with many details varying only slightly many cases or details usually omitted in paper proofs this may lead to erroneous proofs formal proof avoids this risk

Our formalisation includes: formalisation includes general treatment of derivation trees general theorem expressing the appropriate inductive principle general lemmas for many cases in this and other proofs