Structural focalization

By Rob Simmons.

Focusing, introduced by Jean-Marc Andreoli in the context of classical linear logic, defines a normal form for sequent calculus derivations that cuts down on the number of possible derivations by eagerly applying invertible rules and grouping sequences of non-invertible rules. A focused sequent calculus is defined relative to some non-focused sequent calculus; focalization is the property that every non-focused derivation can be transformed into a focused derivation. In the paper Structural Focalization, I present a focused sequent calculus for propositional intuitionistic logic and prove the focalization property relative to a standard presentation of propositional intuitionistic logic.

This version follows the on-paper version very directly; the cost is that the id⁻ rule and the admissible subst⁻ focal substitution principle have to be written out instead of given for free by LF substitution as the id⁺ rule and subst⁻ substitution principles are.

%sort small %.
%sort big %.
%term s small %.
%term b %pi small %-> big %.

Syntax

%sort pol %.
%name pol %.
%term ⁺ pol %.
%term ⁻ pol %.

We define propositions in an environment with free atoms.

%sort atom {_ pol} %.
%name atom %.
%block atom⁺ {Q⁺ atom ⁺}%.
%block atom⁻ {Q⁻ atom ⁻}%.
%sort typ {_ pol} %.
%name typ %.
%term c %pi (atom P) %-> (typ P) %.
%term ↓ %pi (typ ⁻) %-> (typ ⁺) %.
%term ⊥ typ ⁺ %.
%term ∨ %pi (typ ⁺) %-> (typ ⁺) %-> (typ ⁺) %.
%prec %none 5 ∨ %.
%term ⊤⁺ typ ⁺ %.
%term ∧⁺ %pi (typ ⁺) %-> (typ ⁺) %-> (typ ⁺) %.
%prec %none 5 ∧⁺ %.
%term ↑ %pi (typ ⁺) %-> (typ ⁻) %.
%term ⊃ %pi (typ ⁺) %-> (typ ⁻) %-> (typ ⁻) %.
%prec %none 5 ⊃ %.
%term ⊤⁻ typ ⁻ %.
%term ∧⁻ %pi (typ ⁻) %-> (typ ⁻) %-> (typ ⁻) %.
%prec %none 5 ∧⁻ %.

Succedents are things that come to the right of the turnstile.

%sort suc %.
%name suc %.
%term inv %pi (typ ⁻) %-> suc %.
%prec %postfix 3 inv %.
%term true %pi (typ ⁺) %-> suc %.
%prec %postfix 3 true %.
%term susp %pi (typ ⁻) %-> suc %.
%prec %postfix 3 susp %.

Right-stable judgments are ones that are either positive or suspended.

%sort stable {_ suc} %.
%name stable %.
%term sp stable (A⁺ true) %.
%term sn stable (A⁻ susp) %.

An inversion context “Ω” is a list of positive propositions.

%sort pos %.
%name pos %.
%term · pos %.
%term , %pi (typ ⁺) %-> pos %-> pos %.
%prec %right 3 , %.

Sequent calculus

%sort seqform %.
%name seqform %.
%sort exp {_ seqform} %.
%name exp %.
%term rfoc %pi (typ ⁺) %-> seqform %.
%inline value (%pi (typ ⁺) %-> %type) [A⁺] exp (rfoc A⁺) %.
%sort leftform %.
%term hasleft %pi leftform %-> suc %-> seqform %.
%term ininv %pi pos %-> leftform %.
%inline term (%pi pos %-> suc %-> %type) [_Ω] [U] exp (hasleft (ininv _Ω) U) %.
%term infoc %pi (typ ⁻) %-> leftform %.
%inline spine (%pi (typ ⁻) %-> suc %-> %type) [A⁻] [U] exp (hasleft (infoc A⁻) U) %.
%sort hyp {_ typ ⁻} %.
%name hyp %.
%block nprop [A⁻ typ ⁻] {x hyp A⁻}%.
%block aprop [Q⁺ atom ⁺] {z value (c Q⁺)}%.
%block pprop [A⁺ typ ⁺] {z value A⁺}%.
%worlds (atom⁺ atom⁻ nprop) (hyp _) %.
%block gamma_suspnormal%.
% World for cut
%block gamma%.
% World for identity
%sort suspnormal {_ suc} %.
%term snn suspnormal (A⁻ inv) %.
%term snp suspnormal (A⁺ true) %.
%term sna suspnormal (c Q⁻ susp) %.
%sort suspstable {_ suc} %.
%term ss %pi (stable U) %-> (suspnormal U) %-> (suspstable U) %.
%sort suspnormalF {_ seqform} %.
%term snr suspnormalF (rfoc A⁺) %.
%term snl %pi (suspnormalF (hasleft _ U)) %<- (suspnormal U) %.

Values

V ::= z | thunk N | inl V | inr V | ⟨⟩⁺ | ⟨V₁,V₂⟩⁺

The rule id⁺ corresponding to the proof term z comes for free from LF.

%term ↓R %pi (term · (A⁻ inv)) %-> (value (↓ A⁻)) %.
%term ∨R₁ %pi (value A⁺) %-> (value (A⁺ ∨ B⁺)) %.
%term ∨R₂ %pi (value B⁺) %-> (value (A⁺ ∨ B⁺)) %.
%term ⊤⁺R value ⊤⁺ %.
%term ∧⁺R %pi (value A⁺) %-> (value B⁺) %-> (value (A⁺ ∧⁺ B⁺)) %.

Terms

M ::= ret V | x • Sp | ⟨z⟩.N | x.N | abort | [N₁, N₂] | ⟨⟩.N | ×N | ⟨N⟩ | {N} | λN | ⟨⟩⁻ | ⟨N₁,N₂⟩⁻

%term focR %pi (value A⁺) %-> (term · (A⁺ true)) %.
%term focL %pi (stable Suc) %-> (hyp A⁻) %-> (spine A⁻ Suc) %-> (term · Suc) %.
%term η⁺ %pi (%pi (value (c Q⁺)) %-> (term _Ω Suc)) %-> (term (c Q⁺ , _Ω) Suc) %.
%term ↓L %pi (%pi (hyp A⁻) %-> (term _Ω Suc)) %-> (term (↓ A⁻ , _Ω) Suc) %.
%term ⊥L term (⊥ , _Ω) Suc %.
%term ∨L %pi (term (A⁺ , _Ω) Suc) %-> (term (B⁺ , _Ω) Suc) %-> (term (A⁺ ∨ B⁺ , _Ω) Suc) %.
%term ⊤⁺L %pi (term _Ω Suc) %-> (term (⊤⁺ , _Ω) Suc) %.
%term ∧⁺L %pi (term (A⁺ , B⁺ , _Ω) Suc) %-> (term (A⁺ ∧⁺ B⁺ , _Ω) Suc) %.
%term η⁻ %pi (term · (c Q⁻ susp)) %-> (term · (c Q⁻ inv)) %.
%term ↑R %pi (term · (A⁺ true)) %-> (term · (↑ A⁺ inv)) %.
%term ⊃R %pi (term (A⁺ , ·) (B⁻ inv)) %-> (term · (A⁺ ⊃ B⁻ inv)) %.
%term ⊤⁻R term · (⊤⁻ inv) %.
%term ∧⁻R %pi (term · (A⁻ inv)) %-> (term · (B⁻ inv)) %-> (term · (A⁻ ∧⁻ B⁻ inv)) %.

Spines

Sp ::= nil | pm N | V;Sp | π₁;Sp | π₂;Sp

%term id⁻ spine A⁻ (A⁻ susp) %.
%term ↑L %pi (stable Suc) %-> (term (A⁺ , ·) Suc) %-> (spine (↑ A⁺) Suc) %.
%term ⊃L %pi (value A⁺) %-> (spine B⁻ Suc) %-> (spine (A⁺ ⊃ B⁻) Suc) %.
%term ∧⁻L₁ %pi (spine A⁻ Suc) %-> (spine (A⁻ ∧⁻ B⁻) Suc) %.
%term ∧⁻L₂ %pi (spine B⁻ Suc) %-> (spine (A⁻ ∧⁻ B⁻) Suc) %.

Negative focal substitution

Our encoding gives us positive focal substitution for free - it’s very natural to describe suspended propositions ⟨A⁺⟩ in the hypothetical context as variables of type rfoc A⁺, which is adequate and gives us the id⁺ rule for free. By choosing a more traditional way of describing negative suspended propositions (instead of the complicated encoding that gives us id⁻ for free), we have forced ourselves to prove a theorem, negative focal substitution, that we could have avoided.

