Tethered modal logic

Alex Simpson’s thesis shows how to encode a variety of constructive modal logics by making box and diamond into universal and existential quantifiers over accessible Kripke worlds and orthogonally allowing axiomatization of the accessibility relation.

Here we encode and prove cut admissibility for a sequent calculus for a similar spectrum of logics. The difference is that uses of left rules are constrained (`tethered’) to only fire when the label on the conclusion is the same as the label on the hypothesis.

The conjecture was that Pfenning-Davies judgmental modal logic is exactly tethered modal logic where accessibility relation is axiomatized by reflexivity and transitivity. However, this is refuted by considering $\Diamond\Diamond A \Rightarrow \Diamond A$, which is provable in Pfenning-Davies and (apparently?) not in the current system. The exact status of this logic relative to other constructive modal logics is still being determined.

The standard litmus-test entailment that fails in this logic (and succeeds in Simpsons’) is

$\Diamond A \Rightarrow \square B \vdash \square (A \Rightarrow B)$

(Author: Jason Reed, based on Pfenning’s encoding of intuitionistic logic with cut admissibility)

%sort w %.
% worlds
%name w %.
%sort <= {_ w} {_ w} %.
% accessibility relation
%prec %none 3 <= %.
%term refl P <= P %.
%term trans %pi (P <= Q) %-> (Q <= R) %-> (P <= R) %.
%term sym %pi (P <= Q) %-> (Q <= P) %.
%sort o %.
% formulas
%name o %.
%term and %pi o %-> o %-> o %.
%prec %right 11 and %.
%term imp %pi o %-> o %-> o %.
%prec %right 10 imp %.
%term or %pi o %-> o %-> o %.
%prec %right 11 or %.
%term true o %.
%term false o %.
%term box %pi o %-> o %.
%term dia %pi o %-> o %.
% Sequent Calculus
%sort hyp {_ o} {_ w} %.
% Hypotheses (left)
%sort ghyp {_ o} {_ w} %.
% Global-after-P Hypotheses (left)
%sort conc {_ o} {_ w} %.
% Conclusion (right)
%name hyp %.
%name conc %.
%term axiom %pi (hyp A P) %-> (conc A P) %.
%term andr %pi (conc A P) %-> (conc B P) %-> (conc (A and B) P) %.
%term andl1 %pi (%pi (hyp A P) %-> (conc C P)) %-> (hyp (A and B) P) %-> (conc C P) %.
%term andl2 %pi (%pi (hyp B P) %-> (conc C P)) %-> (hyp (A and B) P) %-> (conc C P) %.
%term impr %pi (%pi (hyp A P) %-> (conc B P)) %-> (conc (A imp B) P) %.
%term impl
  %pi (conc A P)
  %-> (%pi (hyp B P) %-> (conc C P))
  %-> (hyp (A imp B) P)
  %-> (conc C P) %.
%term orr1 %pi (conc A P) %-> (conc (A or B) P) %.
%term orr2 %pi (conc B P) %-> (conc (A or B) P) %.
%term orl
  %pi (%pi (hyp A P) %-> (conc C P))
  %-> (%pi (hyp B P) %-> (conc C P))
  %-> (hyp (A or B) P)
  %-> (conc C P) %.
%term truer conc true P %.
%term falsel %pi (hyp false P) %-> (conc C P) %.
%term boxr %pi ({a w} %pi (P <= a) %-> (conc A a)) %-> (conc (box A) P) %.
%term boxl %pi (%pi (ghyp A P) %-> (conc C P)) %-> (hyp (box A) P) %-> (conc C P) %.
% Can copy to any world after P regardless of conc
%term copy %pi (%pi (hyp A Q) %-> (conc C R)) %-> (P <= Q) %-> (ghyp A P) %-> (conc C R) %.
%term diar %pi (conc A Q) %-> (P <= Q) %-> (conc (dia A) P) %.
%term dial
  %pi ({a w} %pi (P <= a) %-> (hyp A a) %-> (conc C P))
  %-> (hyp (dia A) P)
  %-> (conc C P) %.
%%% Termination Metric
%sort little %.
%sort big %.
%term little/ little %.
%term big/ %pi little %-> big %.
%%% Cut admissibility
%sort ca {M little} {A o} {_ conc A P} {_ %pi (hyp A P) %-> (conc C Q)} {_ conc C Q} %.
%sort cag {M big} {A o} {_ {a w} %pi (Q <= a) %-> (conc A a)} {_ %pi (ghyp A Q) %-> (conc C R)} {_ conc C R} %.
%% Axioms
%term ca_axiom_d ca M A (axiom H) E (E H) %.
%term ca_axiom_e ca M A D axiom D %.
%% Principal Cases
%term ca_and1
  %pi (ca M (A1 and A2) (andr D1 D2) ([h] andl1 (E1 h) h) F)
  %<- ({h1} ca M (A1 and A2) (andr D1 D2) ([h] E1 h h1) (E1' h1))
  %<- (ca M A1 D1 E1' F) %.
%term ca_and2
  %pi (ca M (A1 and A2) (andr D1 D2) ([h] andl2 (E2 h) h) F)
  %<- ({h2} ca M (A1 and A2) (andr D1 D2) ([h] E2 h h2) (E2' h2))
  %<- (ca M A2 D2 E2' F) %.
%term ca_imp
  %pi (ca M (A1 imp A2) (impr D2) ([h] impl (E1 h) (E2 h) h) F)
  %<- (ca M (A1 imp A2) (impr D2) E1 E1')
  %<- ({h2} ca M (A1 imp A2) (impr D2) ([h] E2 h h2) (E2' h2))
  %<- (ca M A1 E1' D2 D2')
  %<- (ca M A2 D2' E2' F) %.
%term ca_or1
  %pi (ca M (A1 or A2) (orr1 D1) ([h] orl (E1 h) (E2 h) h) F)
  %<- ({h1} ca M (A1 or A2) (orr1 D1) ([h] E1 h h1) (E1' h1))
  %<- (ca M A1 D1 E1' F) %.
%term ca_or2
  %pi (ca M (A1 or A2) (orr2 D2) ([h] orl (E1 h) (E2 h) h) F)
  %<- ({h2} ca M (A1 or A2) (orr2 D2) ([h] E2 h h2) (E2' h2))
  %<- (ca M A2 D2 E2' F) %.
%term ca_box
  %pi (ca M (box A) (boxr D1) ([h] boxl (E1 h) h) F)
  %<- ({h2} ca M (box A) (boxr D1) ([h] E1 h h2) (F' h2))
  %<- (cag (big/ little/) A D1 F' F) %.
%term ca_dia
  %pi (ca M (dia A) (diar D1 ACC) ([h] dial (E1 h) h) F)
  %<- ({a w} {acc} {h2 hyp A a} ca M (dia A) (diar D1 ACC) ([h] E1 h a acc h2) (F' a acc h2))
  %<- (ca M A D1 ([h2] F' _ ACC h2) F) %.
%% D-Commutative Conversions
%term cad_andl1 %pi (ca M A (andl1 D1 H) E (andl1 D1' H)) %<- ({h1} ca M A (D1 h1) E (D1' h1)) %.
%term cad_andl2 %pi (ca M A (andl2 D2 H) E (andl2 D2' H)) %<- ({h2} ca M A (D2 h2) E (D2' h2)) %.
%term cad_impl
  %pi (ca M A (impl D1 D2 H) E (impl D1 D2' H))
  %<- ({h2} ca M A (D2 h2) E (D2' h2)) %.
%term cad_orl
  %pi (ca M A (orl D1 D2 H) E (orl D1' D2' H))
  %<- ({h1} ca M A (D1 h1) E (D1' h1))
  %<- ({h2} ca M A (D2 h2) E (D2' h2)) %.
%term cad_falsel ca M A (falsel H) E (falsel H) %.
%term cad_boxl %pi (ca M A (boxl D1 H) E (boxl D1' H)) %<- ({h} ca M A (D1 h) E (D1' h)) %.
%term cad_dial
  %pi (ca M A (dial D1 H) E (dial D1' H))
  %<- ({a w} {acc} {h hyp B1 a} ca M A (D1 a acc h) E (D1' a acc h)) %.
%term cad_copy %pi (ca M A (copy D ACC H) E (copy D' ACC H)) %<- ({h} ca M A (D h) E (D' h)) %.
%% E-Commutative Conversions
%term cae_axiom ca M A D ([h] axiom H1) (axiom H1) %.
%term cae_andr
  %pi (ca M A D ([h] andr (E1 h) (E2 h)) (andr E1' E2'))
  %<- (ca M A D E1 E1')
  %<- (ca M A D E2 E2') %.
%term cae_andl1
  %pi (ca M A D ([h] andl1 (E1 h) H) (andl1 E1' H))
  %<- ({h1} ca M A D ([h] E1 h h1) (E1' h1)) %.
%term cae_andl2
  %pi (ca M A D ([h] andl2 (E2 h) H) (andl2 E2' H))
  %<- ({h2} ca M A D ([h] E2 h h2) (E2' h2)) %.
%term cae_impr
  %pi (ca M A D ([h] impr (E2 h)) (impr E2'))
  %<- ({h1} ca M A D ([h] E2 h h1) (E2' h1)) %.
%term cae_impl
  %pi (ca M A D ([h] impl (E1 h) (E2 h) H) (impl E1' E2' H))
  %<- (ca M A D E1 E1')
  %<- ({h2} ca M A D ([h] E2 h h2) (E2' h2)) %.
%term cae_orr1 %pi (ca M A D ([h] orr1 (E1 h)) (orr1 E1')) %<- (ca M A D E1 E1') %.
%term cae_orr2 %pi (ca M A D ([h] orr2 (E2 h)) (orr2 E2')) %<- (ca M A D E2 E2') %.
%term cae_orl
  %pi (ca M A D ([h] orl (E1 h) (E2 h) H) (orl E1' E2' H))
  %<- ({h1} ca M A D ([h] E1 h h1) (E1' h1))
  %<- ({h2} ca M A D ([h] E2 h h2) (E2' h2)) %.
%term cae_truer ca M A D ([h] truer) truer %.
%term cae_falsel ca M A D ([h] falsel H) (falsel H) %.
%term cae_boxr
  %pi (ca M A D ([h] boxr (E1 h)) (boxr E1'))
  %<- ({a w} {acc} ca M A D ([h] E1 h a acc) (E1' a acc)) %.
%term cae_boxl
  %pi (ca M A D ([h] boxl (E1 h) H) (boxl E1' H))
  %<- ({gh1} ca M A D ([h] E1 h gh1) (E1' gh1)) %.
%term cae_diar %pi (ca M A D ([h] diar (E1 h) ACC) (diar E1' ACC)) %<- (ca M A D E1 E1') %.
%term cae_dial
  %pi (ca M A D ([h] dial (E1 h) H) (dial E1' H))
  %<- ({a w} {acc} {h1 hyp B1 a} ca M A D ([h] E1 h a acc h1) (E1' a acc h1)) %.
%term cae_copy
  %pi (ca M A D ([h] copy (E h) ACC H) (copy E' ACC H))
  %<- ({h2} ca M A D ([h] E h h2) (E' h2)) %.
%% E-Commutative Conversions for ca (global)
%term cage_axiom cag M A D ([h] axiom H1) (axiom H1) %.
%term cage_andr
  %pi (cag M A D ([h] andr (E1 h) (E2 h)) (andr E1' E2'))
  %<- (cag M A D E1 E1')
  %<- (cag M A D E2 E2') %.
%term cage_andl1
  %pi (cag M A D ([h] andl1 (E1 h) H) (andl1 E1' H))
  %<- ({h1} cag M A D ([h] E1 h h1) (E1' h1)) %.
%term cage_andl2
  %pi (cag M A D ([h] andl2 (E2 h) H) (andl2 E2' H))
  %<- ({h2} cag M A D ([h] E2 h h2) (E2' h2)) %.
%term cage_impr
  %pi (cag M A D ([h] impr (E2 h)) (impr E2'))
  %<- ({h1} cag M A D ([h] E2 h h1) (E2' h1)) %.
%term cage_impl
  %pi (cag M A D ([h] impl (E1 h) (E2 h) H) (impl E1' E2' H))
  %<- (cag M A D E1 E1')
  %<- ({h2} cag M A D ([h] E2 h h2) (E2' h2)) %.
%term cage_orr1 %pi (cag M A D ([h] orr1 (E1 h)) (orr1 E1')) %<- (cag M A D E1 E1') %.
%term cage_orr2 %pi (cag M A D ([h] orr2 (E2 h)) (orr2 E2')) %<- (cag M A D E2 E2') %.
%term cage_orl
  %pi (cag M A D ([h] orl (E1 h) (E2 h) H) (orl E1' E2' H))
  %<- ({h1} cag M A D ([h] E1 h h1) (E1' h1))
  %<- ({h2} cag M A D ([h] E2 h h2) (E2' h2)) %.
%term cage_truer cag M A D ([h] truer) truer %.
%term cage_falsel cag M A D ([h] falsel H) (falsel H) %.
%term cage_boxr
  %pi (cag M A D ([h] boxr (E1 h)) (boxr E1'))
  %<- ({a w} {acc} cag M A D ([h] E1 h a acc) (E1' a acc)) %.
%term cage_boxl
  %pi (cag M A D ([h] boxl (E1 h) H) (boxl E1' H))
  %<- ({gh1} cag M A D ([h] E1 h gh1) (E1' gh1)) %.
%term cage_diar %pi (cag M A D ([h] diar (E1 h) ACC) (diar E1' ACC)) %<- (cag M A D E1 E1') %.
%term cage_dial
  %pi (cag M A D ([h] dial (E1 h) H) (dial E1' H))
  %<- ({a w} {acc} {h1 hyp B1 a} cag M A D ([h] E1 h a acc h1) (E1' a acc h1)) %.
%term cage_copy
  %pi (cag M A D ([h] copy (E h) ACC H) (copy E' ACC H))
  %<- ({h2} cag M A D ([h] E h h2) (E' h2)) %.
% Single principal case for ca (global)
%term cag_copy
  %pi (cag (big/ M) A D ([h] copy (E h) ACC h) F)
  %<- ({h2} cag (big/ M) A D ([h] E h h2) (E' h2))
  %<- (ca M A (D _ ACC) E' F) %.
%block bacc [Q w] [P w] {d P <= Q}%.
%block bhyp [A o] [P w] {h hyp A P}%.
%block bghyp [A o] [P w] {h ghyp A P}%.
%block bw {a w}%.
%block bo {p o}%.
%worlds (bhyp bghyp bw bo bacc) (ca M A D E F) (cag M A D E F) %.
%mode ca %in %in %in %in %out %.
%mode cag %in %in %in %in %out %.
%total {(A' A) (M' M) [(D' D) (E' E)]} (cag M' A' D' E' _) (ca M A D E _) %.