Focusing
From The Twelf Project
| This is Literate Twelf Code: here Status: %% OK %% Output: here. |
Focusing for polarized logic. This proof has been de-unicoded by a sed script, the original is here.
Contents |
Syntax
pol: type. %name pol P. +: pol. -: pol.
We define propositions in an environment with free atoms.
atom: pol -> type. %name atom Q q. %block atom+: block {Q+: atom +}. %block atom-: block {Q-: atom -}. typ: pol -> type. %name typ A. c: atom P -> typ P. dn: typ - -> typ +. bot: typ +. \/: typ + -> typ + -> typ +. %infix none 5 \/. top+: typ +. *: typ + -> typ + -> typ +. %infix none 5 *. up: typ + -> typ -. top-: typ -. /\: typ - -> typ - -> typ -. %infix none 5 /\. =>: typ + -> typ - -> typ -. %infix none 5 =>.
Judgments (only one unless we're in the middle of an identity expansion)
suc: type. %name suc Suc jmt. true: typ - -> suc. %postfix 3 true.
Hypothetical judgments (two, one for atoms and another for propositions)
hjmt: type. %name hjmt A. h+: atom + -> hjmt. h-: typ - -> hjmt.
Right-stable judgments are ones that are either atomic or shifted.
stable: suc -> type. %name stable St. sa: stable (c Q true). sup: stable (up A+ true).
An inversion or focus context Inv is a list of positive propositions.
pos: type. %name pos Inv. #: pos. ,: typ + -> pos -> pos. %infix right 3 ,.
Sequent calculus
The judgments of the focused language (or, alternatively, syntax of intrinsically typed spine form judgments)
hyp: hjmt -> type. %name hyp X x. %abbrev hyp+ = [Q+] hyp (h+ Q+). %abbrev hyp- = [A-] hyp (h- A-). %block x : some {A: hjmt} block {x: hyp A}. %block gamma = (atom+ | atom- | x). % World for derivations, cut rfoc: typ + -> type. %name rfoc V. conc: pos -> suc -> type. %name conc N. lfoc: typ - -> suc -> type. %name lfoc Sp. %block v : some {A+: typ +} block {v: rfoc A+}. %block sp : some {A-: typ -} block {jmt}{st: stable jmt}{sp: lfoc A- jmt}. %block aleph = (gamma | v | sp). % Extended world for identity expansion
V ::= z ∣ {N}- ∣ inl V ∣ inr V ∣ <> ∣ <V1,V2>
cR: hyp+ Q+ -> rfoc (c Q+). dnR: conc # (A- true) -> rfoc (dn A-). \/R1: rfoc A+ -> rfoc (A+ \/ B+). \/R2: rfoc B+ -> rfoc (A+ \/ B+). top+R: rfoc top+. *R: rfoc A+ -> rfoc B+ -> rfoc (A+ * B+).
N ::= x • Sp ∣ z.p ∣ x.N ∣ abort ∣ [N1,N2] ∣ <>.N ∣ *N ∣ {V}+ ∣ λN ∣ <> ∣ <N1,N2>
foc: hyp- A- -> stable Suc -> lfoc A- Suc -> conc # Suc. cL: (hyp+ Q+ -> conc Inv Suc) -> conc (c Q+ , Inv) Suc. dnL: (hyp- A- -> conc Inv Suc) -> conc (dn A- , Inv) Suc. botL: conc (bot , Inv) Suc. \/L: conc (A+ , Inv) Suc -> conc (B+ , Inv) Suc -> conc (A+ \/ B+ , Inv) Suc. top+L: conc Inv Suc -> conc (top+ , Inv) Suc. *L: conc (A+ , B+ , Inv) Suc -> conc (A+ * B+ , Inv) Suc. upR: rfoc A+ -> conc # (up A+ true). top-R: conc # (top- true). /\R: conc # (A- true) -> conc # (B- true) -> conc # (A- /\ B- true). =>R: conc (A+ , #) (B- true) -> conc # (A+ => B- true).
Sp ::= nil ∣ {N} ∣ π1;Sp ∣ π2;Sp ∣ V;Sp
p-: lfoc (c Q-) (c Q- true). upL: conc (A+ , #) Suc -> lfoc (up A+) Suc. /\L1: lfoc A- Suc -> lfoc (A- /\ B-) Suc. /\L2: lfoc B- Suc -> lfoc (A- /\ B-) Suc. =>L: rfoc A+ -> lfoc B- Suc -> lfoc (A+ => B-) Suc.
Cut admissibility
Cut admissibility has a lot of mutually inductive theorems, but no more than is absolutely necessary given the syntactic classes we're dealing with. Furthermore, the different theorems we use neatly sort out the informal division of cases that we are used to dealing with when proving cut admissibility theorems.
The "principal" substitutions capture the principal cuts:
- V • Ni - positive cut formula, and
- M • Sp - negative cut formula.
In this presentation, we have generalized what it means to be a "positive cut formula": instead of a single formula A+, it is a context of positive formulas Inv. Each inductive call within this group decreases the "size" of the cut formula by a multiset ordering where the positive conjunction * counts for two and the conjunction of positive contexts , counts for one. To make Twelf happy, we turn this into a structural metric.
subst+: {A+} small -> rfoc A+ -> conc (A+ , Inv) (C- true) -> conc Inv (C- true) -> type. subst-: {A-} small -> conc # (A- true) -> lfoc A- (C- true) -> stable (C- true) -> conc # (C- true) -> type. %mode subst+ +A +S +V +N -N'. %mode subst- +A +S +N +Sp +St -N'.
The "rightist" substitutions capture the right commutative cuts:
- [M/x]V - right rules for positive connectives,
- [M/x]Ni - left rules for positive connectives,
- [M/x]N - right rules for negative connectives,
- [M/x]Sp - left rules for negative connectives, and
Each inductive call within this group decreases the size of the formula that we are substituting into.
rightV: {A-} big -> conc # (A- true) -> (hyp- A- -> rfoc C+) -> rfoc C+ -> type. rightN: {A-} big -> conc # (A- true) -> (hyp- A- -> conc Inv (C- true)) -> conc Inv (C- true) -> type. rightSp: {A-} big -> conc # (A- true) -> (hyp- A- -> lfoc B- (C- true)) -> lfoc B- (C- true) -> type. %mode rightV +A +S +M +V -N'. %mode rightN +A +S +M +N -N'. %mode rightSp +A +S +M +Sp -N'.
The "leftist" substitutions capture the left commutative cuts, and are only called when we bottom out of principal substitutions:
- <<Mi>>Ni - left rules for positive connectives, and
- <<Sp>>Ni - left rules for negative connectives.
Each inductive call within this group decreases the size of the formula that we are substituting in, hence "leftist."
leftN: {A+} big -> conc Inv (up A+ true) -> conc (A+ , #) (C- true) -> stable (C- true) -> conc Inv (C- true) -> type. leftSp: {A+} big -> lfoc B- (up A+ true) -> conc (A+ , #) (C- true) -> stable (C- true) -> lfoc B- (C- true) -> type. %mode leftN +A +S +Mi +Ni +Ni' -M'. %mode leftSp +A +S +Sp +Ni +Sp' -Sp'.
Principal substitution/cuts
(V • N) = N'
/: subst+ (c Q+) S (cR Z) (cL ([z'] N z')) (N Z). /: subst+ (dn A-) s (dnR M) (dnL N) N' <- rightN A- (b s) M N (N': conc Inv (C- true)). /: subst+ (A+ \/ B+) S (\/R1 V) (\/L N1 N2) N' <- subst+ A+ S V N1 (N': conc Inv (C- true)). /: subst+ (A+ \/ B+) S (\/R2 V) (\/L N1 N2) N' <- subst+ B+ S V N2 (N': conc Inv (C- true)). /: subst+ top+ S top+R (top+L N) N. /: subst+ (A+ * B+) S (*R V1 V2) (*L N) N' <- subst+ A+ S V1 N (NB: conc (B+ , Inv) (C- true)) <- subst+ B+ S V2 NB (N': conc Inv (C- true)).
(M • Sp) = N'
/: subst- (c Q-) S (foc X sa Sp) p- _ (foc X sa Sp). /: subst- (up A+) s (foc X sup Sp) (upL N) St (foc X St Sp') <- leftSp A+ (b s) Sp N St (Sp': lfoc B- (C- true)). /: subst- (up A+) S (upR V) (upL N) _ N' <- subst+ A+ S V N (N': conc # (C- true)). /: subst- (A+ => B-) S (=>R N) (=>L V Sp) St N' <- subst+ A+ S V N (NB: conc # (B- true)) <- subst- B- S NB Sp St (N': conc # (C- true)). /: subst- (A- /\ B-) S (/\R M1 M2) (/\L1 Sp) St N' <- subst- A- S M1 Sp St (N': conc # (C- true)). /: subst- (A- /\ B-) S (/\R M1 M2) (/\L2 Sp) St N' <- subst- B- S M2 Sp St (N': conc # (C- true)).
Rightist substitution (right commutative cuts)
[[M/x]]V = V'
/: rightV A- S M ([x] cR Z) (cR Z). /: rightV A- S M ([x] dnR (N x)) (dnR N') <- rightN A- S M ([x] N x) (N': conc # (C- true)). /: rightV A- S M ([x] \/R1 (V x)) (\/R1 V') <- rightV A- S M ([x] V x) (V': rfoc C1+). /: rightV A- S M ([x] \/R2 (V x)) (\/R2 V') <- rightV A- S M ([x] V x) (V': rfoc C2+). /: rightV A- S M ([x] top+R) top+R. /: rightV A- S M ([x] *R (V1 x) (V2 x)) (*R V1' V2') <- rightV A- S M ([x] V1 x) (V1': rfoc C1+) <- rightV A- S M ([x] V2 x) (V2': rfoc C2+).
[[M/x]]N = N'
/: rightN A- (b s) M ([x] foc x St (Sp x)) N' <- rightSp A- (b s) M ([x] Sp x) (Sp': lfoc A- (C- true)) <- subst- A- s M Sp' St (N': conc # (C- true)). /: rightN A- S M ([x] foc X' St (Sp x)) (foc X' St Sp') <- rightSp A- S M ([x] Sp x) (Sp': lfoc B- (C- true)). /: rightN A- S M ([x] cL [z] N x z) (cL [z] N' z) <- ({z: hyp+ Q+} rightN A- S M ([x] N x z) (N' z: conc Inv (C- true))). /: rightN A- S M ([x] dnL [x'] N x x') (dnL [x'] N' x') <- ({x': hyp- B-} rightN A- S M ([x] N x x') (N' x': conc Inv (C- true))). /: rightN A- S M ([x] botL) botL. /: rightN A- S M ([x] \/L (N1 x) (N2 x)) (\/L N1' N2') <- rightN A- S M ([x] N1 x) (N1': conc (B1 , Inv) (C- true)) <- rightN A- S M ([x] N2 x) (N2': conc (B2 , Inv) (C- true)). /: rightN A- S M ([x] top+L (N x)) (top+L N') <- rightN A- S M ([x] N x) (N': conc Inv (C- true)). /: rightN A- S M ([x] *L (N x)) (*L N') <- rightN A- S M ([x] N x) (N': conc (A+ , B+ , Inv) (C- true)). /: rightN A- S M ([x] upR (V x)) (upR V') <- rightV A- S M ([x] V x) (V': rfoc C+). /: rightN A- S M ([x] =>R (N x)) (=>R N') <- rightN A- S M ([x] N x) (N': conc (C1+ , #) (C2- true)). /: rightN A- S M ([x] top-R) top-R. /: rightN A- S M ([x] /\R (N1 x) (N2 x)) (/\R N1' N2') <- rightN A- S M ([x] N1 x) (N1': conc # (C1- true)) <- rightN A- S M ([x] N2 x) (N2': conc # (C2- true)).
[[M/x]]Sp = Sp'
/: rightSp A- S M ([x] p-) p-. /: rightSp A- S M ([x] upL (N x)) (upL N') <- rightN A- S M ([x] N x) (N': conc (B+ , #) (C- true)). /: rightSp A- S M ([x] =>L (V x) (Sp x)) (=>L V' Sp') <- rightV A- S M ([x] V x) (V': rfoc B1+) <- rightSp A- S M ([x] Sp x) (Sp': lfoc B2- (C- true)). /: rightSp A- S M ([x] /\L1 (Sp x)) (/\L1 Sp') <- rightSp A- S M ([x] Sp x) (Sp': lfoc B1- (C- true)). /: rightSp A- S M ([x] /\L2 (Sp x)) (/\L2 Sp') <- rightSp A- S M ([x] Sp x) (Sp': lfoc B2- (C- true)).
Leftist substitution (left commutative cuts)
<<M>>N = M'
/: leftN A+ S (foc X _ Sp) N St (foc X St Sp') <- leftSp A+ S Sp N St (Sp': lfoc B- (C- true)). /: leftN A+ S (cL [z] M z) N St (cL [z] M' z) <- ({z: hyp+ Q+} leftN A+ S (M z) N St (M' z: conc Inv (C- true))). /: leftN A+ S (dnL [x'] M x') N St (dnL [x'] M' x') <- ({x': hyp- B-} leftN A+ S (M x') N St (M' x': conc Inv (C- true))). /: leftN A+ S botL N St botL. /: leftN A+ S (\/L M1 M2) N St (\/L M1' M2') <- leftN A+ S M1 N St (M1': conc (B1+ , Inv) (C- true)) <- leftN A+ S M2 N St (M2': conc (B2+ , Inv) (C- true)). /: leftN A+ S (top+L M) N St (top+L M') <- leftN A+ S M N St (M': conc Inv (C- true)). /: leftN A+ S (*L M) N St (*L M') <- leftN A+ S M N St (M': conc (B1+ , B2+ , Inv) (C- true)). /: leftN A+ (b s) (upR V) N St N' <- subst+ A+ s V N (N': conc # (C- true)).
<<Sp>>N = Sp'
/: leftSp A+ S (upL M) N St (upL M') <- leftN A+ S M N St (M': conc (B+ , #) (C- true)). /: leftSp A+ S (=>L V Sp) N St (=>L V Sp') <- leftSp A+ S Sp N St (Sp': lfoc B2- (C- true)). /: leftSp A+ S (/\L1 Sp) N St (/\L1 Sp') <- leftSp A+ S Sp N St (Sp': lfoc B1- (C- true)). /: leftSp A+ S (/\L2 Sp) N St (/\L2 Sp') <- leftSp A+ S Sp N St (Sp': lfoc B2- (C- true)).
Wrap-up
%worlds (gamma) (subst- _ _ _ _ _ _) (subst+ _ _ _ _ _) (rightN _ _ _ _ _ ) (rightV _ _ _ _ _) (rightSp _ _ _ _ _) (leftN _ _ _ _ _ _) (leftSp _ _ _ _ _ _).
With the exception of the "big/small" metric that allows the leftist and rightist substitutions to call principal substitutions at the same type, this is the usual induction metric for structrual cut elimination arguments.
%total {(A1 A2 A3 A4 A5 A6 A7) {(S1 S2 S3 S4 S5 S6 S7) [(MN MV MSp MP VP ML SpL) (N V Sp SpP NiP NiL1 NiL2)]}} (subst- A1 S1 MP SpP _ _) (subst+ A2 S2 VP NiP _) (rightN A3 S3 MN N _) (rightV A4 S4 MV V _) (rightSp A5 S5 MSp Sp _) (leftN A6 S6 ML NiL1 _ _) (leftSp A7 S7 SpL NiL2 _ _).
The following slightly simpler induction metric also works, however, emphasizing that the "derivation" metric matters not at all in the principal cases, that the rightist substitutions are structurally inductive over the second given derivation (the "right" derivation) and that the leftist substitutions are structurally inductive over the first given derivation (the "left" derivation).
%total {(A1 A2 A3 A4 A5 A6 A7) {(S1 S2 S3 S4 S5 S6 S7) (N V Sp S1 S2 ML SpL)}} (subst- A1 S1 _ _ _ _) (subst+ A2 S2 _ _ _) (rightN A3 S3 _ N _) (rightV A4 S4 _ V _) (rightSp A5 S5 _ Sp _) (leftN A6 S6 ML _ _ _) (leftSp A7 S7 SpL _ _ _).
Expansion
expand-: {A-} ({jmt} stable jmt -> lfoc A- jmt -> conc # jmt) -> conc # (A- true) -> type. expand+: {A+} (rfoc A+ -> conc Inv Suc) -> conc (A+ , Inv) Suc -> type. %mode expand- +A- +Sp -N. %mode expand+ +A+ +N -Ni.
η(v.N) = N'
/: expand+ (c Q+) ([v: rfoc (c Q+)] N v) (cL [x: hyp+ Q+] (N (cR x))). /: expand+ (dn A-) ([v: rfoc (dn A-)] N v) (dnL [x: hyp- A-] (N (dnR (N' x)))) <- ({x: hyp- A-} expand- A- ([jmt][st][sp: lfoc A- jmt] foc x st sp) (N' x: conc # (A- true))). /: expand+ bot ([v: rfoc bot] N v) botL. /: expand+ (A+ \/ B+) ([v: rfoc (A+ \/ B+)] N v) (\/L N1 N2) <- expand+ A+ ([v: rfoc A+] N (\/R1 v)) (N1: conc (A+ , Inv) Suc) <- expand+ B+ ([v: rfoc B+] N (\/R2 v)) (N2: conc (B+ , Inv) Suc). /: expand+ top+ ([v: rfoc top+] N v) (top+L (N top+R)). /: expand+ (A+ * B+) ([v: rfoc (A+ * B+)] N v) (*L N2) <- ({v1: rfoc A+} expand+ B+ ([v2: rfoc B+] N (*R v1 v2)) (N1 v1: conc (B+ , Inv) Suc)) <- expand+ A+ ([v1: rfoc A+] N1 v1) (N2: conc (A+ , B+ , Inv) Suc).
η(s.N) = N'
/: expand- (c Q-) ([jmt][st][sp: lfoc (c Q-) jmt] N jmt st sp) (N _ sa p-). /: expand- (up A+) ([jmt][st][sp: lfoc (up A+) jmt] N jmt st sp) (N _ sup (upL N')) <- expand+ A+ ([v: rfoc A+] upR v) (N': conc (A+ , #) (up A+ true)). /: expand- top- ([jmt][st][sp: lfoc top- jmt] N jmt st sp) top-R. /: expand- (A- /\ B-) ([jmt][st][sp: lfoc (A- /\ B-) jmt] N jmt st sp) (/\R N1 N2) <- expand- A- ([jmt][st][sp: lfoc A- jmt] N jmt st (/\L1 sp)) (N1: conc # (A- true)) <- expand- B- ([jmt][st][sp: lfoc B- jmt] N jmt st (/\L2 sp)) (N2: conc # (B- true)). /: expand- (A+ => B-) ([jmt][st][sp: lfoc (A+ => B-) jmt] N jmt st sp) (=>R N2) <- ({v: rfoc A+} expand- B- ([jmt][st][sp: lfoc B- jmt] N jmt st (=>L v sp)) (N1 v: conc # (B- true))) <- expand+ A+ ([v: rfoc A+] N1 v) (N2: conc (A+ , #) (B- true)). %worlds (aleph) (expand+ _ _ _) (expand- _ _ _). %total (A+ A-) (expand+ A+ _ _) (expand- A- _ _).
Identity is a corollary, though not one we'll actually use:
identity: (hyp- A- -> conc # (A- true)) -> type. %mode +{A-} -{N: hyp- A- -> conc # (A- true)} identity N. /: identity N <- ({x: hyp- A-} expand- A- ([jmt][st][sp: lfoc A- jmt] foc x st sp) (N x: conc # (A- true))). %worlds (gamma) (identity _). %total [] (identity _).
Unfocused admissibility
The key lemmas for establishing the completeness of the focused sequent calculus are the "unfocused admissibility" lemmas, which establish that the normal rules of the sequent calculus are usable in the context of the focused calculus.
These lemmas are all provable by use of the cut and identity principles, though the proofs are hardly straightfoward. The shift and unshift lemmas simplify matters somewhat, though shift is simply derivable.
shift: conc # (A- true) -> conc # (up (dn A-) true) -> type. %mode shift +D -E. /: shift N (upR (dnR N)). %worlds (gamma) (shift _ _). %total [] (shift _ _). unshift: conc # (up (dn A-) true) -> conc # (A- true) -> type. %mode unshift +D -E. /: unshift N M <- ({x: hyp- (up (dn A-))} expand- A- ([jmt][st][sp: lfoc A- jmt] foc x st (upL (dnL [x'] foc x' st sp))) (N' x: conc # (A- true))) <- rightN _ (b s) N ([x: hyp- (up (dn A-))] N' x) (M: conc # (A- true)). %worlds (gamma) (unshift _ _). %total [] (unshift _ _).
Initial rules
adm-init-: (hyp- (c Q) -> conc # (c Q true)) -> type. %mode +{Q} -{N': hyp- (c Q) -> conc # (c Q true)} adm-init- N'. /: adm-init- ([x: hyp- (c Q)] foc x sa p-). %worlds (gamma) (adm-init- _). %total [] (adm-init- _). adm-init1+: (hyp- (up (c Q)) -> conc # (up (c Q) true)) -> type. %mode +{Q} -{N': hyp- (up (c Q)) -> conc # (up (c Q) true)} adm-init1+ N'. /: adm-init1+ ([x: hyp- (up (c Q))] foc x sup (upL (cL [z] upR (cR z)))). %worlds (gamma) (adm-init1+ _). %total [] (adm-init1+ _). adm-init2+: (hyp+ Q -> conc # (up (c Q) true)) -> type. %mode +{Q} -{N': hyp+ Q -> conc # (up (c Q) true)} adm-init2+ N'. /: adm-init2+ ([z: hyp+ Q] upR (cR z)). %worlds (gamma) (adm-init2+ _). %total [] (adm-init2+ _).
Disjunction
adm-botL: (hyp- (up bot) -> conc # (C- true)) -> type. %mode +{C-} -{N': hyp- (up bot) -> conc # (C- true)} adm-botL N'. /: adm-botL N' <- {x: hyp- (up bot)} unshift (foc x sup (upL botL)) (N' x: conc # (C- true)). %worlds (gamma) (adm-botL _). %total [] (adm-botL _). adm-\/R1: conc # (up A+ true) -> conc # (up (A+ \/ B+) true) -> type. %mode +{A+} +{B+} +{N1} -{N': conc # (up (A+ \/ B+) true)} adm-\/R1 N1 N'. /: adm-\/R1 (N1: conc # (up A+ true)) N' <- expand+ A+ ([v: rfoc A+] upR (\/R1 v)) (NId1: conc (A+ , #) (up (A+ \/ B+) true)) <- subst- _ s N1 (upL NId1) sup (N': conc # (up (A+ \/ B+) true)). %worlds (gamma) (adm-\/R1 _ _). %total [] (adm-\/R1 _ _). adm-\/R2: conc # (up B+ true) -> conc # (up (A+ \/ B+) true) -> type. %mode +{A+} +{B+} +{N2} -{N': conc # (up (A+ \/ B+) true)} adm-\/R2 N2 N'. /: adm-\/R2 (N2: conc # (up B+ true)) N' <- expand+ B+ ([v: rfoc B+] upR (\/R2 v)) (NId2: conc (B+ , #) (up (A+ \/ B+) true)) <- subst- _ s N2 (upL NId2) sup (N': conc # (up (A+ \/ B+) true)). %worlds (gamma) (adm-\/R2 _ _). %total [] (adm-\/R2 _ _). adm-\/L: (hyp- (up A+) -> conc # (C- true)) -> (hyp- (up B+) -> conc # (C- true)) -> (hyp- (up (A+ \/ B+)) -> conc # (C- true)) -> type. %mode adm-\/L +N1 +N2 -N'. /: adm-\/L (N1: hyp- (up A+) -> conc # (C- true)) (N2: hyp- (up B+) -> conc # (C- true)) N' <- ({x1: hyp- (up A+)} shift (N1 x1) (NShift1 x1: conc # (up (dn C-) true))) <- ({x2: hyp- (up B+)} shift (N2 x2) (NShift2 x2: conc # (up (dn C-) true))) <- expand+ A+ ([v1: rfoc A+] upR (\/R1 (dnR (upR v1)))) (NId1: conc (A+ , #) (up (dn (up A+) \/ dn (up B+)) true)) <- expand+ B+ ([v2: rfoc B+] upR (\/R2 (dnR (upR v2)))) (NId2: conc (B+ , #) (up (dn (up A+) \/ dn (up B+)) true)) <- ({x: hyp- (up (A+ \/ B+))} leftN _ (b s) (\/L NId1 NId2) (\/L (dnL NShift1) (dnL NShift2)) sup (NShift x: conc (A+ \/ B+ , #) (up (dn C-) true))) <- ({x: hyp- (up (A+ \/ B+))} unshift (foc x sup (upL (NShift x))) (N' x: conc # (C- true))). %worlds (gamma) (adm-\/L _ _ _). %total [] (adm-\/L _ _ _).
Positive conjunction
adm-top+R: conc # (up top+ true) -> type. %mode adm-top+R -N'. /: adm-top+R (upR top+R). %worlds (gamma) (adm-top+R _). %total [] (adm-top+R _). adm-top+L: conc # (C- true) -> (hyp- (up top+) -> conc # (C- true)) -> type. %mode adm-top+L +N1 -N. /: adm-top+L N1 N' <- shift N1 (NShift: conc # (up (dn C-) true)) <- ({x: hyp- (up top+)} unshift (foc x sup (upL (top+L NShift))) (N' x: conc # (C- true))). %worlds (gamma) (adm-top+L _ _). %total [] (adm-top+L _ _). adm-*R: conc # (up A+ true) -> conc # (up B+ true) -> conc # (up (A+ * B+) true) -> type. %mode adm-*R +N1 +N2 -N. /: adm-*R (N1: conc # (up A+ true)) (N2: conc # (up B+ true)) N' <- ({v1: rfoc A+} expand+ B+ ([v2: rfoc B+] (upR (*R v1 v2))) (NIdA v1: conc (B+ , #) (up (A+ * B+) true))) <- ({x2: hyp- (up B+)} expand+ A+ ([v1: rfoc A+] foc x2 sup (upL (NIdA v1))) (NId x2: conc (A+ , #) (up (A+ * B+) true))) <- ({x2: hyp- (up B+)} subst- _ s N1 (upL (NId x2)) sup (NB x2: conc # (up (A+ * B+) true))) <- rightN _ (b s) N2 ([x2: hyp- (up B+)] NB x2) (N': conc # (up (A+ * B+) true)). %worlds (gamma) (adm-*R _ _ _). %total [] (adm-*R _ _ _). adm-*L: (hyp- (up A+) -> hyp- (up B+) -> conc # (C- true)) -> (hyp- (up (A+ * B+)) -> conc # (C- true)) -> type. %mode adm-*L +N1 -N. /: adm-*L (N1: hyp- (up A+) -> hyp- (up B+) -> conc # (C- true)) N' <- ({x1: hyp- (up A+)}{x2: hyp- (up B+)} shift (N1 x1 x2) (NShift1 x1 x2: conc # (up (dn C-) true))) <- ({v1: rfoc A+} expand+ B+ ([v2: rfoc B+] upR (*R (dnR (upR v1)) (dnR (upR v2)))) (NIdA v1: conc (B+ , #) (up (dn (up A+) * dn (up B+)) true))) <- expand+ A+ ([v1: rfoc A+] NIdA v1) (NId: conc (A+ , B+ , #) (up (dn (up A+) * dn (up B+)) true)) <- ({x: hyp- (up (A+ * B+))} leftN _ (b s) (*L NId) (*L (dnL [x1] dnL [x2] NShift1 x1 x2)) sup (NShift x: conc (A+ * B+ , #) (up (dn C-) true))) <- ({x: hyp- (up (A+ * B+))} unshift (foc x sup (upL (NShift x))) (N' x: conc # (C- true))). %worlds (gamma) (adm-*L _ _). %total [] (adm-*L _ _).
Implication
adm-=>R: (hyp- (up A+) -> conc # (B- true)) -> conc # (A+ => B- true) -> type. %mode adm-=>R +N1 -N. /: adm-=>R (N1: hyp- (up A+) -> conc # (B- true)) N' <- ({x: hyp- (dn (up A+) => B-)}{v: rfoc A+} expand- B- ([jmt][st][sp: lfoc B- jmt] foc x st (=>L (dnR (upR v)) sp)) (NId1 x v: conc # (B- true))) <- ({x: hyp- (dn (up A+) => B-)} expand+ A+ ([v: rfoc A+] NId1 x v) (NId x: conc (A+ , #) (B- true))) <- rightN _ (b s) (=>R (dnL [x1: hyp- (up A+)] N1 x1)) ([x: hyp- (dn (up A+) => B-)] =>R (NId x)) (N': conc # (A+ => B- true)). %worlds (gamma) (adm-=>R _ _). %total [] (adm-=>R _ _). adm-=>L: conc # (up A+ true) -> (hyp- B- -> conc # (C- true)) -> (hyp- (A+ => B-) -> conc # (C- true)) -> type. %mode adm-=>L +N1 +N2 -N'. /: adm-=>L (N1: conc # (up A+ true)) (N2: hyp- B- -> conc # (C- true)) N' <- ({x2: hyp- B-} shift (N2 x2) (NShift2 x2: conc # (up (dn C-) true))) <- ({x: hyp- (A+ => B-)} {v: rfoc A+} expand- B- ([jmt][st][sp: lfoc B- jmt] foc x st (=>L v sp)) (NId1 x v: conc # (B- true))) <- ({x: hyp- (A+ => B-)} expand+ A+ ([v: rfoc A+] upR (dnR (NId1 x v))) (NId2 x: conc (A+ , #) (up (dn B-) true))) <- ({x: hyp- (A+ => B-)} subst- _ s N1 (upL (NId2 x)) sup (NA x: conc # (up (dn B-) true))) <- ({x: hyp- (A+ => B-)} subst- _ s (NA x) (upL (dnL NShift2)) sup (NShift x: conc # (up (dn C-) true))) <- ({x: hyp- (A+ => B-)} unshift (NShift x) (N' x: conc # (C- true))). %worlds (gamma) (adm-=>L _ _ _). %total [] (adm-=>L _ _ _).
Negative conjunction
adm-top-R: conc # (top- true) -> type. %mode adm-top-R -N'. /: adm-top-R top-R. %worlds (gamma) (adm-top-R _). %total [] (adm-top-R _). adm-/\R: conc # (A- true) -> conc # (B- true) -> conc # (A- /\ B- true) -> type. %mode adm-/\R +N1 +N2 -N'. /: adm-/\R N1 N2 (/\R N1 N2). %worlds (gamma) (adm-/\R _ _ _). %total [] (adm-/\R _ _ _). adm-/\L1: (hyp- A- -> conc # (C- true)) -> (hyp- (A- /\ B-) -> conc # (C- true)) -> type. %mode +{A-} +{B-} +{C-} +{N1} -{N': hyp- (A- /\ B-) -> conc # (C- true)} adm-/\L1 N1 N'. /: adm-/\L1 (N1: hyp- A- -> conc # (C- true)) N' <- ({x: hyp- (A- /\ B-)} expand- A- ([jmt][st][sp: lfoc A- jmt] foc x st (/\L1 sp)) (NId x: conc # (A- true))) <- ({x: hyp- (A- /\ B-)} rightN _ (b s) (NId x) ([x1: hyp- A-] N1 x1) (N' x: conc # (C- true))). %worlds (gamma) (adm-/\L1 _ _). %total [] (adm-/\L1 _ _). adm-/\L2: (hyp- B- -> conc # (C- true)) -> (hyp- (A- /\ B-) -> conc # (C- true)) -> type. %mode +{A-} +{B-} +{C-} +{N1} -{N': hyp- (A- /\ B-) -> conc # (C- true)} adm-/\L2 N1 N'. /: adm-/\L2 (N2: hyp- B- -> conc # (C- true)) N' <- ({x: hyp- (A- /\ B-)} expand- B- ([jmt][st][sp: lfoc B- jmt] foc x st (/\L2 sp)) (NId x: conc # (B- true))) <- ({x: hyp- (A- /\ B-)} rightN _ (b s) (NId x) ([x1: hyp- B-] N2 x1) (N' x: conc # (C- true))). %worlds (gamma) (adm-/\L2 _ _). %total [] (adm-/\L2 _ _).
Shift removal
shifthyp: (hyp- A- -> conc # (C- true)) -> (hyp- (up (dn A-)) -> conc # (C- true)) -> type. /: shifthyp (N1: hyp- A- -> conc # (C- true)) N' <- ({x1: hyp- A-} shift (N1 x1) (NShift x1)) <- ({x: hyp- (up (dn A-))} unshift (foc x sup (upL (dnL NShift))) (N' x: conc # (C- true))). %mode shifthyp +N1 -N'. %worlds (gamma) (shifthyp _ _). %total [] (shifthyp _ _).
Unfocused system
Syntax
prop: type. %name prop P. a: atom P -> prop. ff: prop. or: prop -> prop -> prop. tt: prop. and: prop -> prop -> prop. imp: prop -> prop -> prop. props: type. %name props Psi. ##: props. ;: prop -> props -> props. %infix right 3 ;.
The judgment t P A relates unpolarized propositions P and polarized propositions A. The judgment can be effectively run as an erasure function from polarized to unpolarized propositions.
t: typ P -> prop -> type. %name t Trans. tc: t (c Q) (a Q). tup: t A+ P -> t (up A+) P. tbot: t bot ff. t\/: t A+ P1 -> t B+ P2 -> t (A+ \/ B+) (or P1 P2). ttop+: t top+ tt. t*: t A+ P1 -> t B+ P2 -> t (A+ * B+) (and P1 P2). tdn: t A- P -> t (dn A-) P. ttop-: t top- tt. t/\: t A- P1 -> t B- P2 -> t (A- /\ B-) (and P1 P2). t=>: t A+ P1 -> t B- P2 -> t (A+ => B-) (imp P1 P2). %mode t +A -P. %worlds (gamma) (t _ _). %total A (t A _). th: hjmt -> prop -> type. %name th TransH. t+: th (h+ Q) (a Q). t-: th (h- A-) P <- t A- P. %mode th +A -P. %worlds (gamma) (th _ _). %total [] (th _ _). tInv: pos -> props -> type. %name tInv TransInv. t#: tInv # ##. t,: t A+ P -> tInv Inv Psi -> tInv (A+ , Inv) (P ; Psi). %mode tInv +A -P. %worlds (gamma) (tInv _ _). %total Inv (tInv Inv _).
Sequent rules
left: prop -> type. %name left H. right: prop -> type. %name right D. right': props -> prop -> type. %name right' D. %block h: some {P} block {h: left P}. init: left (a Q) -> right (a Q). ffL: left ff -> right P. orR1: right P1 -> right (or P1 P2). orR2: right P2 -> right (or P1 P2). orL: (left P1 -> right Q) -> (left P2 -> right Q) -> (left (or P1 P2) -> right Q). ttR: right tt. andR: right P1 -> right P2 -> right (and P1 P2). andL1: (left P1 -> right Q) -> (left (and P1 P2) -> right Q). andL2: (left P2 -> right Q) -> (left (and P1 P2) -> right Q). impR: (left P1 -> right P2) -> right (imp P1 P2). impL: right P1 -> (left P2 -> right Q) -> (left (imp P1 P2) -> right Q). nil: right P -> right' ## P. cons: (left P -> right' Psi Q) -> right' (P ; Psi) Q.
Identity on derivations
id: right P -> right P -> type. refl: id D D.
Soundness
Soundness is established in a context where each polarized hypothesis is mapped to its erasure.
soundhyp: hyp A -> th A P -> left P -> type. %block soundhyps: some {A}{P}{T: th A P} block {x: hyp A}{h: left P}{_: soundhyp x T h}. %block soundctx = (atom+ | atom- | soundhyps). %mode +{A} -{P} +{X} -{T: th A P} -{H} soundhyp X T H. %worlds (soundctx) (soundhyp _ _ _). %total [] (soundhyp _ _ _).
The three mutually inductive theorems deal with the three classes of syntax.
soundV: rfoc A+ -> t A+ P -> right P -> type. soundN: conc Inv (A- true) -> tInv Inv Psi -> t A- P -> right' Psi P -> type. soundSp: lfoc A- (C- true) -> t A- P -> t C- Q -> (left P -> right Q) -> type. %mode soundV +V +T -D. %mode soundN +N +TInv +T -D. %mode soundSp +Sp +T1 +T2 -D. sound-lem: th (h+ Q) P -> left P -> left (a Q) -> type. /: sound-lem t+ H H. %mode sound-lem +TH +H -H'. %worlds (soundctx) (sound-lem _ _ _). %total [] (sound-lem _ _ _). /: soundV (cR Z) tc (init H') <- soundhyp Z TH H <- sound-lem TH H H'. /: soundV (dnR N) (tdn T) D <- soundN N t# T (nil D). /: soundV (\/R1 V) (t\/ T1 _) (orR1 D) <- soundV V T1 D. /: soundV (\/R2 V) (t\/ _ T2) (orR2 D) <- soundV V T2 D. /: soundV top+R ttop+ ttR. /: soundV (*R V1 V2) (t* T1 T2) (andR D1 D2) <- soundV V1 T1 D1 <- soundV V2 T2 D2. /: soundN (foc X _ Sp) t# (TCQ: t C- Q) (nil (D H)) <- soundhyp X (t- (TAP: t A- P)) (H: left P) <- soundSp Sp TAP TCQ (D: left P -> right Q). /: soundN (upR V) t# (tup T) (nil D) <- soundV V T D. /: soundN top-R t# ttop- (nil ttR). /: soundN (=>R N) t# (t=> T1 T2) (nil (impR D)) <- soundN N (t, T1 t#) T2 (cons [h: left P1] (nil (D h: right P2))). /: soundN (/\R N1 N2) t# (t/\ T1 T2) (nil (andR D1 D2)) <- soundN N1 t# T1 (nil D1) <- soundN N2 t# T2 (nil D2). /: soundN (cL [x: hyp+ Q+] N x) (t, tc TInv) TCQ (cons D) <- ({x: hyp+ Q+}{h: left (a Q+)} soundhyp x t+ h -> soundN (N x) TInv TCQ (D h: right' Psi Q)). /: soundN (dnL [x: hyp- A-] N x) (t, (tdn T) TInv) TCQ (cons D) <- ({x: hyp- A-}{h: left P} soundhyp x (t- T) h -> soundN (N x) TInv TCQ (D h: right' Psi Q)). sound-ffL: {Psi} left ff -> right' Psi Q -> type. /: sound-ffL _ H (nil (ffL H)). /: sound-ffL _ H (cons D) <- {h} sound-ffL _ H (D h). %mode +{Psi} +{Q} +{H: left ff} -{D: right' Psi Q} sound-ffL Psi H D. %worlds (atom+ | atom- | h) (sound-ffL _ _ _). %total Psi (sound-ffL Psi _ _). /: soundN botL TInv TCQ (cons D) <- ({h: left ff} sound-ffL _ h (D h)). sound-orL: {Psi} left (or P1 P2) -> (left P1 -> right' Psi Q) -> (left P2 -> right' Psi Q) -> right' Psi Q -> type. /: sound-orL _ H ([h1] nil (D1 h1)) ([h2] nil (D2 h2)) (nil (orL D1 D2 H)). /: sound-orL _ H ([h1] cons (D1 h1)) ([h2] cons (D2 h2)) (cons D) <- {h} sound-orL _ H ([h1] D1 h1 h) ([h2] D2 h2 h) (D h). %mode sound-orL +Psi +H +D1 +D2 -D. %worlds (atom+ | atom- | h) (sound-orL _ _ _ _ _). %total Psi (sound-orL Psi _ _ _ _). /: soundN (\/L N1 N2) (t, (t\/ T1 T2) TInv) TCQ (cons D) <- soundN N1 (t, T1 TInv) TCQ (cons (D1: left P1 -> right' Psi Q)) <- soundN N2 (t, T2 TInv) TCQ (cons (D2: left P2 -> right' Psi Q)) <- ({h: left (or P1 P2)} sound-orL _ h D1 D2 (D h)). /: soundN (top+L N) (t, ttop+ TInv) TCQ (cons [h: left tt] D) <- soundN N TInv TCQ (D: right' Psi Q). sound-andL: {Psi} left (and P1 P2) -> (left P1 -> left P2 -> right' Psi Q) -> right' Psi Q -> type. /: sound-andL _ H ([h1] [h2] nil (D1 h1 h2)) (nil (andL1 ([h1] andL2 ([h2] D1 h1 h2) H) H)). /: sound-andL _ H ([h1] [h2] cons (D1 h1 h2)) (cons D) <- {h} sound-andL _ H ([h1] [h2] D1 h1 h2 h) (D h). %mode sound-andL +Psi +H +D1 -D. %worlds (atom+ | atom- | h) (sound-andL _ _ _ _). %total Psi (sound-andL Psi _ _ _). /: soundN (*L N) (t, (t* T1 T2) TInv) TCQ (cons D) <- soundN N (t, T1 (t, T2 TInv)) TCQ (cons [h1] cons [h2] D1 h1 h2) <- ({h: left (and P1 P2)} sound-andL _ h D1 (D h: right' Psi Q)). /: soundSp p- tc tc ([h] init h). /: soundSp (upL N) (tup T1) TCQ D <- soundN N (t, T1 t#) TCQ (cons [h: left P] nil (D h: right Q)). /: soundSp (=>L V Sp) (t=> T1 T2) TCQ (impL D1 ([h2: left P2] D2 h2)) <- soundV V T1 (D1: right P1) <- soundSp Sp T2 TCQ (D2: left P2 -> right Q). /: soundSp (/\L1 Sp) (t/\ T1 T2) TCQ (andL1 ([h1: left P1] D h1)) <- soundSp Sp T1 TCQ (D: left P1 -> right Q). /: soundSp (/\L2 Sp) (t/\ T1 T2) TCQ (andL2 ([h2: left P2] D h2)) <- soundSp Sp T2 TCQ (D: left P2 -> right Q). %worlds (soundctx) (soundV _ _ _) (soundN _ _ _ _) (soundSp _ _ _ _). %total (V N Sp) (soundV V _ _) (soundN N _ _ _) (soundSp Sp _ _ _).
Completeness
Completeness is established in a context where each erased hypothesis is mapped to some polarization. This is the same, type-wise, as the context for soundness, but the computational interpretation runs the opposite way 'round.
completehyp: left P -> th A P -> hyp A -> type. %block completehyps: some {A}{P}{T: th A P} block {x: hyp A}{h: left P}{_: completehyp h T x}. %block completectx = (atom+ | atom- | completehyps). %mode completehyp +H -T -X. %worlds (completectx) (completehyp _ _ _). %total [] (completehyp _ _ _). complete: big -> right P -> t A- P -> conc # (A- true) -> type. %mode complete +S +D +T -N. /: complete S D (tup (tdn T)) (upR (dnR M)) <- complete S D T M.
Initial rules
cinit-: t B- (a Q) -> {D: right (a Q)} id D (init (H: left (a Q))) -> (hyp- B- -> conc # (c Q true)) -> type. %mode cinit- +TH +D +ID -M. /: cinit- (tup (tdn TH)) D Id M <- cinit- TH D Id (N: hyp- B- -> conc # (c Q true)) <- shifthyp N (M: hyp- (up (dn B-)) -> conc # (c Q true)). /: cinit- tc (init (H: left (a Q))) refl M <- adm-init- (M: hyp- (c Q) -> conc # (c Q true)). %worlds (completectx) (cinit- _ _ _ _). %total TH (cinit- TH _ _ _). /: complete S (init H) tc (M X) <- completehyp H (t- TH) X <- cinit- TH (init H) refl (M: hyp- B- -> conc # (c Q true)). cinit+: t B- (a Q) -> {D: right (a Q)} id D (init (H: left (a Q))) -> (hyp- B- -> conc # (up (c Q) true)) -> type. %mode cinit+ +TH +D +ID -M. /: cinit+ (tup (tdn TH)) D Id M <- cinit+ TH D Id (N: hyp- B- -> conc # (up (c Q) true)) <- shifthyp N (M: hyp- (up (dn B-)) -> conc # (up (c Q) true)). /: cinit+ (tup tc) (init (H: left (a Q))) refl M <- adm-init1+ (M: hyp- (up (c Q)) -> conc # (up (c Q) true)). %worlds (completehyps) (cinit+ _ _ _ _). %total TH (cinit+ TH _ _ _). cinith: th B (a (Q: atom +)) -> {D: right (a Q)} id D (init (H: left (a Q))) -> (hyp B -> conc # (up (c Q) true)) -> type. %mode cinith +TH +D +ID -M. /: cinith t+ (init (H: left (a Q))) refl M <- adm-init2+ (M: hyp+ Q -> conc # (up (c Q) true)). /: cinith (t- TH) D Id M <- cinit+ TH D Id M. %worlds (completehyps) (cinith _ _ _ _). %total TH (cinith TH _ _ _). /: complete S (init H) (tup tc) (M X) <- completehyp H TH X <- cinith TH (init H) refl (M: hyp B -> conc # (up (c Q) true)).
Disjunction
cffL: t B- ff -> {D: right Q} id D (ffL (H: left ff)) -> t C- Q -> (hyp- B- -> conc # (C- true)) -> type. %mode cffL +TH +D +Id +T -M. /: cffL (tup (tdn TH)) D Id T M <- cffL TH D Id T (N: hyp- B- -> conc # (C- true)) <- shifthyp N (M: hyp- (up (dn B-)) -> conc # (C- true)). /: cffL (tup tbot) (ffL (H: left ff)) refl T M <- adm-botL (M: hyp- (up bot) -> conc # (C- true)). %worlds (completehyps) (cffL _ _ _ _ _). %total T (cffL T _ _ _ _). /: complete S (ffL H) T (M X) <- completehyp H (t- (TH: t B- ff)) (X: hyp- B-) <- cffL TH (ffL H) refl T (M: hyp- B- -> conc # (C- true)). /: complete S (orR1 D1) (tup (t\/ T1 T2)) M <- complete S D1 (tup T1) (N1: conc # (up A+ true)) <- adm-\/R1 N1 (M: conc # (up (A+ \/ B+) true)). /: complete S (orR2 D2) (tup (t\/ T1 T2)) M <- complete S D2 (tup T2) (N2: conc # (up B+ true)) <- adm-\/R2 N2 (M: conc # (up (A+ \/ B+) true)). corL: small -> t B- (or P1 P2) -> {D: right Q} id D (orL D1 D2 (H: left (or P1 P2))) -> t C- Q -> (hyp- B- -> conc # (C- true)) -> type. %mode corL +S +TH +D +Id +T -M. /: corL S (tup (tdn TH)) D Id T M <- corL S TH D Id T (N: hyp- B- -> conc # (C- true)) <- shifthyp N (M: hyp- (up (dn B-)) -> conc # (C- true)). /: corL S (tup (t\/ T1 T2)) (orL D1 D2 (H: left (or P1 P2))) refl T N <- ({x1: hyp- (up B1+)} {h1: left P1} completehyp h1 (t- (tup T1)) x1 -> complete (b s) (D1 h1) T (N1 x1: conc # (C- true))) <- ({x2: hyp- (up B2+)} {h2: left P2} completehyp h2 (t- (tup T2)) x2 -> complete (b s) (D2 h2) T (N2 x2: conc # (C- true))) <- adm-\/L N1 N2 (N: hyp- (up (B1+ \/ B2+)) -> conc # (C- true)). /: complete (b S) (orL D1 D2 H) T (N X) <- completehyp H (t- TH) X <- corL S TH (orL D1 D2 H) refl T (N: hyp- A- -> conc # (C- true)).
Conjunction
/: complete S ttR (tup ttop+) M <- adm-top+R (M: conc # (up top+ true)). /: complete S ttR ttop- M <- adm-top-R (M: conc # (top- true)). /: complete S (andR D1 D2) (tup (t* T1 T2)) M <- complete S D1 (tup T1) (N1: conc # (up A+ true)) <- complete S D2 (tup T2) (N2: conc # (up B+ true)) <- adm-*R N1 N2 (M: conc # (up (A+ * B+) true)). /: complete S (andR D1 D2) (t/\ T1 T2) M <- complete S D1 T1 (N1: conc # (A- true)) <- complete S D2 T2 (N2: conc # (B- true)) <- adm-/\R N1 N2 (M: conc # (A- /\ B- true)). candL1: small -> t B- (and P1 P2) -> {D: right Q} id D (andL1 D1 (H: left (and P1 P2))) -> t C- Q -> (hyp- B- -> conc # (C- true)) -> type. %mode candL1 +S +TH +D +Id +T -M. /: candL1 S (tup (tdn TH)) D Id T M <- candL1 S TH D Id T (N: hyp- B- -> conc # (C- true)) <- shifthyp N (M: hyp- (up (dn B-)) -> conc # (C- true)). /: candL1 S (tup (t* T1 T2)) (andL1 D1 (H: left (and P1 P2))) refl T M <- ({x1: hyp- (up B1+)}{h1: left P1} completehyp h1 (t- (tup T1)) x1 -> complete (b s) (D1 h1) T (N1 x1: conc # (C- true))) <- adm-*L ([x1: hyp- (up B1+)][x2: hyp- (up B2+)] N1 x1) (M: hyp- (up (B1+ * B2+)) -> conc # (C- true)). /: candL1 S (t/\ T1 T2) (andL1 D1 (H: left (and P1 P2))) refl T M <- ({x1: hyp- B1-}{h1: left P1} completehyp h1 (t- T1) x1 -> complete (b s) (D1 h1) T (N1 x1: conc # (C- true))) <- adm-/\L1 N1 (M: hyp- (B1- /\ B2-) -> conc # (C- true)). /: complete (b S) (andL1 D1 H) T (M X) <- completehyp H (t- TH) X <- candL1 S TH (andL1 D1 H) refl T (M: hyp- A- -> conc # (C- true)). candL2: small -> t B- (and P1 P2) -> {D: right Q} id D (andL2 D1 (H: left (and P1 P2))) -> t C- Q -> (hyp- B- -> conc # (C- true)) -> type. %mode candL2 +S +TH +D +Id +T -M. /: candL2 S (tup (tdn TH)) D Id T M <- candL2 S TH D Id T (N: hyp- B- -> conc # (C- true)) <- shifthyp N (M: hyp- (up (dn B-)) -> conc # (C- true)). /: candL2 S (tup (t* T1 T2)) (andL2 D2 (H: left (and P1 P2))) refl T M <- ({x2: hyp- (up B2+)}{h2: left P2} completehyp h2 (t- (tup T2)) x2 -> complete (b s) (D2 h2) T (N2 x2: conc # (C- true))) <- adm-*L ([x1: hyp- (up B1+)][x2: hyp- (up B2+)] N2 x2) (M: hyp- (up (B1+ * B2+)) -> conc # (C- true)). /: candL2 S (t/\ T1 T2) (andL2 D2 (H: left (and P1 P2))) refl T M <- ({x2: hyp- B2-}{h2: left P2} completehyp h2 (t- T2) x2 -> complete (b s) (D2 h2) T (N2 x2: conc # (C- true))) <- adm-/\L2 N2 (M: hyp- (B1- /\ B2-) -> conc # (C- true)). /: complete (b S) (andL2 D2 H) T (M X) <- completehyp H (t- TH) X <- candL2 S TH (andL2 D2 H) refl T (M: hyp- A- -> conc # (C- true)).
Implication
/: complete S (impR D1) (t=> T1 T2) M <- ({x: hyp- (up A+)}{h: left P1} completehyp h (t- (tup T1)) x -> complete S (D1 h) T2 (N1 x: conc # (B- true))) <- adm-=>R N1 (M: conc # (A+ => B- true)). cimpL: small -> t B- (imp P1 P2) -> {D: right Q} id D (impL D1 D2 (H: left (imp P1 P2))) -> t C- Q -> (hyp- B- -> conc # (C- true)) -> type. %mode cimpL +S +TH +D +Id +T -N. /: cimpL S (tup (tdn TH)) D Id T M <- cimpL S TH D Id T (N: hyp- B- -> conc # (C- true)) <- shifthyp N (M: hyp- (up (dn B-)) -> conc # (C- true)). /: cimpL S (t=> T1 T2) (impL D1 D2 (H: left (imp P1 P2))) refl T N <- complete (b s) D1 (tup T1) (N1: conc # (up A+ true)) <- ({x2: hyp- B-}{h2: left P2} completehyp h2 (t- T2) x2 -> complete (b s) (D2 h2) T (N2 x2: conc # (C- true))) <- adm-=>L N1 N2 (N: hyp- (A+ => B-) -> conc # (C- true)). /: complete (b S) (impL D1 D2 H) T (N X) <- completehyp H (t- TH) X <- cimpL S TH (impL D1 D2 H) refl T N. %worlds (completehyps) (corL _ _ _ _ _ _) (candL1 _ _ _ _ _ _) (candL2 _ _ _ _ _ _) (cimpL _ _ _ _ _ _) (complete _ _ _ _). %total {(D DorL DandL1 DandL2 DimpL) (S SorL SandL1 SandL2 SimpL) (T TorL TandL1 TandL2 TimpL)} (corL SorL TorL DorL _ _ _) (candL1 SandL1 TandL1 DandL1 _ _ _) (candL2 SandL2 TandL2 DandL2 _ _ _) (cimpL SimpL TimpL DimpL _ _ _) (complete S D T _).
Inheriting the focused calculus's metatheory
We need the existance of some polarization strategy; we intentionally pick a middling, undistinghished sort of translation that translates everything as a negative proposition. It will work great on hereditary Harrop formulas and not so good if you have lots of disjunction and positive propositions; the only interesting thing about it is that it's results are reminiscent of Howe's semi-focused lax logic..
polarize: {P} t (A-: typ -) P -> type. %mode polarize +P -T. /: polarize (a Q) tc. /: polarize (a Q) (tup tc). /: polarize ff (tup tbot). /: polarize (or P1 P2) (tup (t\/ (tdn T1) (tdn T2))) <- polarize P1 T1 <- polarize P2 T2. /: polarize tt ttop-. /: polarize (and P1 P2) (t/\ T1 T2) <- polarize P1 T1 <- polarize P2 T2. /: polarize (imp P1 P2) (t=> (tdn T1) T2) <- polarize P1 T1 <- polarize P2 T2. %worlds (atom+ | atom-) (polarize _ _). %total P (polarize P _). %block translate: some {A}{P}{TH: th A P} block {x: hyp A}{h: left P}{_: soundhyp x TH h}{_: completehyp h TH x}. unfocused-cut: right P -> (left P -> right Q) -> right Q -> type. %mode unfocused-cut +D +E -F. /: unfocused-cut (D: right P) (E: left P -> right Q) F <- polarize P (TP: t A- P) <- complete (b s) D TP (M: conc # (A- true)) <- polarize Q (TQ: t C- Q) <- ({x: hyp- A-}{h: left P} completehyp h (t- TP) x -> complete (b s) (E h) TQ (N x: conc # (C- true))) <- rightN _ (b s) M N N' <- soundN N' t# TQ (nil (F: right Q)). %worlds (translate) (unfocused-cut _ _ _). %total [] (unfocused-cut _ _ _). unfocused-identity: (left P -> right P) -> type. %mode +{P} -{D: left P -> right P} unfocused-identity D. /: unfocused-identity D <- polarize P (TP: t A- P) <- identity (N: hyp- A- -> conc # (A- true)) <- ({x: hyp- A-}{h: left P} soundhyp x (t- TP) h -> soundN (N x) t# TP (nil (D h: right P))). %worlds (translate) (unfocused-identity _). %total [] (unfocused-identity _).
Running the theorems
Here are two unfocused derivations of (p ∧ q) => (r ∧ s) => (p ∧ t).
d1: {P}{p: atom P}{q: atom P}{r: atom P}{s: atom P} right (imp (and (a p) (a q)) (imp (and (a r) (a s)) (and (a p) (a r)))) = [P][p][q][r][s] impR [h1: left (and (a p) (a q))] impR [h2: left (and (a r) (a s))] andR (andL1 ([h1': left (a p)] init h1') h1) (andL1 ([h2': left (a r)] init h2') h2). d2: {P}{p: atom P}{q: atom P}{r: atom P}{s: atom P} right (imp (and (a p) (a q)) (imp (and (a r) (a s)) (and (a p) (a r)))) = [P][p][q][r][s] impR [h1: left (and (a p) (a q))] impR [h2: left (and (a r) (a s))] andL1 ([h1': left (a p)] andR (andL2 ([_] (andL2 ([_] (init h1')) h1)) h1) (andL1 ([h2': left (a r)] init h2') h2)) h1.
Here are three different polarizations.
%solve t-: {p}{q}{r}{s} t (dn(c p /\ c q) => (dn(c r /\ c s) => (c p /\ c r))) _. %solve t+: {p}{q}{r}{s} t ((c p * c q) => ((c r * c s) => up(c p * c r))) _. %solve te: {p}{q}{r}{s} t (dn(up(c p) /\ up(c q)) => up(dn(dn(up(c r) /\ up(c s)) => up(dn(up(c p) /\ up(c r)))))) _.
Under the same "good" polarization, different derivations translate to a single unique proof.
%query 1 * {p}{q}{r}{s} complete _ (d1 - p q r s) (t- p q r s) (N p q r s). %query 1 * {p}{q}{r}{s} complete _ (d2 - p q r s) (t- p q r s) (N p q r s).
Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)%query 1 * {p:atom -} {q:atom -} {r:atom -} {s1:atom -} complete (X1 p q r s1) (d1 - p q r s1) (t- p q r s1) (N p q r s1). ---------- Solution 1 ---------- N = [q:atom -] [q1:atom -] [q2:atom -] [q3:atom -] =>R (dnL ([x':hyp (h- (c q /\ c q1))] =>R (dnL ([x'10:hyp (h- (c q2 /\ c q3))] /\R (foc x' sa (/\L1 p-)) (foc x'10 sa (/\L1 p-)))))). ____________________________________________ %query 1 * {p:atom -} {q:atom -} {r:atom -} {s1:atom -} complete (X1 p q r s1) (d2 - p q r s1) (t- p q r s1) (N p q r s1). ---------- Solution 1 ---------- N = [q:atom -] [q1:atom -] [q2:atom -] [q3:atom -] =>R (dnL ([x':hyp (h- (c q /\ c q1))] =>R (dnL ([x'23:hyp (h- (c q2 /\ c q3))] /\R (foc x' sa (/\L1 p-)) (foc x'23 sa (/\L1 p-)))))). ____________________________________________
%% OK %%
Different polarizations may lead to very differently shaped derivations.
%query 1 * {p}{q}{r}{s} complete _ (d2 + p q r s) (t+ p q r s) (N p q r s). %query 2 * {p}{q}{r}{s} complete _ (d2 + p q r s) (te p q r s) (N p q r s).
Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)%query 1 * {p:atom +} {q:atom +} {r:atom +} {s1:atom +} complete (X1 p q r s1) (d2 + p q r s1) (t+ p q r s1) (N p q r s1). ---------- Solution 1 ---------- N = [q:atom +] [q1:atom +] [q2:atom +] [q3:atom +] =>R (*L (cL ([z:hyp (h+ q)] cL ([z88:hyp (h+ q1)] =>R (*L (cL ([z89:hyp (h+ q2)] cL ([z90:hyp (h+ q3)] upR (*R (cR z) (cR z89)))))))))). ____________________________________________ %query 2 * {p:atom +} {q:atom +} {r:atom +} {s1:atom +} complete (X1 p q r s1) (d2 + p q r s1) (te p q r s1) (N p q r s1). ---------- Solution 1 ---------- N = [q:atom +] [q1:atom +] [q2:atom +] [q3:atom +] =>R (dnL ([x':hyp (h- (up (c q) /\ up (c q1)))] upR (dnR (=>R (dnL ([x'26:hyp (h- (up (c q2) /\ up (c q3)))] upR ( dnR (/\R (foc x' sup (/\L1 (upL (cL ([z:hyp (h+ q)] upR (cR z)))))) (foc x'26 sup (/\L1 (upL (cL ([z:hyp (h+ q2)] upR (cR z)))))))))))))). ---------- Solution 2 ---------- N = [q:atom +] [q1:atom +] [q2:atom +] [q3:atom +] =>R (dnL ([x':hyp (h- (up (c q) /\ up (c q1)))] upR (dnR (=>R (dnL ([x'51:hyp (h- (up (c q2) /\ up (c q3)))] upR ( dnR (/\R (foc x' sup (/\L1 (upL (cL ([z:hyp (h+ q)] upR (cR z)))))) (foc x'51 sup (/\L1 (upL (cL ([z:hyp (h+ q2)] upR (cR z)))))))))))))). ____________________________________________
%% OK %%
