o : type. % propositions %name o A. pol : type. % polarities %name pol P. + : pol. - : pol. p : pol -> type. % polarized formulae %name p F. foc : p P -> o. % "focus" = root of focal monopole blr : o -> p P. % "blur" = leaf of focal monopole base : type. % base types k1 : base. k2 : base. atom : base -> o. @ : p + -> p + -> p +. % tensor %infix right 6 @. v : p + -> p + -> p +. % oplus %infix right 4 v. -o : p + -> p - -> p -. % lolli %infix right 3 -o. & : p - -> p - -> p -. % amp %infix right 5 &. ps : type. % ordered contexts ( = lists of polarized propositions ) %name ps PS. ps/nil : ps. ps/cons : p P -> ps -> ps. %abbrev ps/sing = [x] ps/cons x ps/nil. % conc : o -> type. % (defined below in terms of act') hyp : o -> type. % ordinary hypothesis act : ps -> p P -> type. % active conclusion act' : ps -> o -> type. % possibly active hypotheses %abbrev conc = [x] act' ps/nil x. % conclusion %abbrev sing = [x] [y] act' (ps/sing x) y. % singleton ordered context %%% Proof rules %%% % Structural rules init : hyp (atom B) -> conc (atom B). actr : conc (foc F) <- act ps/nil F. actl : (hyp (foc F) -> conc C) <- sing F C. deactr : act PS (blr C) <- act' PS C. deactl : act' (ps/cons (blr A) PS) C <- (hyp A -> act' PS C). % Connective rules @L : act' (ps/cons (F @ G) PS) C <- act' (ps/cons F (ps/cons G PS)) C. @R : act ps/nil (F @ G) <- act ps/nil F <- act ps/nil G. -oL : sing (F -o G) C <- act ps/nil F <- sing G C. -oR : act PS (F -o G) <- act (ps/cons F PS) G. &L1 : sing (F & G) C <- sing F C. &L2 : sing (F & G) C <- sing G C. &R : act PS (F & G) <- act PS F <- act PS G. vR1 : act ps/nil (F v G) <- act ps/nil F. vR2 : act ps/nil (F v G) <- act ps/nil G. vL : act' (ps/cons (F v G) PS) C <- act' (ps/cons F PS) C <- act' (ps/cons G PS) C. %%% Cut admissibility theorems ca : {A} conc A -> (hyp A -> conc C) -> conc C -> type. pc+ : {F} act ps/nil (F : p +) -> act' (ps/cons F PS) C -> act' PS C -> type. pc- : {F} act PS (F : p -) -> sing F C -> act' PS C -> type. lcl : {A} conc A -> (hyp A -> act' PS C) -> act' PS C -> type. lcr : {A} act' PS A -> (hyp A -> conc C) -> act' PS C -> type. rc : {A} conc A -> (hyp A -> act PS F) -> act PS F -> type. %%% Proof of ca % init cases are easy / : ca _ (init H) D (D H). % / : ca _ D ([h] init h) D. % redundant and so unnecessary! I was somewhat surprised. / : ca _ D ([h] init H) (init H). % on the second derivation: left activation not for the cut formula? / : ca _ D ([h] actl (E h) H) (actl F H) <- lcl _ D E F. % on the second derivation: right activation? / : ca _ D ([h] actr (E h)) (actr F) <- rc _ D E F. % from here on, second derivation is activation for the cut formula. % Analyze the first derivation: left activation? / : ca _ (actl D H) E (actl F H) <- lcr _ D E F. % o/w, it's right activation, so principal cut! / : ca _ (actr D) ([h] actl (E h) h) F <- lcl _ (actr D) E E' <- pc+ _ D E' F. / : ca _ (actr D) ([h] actl (E h) h) F <- lcl _ (actr D) E E' <- pc- _ D E' F. %%% Proof of pc+ / : pc+ _ (@R D2 D1) (@L E) F <- pc+ _ D1 E E' <- pc+ _ D2 E' F. / : pc+ _ (vR1 D) (vL E2 E1) F <- pc+ _ D E1 F. / : pc+ _ (vR2 D) (vL E2 E1) F <- pc+ _ D E2 F. / : pc+ _ (deactr D) (deactl E) F <- lcl _ D E F. %%% Proof of pc- % XXX There is an error in the paper! It does this case in the wrong order, % pc+, then pc-, which doesn't work. / : pc- _ (-oR D) (-oL E2 E1) F <- pc- _ D E2 F' <- pc+ _ E1 F' F. / : pc- _ (&R D2 D1) (&L1 E) F <- pc- _ D1 E F. / : pc- _ (&R D2 D1) (&L2 E) F <- pc- _ D2 E F. / : pc- _ (deactr D) (deactl E) F <- lcr _ D E F. %%% Proof of lcl % When the ordered context runs out, appeal to toplevel ca / : lcl _ D E F <- ca _ D E F. / : lcl _ D ([x] deactl ([y] E x y)) (deactl E') <- ({y} lcl _ D ([x] E x y) (E' y)). / : lcl _ D ([x] @L (E x)) (@L E') <- (lcl _ D E E'). % XXX: Another mistake in the paper!! It does 2 LCLs instead of LCL+RC / : lcl _ D ([x] -oL (E2 x) (E1 x)) (-oL E2' E1') <- (lcl _ D E2 E2') <- (rc _ D E1 E1'). / : lcl _ D ([x] &L1 (E x)) (&L1 E') <- lcl _ D E E'. / : lcl _ D ([x] &L2 (E x)) (&L2 E') <- lcl _ D E E'. / : lcl _ D ([x] vL (E2 x) (E1 x)) (vL E2' E1') <- lcl _ D E1 E1' <- lcl _ D E2 E2'. %%% Proof of lcr % When the ordered context runs out, appeal to toplevel ca / : lcr _ D E F <- ca _ D E F. / : lcr _ (deactl [x] (D x)) E (deactl [x] D' x) <- ({x} lcr _ (D x) E (D' x)). / : lcr _ (@L D) E (@L D') <- (lcr _ D E D'). / : lcr _ (&L1 D) E (&L1 D') <- (lcr _ D E D'). / : lcr _ (&L2 D) E (&L2 D') <- (lcr _ D E D'). / : lcr _ (vL D2 D1) E (vL D2' D1') <- (lcr _ D1 E D1') <- (lcr _ D2 E D2'). % For once, the paper is right about a -o case! / : lcr _ (-oL D2 D1) E (-oL D2' D1) <- (lcr _ D2 E D2'). %%% Proof of rc / : rc _ D ([x] deactr (E x)) (deactr E') <- lcl _ D E E'. / : rc _ D ([x] @R (E2 x) (E1 x)) (@R E2' E1') <- rc _ D E1 E1' <- rc _ D E2 E2'. / : rc _ D ([x] &R (E2 x) (E1 x)) (&R E2' E1') <- rc _ D E1 E1' <- rc _ D E2 E2'. / : rc _ D ([x] vR1 (E x)) (vR1 E') <- rc _ D E E'. / : rc _ D ([x] vR2 (E x)) (vR2 E') <- rc _ D E E'. / : rc _ D ([x] -oR (E x)) (-oR E') <- rc _ D E E'. %mode (ca +A +D +E -F) (lcl +A +D +E -F) (lcr +A +D +E -F) (rc +A +D +E -F) (pc+ +A +D +E -F) (pc- +A +D +E -F) . %block b : some {A : o} block {x : hyp A}. %worlds (b) (ca _ _ _ _) (lcl _ _ _ _) (lcr _ _ _ _) (rc _ _ _ _) (pc+ _ _ _ _) (pc- _ _ _ _). %total {(CAA LCLA LCRA RCA PCPA PCMA) [(CAD LCLD LCRD RCD PCPD PCMD) (CAE LCLE LCRE RCE PCPE PCME)]} (ca CAA CAD CAE CAF) (lcl LCLA LCLD LCLE LCLF) (lcr LCRA LCRD LCRE LCRF) (rc RCA RCD RCE RCF) (pc+ PCPA PCPD PCPE PCPF) (pc- PCMA PCMD PCME PCMF) .