Issues in Machine-checking the Decidability of Implicational Ticket Entailment

\underline{Jeremy Dawson}^{1}, Rajeev Goré^{1}

Logic and Computation Group Research School of Computer Science The Australian National University

 jeremy.dawson@anu.edu.au

September 21, 2017

Overview

The logics, and their calculi Modelling derivations in Isabelle (sample!) Admissibility results confirmed Relations between the calculi The decidability argument

TODO include info re modelling in Isabelle, derl, derrec, sctxt, lctxt etc

Axiomatisations of various logics

Name Axioms  Logic
T_{→} T\underrightarrow{t} R_{→} R\underrightarrow{t}
(A1) A → A  ✓  ✓  ✓  ✓
(A2) (A → B) → (C → A) → (C → B) ✓  ✓  ✓  ✓
(A3) (A → B → C) → (B → A → C)  ✓  ✓
(A4) (A → A → B) → (A → B)  ✓  ✓  ✓  ✓
(A5) (A → B) → (B → C) → (A → C) ✓  ✓
Name Rules of Inference
(R1) from A → B and A, deduce B  ✓  ✓  ✓  ✓
(R2) ⊢ A // ⊢ t → A  ✓  ✓

(Multiset) Sequent Rules and Calculi

\begin{aligned}(id) \\ & A ⊢ A \end{aligned} Γ_{1} ⊢ A  B, Γ_{2} ⊢ C (→⊢) Γ_{1}, A → B, Γ_{2} ⊢ C \begin{aligned}& Γ, A ⊢ B \\ (⊢→) \\ & Γ ⊢ A → B \end{aligned}

Γ, A, A ⊢ C ; (W⊢) ; Γ, A ⊢ C  \begin{aligned}& Γ ⊢ C \\ (t ⊢) \\ & t, Γ ⊢ C \end{aligned}  \begin{aligned}(⊢ t) \\ & ⊢ t \end{aligned}
Γ_{1} ⊢ A  B, Γ_{2} ⊢ C [→⊢]  †

[Γ_{1}, A → B, Γ_{2}] ⊢ C

In the [→⊢] rule, [Γ_{1}, A → B, Γ_{2}] ⊢ C means Γ_{1}, A → B, Γ_{2} ⊢ C, then some contraction

(id) (→⊢) (⊢→) (W⊢) (t ⊢) (⊢ t) [→⊢]
LR_{→}  ✓  ✓  ✓  ✓
LR\underrightarrow{t}  ✓  ✓  ✓  ✓  ✓  ✓
[LR_{→}] ✓  ✓  ✓  ✓
[LR\underrightarrow{t}] ✓  ✓  ✓  ✓  ✓  ✓

(Structure) Consecution Rules and Calculi

LT\underrightarrow{t}

\begin{aligned}(id;) \\ & A ⊢ A \end{aligned}

U{X ; Y ; Y } ⊢ C
(W⊢;)
U{X ; Y } ⊢ C
V ⊢ A  U{B} ⊢ C

(→⊢;)

U{A → B ; V } ⊢ C

\begin{aligned}& U ; A ⊢ B \\ (⊢→;) \\ & U ⊢ A → B \end{aligned}

U{X ; (Y ; Z)} ⊢ C (B⊢;)

U{X ; Y ; Z} ⊢ C

U{X ; (Z ; Y )} ⊢ C
(B′ ⊢;)
U{Z ; X ; Y } ⊢ C

U{Y } ⊢ C ; (KI_{t} ⊢;) ; U{t ; Y } ⊢ C

U{t ; t} ⊢ C ; (M_{t} ⊢;) ; U{t} ⊢ C

LT\underrightarrow{◯ t} := LT\underrightarrow{t} + (K_{t} ⊢;) + (T_{t} ⊢;)

U{Y } ⊢ C ; (K_{t} ⊢;) ; U{Y ; t} ⊢ C

U{Y ; t} ⊢ C ; (T_{t} ⊢;) ; U{t ; Y } ⊢ C

Derivability in Isabelle