%sort subst⁻ {_ stable U} {_ exp (hasleft L (A⁻ susp))} {_ spine A⁻ U} {_ exp (hasleft L U)} %.
%mode subst⁻ %in %in %in %out %.
%term _ %pi (subst⁻ Pf (focL _ X Sp0) Sp (focL Pf X Sp0')) %<- (subst⁻ Pf Sp0 Sp Sp0') %.
%term _
  %pi (subst⁻ Pf (η⁺ ([z] N z)) Sp (η⁺ ([z] N' z)))
  %<- ({z} subst⁻ Pf (N z) Sp (N' z)) %.
%term _
  %pi (subst⁻ Pf (↓L ([x] N x)) Sp (↓L ([x] N' x)))
  %<- ({x} subst⁻ Pf (N x) Sp (N' x)) %.
%term _ subst⁻ Pf ⊥L Sp ⊥L %.
%term _
  %pi (subst⁻ Pf (∨L N1 N2) Sp (∨L N1' N2'))
  %<- (subst⁻ Pf N1 Sp N1')
  %<- (subst⁻ Pf N2 Sp N2') %.
%term _ %pi (subst⁻ Pf (⊤⁺L N) Sp (⊤⁺L N')) %<- (subst⁻ Pf N Sp N') %.
%term _ %pi (subst⁻ Pf (∧⁺L N) Sp (∧⁺L N')) %<- (subst⁻ Pf N Sp N') %.
%term _ subst⁻ Pf id⁻ Sp Sp %.
%term _ %pi (subst⁻ Pf (↑L _ N) Sp (↑L Pf N')) %<- (subst⁻ Pf N Sp N') %.
%term _ %pi (subst⁻ Pf (⊃L V Sp0) Sp (⊃L V Sp0')) %<- (subst⁻ Pf Sp0 Sp Sp0') %.
%term _ %pi (subst⁻ Pf (∧⁻L₁ Sp0) Sp (∧⁻L₁ Sp0')) %<- (subst⁻ Pf Sp0 Sp Sp0') %.
%term _ %pi (subst⁻ Pf (∧⁻L₂ Sp0) Sp (∧⁻L₂ Sp0')) %<- (subst⁻ Pf Sp0 Sp Sp0') %.
%worlds (gamma) (subst⁻ _ _ _ _) %.
%total E (subst⁻ _ E _ _) %.

Cut admissibility

Cut admissibility has a couple 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
• N • Sp - negative cut formula.

%sort cut⁺ {A⁺} {_ small} {_ suspnormal U} {_ value A⁺} {_ term (A⁺ , _Ω) U} {_ term _Ω U} %.
%sort cut⁻ {A⁻} {_ small} {_ suspstable U} {_ term · (A⁻ inv)} {_ spine A⁻ U} {_ term · U} %.
%mode cut⁺ %in %in %in %in %in %out %.
%mode cut⁻ %in %in %in %in %in %out %.

The “rightist” substitution N/xE captures all right commutative cuts. Each inductive call within this group decreases the size of the expression E that we are substituting into.

%sort rsubst {A⁻} {_ big} {_ suspnormalF Form} {_ term · (A⁻ inv)} {_ %pi (hyp A⁻) %-> (exp Form)} {_ exp Form} %.
%mode rsubst %in %in %in %in %in %out %.

The “leftist” substitution <<E>>N captures all left commutative cuts. Each inductive call within this group decreases the size of the expression E that we are substituting in, hence “leftist.”

%sort lsubst {A⁺} {_ big} {_ suspstable U} {_ exp (hasleft L (A⁺ true))} {_ term (A⁺ , ·) U} {_ exp (hasleft L U)} %.
%mode lsubst %in %in %in %in %in %out %.

Principal substitution/cuts

(V • N) = N'

%term _ cut⁺ (c Q⁺) S _ X (η⁺ ([z] N z)) (N X) %.
%term _
  %pi (cut⁺ (↓ A⁻) s Pf (↓R M) (↓L N) N')
  %<- (rsubst A⁻ (b s) (snl Pf) M N (%the (term _Ω U) N')) %.
%term _
  %pi (cut⁺ (A⁺ ∨ B⁺) S Pf (∨R₁ V) (∨L N₁ N₂) N')
  %<- (cut⁺ A⁺ S Pf V N₁ (%the (term _Ω U) N')) %.
%term _
  %pi (cut⁺ (A⁺ ∨ B⁺) S Pf (∨R₂ V) (∨L N₁ N₂) N')
  %<- (cut⁺ B⁺ S Pf V N₂ (%the (term _Ω U) N')) %.
%term _ cut⁺ ⊤⁺ S Pf ⊤⁺R (⊤⁺L N) N %.
%term _
  %pi (cut⁺ (A⁺ ∧⁺ B⁺) S Pf (∧⁺R V₁ V₂) (∧⁺L N) N')
  %<- (cut⁺ A⁺ S Pf V₁ N (%the (term (B⁺ , _Ω) U) NB))
  %<- (cut⁺ B⁺ S Pf V₂ NB (%the (term _Ω U) N')) %.

(M • Sp) = N'

%term _ cut⁻ (c Q⁻) S Pf (η⁻ N) id⁻ N %.
%term _ %pi (cut⁻ (↑ A⁺) s Pf (↑R N) (↑L _ M) N') %<- (lsubst A⁺ (b s) Pf N M N') %.
%term _
  %pi (cut⁻ (A⁺ ⊃ B⁻) S (ss Pf1 Pf2) (⊃R N) (⊃L V Sp) N')
  %<- (cut⁺ A⁺ S snn V N (%the (term · (B⁻ inv)) NB))
  %<- (cut⁻ B⁻ S (ss Pf1 Pf2) NB Sp (%the (term · U) N')) %.
%term _
  %pi (cut⁻ (A⁻ ∧⁻ B⁻) S Pf (∧⁻R N₁ N₂) (∧⁻L₁ Sp) N')
  %<- (cut⁻ A⁻ S Pf N₁ Sp (%the (term · U) N')) %.
%term _
  %pi (cut⁻ (A⁻ ∧⁻ B⁻) S Pf (∧⁻R N₁ N₂) (∧⁻L₂ Sp) N')
  %<- (cut⁻ B⁻ S Pf N₂ Sp (%the (term · U) N')) %.

Rightist substitution (right commutative cuts)

M/xV = V'

%term _ rsubst A⁻ S snr M ([x] V) (%the (value (c Q⁺)) V) %.
%term _
  %pi (rsubst A⁻ S snr M ([x] ↓R (N x)) (↓R N'))
  %<- (rsubst A⁻ S (snl snn) M ([x] N x) (%the (term · (C⁻ inv)) N')) %.
%term _
  %pi (rsubst A⁻ S snr M ([x] ∨R₁ (V x)) (∨R₁ V'))
  %<- (rsubst A⁻ S snr M ([x] V x) (%the (value C₁⁺) V')) %.
%term _
  %pi (rsubst A⁻ S snr M ([x] ∨R₂ (V x)) (∨R₂ V'))
  %<- (rsubst A⁻ S snr M ([x] V x) (%the (value C₂⁺) V')) %.
%term _ rsubst A⁻ S snr M ([x] ⊤⁺R) ⊤⁺R %.
%term _
  %pi (rsubst A⁻ S snr M ([x] ∧⁺R (V₁ x) (V₂ x)) (∧⁺R V₁' V₂'))
  %<- (rsubst A⁻ S snr M ([x] V₁ x) (%the (value C₁⁺) V₁'))
  %<- (rsubst A⁻ S snr M ([x] V₂ x) (%the (value C₂⁺) V₂')) %.

M/xN = N'

% Entering principal substitution (cut⁻)
%term _
  %pi (rsubst A⁻ (b s) (snl Pf) M ([x] focR (V x)) (focR V'))
  %<- (rsubst A⁻ (b s) snr M ([x] V x) V') %.
%term _
  %pi (rsubst A⁻ (b s) (snl Pf) M ([x] focL Pf' x (Sp x)) N')
  %<- (rsubst A⁻ (b s) (snl Pf) M ([x] Sp x) (%the (spine A⁻ U) Sp'))
  %<- (cut⁻ A⁻ s (ss Pf' Pf) M Sp' (%the (term · U) N')) %.
%term _
  %pi (rsubst A⁻ S (snl Pf) M ([x] focL Pf' X' (Sp x)) (focL Pf' X' Sp'))
  %<- (rsubst A⁻ S (snl Pf) M ([x] Sp x) (%the (spine B⁻ U) Sp')) %.
%term _
  %pi (rsubst A⁻ S (snl Pf) M ([x] η⁺ ([z] N x z)) (η⁺ ([z] N' z)))
  %<- ({z value (c Q⁺)} rsubst A⁻ S (snl Pf) M ([x] N x z) (%the (term _Ω U) (N' z))) %.
%term _
  %pi (rsubst A⁻ S (snl Pf) M ([x] ↓L ([x'] N x x')) (↓L ([x'] N' x')))
  %<- ({x' hyp B⁻} rsubst A⁻ S (snl Pf) M ([x] N x x') (%the (term _Ω U) (N' x'))) %.
%term _ rsubst A⁻ S (snl Pf) M ([x] ⊥L) ⊥L %.
%term _
  %pi (rsubst A⁻ S (snl Pf) M ([x] ∨L (N₁ x) (N₂ x)) (∨L N₁' N₂'))
  %<- (rsubst A⁻ S (snl Pf) M ([x] N₁ x) (%the (term (B₁ , _Ω) U) N₁'))
  %<- (rsubst A⁻ S (snl Pf) M ([x] N₂ x) (%the (term (B₂ , _Ω) U) N₂')) %.
%term _
  %pi (rsubst A⁻ S (snl Pf) M ([x] ⊤⁺L (N x)) (⊤⁺L N'))
  %<- (rsubst A⁻ S (snl Pf) M ([x] N x) (%the (term _Ω U) N')) %.
%term _
  %pi (rsubst A⁻ S (snl Pf) M ([x] ∧⁺L (N x)) (∧⁺L N'))
  %<- (rsubst A⁻ S (snl Pf) M ([x] N x) (%the (term (A⁺ , B⁺ , _Ω) U) N')) %.
%term _
  %pi (rsubst A⁻ S (snl snn) M ([x] η⁻ (N x)) (η⁻ N'))
  %<- (rsubst A⁻ S (snl sna) M ([x] N x) (%the (term · (c Q⁻ susp)) N')) %.
%term _
  %pi (rsubst A⁻ S (snl snn) M ([x] ↑R (N x)) (↑R N'))
  %<- (rsubst A⁻ S (snl snp) M ([x] N x) (%the (term · (C⁺ true)) N')) %.
%term _
  %pi (rsubst A⁻ S (snl snn) M ([x] ⊃R (N x)) (⊃R N'))
  %<- (rsubst A⁻ S (snl snn) M ([x] N x) (%the (term (C₁⁺ , ·) (C₂⁻ inv)) N')) %.
%term _ rsubst A⁻ S (snl snn) M ([x] ⊤⁻R) ⊤⁻R %.
%term _
  %pi (rsubst A⁻ S (snl snn) M ([x] ∧⁻R (N₁ x) (N₂ x)) (∧⁻R N₁' N₂'))
  %<- (rsubst A⁻ S (snl snn) M ([x] N₁ x) (%the (term · (C₁⁻ inv)) N₁'))
  %<- (rsubst A⁻ S (snl snn) M ([x] N₂ x) (%the (term · (C₂⁻ inv)) N₂')) %.

M/xSp = Sp'

%term _ rsubst A⁻ S (snl sna) M ([x] id⁻) id⁻ %.
%term _
  %pi (rsubst A⁻ S (snl Pf) M ([x] ↑L Pf' (N x)) (↑L Pf' N'))
  %<- (rsubst A⁻ S (snl Pf) M ([x] N x) (%the (term (B⁺ , ·) U) N')) %.
%term _
  %pi (rsubst A⁻ S (snl Pf) M ([x] ⊃L (V x) (Sp x)) (⊃L V' Sp'))
  %<- (rsubst A⁻ S snr M ([x] V x) (%the (value B₁⁺) V'))
  %<- (rsubst A⁻ S (snl Pf) M ([x] Sp x) (%the (spine B₂⁻ U) Sp')) %.
%term _
  %pi (rsubst A⁻ S (snl Pf) M ([x] ∧⁻L₁ (Sp x)) (∧⁻L₁ Sp'))
  %<- (rsubst A⁻ S (snl Pf) M ([x] Sp x) (%the (spine B₁⁻ U) Sp')) %.
%term _
  %pi (rsubst A⁻ S (snl Pf) M ([x] ∧⁻L₂ (Sp x)) (∧⁻L₂ Sp'))
  %<- (rsubst A⁻ S (snl Pf) M ([x] Sp x) (%the (spine B₂⁻ U) Sp')) %.

Leftist substitution (left commutative cuts)

<<M>>N = M'

% Entering principal substitution (cut⁺)
%term _ %pi (lsubst A⁺ (b s) (ss Pf Pf') (focR V) N N') %<- (cut⁺ A⁺ s Pf' V N N') %.
%term _
  %pi (lsubst A⁺ S (ss Pf Pf') (focL _ X Sp) N (focL Pf X Sp'))
  %<- (lsubst A⁺ S (ss Pf Pf') Sp N (%the (spine B⁻ U) Sp')) %.
%term _
  %pi (lsubst A⁺ S Pf (η⁺ ([z] M z)) N (η⁺ ([z] M' z)))
  %<- ({z value (c Q⁺)} lsubst A⁺ S Pf (M z) N (%the (term _Ω U) (M' z))) %.
%term _
  %pi (lsubst A⁺ S (ss Pf Pf') (↓L ([x'] M x')) N (↓L ([x'] M' x')))
  %<- ({x' hyp B⁻} lsubst A⁺ S (ss Pf Pf') (M x') N (%the (term _Ω U) (M' x'))) %.
%term _ lsubst A⁺ S Pf ⊥L N ⊥L %.
%term _
  %pi (lsubst A⁺ S Pf (∨L M₁ M₂) N (∨L M₁' M₂'))
  %<- (lsubst A⁺ S Pf M₁ N (%the (term (B₁⁺ , _Ω) U) M₁'))
  %<- (lsubst A⁺ S Pf M₂ N (%the (term (B₂⁺ , _Ω) U) M₂')) %.
%term _
  %pi (lsubst A⁺ S Pf (⊤⁺L M) N (⊤⁺L M'))
  %<- (lsubst A⁺ S Pf M N (%the (term _Ω U) M')) %.
%term _
  %pi (lsubst A⁺ S Pf (∧⁺L M) N (∧⁺L M'))
  %<- (lsubst A⁺ S Pf M N (%the (term (B₁⁺ , B₂⁺ , _Ω) U) M')) %.

<<Sp>>N = Sp'

%term _
  %pi (lsubst A⁺ S (ss Pf Pf') (↑L _ M) N (↑L Pf M'))
  %<- (lsubst A⁺ S (ss Pf Pf') M N (%the (term (B⁺ , ·) U) M')) %.
%term _
  %pi (lsubst A⁺ S Pf (⊃L V Sp) N (⊃L V Sp'))
  %<- (lsubst A⁺ S Pf Sp N (%the (spine B₂⁻ U) Sp')) %.
%term _
  %pi (lsubst A⁺ S Pf (∧⁻L₁ Sp) N (∧⁻L₁ Sp'))
  %<- (lsubst A⁺ S Pf Sp N (%the (spine B₁⁻ U) Sp')) %.
%term _
  %pi (lsubst A⁺ S Pf (∧⁻L₂ Sp) N (∧⁻L₂ Sp'))
  %<- (lsubst A⁺ S Pf Sp N (%the (spine B₂⁻ U) Sp')) %.

Wrap-up

%worlds (gamma_suspnormal) (cut⁺ _ _ _ _ _ _) (cut⁻ _ _ _ _ _ _) (rsubst _ _ _ _ _ _) (lsubst _ _ _ _ _ _) %.

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 structural cut elimination arguments.

%total {(A1 A2 A3 A4) {(S1 S2 S3 S4) [(V N⁻ MR EL) (N⁺ S ER NL)]}} (cut⁺ A1 S1 _ V N⁺ _) (cut⁻ A2 S2 _ N⁻ S _) (rsubst A3 S3 _ MR ER _) (lsubst A4 S4 _ EL NL _) %.

The following simpler induction metric also works, 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) {(S1 S2 S3 S4) (S1 S2 ER EL)}} (cut⁻ A1 S1 _ _ _ _) (cut⁺ A2 S2 _ _ _ _) (rsubst A3 S3 _ _ ER _) (lsubst A4 S4 _ EL _ _) %.

Expansion

%sort expand⁺ {A⁺} {_ %pi (value A⁺) %-> (term _Ω U)} {_ term (A⁺ , _Ω) U} %.
%sort expand⁻ {A⁻} {_ term · (A⁻ susp)} {_ term · (A⁻ inv)} %.
%mode expand⁺ %in %in %out %.
%mode expand⁻ %in %in %out %.

η(z.N) = N'

%term _ expand⁺ (c Q⁺) ([z value (c Q⁺)] N z) (η⁺ ([z value (c Q⁺)] N z)) %.
%term _
  %pi (expand⁺ (↓ A⁻) ([z value (↓ A⁻)] N z) (↓L ([x hyp A⁻] N (↓R (N' x)))))
  %<- ({x hyp A⁻} expand⁻ A⁻ (focL sn x id⁻) (%the (term · (A⁻ inv)) (N' x))) %.
%term _ expand⁺ ⊥ ([z value ⊥] N z) ⊥L %.
%term _
  %pi (expand⁺ (A⁺ ∨ B⁺) ([z value (A⁺ ∨ B⁺)] N z) (∨L N₁ N₂))
  %<- (expand⁺ A⁺ ([z₁ value A⁺] N (∨R₁ z₁)) (%the (term (A⁺ , _Ω) U) N₁))
  %<- (expand⁺ B⁺ ([z₂ value B⁺] N (∨R₂ z₂)) (%the (term (B⁺ , _Ω) U) N₂)) %.
%term _ expand⁺ ⊤⁺ ([z value ⊤⁺] N z) (⊤⁺L (N ⊤⁺R)) %.
%term _
  %pi (expand⁺ (A⁺ ∧⁺ B⁺) ([z value (A⁺ ∧⁺ B⁺)] N z) (∧⁺L N₂))
  %<- ({z₁ value A⁺} expand⁺ B⁺ ([z₂ value B⁺] N (∧⁺R z₁ z₂)) (%the (term (B⁺ , _Ω) U) (N₁ z₁)))
  %<- (expand⁺ A⁺ ([z₁ value A⁺] N₁ z₁) (%the (term (A⁺ , B⁺ , _Ω) U) N₂)) %.

η(s.N) = N'

%term _ expand⁻ (c Q⁻) N (η⁻ N) %.
%term _
  %pi (expand⁻ (↑ A⁺) N (↑R N''))
  %<- (expand⁺ A⁺ ([z value A⁺] focR z) (%the (term (A⁺ , ·) (A⁺ true)) N'))
  %<- (subst⁻ sp N (↑L sp N') (%the (term · (A⁺ true)) N'')) %.
%term _
  %pi (expand⁻ (A⁺ ⊃ B⁻) N (⊃R N₃))
  %<- ({z value A⁺} subst⁻ sn N (⊃L z id⁻) (%the (term · (B⁻ susp)) (N₁ z)))
  %<- ({z value A⁺} expand⁻ B⁻ (N₁ z) (%the (term · (B⁻ inv)) (N₂ z)))
  %<- (expand⁺ A⁺ N₂ (%the (term (A⁺ , ·) (B⁻ inv)) N₃)) %.
%term _ expand⁻ ⊤⁻ N ⊤⁻R %.
%term _
  %pi (expand⁻ (A⁻ ∧⁻ B⁻) N (∧⁻R N₁' N₂'))
  %<- (subst⁻ sn N (∧⁻L₁ id⁻) (%the (term · (A⁻ susp)) N₁))
  %<- (expand⁻ A⁻ N₁ (%the (term · (A⁻ inv)) N₁'))
  %<- (subst⁻ sn N (∧⁻L₂ id⁻) (%the (term · (B⁻ susp)) N₂))
  %<- (expand⁻ B⁻ N₂ (%the (term · (B⁻ inv)) N₂')) %.
%worlds (gamma) (expand⁺ _ _ _) (expand⁻ _ _ _) %.
%total (A⁺ A⁻) (expand⁺ A⁺ _ _) (expand⁻ A⁻ _ _) %.

Identity is a corollary, though we’ll only use it at the very end when we prove the identity principle for the unfocused sequent calculus:

%sort identity⁻ {_ %pi (hyp A⁻) %-> (term · (A⁻ inv))} %.
%mode {%in A⁻} {%out N %pi (hyp A⁻) %-> (term · (A⁻ inv))} identity⁻ N %.
%term _
  %pi (identity⁻ N)
  %<- ({x hyp A⁻} expand⁻ A⁻ (focL sn x id⁻) (%the (term · (A⁻ inv)) (N x))) %.
%worlds (gamma) (identity⁻ _) %.
%total [] (identity⁻ _) %.
%sort identity⁺ {_ term (A⁺ , ·) (A⁺ true)} %.
%mode {%in A⁺} {%out N term (A⁺ , ·) (A⁺ true)} identity⁺ N %.
%term _
  %pi (identity⁺ N)
  %<- (expand⁺ A⁺ ([z value A⁺] focR z) (%the (term (A⁺ , ·) (A⁺ true)) N)) %.
%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; while the proofs are hardly straightforward, they share a certain high-level structure.

Initial rules

%sort adm-initsusp⁻ {_ %pi (hyp (c Q)) %-> (term · (c Q susp))} %.
%mode {%in Q} {%out N %pi (hyp (c Q)) %-> (term · (c Q susp))} adm-initsusp⁻ N %.
%term _ adm-initsusp⁻ ([x hyp (c Q)] focL sn x id⁻) %.
%worlds (gamma_suspnormal) (adm-initsusp⁻ _) %.
%total [] (adm-initsusp⁻ _) %.
%sort adm-init⁻ {_ %pi (hyp (c Q)) %-> (term · (↓ (c Q) true))} %.
%mode {%in Q} {%out N %pi (hyp (c Q)) %-> (term · (↓ (c Q) true))} adm-init⁻ N %.
%term _ adm-init⁻ ([x hyp (c Q)] focR (↓R (η⁻ (focL sn x id⁻)))) %.
%worlds (gamma_suspnormal) (adm-init⁻ _) %.
%total [] (adm-init⁻ _) %.
%sort adm-initsusp⁺ {_ %pi (value (c Q)) %-> (term · (c Q true))} %.
%mode {%in Q} {%out N %pi (value (c Q)) %-> (term · (c Q true))} adm-initsusp⁺ N %.
%term _ adm-initsusp⁺ ([z value (c Q)] focR z) %.
%worlds (gamma_suspnormal) (adm-initsusp⁺ _) %.
%total [] (adm-initsusp⁺ _) %.
%sort adm-init⁺ {_ %pi (hyp (↑ (c Q))) %-> (term · (c Q true))} %.
%mode {%in Q} {%out N %pi (hyp (↑ (c Q))) %-> (term · (c Q true))} adm-init⁺ N %.
%term _ adm-init⁺ ([x hyp (↑ (c Q))] focL sp x (↑L sp (η⁺ ([z] focR z)))) %.
%worlds (gamma_suspnormal) (adm-init⁺ _) %.
%total [] (adm-init⁺ _) %.

Disjunction

%sort adm-⊥L {_ stable U} {_ %pi (hyp (↑ ⊥)) %-> (term · U)} %.
%mode adm-⊥L %in %out %.
%term _ adm-⊥L Pf ([x hyp (↑ ⊥)] focL Pf x (↑L Pf ⊥L)) %.
%worlds (gamma_suspnormal) (adm-⊥L _ _) %.
%total [] (adm-⊥L _ _) %.
%sort adm-∨R₁ {_ term · (A⁺ true)} {_ term · (A⁺ ∨ B⁺ true)} %.
%mode {%in A⁺} {%in B⁺} {%in N₁} {%out N' term · (A⁺ ∨ B⁺ true)} adm-∨R₁ N₁ N' %.
%term _
  %pi (adm-∨R₁ (%the (term · (A⁺ true)) N₁) N')
  %<- (expand⁺ A⁺ ([z value A⁺] focR (∨R₁ z)) (%the (term (A⁺ , ·) (A⁺ ∨ B⁺ true)) NId₁))
  %<- (lsubst A⁺ (b s) (ss sp snp) N₁ NId₁ (%the (term · (A⁺ ∨ B⁺ true)) N')) %.
%worlds (gamma_suspnormal) (adm-∨R₁ _ _) %.
%total [] (adm-∨R₁ _ _) %.
%sort adm-∨R₂ {_ term · (B⁺ true)} {_ term · (A⁺ ∨ B⁺ true)} %.
%mode {%in A⁺} {%in B⁺} {%in N₂} {%out N' term · (A⁺ ∨ B⁺ true)} adm-∨R₂ N₂ N' %.
%term _
  %pi (adm-∨R₂ (%the (term · (B⁺ true)) N₂) N')
  %<- (expand⁺ B⁺ ([z value B⁺] focR (∨R₂ z)) (%the (term (B⁺ , ·) (A⁺ ∨ B⁺ true)) NId₂))
  %<- (lsubst B⁺ (b s) (ss sp snp) N₂ NId₂ (%the (term · (A⁺ ∨ B⁺ true)) N')) %.
%worlds (gamma_suspnormal) (adm-∨R₂ _ _) %.
%total [] (adm-∨R₂ _ _) %.
%sort adm-∨L {_ suspstable U} {_ %pi (hyp (↑ A⁺)) %-> (term · U)} {_ %pi (hyp (↑ B⁺)) %-> (term · U)} {_ %pi (hyp (↑ (A⁺ ∨ B⁺))) %-> (term · U)} %.
%mode adm-∨L %in %in %in %out %.
%term _
  %pi (adm-∨L (ss Pf Pf') (%the (%pi (hyp (↑ A⁺)) %-> (term · U)) N₁) (%the (%pi (hyp (↑ B⁺)) %-> (term · U)) N₂) ([x hyp (↑ (A⁺ ∨ B⁺))] focL Pf x (↑L Pf N')))
  %<- (expand⁺ A⁺ ([z₁ value A⁺] focR (∨R₁ (↓R (↑R (focR z₁))))) (%the (term (A⁺ , ·) (↓ (↑ A⁺) ∨ ↓ (↑ B⁺) true)) NId₁))
  %<- (expand⁺ B⁺ ([z₂ value B⁺] focR (∨R₂ (↓R (↑R (focR z₂))))) (%the (term (B⁺ , ·) (↓ (↑ A⁺) ∨ ↓ (↑ B⁺) true)) NId₂))
  %<- (lsubst (↓ (↑ A⁺) ∨ ↓ (↑ B⁺)) (b s) (ss Pf Pf') (∨L NId₁ NId₂) (∨L (↓L N₁) (↓L N₂)) (%the (term (A⁺ ∨ B⁺ , ·) U) N')) %.
%worlds (gamma_suspnormal) (adm-∨L _ _ _ _) %.
%total [] (adm-∨L _ _ _ _) %.

Positive conjunction

%sort adm-⊤⁺R {_ term · (⊤⁺ true)} %.
%mode adm-⊤⁺R %out %.
%term _ adm-⊤⁺R (focR ⊤⁺R) %.
%worlds (gamma_suspnormal) (adm-⊤⁺R _) %.
%total [] (adm-⊤⁺R _) %.
%sort adm-⊤⁺L {_ stable U} {_ term · U} {_ %pi (hyp (↑ ⊤⁺)) %-> (term · U)} %.
%mode adm-⊤⁺L %in %in %out %.
%term _ adm-⊤⁺L Pf N₁ ([x hyp (↑ ⊤⁺)] focL Pf x (↑L Pf (⊤⁺L N₁))) %.
%worlds (gamma_suspnormal) (adm-⊤⁺L _ _ _) %.
%total [] (adm-⊤⁺L _ _ _) %.
%sort adm-∧⁺R {_ term · (A⁺ true)} {_ term · (B⁺ true)} {_ term · (A⁺ ∧⁺ B⁺ true)} %.
%mode adm-∧⁺R %in %in %out %.
%term _
  %pi (adm-∧⁺R (%the (term · (A⁺ true)) N₁) (%the (term · (B⁺ true)) N₂) N')
  %<- ({v₂ value B⁺} expand⁺ A⁺ ([v₁ value A⁺] focR (∧⁺R v₁ v₂)) (%the (term (A⁺ , ·) (A⁺ ∧⁺ B⁺ true)) (NIdB v₂)))
  %<- ({x hyp (↑ A⁺)} expand⁺ B⁺ ([z₂ value B⁺] focL sp x (↑L sp (NIdB z₂))) (%the (term (B⁺ , ·) (A⁺ ∧⁺ B⁺ true)) (NId x)))
  %<- ({x hyp (↑ A⁺)} lsubst B⁺ (b s) (ss sp snp) N₂ (NId x) (%the (term · (A⁺ ∧⁺ B⁺ true)) (NA x)))
  %<- (rsubst (↑ A⁺) (b s) (snl snp) (↑R N₁) ([x hyp (↑ A⁺)] NA x) N') %.
%worlds (gamma_suspnormal) (adm-∧⁺R _ _ _) %.
%total [] (adm-∧⁺R _ _ _) %.
%sort adm-∧⁺L {_ suspstable U} {_ %pi (hyp (↑ A⁺)) %-> (hyp (↑ B⁺)) %-> (term · U)} {_ %pi (hyp (↑ (A⁺ ∧⁺ B⁺))) %-> (term · U)} %.
%mode adm-∧⁺L %in %in %out %.
%term _
  %pi (adm-∧⁺L (ss Pf Pf') (%the (%pi (hyp (↑ A⁺)) %-> (hyp (↑ B⁺)) %-> (term · U)) N₁) ([x hyp (↑ (A⁺ ∧⁺ B⁺))] focL Pf x (↑L Pf N')))
  %<- ({z₁ value A⁺} expand⁺ B⁺ ([z₂ value B⁺] focR (∧⁺R (↓R (↑R (focR z₁))) (↓R (↑R (focR z₂))))) (%the (term (B⁺ , ·) (↓ (↑ A⁺) ∧⁺ ↓ (↑ B⁺) true)) (NIdA z₁)))
  %<- (expand⁺ A⁺ ([z₁ value A⁺] NIdA z₁) (%the (term (A⁺ , B⁺ , ·) (↓ (↑ A⁺) ∧⁺ ↓ (↑ B⁺) true)) NId))
  %<- (lsubst (↓ (↑ A⁺) ∧⁺ ↓ (↑ B⁺)) (b s) (ss Pf Pf') (∧⁺L NId) (∧⁺L (↓L ([x₁ hyp (↑ A⁺)] ↓L ([x₂ hyp (↑ B⁺)] N₁ x₁ x₂)))) (%the (term (A⁺ ∧⁺ B⁺ , ·) U) N')) %.
%worlds (gamma_suspnormal) (adm-∧⁺L _ _ _) %.
%total [] (adm-∧⁺L _ _ _) %.

Implication

%sort adm-⊃R {_ %pi (hyp (↑ A⁺)) %-> (term · (↓ B⁻ true))} {_ term · (↓ (A⁺ ⊃ B⁻) true)} %.
%mode adm-⊃R %in %out %.
%term _
  %pi (adm-⊃R (%the (%pi (hyp (↑ A⁺)) %-> (term · (↓ B⁻ true))) N₁) (focR (↓R N')))
  %<- ({x hyp (↓ (↑ A⁺) ⊃ ↑ (↓ B⁻))} {z value A⁺} expand⁻ B⁻ (focL sn x (⊃L (↓R (↑R (focR z))) (↑L sn (↓L ([x' hyp B⁻] focL sn x' id⁻))))) (%the (term · (B⁻ inv)) (NIdA x z)))
  %<- ({x hyp (↓ (↑ A⁺) ⊃ ↑ (↓ B⁻))} expand⁺ A⁺ ([z value A⁺] NIdA x z) (%the (term (A⁺ , ·) (B⁻ inv)) (NId x)))
  %<- (rsubst (↓ (↑ A⁺) ⊃ ↑ (↓ B⁻)) (b s) (snl snn) (⊃R (↓L ([x₁ hyp (↑ A⁺)] ↑R (N₁ x₁)))) ([x hyp (↓ (↑ A⁺) ⊃ ↑ (↓ B⁻))] ⊃R (NId x)) (%the (term · (A⁺ ⊃ B⁻ inv)) N')) %.
%worlds (gamma_suspnormal) (adm-⊃R _ _) %.
%total [] (adm-⊃R _ _) %.
%sort adm-⊃L {_ suspstable U} {_ term · (A⁺ true)} {_ %pi (hyp B⁻) %-> (term · U)} {_ %pi (hyp (A⁺ ⊃ B⁻)) %-> (term · U)} %.
%mode adm-⊃L %in %in %in %out %.
%term _
  %pi (adm-⊃L (ss Pf Pf') (%the (term · (A⁺ true)) N₁) (%the (%pi (hyp B⁻) %-> (term · U)) N₂) N')
  %<- ({x hyp (A⁺ ⊃ B⁻)} {z value A⁺} expand⁻ B⁻ (focL sn x (⊃L z id⁻)) (%the (term · (B⁻ inv)) (NIdB x z)))
  %<- ({x hyp (A⁺ ⊃ B⁻)} expand⁺ A⁺ ([z value A⁺] focR (↓R (NIdB x z))) (%the (term (A⁺ , ·) (↓ B⁻ true)) (NId x)))
  %<- ({x hyp (A⁺ ⊃ B⁻)} lsubst A⁺ (b s) (ss sp snp) N₁ (NId x) (%the (term · (↓ B⁻ true)) (NB x)))
  %<- ({x hyp (A⁺ ⊃ B⁻)} lsubst (↓ B⁻) (b s) (ss Pf Pf') (NB x) (↓L ([x₂ hyp B⁻] N₂ x₂)) (%the (term · U) (N' x))) %.
%worlds (gamma_suspnormal) (adm-⊃L _ _ _ _) %.
%total [] (adm-⊃L _ _ _ _) %.

Negative conjunction

%sort adm-⊤⁻R {_ term · (↓ ⊤⁻ true)} %.
%mode adm-⊤⁻R %out %.
%term _ adm-⊤⁻R (focR (↓R ⊤⁻R)) %.
%worlds (gamma_suspnormal) (adm-⊤⁻R _) %.
%total [] (adm-⊤⁻R _) %.
%sort adm-∧⁻R {_ term · (↓ A⁻ true)} {_ term · (↓ B⁻ true)} {_ term · (↓ (A⁻ ∧⁻ B⁻) true)} %.
%mode adm-∧⁻R %in %in %out %.
%term _
  %pi (adm-∧⁻R N₁ N₂ (focR (↓R N')))
  %<- ({x hyp (↑ (↓ A⁻) ∧⁻ ↑ (↓ B⁻))} expand⁻ A⁻ (focL sn x (∧⁻L₁ (↑L sn (↓L ([y] focL sn y id⁻))))) (%the (term · (A⁻ inv)) (NId₁ x)))
  %<- ({x hyp (↑ (↓ A⁻) ∧⁻ ↑ (↓ B⁻))} expand⁻ B⁻ (focL sn x (∧⁻L₂ (↑L sn (↓L ([y] focL sn y id⁻))))) (%the (term · (B⁻ inv)) (NId₂ x)))
  %<- (rsubst (↑ (↓ A⁻) ∧⁻ ↑ (↓ B⁻)) (b s) (snl snn) (∧⁻R (↑R N₁) (↑R N₂)) ([x hyp (↑ (↓ A⁻) ∧⁻ ↑ (↓ B⁻))] ∧⁻R (NId₁ x) (NId₂ x)) (%the (term · (A⁻ ∧⁻ B⁻ inv)) N')) %.
%worlds (gamma_suspnormal) (adm-∧⁻R _ _ _) %.
%total [] (adm-∧⁻R _ _ _) %.
%sort adm-∧⁻L₁ {_ suspnormal U} {_ %pi (hyp A⁻) %-> (term · U)} {_ %pi (hyp (A⁻ ∧⁻ B⁻)) %-> (term · U)} %.
%mode {%in A⁻} {%in B⁻} {%in U} {%in Pf} {%in N₁} {%out N' %pi (hyp (A⁻ ∧⁻ B⁻)) %-> (term · U)} adm-∧⁻L₁ Pf N₁ N' %.
%term _
  %pi (adm-∧⁻L₁ Pf (%the (%pi (hyp A⁻) %-> (term · U)) N₁) N')
  %<- ({x hyp (A⁻ ∧⁻ B⁻)} expand⁻ A⁻ (focL sn x (∧⁻L₁ id⁻)) (%the (term · (A⁻ inv)) (NId x)))
  %<- ({x hyp (A⁻ ∧⁻ B⁻)} rsubst A⁻ (b s) (snl Pf) (NId x) N₁ (%the (term · U) (N' x))) %.
%worlds (gamma_suspnormal) (adm-∧⁻L₁ _ _ _) %.
%total [] (adm-∧⁻L₁ _ _ _) %.
%sort adm-∧⁻L₂ {_ suspnormal U} {_ %pi (hyp B⁻) %-> (term · U)} {_ %pi (hyp (A⁻ ∧⁻ B⁻)) %-> (term · U)} %.
%mode {%in A⁻} {%in B⁻} {%in U} {%in Pf} {%in N₂} {%out N' %pi (hyp (A⁻ ∧⁻ B⁻)) %-> (term · U)} adm-∧⁻L₂ Pf N₂ N' %.
%term _
  %pi (adm-∧⁻L₂ Pf (%the (%pi (hyp B⁻) %-> (term · U)) N₂) N')
  %<- ({x hyp (A⁻ ∧⁻ B⁻)} expand⁻ B⁻ (focL sn x (∧⁻L₂ id⁻)) (%the (term · (B⁻ inv)) (NId x)))
  %<- ({x hyp (A⁻ ∧⁻ B⁻)} rsubst B⁻ (b s) (snl Pf) (NId x) N₂ (%the (term · U) (N' x))) %.
%worlds (gamma_suspnormal) (adm-∧⁻L₂ _ _ _) %.
%total [] (adm-∧⁻L₂ _ _ _) %.

Unfocused system

Syntax

%sort prop %.
%name prop %.
%term a %pi (atom P) %-> prop %.
%term ff prop %.
%term or %pi prop %-> prop %-> prop %.
%term tt prop %.
%term and %pi prop %-> prop %-> prop %.
%term imp %pi prop %-> prop %-> prop %.
%sort props %.
%name props %.
%term ○ props %.
%term ; %pi prop %-> props %-> props %.
%prec %right 3 ; %.

Erasure

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.

%sort t {_ typ P} {_ prop} %.
%name t %.
%term tQ t (c Q) (a Q) %.
%term t↑ %pi (t A⁺ P) %-> (t (↑ A⁺) P) %.
%term t⊥ t ⊥ ff %.
%term t∨ %pi (t A⁺ P₁) %-> (t B⁺ P₂) %-> (t (A⁺ ∨ B⁺) (or P₁ P₂)) %.
%term t⊤⁺ t ⊤⁺ tt %.
%term t∧⁺ %pi (t A⁺ P₁) %-> (t B⁺ P₂) %-> (t (A⁺ ∧⁺ B⁺) (and P₁ P₂)) %.
%term t↓ %pi (t A⁻ P) %-> (t (↓ A⁻) P) %.
%term t⊃ %pi (t A⁺ P₁) %-> (t B⁻ P₂) %-> (t (A⁺ ⊃ B⁻) (imp P₁ P₂)) %.
%term t⊤⁻ t ⊤⁻ tt %.
%term t∧⁻ %pi (t A⁻ P₁) %-> (t B⁻ P₂) %-> (t (A⁻ ∧⁻ B⁻) (and P₁ P₂)) %.
%mode t %in %out %.
%worlds (atom⁺ atom⁻) (t _ _) %.
%total A (t A _) %.
%sort tΩ {_ pos} {_ props} %.
%name tΩ %.
%term t· tΩ · ○ %.
%term t, %pi (t A⁺ P) %-> (tΩ _Ω _Ψ) %-> (tΩ (A⁺ , _Ω) (P ; _Ψ)) %.
%mode tΩ %in %out %.
%worlds (gamma) (tΩ _ _) %.
%total _Ω (tΩ _Ω _) %.
%sort tU {_ suc} {_ prop} %.
%name tU %.
%term tp %pi (tU (A⁺ true) P) %<- (t A⁺ P) %.
%term tn %pi (tU (A⁻ inv) P) %<- (t A⁻ P) %.
%term ta tU (c Q⁻ susp) (a Q⁻) %.
%sort tseq {_ seqform} {_ props} {_ prop} %.
%term tV %pi (tseq (rfoc A⁺) ○ P) %<- (t A⁺ P) %.
%term tN %pi (tseq (hasleft (ininv _Ω) U) _Ψ Q) %<- (tU U Q) %<- (tΩ _Ω _Ψ) %.
%term tS %pi (tseq (hasleft (infoc A⁻) U) (P ; ○) Q) %<- (tU U Q) %<- (t A⁻ P) %.

Shift removal

There may be a more elegant way to do this, but the last missing piece of our unfocused admissibility lemma - the last thing we need to know about the polarized calculus - is that if we need to prove (or use) a deeply-shifted proposition, then it suffices to prove (or use) a non-deeply-shifted proposition that erases to the same thing.

%sort not-doubleshifted {_ typ Pol} %.
%term ndQ not-doubleshifted (c Q) %.
%term ndQ⁺ not-doubleshifted (↓ (c Q)) %.
%term ndQ⁻ not-doubleshifted (↑ (c Q)) %.
%term nd⊥⁺ not-doubleshifted ⊥ %.
%term nd⊥⁻ not-doubleshifted (↑ ⊥) %.
%term nd∨⁺ not-doubleshifted (A⁺ ∨ B⁺) %.
%term nd∨⁻ not-doubleshifted (↑ (A⁺ ∨ B⁺)) %.
%term nd⊤⁺⁺ not-doubleshifted ⊤⁺ %.
%term nd⊤⁺⁻ not-doubleshifted (↑ ⊤⁺) %.
%term nd∧⁺⁺ not-doubleshifted (A⁺ ∧⁺ B⁺) %.
%term nd∧⁺⁻ not-doubleshifted (↑ (A⁺ ∧⁺ B⁺)) %.
%term nd⊃⁺ not-doubleshifted (↓ (A⁺ ⊃ B⁻)) %.
%term nd⊃⁻ not-doubleshifted (A⁺ ⊃ B⁻) %.
%term nd⊤⁻⁺ not-doubleshifted (↓ ⊤⁻) %.
%term nd⊤⁻⁻ not-doubleshifted ⊤⁻ %.
%term nd∧⁻⁺ not-doubleshifted (↓ (A⁻ ∧⁻ B⁻)) %.
%term nd∧⁻⁻ not-doubleshifted (A⁻ ∧⁻ B⁻) %.
%sort rshifty {_ t A P} {_ t A' P} {_ not-doubleshifted A'} {_ %pi (term · (A' true)) %-> (term · (A true))} %.
%mode rshifty %in %out %out %out %.
%term _
  %pi (rshifty (t↓ (t↑ T)) T' ND ([n] focR (↓R (↑R (N n)))))
  %<- (rshifty T T' ND N) %.
%term _ rshifty tQ tQ ndQ ([n] n) %.
%term _ rshifty t⊥ t⊥ nd⊥⁺ ([n] n) %.
%term _ rshifty (t∨ T₁ T₂) (t∨ T₁ T₂) nd∨⁺ ([n] n) %.
%term _ rshifty t⊤⁺ t⊤⁺ nd⊤⁺⁺ ([n] n) %.
%term _ rshifty (t∧⁺ T₁ T₂) (t∧⁺ T₁ T₂) nd∧⁺⁺ ([n] n) %.
%term _ rshifty (t↓ tQ) (t↓ tQ) ndQ⁺ ([n] n) %.
%term _ rshifty (t↓ (t⊃ T₁ T₂)) (t↓ (t⊃ T₁ T₂)) nd⊃⁺ ([n] n) %.
%term _ rshifty (t↓ t⊤⁻) (t↓ t⊤⁻) nd⊤⁻⁺ ([n] n) %.
%term _ rshifty (t↓ (t∧⁻ T₁ T₂)) (t↓ (t∧⁻ T₁ T₂)) nd∧⁻⁺ ([n] n) %.
%worlds (gamma_suspnormal) (rshifty _ _ _ _) %.
%total T (rshifty T _ _ _) %.
%sort lshifty {_ t A P} {_ t A' P} {_ not-doubleshifted A'} {_ {U} %pi (stable U) %-> (%pi (hyp A') %-> (term · U)) %-> (hyp A) %-> (term · U)} %.
%mode lshifty %in %out %out %out %.
%term _
  %pi (lshifty (t↑ (t↓ T)) T' ND ([u] [pf] [n] [x] focL pf x (↑L pf (↓L (N u pf n)))))
  %<- (lshifty T T' ND N) %.
%term _ lshifty (t↑ tQ) (t↑ tQ) ndQ⁻ ([u] [pf] [n] n) %.
%term _ lshifty (t↑ t⊥) (t↑ t⊥) nd⊥⁻ ([u] [pf] [n] n) %.
%term _ lshifty (t↑ (t∨ T₁ T₂)) (t↑ (t∨ T₁ T₂)) nd∨⁻ ([u] [pf] [n] n) %.
%term _ lshifty (t↑ t⊤⁺) (t↑ t⊤⁺) nd⊤⁺⁻ ([u] [pf] [n] n) %.
%term _ lshifty (t↑ (t∧⁺ T₁ T₂)) (t↑ (t∧⁺ T₁ T₂)) nd∧⁺⁻ ([u] [pf] [n] n) %.
%term _ lshifty tQ tQ ndQ ([u] [pf] [n] n) %.
%term _ lshifty (t⊃ T₁ T₂) (t⊃ T₁ T₂) nd⊃⁻ ([u] [pf] [n] n) %.
%term _ lshifty t⊤⁻ t⊤⁻ nd⊤⁻⁻ ([u] [pf] [n] n) %.
%term _ lshifty (t∧⁻ T₁ T₂) (t∧⁻ T₁ T₂) nd∧⁻⁻ ([u] [pf] [n] n) %.
%worlds (gamma_suspnormal) (lshifty _ _ _ _) %.
%total T (lshifty T _ _ _) %.

Sequent rules

%sort left {_ prop} %.
%name left %.
%sort right {_ prop} %.
%name right %.
%sort right' {_ props} {_ prop} %.
%name right' %.
%block h [P] {h left P}%.
%term init %pi (left (a Q)) %-> (right (a Q)) %.
%term ffL %pi (left ff) %-> (right P) %.
%term orR₁ %pi (right P₁) %-> (right (or P₁ P₂)) %.
%term orR₂ %pi (right P₂) %-> (right (or P₁ P₂)) %.
%term orL
  %pi (%pi (left P₁) %-> (right Q))
  %-> (%pi (left P₂) %-> (right Q))
  %-> (left (or P₁ P₂))
  %-> (right Q) %.
%term ttR right tt %.
%term andR %pi (right P₁) %-> (right P₂) %-> (right (and P₁ P₂)) %.
%term andL₁ %pi (%pi (left P₁) %-> (right Q)) %-> (left (and P₁ P₂)) %-> (right Q) %.
%term andL₂ %pi (%pi (left P₂) %-> (right Q)) %-> (left (and P₁ P₂)) %-> (right Q) %.
%term impR %pi (%pi (left P₁) %-> (right P₂)) %-> (right (imp P₁ P₂)) %.
%term impL
  %pi (right P₁)
  %-> (%pi (left P₂) %-> (right Q))
  %-> (left (imp P₁ P₂))
  %-> (right Q) %.
%term nil %pi (right P) %-> (right' ○ P) %.
%term cons %pi (%pi (left P) %-> (right' _Ψ Q)) %-> (right' (P ; _Ψ) Q) %.

Syntactic identity on derivations is used for completeness — it keeps the derivation size the same when we do case analysis.

%sort id {_ right P} {_ right P} %.
%term refl id D D %.

De-focalization (soundness)

Soundness is established in a context where each polarized hypothesis is mapped to its erasure.

%sort soundhyp {_ hyp A⁻} {_ t A⁻ P} {_ left P} %.
%block soundhyps [A⁻] [P] [T t A⁻ P] {x hyp A⁻} {h left P} {_ soundhyp x T h}%.
%sort soundsusp {_ value (c Q⁺)} {_ left (a Q⁺)} %.
%block soundsusps [Q⁺] {z value (c Q⁺)} {h left (a Q⁺)} {_ soundsusp z h}%.
%block soundctx%.
%mode {%in A⁻} {%out P} {%in X hyp A⁻} {%out T t A⁻ P} {%out H left P} soundhyp X T H %.
%worlds (soundctx) (soundhyp _ _ _) %.
%total [] (soundhyp _ _ _) %.
%mode {%in Q⁺} {%in Z value (c Q⁺)} {%out H left (a Q⁺)} soundsusp Z H %.
%worlds (soundctx) (soundsusp _ _) %.
%total [] (soundsusp _ _) %.
%sort sound {_ exp Form} {_ tseq Form _Ψ P} {_ right' _Ψ P} %.
%mode sound %in %in %out %.
%term _ %pi (sound (%the (value (c Q⁺)) Z) (tV tQ) (nil (init H))) %<- (soundsusp Z H) %.
%term _ %pi (sound (↓R N) (tV (t↓ T)) (nil D)) %<- (sound N (tN t· (tn T)) (nil D)) %.
%term _ %pi (sound (∨R₁ V) (tV (t∨ T₁ _)) (nil (orR₁ D))) %<- (sound V (tV T₁) (nil D)) %.
%term _ %pi (sound (∨R₂ V) (tV (t∨ _ T₂)) (nil (orR₂ D))) %<- (sound V (tV T₂) (nil D)) %.
%term _ sound ⊤⁺R (tV t⊤⁺) (nil ttR) %.
%term _
  %pi (sound (∧⁺R V₁ V₂) (tV (t∧⁺ T₁ T₂)) (nil (andR D₁ D₂)))
  %<- (sound V₁ (tV T₁) (nil D₁))
  %<- (sound V₂ (tV T₂) (nil D₂)) %.
%term _ %pi (sound (focR V) (tN t· (tp T)) D) %<- (sound V (tV T) D) %.
%term _
  %pi (sound (focL _ X Sp) (tN t· (%the (tU U Q) TCQ)) (nil (D H)))
  %<- (soundhyp X (%the (t A⁻ P) TAP) (%the (left P) H))
  %<- (sound Sp (tS TAP TCQ) (cons ([x left P] nil (%the (right Q) (D x))))) %.
%term _
  %pi (sound (η⁺ ([z value (c Q⁺)] N z)) (tN (t, tQ TΩ) TCQ) (cons D))
  %<- ({z value (c Q⁺)} {h left (a Q⁺)} %pi (soundsusp z h) %-> (sound (N z) (tN TΩ TCQ) (%the (right' _Ψ Q) (D h)))) %.
%term _
  %pi (sound (↓L ([x hyp A⁻] N x)) (tN (t, (t↓ T) TΩ) TCQ) (cons D))
  %<- ({x hyp A⁻} {h left P} %pi (soundhyp x T h) %-> (sound (N x) (tN TΩ TCQ) (%the (right' _Ψ Q) (D h)))) %.
%sort sound-ffL {_Ψ} {_ left ff} {_ right' _Ψ Q} %.
%term _ sound-ffL _ H (nil (ffL H)) %.
%term _ %pi (sound-ffL _ H (cons D)) %<- ({h} sound-ffL _ H (D h)) %.
%mode {%in _Ψ} {%in Q} {%in H left ff} {%out D right' _Ψ Q} sound-ffL _Ψ H D %.
%worlds (atom⁺ atom⁻ h) (sound-ffL _ _ _) %.
%total _Ψ (sound-ffL _Ψ _ _) %.
%term _ %pi (sound ⊥L (tN TΩ TCQ) (cons D)) %<- ({h left ff} sound-ffL _ h (D h)) %.
%sort sound-orL {_Ψ} {_ left (or P₁ P₂)} {_ %pi (left P₁) %-> (right' _Ψ Q)} {_ %pi (left P₂) %-> (right' _Ψ Q)} {_ right' _Ψ Q} %.
%term _ sound-orL _ H ([h₁] nil (D₁ h₁)) ([h₂] nil (D₂ h₂)) (nil (orL D₁ D₂ H)) %.
%term _
  %pi (sound-orL _ H ([h₁] cons (D₁ h₁)) ([h₂] cons (D₂ h₂)) (cons D))
  %<- ({h} sound-orL _ H ([h₁] D₁ h₁ h) ([h₂] D₂ h₂ h) (D h)) %.
%mode sound-orL %in %in %in %in %out %.
%worlds (atom⁺ atom⁻ h) (sound-orL _ _ _ _ _) %.
%total _Ψ (sound-orL _Ψ _ _ _ _) %.
%term _
  %pi (sound (∨L N₁ N₂) (tN (t, (t∨ T₁ T₂) TΩ) TCQ) (cons D))
  %<- (sound N₁ (tN (t, T₁ TΩ) TCQ) (cons (%the (%pi (left P₁) %-> (right' _Ψ Q)) D₁)))
  %<- (sound N₂ (tN (t, T₂ TΩ) TCQ) (cons (%the (%pi (left P₂) %-> (right' _Ψ Q)) D₂)))
  %<- ({h left (or P₁ P₂)} sound-orL _ h D₁ D₂ (D h)) %.
%term _
  %pi (sound (⊤⁺L N) (tN (t, t⊤⁺ TΩ) TCQ) (cons ([h left tt] D)))
  %<- (sound N (tN TΩ TCQ) (%the (right' _Ψ Q) D)) %.
%sort sound-andL {_Ψ} {_ left (and P₁ P₂)} {_ %pi (left P₁) %-> (left P₂) %-> (right' _Ψ Q)} {_ right' _Ψ Q} %.
%term _ sound-andL _ H ([h₁] [h₂] nil (D₁ h₁ h₂)) (nil (andL₁ ([h₁] andL₂ ([h₂] D₁ h₁ h₂) H) H)) %.
%term _
  %pi (sound-andL _ H ([h₁] [h₂] cons (D₁ h₁ h₂)) (cons D))
  %<- ({h} sound-andL _ H ([h₁] [h₂] D₁ h₁ h₂ h) (D h)) %.
%mode sound-andL %in %in %in %out %.
%worlds (atom⁺ atom⁻ h) (sound-andL _ _ _ _) %.
%total _Ψ (sound-andL _Ψ _ _ _) %.
%term _
  %pi (sound (∧⁺L N) (tN (t, (t∧⁺ T₁ T₂) TΩ) TCQ) (cons D))
  %<- (sound N (tN (t, T₁ (t, T₂ TΩ)) TCQ) (cons ([h₁] cons ([h₂] D₁ h₁ h₂))))
  %<- ({h left (and P₁ P₂)} sound-andL _ h D₁ (%the (right' _Ψ Q) (D h))) %.
%term _ %pi (sound (η⁻ N) (tN t· (tn tQ)) (nil D)) %<- (sound N (tN t· ta) (nil D)) %.
%term _
  %pi (sound (↑R N) (tN t· (tn (t↑ T))) (nil D))
  %<- (sound N (tN t· (tp T)) (nil D)) %.
%term _
  %pi (sound (⊃R N) (tN t· (tn (t⊃ T₁ T₂))) (nil (impR D)))
  %<- (sound N (tN (t, T₁ t·) (tn T₂)) (cons ([h left P₁] nil (%the (right P₂) (D h))))) %.
%term _ sound ⊤⁻R (tN t· (tn t⊤⁻)) (nil ttR) %.
%term _
  %pi (sound (∧⁻R N₁ N₂) (tN t· (tn (t∧⁻ T₁ T₂))) (nil (andR D₁ D₂)))
  %<- (sound N₁ (tN t· (tn T₁)) (nil D₁))
  %<- (sound N₂ (tN t· (tn T₂)) (nil D₂)) %.
%term _ sound id⁻ (tS tQ ta) (cons ([h] nil (init h))) %.
%term _
  %pi (sound (↑L _ N) (tS (t↑ T₁) TCQ) D)
  %<- (sound N (tN (t, T₁ t·) TCQ) (%the (right' (P ; ○) Q) D)) %.
%term _
  %pi (sound (⊃L V Sp) (tS (t⊃ T₁ T₂) TCQ) (cons ([h] nil (impL D₁ D₂ h))))
  %<- (sound V (tV T₁) (nil (%the (right P₁) D₁)))
  %<- (sound Sp (tS T₂ TCQ) (cons ([h left P₂] nil (%the (right Q) (D₂ h))))) %.
%term _
  %pi (sound (∧⁻L₁ Sp) (tS (t∧⁻ T₁ T₂) TCQ) (cons ([h left (and P₁ P₂)] nil (andL₁ D h))))
  %<- (sound Sp (tS T₁ TCQ) (cons ([h₁ left P₁] nil (%the (right Q) (D h₁))))) %.
%term _
  %pi (sound (∧⁻L₂ Sp) (tS (t∧⁻ T₁ T₂) TCQ) (cons ([h left (and P₁ P₂)] nil (andL₂ D h))))
  %<- (sound Sp (tS T₂ TCQ) (cons ([h₂ left P₂] nil (%the (right Q) (D h₂))))) %.
%worlds (soundctx) (sound _ _ _) %.
%total (E) (sound E _ _) %.

Focalization (completeness)

Completeness is established in a context where each erased hypothesis is mapped to some polarization. This is the almost same, type-wise, as the context for soundness, but the computational interpretation runs the opposite way ‘round.

%sort completehyp_res {_ typ Pol} %.
%term cn %pi (hyp A⁻) %-> (completehyp_res A⁻) %.
%term ca %pi (value (c Q⁺)) %-> (completehyp_res (c Q⁺)) %.
%sort completehyp {_ left P} {_ t A P} {_ completehyp_res A} %.
%block completehypn [A⁻ typ ⁻] [P] [T t A⁻ P] {x hyp A⁻} {h left P} {_ completehyp h T (cn x)}%.
%block completehypa [Q⁺ atom ⁺] [P] [T t (c Q⁺) P] {z value (c Q⁺)} {h left P} {_ completehyp h T (ca z)}%.
%block completectx%.
%sort transnormal {_ tU U P} {_ suspnormal U} %.
%mode transnormal %in %out %.
%term _ transnormal (tp _) snp %.
%term _ transnormal (tn _) snn %.
%term _ transnormal ta sna %.
%worlds (atom⁺ atom⁻) (transnormal _ _) %.
%total [] (transnormal _ _) %.
%mode completehyp %in %out %out %.
%worlds (completectx) (completehyp _ _ _) %.
%total [] (completehyp _ _ _) %.
%sort complete {_ stable U} {_ right P} {_ tU U P} {_ term · U} %.
%mode complete %in %in %in %out %.

Initial rules

%sort comp-init-susp {_ not-doubleshifted A'} {_ t A' (a Q)} {_ %pi (hyp A') %-> (term · (c Q susp))} %.
%term _ %pi (comp-init-susp _ tQ M) %<- (adm-initsusp⁻ M) %.
%mode comp-init-susp %in %in %out %.
%worlds (completectx) (comp-init-susp _ _ _) %.
%total [] (comp-init-susp _ _ _) %.
%term _
  %pi (complete Pf (init H) ta (NS _ sn M X))
  %<- (completehyp H (%the (t A (a Q)) TH) (cn (%the (hyp A) X)))
  %<- (lshifty TH (%the (t A' (a Q)) TH') (%the (not-doubleshifted A') ND) (%the ({U} %pi (stable U) %-> (%pi (hyp A') %-> (term · U)) %-> (hyp A) %-> (term · U)) NS))
  %<- (comp-init-susp ND TH' M) %.
%sort comp-init-case {_ not-doubleshifted Aleft'} {_ t Aleft' (a Q)} {_ not-doubleshifted Aright'} {_ t Aright' (a Q)} {_ %pi (hyp Aleft') %-> (term · (Aright' true))} %.
%mode comp-init-case %in %in %in %in %out %.
%term _ %pi (comp-init-case ndQ tQ ndQ⁺ (t↓ tQ) M) %<- (adm-init⁻ M) %.
%term _ %pi (comp-init-case ndQ⁻ (t↑ tQ) ndQ tQ M) %<- (adm-init⁺ M) %.
%worlds (completectx) (comp-init-case _ _ _ _ _) %.
%total [] (comp-init-case _ _ _ _ _) %.
%sort comp-init {_ t Aleft (a Q)} {_ completehyp_res Aleft} {_ not-doubleshifted Aright'} {_ t Aright' (a Q)} {_ term · (Aright' true)} %.
%term _ %pi (comp-init tQ (ca Z) ndQ tQ (M Z)) %<- (adm-initsusp⁺ M) %.
%term _
  %pi (comp-init TH (cn X) ND T' (NS _ sp M X))
  %<- (lshifty TH (%the (t Aleft' (a Q)) TH') (%the (not-doubleshifted Aleft') NDH) (%the ({U} %pi (stable U) %-> (%pi (hyp Aleft') %-> (term · U)) %-> (hyp Aleft) %-> (term · U)) NS))
  %<- (comp-init-case NDH TH' ND T' M) %.
%mode comp-init %in %in %in %in %out %.
%worlds (completectx) (comp-init _ _ _ _ _) %.
%total [] (comp-init _ _ _ _ _) %.
%term _
  %pi (complete Pf (init H) (tp (%the (t Aright (a Q)) T)) (NSright M))
  %<- (rshifty T (%the (t Aright' (a Q)) T') (%the (not-doubleshifted Aright') NDright) (%the (%pi (term · (Aright' true)) %-> (term · (Aright true))) NSright))
  %<- (completehyp H (%the (t Aleft (a Q)) TH) (%the (completehyp_res Aleft) HypRes))
  %<- (comp-init TH HypRes NDright T' M) %.

Disjunction

%sort comp-ffL {_ stable U} {_ not-doubleshifted A'} {_ t A' ff} {_ %pi (hyp A') %-> (term · U)} %.
%term _ %pi (comp-ffL Pf nd⊥⁻ (t↑ t⊥) M) %<- (adm-⊥L Pf M) %.
%mode comp-ffL %in %in %in %out %.
%worlds (completectx) (comp-ffL _ _ _ _) %.
%total [] (comp-ffL _ _ _ _) %.
%term _
  %pi (complete Pf (ffL H) T (NS _ Pf M X))
  %<- (completehyp H (%the (t A ff) TH) (cn (%the (hyp A) X)))
  %<- (lshifty TH (%the (t A' ff) TH') (%the (not-doubleshifted A') ND) (%the ({U} %pi (stable U) %-> (%pi (hyp A') %-> (term · U)) %-> (hyp A) %-> (term · U)) NS))
  %<- (comp-ffL Pf ND TH' M) %.
%sort comp-orR₁ {D right (or P₁ P₂)} {_ id D (orR₁ D₁)} {_ not-doubleshifted A'} {_ t A' (or P₁ P₂)} {_ term · (A' true)} %.
%mode comp-orR₁ %in %in %in %in %out %.
%term _
  %pi (comp-orR₁ (orR₁ D₁) refl nd∨⁺ (t∨ (%the (t A⁺ P₁) T₁) (%the (t B⁺ P₂) T₂)) M)
  %<- (complete sp D₁ (tp T₁) (%the (term · (A⁺ true)) N₁))
  %<- (adm-∨R₁ N₁ (%the (term · (A⁺ ∨ B⁺ true)) M)) %.
%term _
  %pi (complete Pf (orR₁ D₁) (tp T) (NS M))
  %<- (rshifty T (%the (t A' (or P₁ P₂)) T') (%the (not-doubleshifted A') ND) (%the (%pi (term · (A' true)) %-> (term · (A true))) NS))
  %<- (comp-orR₁ (orR₁ D₁) refl ND T' M) %.
%sort comp-orR₂ {D right (or P₁ P₂)} {_ id D (orR₂ D₂)} {_ not-doubleshifted A'} {_ t A' (or P₁ P₂)} {_ term · (A' true)} %.
%mode comp-orR₂ %in %in %in %in %out %.
%term _
  %pi (comp-orR₂ (orR₂ D₂) refl nd∨⁺ (t∨ (%the (t A⁺ P₁) T₁) (%the (t B⁺ P₂) T₂)) M)
  %<- (complete sp D₂ (tp T₂) (%the (term · (B⁺ true)) N₂))
  %<- (adm-∨R₂ N₂ (%the (term · (A⁺ ∨ B⁺ true)) M)) %.
%term _
  %pi (complete Pf (orR₂ D₂) (tp T) (NS M))
  %<- (rshifty T (%the (t A' (or P₁ P₂)) T') (%the (not-doubleshifted A') ND) (%the (%pi (term · (A' true)) %-> (term · (A true))) NS))
  %<- (comp-orR₂ (orR₂ D₂) refl ND T' M) %.
%sort comp-orL {_ stable U} {D right Q} {_ id D (orL D₁ D₂ (%the (left (or P₁ P₂)) H))} {_ not-doubleshifted A'} {_ t A' (or P₁ P₂)} {_ tU U Q} {_ %pi (hyp A') %-> (term · U)} %.
%mode comp-orL %in %in %in %in %in %in %out %.
%term _
  %pi (comp-orL Pf (orL D₁ D₂ H) refl nd∨⁻ (t↑ (t∨ T₁ T₂)) T M)
  %<- ({x₁ hyp (↑ B₁⁺)} {h₁ left P₁}
  %pi (completehyp h₁ (t↑ T₁) (cn x₁))
  %-> (complete Pf (D₁ h₁) T (%the (term · U) (N₁ x₁))))
  %<- ({x₂ hyp (↑ B₂⁺)} {h₂ left P₂}
  %pi (completehyp h₂ (t↑ T₂) (cn x₂))
  %-> (complete Pf (D₂ h₂) T (%the (term · U) (N₂ x₂))))
  %<- (transnormal T Pf')
  %<- (adm-∨L (ss Pf Pf') N₁ N₂ (%the (%pi (hyp (↑ (B₁⁺ ∨ B₂⁺))) %-> (term · U)) M)) %.
%term _
  %pi (complete Pf (orL D₁ D₂ H) (%the (tU U Q) T) (NS _ Pf M X))
  %<- (completehyp H (%the (t A (or P₁ P₂)) TH) (cn (%the (hyp A) X)))
  %<- (lshifty TH TH' ND NS)
  %<- (comp-orL Pf (orL D₁ D₂ H) refl ND TH' T M) %.

Conjunction

%sort comp-ttR {D right tt} {_ id D ttR} {_ not-doubleshifted A'} {_ t A' tt} {_ term · (A' true)} %.
%term _ %pi (comp-ttR ttR refl nd⊤⁺⁺ t⊤⁺ M) %<- (adm-⊤⁺R M) %.
%term _ %pi (comp-ttR ttR refl nd⊤⁻⁺ (t↓ t⊤⁻) M) %<- (adm-⊤⁻R M) %.
%mode comp-ttR %in %in %in %in %out %.
%worlds (completectx) (comp-ttR _ _ _ _ _) %.
%total [] (comp-ttR _ _ _ _ _) %.
%term _
  %pi (complete Pf ttR (tp T) (NS M))
  %<- (rshifty T (%the (t A' tt) T') (%the (not-doubleshifted A') ND) (%the (%pi (term · (A' true)) %-> (term · (A true))) NS))
  %<- (comp-ttR ttR refl ND T' M) %.
%sort comp-andR {D right (and P₁ P₂)} {_ id D (andR D₁ D₂)} {_ not-doubleshifted A'} {_ t A' (and P₁ P₂)} {_ term · (A' true)} %.
%mode comp-andR %in %in %in %in %out %.
%term _
  %pi (comp-andR (andR D₁ D₂) refl nd∧⁺⁺ (t∧⁺ (%the (t A⁺ P₁) T₁) (%the (t B⁺ P₂) T₂)) M)
  %<- (complete sp D₁ (tp T₁) (%the (term · (A⁺ true)) N₁))
  %<- (complete sp D₂ (tp T₂) (%the (term · (B⁺ true)) N₂))
  %<- (adm-∧⁺R N₁ N₂ M) %.
%term _
  %pi (comp-andR (andR D₁ D₂) refl nd∧⁻⁺ (t↓ (t∧⁻ (%the (t A⁻ P₁) T₁) (%the (t B⁻ P₂) T₂))) M)
  %<- (complete sp D₁ (tp (t↓ T₁)) (%the (term · (↓ A⁻ true)) N₁))
  %<- (complete sp D₂ (tp (t↓ T₂)) (%the (term · (↓ B⁻ true)) N₂))
  %<- (adm-∧⁻R N₁ N₂ M) %.
%term _
  %pi (complete Pf (andR D₁ D₂) (tp T) (NS M))
  %<- (rshifty T (%the (t A' (and P₁ P₂)) T') (%the (not-doubleshifted A') ND) (%the (%pi (term · (A' true)) %-> (term · (A true))) NS))
  %<- (comp-andR (andR D₁ D₂) refl ND T' M) %.
%sort comp-andL₁ {_ stable U} {D right Q} {_ id D (andL₁ D₁ (%the (left (and P₁ P₂)) H))} {_ not-doubleshifted A'} {_ t A' (and P₁ P₂)} {_ tU U Q} {_ %pi (hyp A') %-> (term · U)} %.
%mode comp-andL₁ %in %in %in %in %in %in %out %.
%term _
  %pi (comp-andL₁ Pf (andL₁ D₁ H) refl nd∧⁺⁻ (t↑ (t∧⁺ (%the (t A⁺ P₁) T₁) (%the (t B⁺ P₂) T₂))) T M)
  %<- ({x hyp (↑ A⁺)} {h left P₁}
  %pi (completehyp h (t↑ T₁) (cn x))
  %-> (complete Pf (D₁ h) T (%the (term · U) (N₁ x))))
  %<- (transnormal T Pf')
  %<- (adm-∧⁺L (ss Pf Pf') ([x] [y] N₁ x) M) %.
%term _
  %pi (comp-andL₁ Pf (andL₁ D₁ H) refl nd∧⁻⁻ (t∧⁻ (%the (t A⁻ P₁) T₁) (%the (t B⁻ P₂) T₂)) T M)
  %<- ({x hyp A⁻} {h left P₁} %pi (completehyp h T₁ (cn x)) %-> (complete Pf (D₁ h) T (%the (term · U) (N₁ x))))
  %<- (transnormal T Pf')
  %<- (adm-∧⁻L₁ Pf' N₁ M) %.
%term _
  %pi (complete Pf (andL₁ D₁ H) (%the (tU U Q) T) (NS _ Pf M X))
  %<- (completehyp H (%the (t A (and P₁ P₂)) TH) (cn (%the (hyp A) X)))
  %<- (lshifty TH TH' ND NS)
  %<- (comp-andL₁ Pf (andL₁ D₁ H) refl ND TH' T M) %.
%sort comp-andL₂ {_ stable U} {D right Q} {_ id D (andL₂ D₁ (%the (left (and P₁ P₂)) H))} {_ not-doubleshifted A'} {_ t A' (and P₁ P₂)} {_ tU U Q} {_ %pi (hyp A') %-> (term · U)} %.
%mode comp-andL₂ %in %in %in %in %in %in %out %.
%term _
  %pi (comp-andL₂ Pf (andL₂ D₂ H) refl nd∧⁺⁻ (t↑ (t∧⁺ (%the (t A⁺ P₁) T₁) (%the (t B⁺ P₂) T₂))) T M)
  %<- ({x hyp (↑ B⁺)} {h left P₂}
  %pi (completehyp h (t↑ T₂) (cn x))
  %-> (complete Pf (D₂ h) T (%the (term · U) (N₂ x))))
  %<- (transnormal T Pf')
  %<- (adm-∧⁺L (ss Pf Pf') ([x] [y] N₂ y) M) %.
%term _
  %pi (comp-andL₂ Pf (andL₂ D₂ H) refl nd∧⁻⁻ (t∧⁻ (%the (t A⁻ P₁) T₁) (%the (t B⁻ P₂) T₂)) T M)
  %<- ({x hyp B⁻} {h left P₂} %pi (completehyp h T₂ (cn x)) %-> (complete Pf (D₂ h) T (%the (term · U) (N₂ x))))
  %<- (transnormal T Pf')
  %<- (adm-∧⁻L₂ Pf' N₂ M) %.
%term _
  %pi (complete Pf (andL₂ D₂ H) (%the (tU U Q) T) (NS _ Pf M X))
  %<- (completehyp H (%the (t A (and P₁ P₂)) TH) (cn (%the (hyp A) X)))
  %<- (lshifty TH TH' ND NS)
  %<- (comp-andL₂ Pf (andL₂ D₂ H) refl ND TH' T M) %.

Implication

%sort comp-impR {D right (imp P₁ P₂)} {_ id D (impR D₁)} {_ not-doubleshifted A'} {_ t A' (imp P₁ P₂)} {_ term · (A' true)} %.
%mode comp-impR %in %in %in %in %out %.
%term _
  %pi (comp-impR (impR D₁) refl nd⊃⁺ (t↓ (t⊃ (%the (t A⁺ P₁) T₁) (%the (t B⁻ P₂) T₂))) M)
  %<- ({x hyp (↑ A⁺)} {h left P₁} %pi (completehyp h (t↑ T₁) (cn x)) %-> (complete sp (D₁ h) (tp (t↓ T₂)) (N₁ x)))
  %<- (adm-⊃R N₁ M) %.
%term _
  %pi (complete Pf (impR D₁) (tp T) (NS M))
  %<- (rshifty T (%the (t A' (imp P₁ P₂)) T') (%the (not-doubleshifted A') ND) (%the (%pi (term · (A' true)) %-> (term · (A true))) NS))
  %<- (comp-impR (impR D₁) refl ND T' M) %.
%sort comp-impL {_ stable U} {D right Q} {_ id D (impL D₁ D₂ (%the (left (imp P₁ P₂)) H))} {_ not-doubleshifted A'} {_ t A' (imp P₁ P₂)} {_ tU U Q} {_ %pi (hyp A') %-> (term · U)} %.
%mode comp-impL %in %in %in %in %in %in %out %.
%term _
  %pi (comp-impL Pf (impL D₁ D₂ _) refl nd⊃⁻ (t⊃ (%the (t A⁺ P₁) T₁) (%the (t B⁻ P₂) T₂)) T M)
  %<- (complete sp D₁ (tp T₁) (%the (term · (A⁺ true)) N₁))
  %<- ({x hyp B⁻} {h left P₂} %pi (completehyp h T₂ (cn x)) %-> (complete Pf (D₂ h) T (N₂ x)))
  %<- (transnormal T Pf')
  %<- (adm-⊃L (ss Pf Pf') N₁ N₂ M) %.
%term _
  %pi (complete Pf (impL D₁ D₂ H) T (NS _ Pf M X))
  %<- (completehyp H (%the (t A (imp P₁ P₂)) TH) (cn (%the (hyp A) X)))
  %<- (lshifty TH TH' ND NS)
  %<- (comp-impL Pf (impL D₁ D₂ H) refl ND TH' T M) %.
%worlds (completectx) (comp-orR₁ _ _ _ _ _) (comp-orR₂ _ _ _ _ _) (comp-orL _ _ _ _ _ _ _) (comp-andR _ _ _ _ _) (comp-andL₁ _ _ _ _ _ _ _) (comp-andL₂ _ _ _ _ _ _ _) (comp-impR _ _ _ _ _) (comp-impL _ _ _ _ _ _ _) (complete _ _ _ _) %.
%total (D D1 D2 D3 D4 D5 D6 D7 D8) (comp-orR₁ D1 _ _ _ _) (comp-orR₂ D2 _ _ _ _) (comp-orL _ D3 _ _ _ _ _) (comp-andR D4 _ _ _ _) (comp-andL₁ _ D5 _ _ _ _ _) (comp-andL₂ _ D6 _ _ _ _ _) (comp-impR D7 _ _ _ _) (comp-impL _ D8 _ _ _ _ _) (complete _ D _ _) %.

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 its results are reminiscent of Howe’s semi-focused lax logic.

%sort polarize {P} {_ t (%the (typ ⁻) A⁻) P} %.
%mode polarize %in %out %.
%term _ polarize (a Q) tQ %.
%term _ polarize (a Q) (t↑ tQ) %.
%term _ polarize ff (t↑ t⊥) %.
%term _
  %pi (polarize (or P₁ P₂) (t↑ (t∨ (t↓ T₁) (t↓ T₂))))
  %<- (polarize P₁ T₁)
  %<- (polarize P₂ T₂) %.
%term _ polarize tt t⊤⁻ %.
%term _ %pi (polarize (and P₁ P₂) (t∧⁻ T₁ T₂)) %<- (polarize P₁ T₁) %<- (polarize P₂ T₂) %.
%term _
  %pi (polarize (imp P₁ P₂) (t⊃ (t↓ T₁) T₂))
  %<- (polarize P₁ T₁)
  %<- (polarize P₂ T₂) %.
%worlds (atom⁺ atom⁻) (polarize _ _) %.
%total P (polarize P _) %.
%block translate [A] [P] [TH t A P] {x hyp A} {h left P} {_ soundhyp x TH h} {_ completehyp h TH (cn x)}%.
%sort unfocused-cut {_ right P} {_ %pi (left P) %-> (right Q)} {_ right Q} %.
%mode unfocused-cut %in %in %out %.
%term _
  %pi (unfocused-cut (%the (right P) D) (%the (%pi (left P) %-> (right Q)) E) F)
  %<- (polarize P (%the (t A⁻ P) TP))
  %<- (complete sp D (tp (t↓ TP)) (%the (term · (↓ A⁻ true)) M))
  %<- (polarize Q (%the (t C⁻ Q) TQ))
  %<- ({x hyp A⁻} {h left P}
  %pi (completehyp h TP (cn x))
  %-> (complete sp (E h) (tp (t↓ TQ)) (%the (term · (↓ C⁻ true)) (N x))))
  %<- (lsubst _ (b s) (ss sp snp) M (↓L N) N')
  %<- (sound N' (tN t· (tp (t↓ TQ))) (nil (%the (right Q) F))) %.
%worlds (translate) (unfocused-cut _ _ _) %.
%total [] (unfocused-cut _ _ _) %.
%sort unfocused-identity {_ %pi (left P) %-> (right P)} %.
%mode {%in P} {%out D %pi (left P) %-> (right P)} unfocused-identity D %.
%term _
  %pi (unfocused-identity D)
  %<- (polarize P (%the (t A⁻ P) TP))
  %<- (identity⁻ (%the (%pi (hyp A⁻) %-> (term · (A⁻ inv))) N))
  %<- ({x hyp A⁻} {h left P}
  %pi (soundhyp x TP h)
  %-> (sound (N x) (tN t· (tn TP)) (nil (%the (right P) (D h))))) %.
%worlds (translate) (unfocused-identity _) %.
%total [] (unfocused-identity _) %.

Running the theorems

Here are two unfocused derivations of (p ∧ q) ⊃ (r ∧ s) ⊃ (p ∧ t).

%define d₁ ({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 ([h₁ left (and (a p) (a q))] impR ([h₂ left (and (a r) (a s))] andR (andL₁ ([h₁' left (a p)] init h₁') h₁) (andL₁ ([h₂' left (a r)] init h₂') h₂))) %.
%define d₂ ({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 ([h₁ left (and (a p) (a q))] impR ([h₂ left (and (a r) (a s))] andL₁ ([h₁' left (a p)] andR (andL₂ ([_] andL₂ ([_] init h₁') h₁) h₁) (andL₁ ([h₂' left (a r)] init h₂') h₂)) h₁)) %.

Here are three different polarizations.

%solve t⁻ : {p} {q} {r} {s} t (↓ (c p ∧⁻ c q) ⊃ (↓ (c r ∧⁻ c s) ⊃ (c p ∧⁻ c r))) _ %.
%solve t⁺ : {p} {q} {r} {s} t (c p ∧⁺ c q ⊃ (c r ∧⁺ c s ⊃ ↑ (c p ∧⁺ c r))) _ %.
%solve t⁼ : {p} {q} {r} {s} t (↓ (↑ (c p) ∧⁻ ↑ (c q)) ⊃ ↑ (↓ (↓ (↑ (c r) ∧⁻ ↑ (c s)) ⊃ ↑ (↓ (↑ (c p) ∧⁻ ↑ (c r)))))) _ %.

Under the same “good” polarization, different derivations translate to a single unique proof.

%query 1 _ _ {p} {q} {r} {s} complete _ (d₁ ⁻ p q r s) (tp (t↓ (t⁻ p q r s))) (N p q r s) %.
%query 1 _ _ {p} {q} {r} {s} complete _ (d₂ ⁻ p q r s) (tp (t↓ (t⁻ p q r s))) (N p q r s) %.

Different polarizations may lead to very differently shaped derivations.

%query 1 _ _ {p} {q} {r} {s} complete _ (d₂ ⁺ p q r s) (tp (t↓ (t⁺ p q r s))) (N p q r s) %.
%query 1 _ _ {p} {q} {r} {s} complete _ (d₂ ⁺ p q r s) (tp (t↓ (t⁼ p q r s))) (N p q r s) %.