▶ Concrete structure representing derivation tree

 datatype 'a dertree = Der 'a ('a dertree list)
         | Unf 'a (* unfinished, unproved leaf *)

▶ Alternatively, represent the fact of derivability

 'a psc = "'a list * 'a" (* single inference *)
derl ::  "'a psc set => 'a psc set"
derrec ::  "'a psc set => 'a set => 'a set"

▶ Neat example theorems

"derrec ?rls (derrec ?rls ?ps) = derrec ?rls ?ps"
"derl (derl ?rls) = derl ?rls"
"derrec (derl ?rls) ?prems = derrec ?rls ?prems"

▶ Link these concepts

Theorem

c is derivable (derrec) iff there is a valid derivation tree with conclusion c

Substitution in a hole in a structure

▶ We build the structure around the required substitution

 inductive "sctxt r"
intrs
scL "(a, b) :  sctxt r ==> (C;a, C;b) :  sctxt r"
scR "(a, b) :  sctxt r ==> (a;C, b;C) : sctxt r"
scid "(a, b) :  r ==> (a, b) :  sctxt r"

▶ We turn this into a one-premise rule which does this substitution in the antecedent

 inductive "lctxt r"
  intrs
   I "(As, Bs) :  sctxt r ==>
         ([As |- E], Bs |- E) : lctxt r"

The complexity this adds to cut-admissibility proofs

▶ Cut-admiissibility proofs require re-ordering rule applications ▶ Define: (u, v) ∈ strrep S, u and v same except may differ at

(several) subterms u′ and v′, where (u′, v′) ∈ S

inductive "strrep S"
intrs
same "(s, s) :  strrep S"
repl "p :  S ==> p :  strrep S"
sc "(u, v) :  strrep S ==> (x, y) :  strrep S
   ==> (u; x, v; y) :  strrep S"

▶ “Closing the loop” lemma: if

\frac{C[p]}{C[c_{A}]} ⟶^{A→X} C_{X}

then we have C_{X} = C′[c_{X}] where

\frac{C[p] ⟶^{A→X} C′[p]}{C[c_{A}] ⟶^{A→X} C′[c_{X}]} and c_{A} ⟶^{A→X} c_{X}

Inductive Multi-cut Admissibility via gen step2

Suppose the conclusions cl and cr have respective derivations as shown below:

pl_{1} … pl_{n} ; ρ_{l} ; cl pr_{1} … pr_{m} ; ρ_{r} ; cr
........................... (cut ?)

?

▶ We want to prove an arbitrary property P of these derivations,

eg (multi)cut-admissibility for a cut-formula A. ▶ Proof is first, by induction on A, then on “stage in the proof” ▶ gen step2 expresses a single case of the inductive argument

gen step2 definition

gen step2 P A sub (dls, drs) ((psl, cl), psr, cr)

means: (assuming dls and drs are the set of derivable sequents) if

▶ P A' (dl, dr) holds for all subformulae (sub) A' of A and

derivable sequents dl and dr ; ▶ for each pl ∈ psl, P A (pl, cr) holds; ▶ for each pr ∈ psr, P A (cl, pr) holds; ▶ (and cl and cr and each pl and pr is derivable);

then P A (cl, cr) holds

So for example P A (cl, cr) could mean that the result of cutting cl with cr (cut-formula A) is derivable.

gen step2 lemma

▶ Lemma: (assuming sub is well-founded):

▶ If, for all rules (psl, cl) and (psr, cr),

gen step2 … (ie, args as above) holds, ▶ then for all derivable sequents seql and seqr,

    P A (seqa, seqb) holds

▶ This reflects that an inductive cut-admissibility proof works by

a case analysis: cases are the last rules on the left and right. ▶ Where these cases are similar for (eg) LR_{→} and LR\underrightarrow{t} we avoid

duplicating effort by proving intermediate lemmas like

 impL <= ?rls ==>
gen step2 (mcd ?rls) ?A ?a (derrec ?rls {}, ?drsr)
(([?G |- ?Aa, mins ?B ?H |- ?C],
     mins (?Aa -> ?B) ?G + ?H |- ?C), (?psr, ?cr))

Results for LR_{→}, LR\underrightarrow{t}, [LR_{→}], and [LR\underrightarrow{t}] in Isabelle

Theorem

LR_{→} and LR\underrightarrow{t} enjoy multi-cut admissibility.

Theorem

[LR_{→}] and [LR\underrightarrow{t}] enjoy contraction admissibility.

Corollary

[LR_{→}] and [LR\underrightarrow{t}] enjoy multi-cut admissibility.

Cut-admissibility of [LR\underrightarrow{t}]

Theorem 2.2 The single cut rule is admissible in LR\underrightarrow{t} Theorem 2.4 The single cut rule is admissible in [LR\underrightarrow{t}] Lemma 2.5 … LR\underrightarrow{t} and [LR\underrightarrow{t}] have the same set of theorems

▶ we couldn’t prove Theorem 2.4 in the usual way ▶ we first proved contraction-admissibility of [LR\underrightarrow{t}]

(giving the part of Lemma 2.5 shown) ▶ Theorem 2.4 follows

Multi-cut admissibility for LT\underrightarrow{t} and LT\underrightarrow{◯ t}

▶ For (multiset) sequents, “multi-cut” meant this:

\frac{X ⊢ A A^{n}, Y ⊢ B}{X , Y ⊢ B}

(just one ‘X ’ in the consequent)

▶ For (structure) consecutions, we have to define what we mean by multi-cut admissibility.

X ⊢ A  Y {A}{A} ⋯ {A} ⊢ B

(multicut)

Y {X }{X } ⋯ {X } ⊢ B

(multiple occurrences of ‘X ’ in the consequent)

Theorem

LT\underrightarrow{t} and LT\underrightarrow{◯ t} enjoy multi-cut admissibility.

Soundness and Completeness

Theorem

LT\underrightarrow{t} is complete for T\underrightarrow{t} LT\underrightarrow{◯ t} is complete for R\underrightarrow{t} For the sequent systems, we have proved

Lemma

for each rule of LR_{→} there is a “corresponding” proof in R_{→} (for some ordering of antecedents) We still need to prove that any re-ordering of antecedents in A_{1} → A_{2} → … → A_{n} → B is provable in R_{→}

Linking the sequent and consecution systems

Theorem

Given a derivation in LT\underrightarrow{◯ t}, we can, by turning structures into multi-sets, obtain an “equivalent” derivation in LR\underrightarrow{t}. (“equivalent” means “same” premises and conclusion, not necessarily same proof steps)

▶ This is the transformation π, which we have not actually

defined, we have just shown it exists. ▶ For the converse (using the τ transformation), we need to

prove that the rules of LT\underrightarrow{◯ t} permit any permutation and grouping, into a structure, of any multiset of formulae.

▶ Lemmas 8,9 and 10 do this for up to 3 formulae.

Background to decidability argument

▶ multiset sequent system LR_{→} for T_{→}, includes contraction ▶ [LR_{→}] incorporates limited contraction into →⊢ rule, (called

[→⊢]) therefore decidable (Kripke and König lemmas) ▶ likewise LR\underrightarrow{t} and [LR\underrightarrow{t}] for T\underrightarrow{t} ▶ structure sequent systems LT\underrightarrow{◯ t} for R\underrightarrow{t}, and LT\underrightarrow{t} for T\underrightarrow{t} ▶ proof transformations:

▶ π, LT\underrightarrow{◯ t} to LR\underrightarrow{t} (loses ordering/grouping) ▶ τ, LR\underrightarrow{t} to LT\underrightarrow{◯ t} (recreates ordering/grouping) ▶ difference between T\underrightarrow{t} and R\underrightarrow{t} (ie, between LR\underrightarrow{t} and LT\underrightarrow{◯ t})

is (complete) availability of re-ordering ▶ τ produces several proofs in LT\underrightarrow{◯ t} (choice of

ordering/grouping)

the decidability procedure

▶ get all proofs in [LR\underrightarrow{t}] ▶ convert these into proofs in LR\underrightarrow{t} ▶ transform them, using τ, to proofs in LT\underrightarrow{◯ t} ▶ examine which of these are proofs in LT\underrightarrow{t}

Issues arising:

▶ τ involves “all permutations and groupings”:

should this be “all proofs of all permutations and groupings”? (to find proof in LT\underrightarrow{t}, if any)

▶ even so, τ produces only proofs whose ⊢→, →⊢ and W⊢ are

in the same order as the given proof in LR\underrightarrow{t} — is this enough? ▶ that is, the algorithm produces only LT\underrightarrow{◯ t}-proofs in which

contains these rules in a the same order as a proof in [LR\underrightarrow{t}] — what if the only LT\underrightarrow{t}-proof contains them in a different order?

▶ (note that deriving an [LR\underrightarrow{t}]-proof from an LR\underrightarrow{t}-proof changes the order of these rules)

Lemmas supporting τ transformation

8 If C[A; B] ⊢ A provable in LT\underrightarrow{◯ t} then so is C[t; (B; A)] ⊢ A

(C is any structure with a “hole”) 9 If C[A_{1}; A_{2}; A_{3}] ⊢ A provable in LT\underrightarrow{◯ t} then so are

C[t; A_{i}; A_{j}; A_{k}] ⊢ A and C[t; A_{i}; (A_{j}; A_{k})] ⊢ A (for all permutations i, j, k of 1, 2, 3)

10 If C[A_{1}; A_{2}; A_{3}] ⊢ A provable in LT\underrightarrow{◯ t} then so are

C[t; (A_{i}; A_{j}; A_{k})] ⊢ A and C[t; (A_{i}; (A_{j}; A_{k}))] ⊢ A ▶ The proof we found for 9 actually uses 10, which we proved

first: we didn’t find the proof used by B&D ▶ We also formulated an argument to deal with four or more

substructures

Do we actually need these lemmas?

▶ Lemmas 8,9 and 10: to prove any permutation of antecedents

is available in certain sequents are provable in LT\underrightarrow{◯ t}. ▶ this is needed to translate LR\underrightarrow{t}-proofs to LT\underrightarrow{◯ t} ▶ We haven’t yet found this to be necessary. ▶ The constructions may be relevant to an argument that we

will find a proof in LT\underrightarrow{t}, if one exists; ▶ BUT: if there is no proof in LT\underrightarrow{t}, does it matter if these is no

proof in LT\underrightarrow{◯ t} either? ▶ We noticed this only when putting together the skeleton of a

proof in Isabelle.

Proof trees and König’s Lemma

▶ König’s Lemma:

an infinite, finitely branching, tree has an infinite branch ▶ When we build a proof tree, bottom (endsequent) up, the

intermediate stages have leaves yet unproved. ▶ We call these partial proof trees. We represent an “infinite

proof tree” by an increasing sequence of partial proof trees: ▶ By König’s Lemma, if such a sequence is infinite, then there

must be a single infinitely increasing branch ▶ Note: finite branching property, because each rule has finitely

many premises ▶ And by Kripke’s lemma there is no infinite irredundant branch

of a (partial) proof tree in [LR\underrightarrow{t}] ▶ Where does this get us?

Proof search trees and König’s Lemma

Now consider a proof search tree:

▶ node: partial proof tree,

edge: extending a partial proof tree by adding one rule.

▶ This is a different tree!! This one is finitely branching because

▶ a partial proof tree has only finitely many unproved leaves, and ▶ at each leaf, only finitely many rules can be applied.

▶ The previous result (“no infinite proof tree”) says proof search

tree has no infinite branch. ▶ König’s Lemma, again, tells us that the proof search tree is

finite, that is, complete proof search is a finite process ▶ so this logic is decidable. ▶ This outline uses König’s Lemma twice! Is this necessary? ▶ Literature seems to use König’s Lemma just once!

and to confuse proof trees with proof search trees

Proving decidability

▶ To really formalise decidability, we would need to formalise

steps of computation (very low level) ▶ A finite proof search tree is not enough:

▶ imagine a logic L, and we define a new logic L’, by

▶ Axioms of L’: theorems of L ▶ Rules of L’: none

▶ In L’, proof search tree (for given endsequent) is tiny,

but L’ (may be) not decidable.

▶ We need further informal arguments, eg, that at any point it is straightforward to determine which rules are applicable.

Formalisation

use of Isabelle: work verified in Isabelle theorem prover value of formal verification: detects gaps which may be overlooked

in a proof

value of formalisation without verification: even planning/preparing for formal verification alerts us to problems in a proof

difficult issues: König’s lemma: what is an infinite proof tree? how to formalise branch of it