Polarized propositional intuitionistic focusing

The unfocused reference calculus uses finite-set contexts and is generated by

$a\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⟹a$

$\mathrm{\perp }\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⟹C$

$\mathrm{\Gamma }⟹\mathrm{\top }$

$\mathrm{\Gamma }⟹A$

$\mathrm{\Gamma }⟹A\vee B$

$\mathrm{\Gamma }⟹B$

$\mathrm{\Gamma }⟹A\vee B$

$\mathrm{\Gamma },A\vee B,A⟹C$$\mathrm{\Gamma },A\vee B,B⟹C$

$\mathrm{\Gamma },A\vee B⟹C$

$\mathrm{\Gamma }⟹A$$\mathrm{\Gamma }⟹B$

$\mathrm{\Gamma }⟹A\wedge B$

$\mathrm{\Gamma },A\wedge B,A⟹C$

$\mathrm{\Gamma },A\wedge B⟹C$

$\mathrm{\Gamma },A\wedge B,B⟹C$

$\mathrm{\Gamma },A\wedge B⟹C$

$\mathrm{\Gamma },A⟹B$

$\mathrm{\Gamma }⟹A\to B$

$\mathrm{\Gamma },A\to B⟹A$$\mathrm{\Gamma },A\to B,B⟹C$

$\mathrm{\Gamma },A\to B⟹C$

For an ordered queue, erasure into the finite-set context is generated by

$\mathrm{\Gamma }⟹C$

$\mathrm{\Gamma };\cdot ⟹C$

$\mathrm{\Gamma },A;\mathrm{\Psi }⟹C$

$\mathrm{\Gamma };A,\mathrm{\Psi }⟹C$

The exact polarized grammar of chapter 39 is Persistent contexts contain negative formulas and suspended positives; inversion contexts are ordered positive queues: $$\mathrm{\Gamma }::=\cdot \mid \mathrm{\Gamma },N\mid \mathrm{\Gamma },⟨P⟩,\mathrm{\Omega }::=\cdot \mid P,\mathrm{\Omega },U::=P\mid N\mid ⟨N⟩.$$ The three judgments are right focus $\mathrm{\Gamma }⊢[P]$, inversion $\mathrm{\Gamma };\mathrm{\Omega }⊢U$, and left focus $\mathrm{\Gamma };[N]⊢U$. A left-focus succedent is stable: it is either $P$ or $⟨N⟩$.

Right focus is generated by

$\mathrm{\Gamma };\cdot ⊢N$

$\mathrm{\Gamma }⊢[\downarrow N]$

$\mathrm{\Gamma }⊢[P]$

$\mathrm{\Gamma }⊢[P\vee Q]$

$\mathrm{\Gamma }⊢[Q]$

$\mathrm{\Gamma }⊢[P\vee Q]$

$\mathrm{\Gamma }⊢[{\mathbf{1}}^{+}]$

$\mathrm{\Gamma }⊢[P]$$\mathrm{\Gamma }⊢[Q]$

$\mathrm{\Gamma }⊢[P\otimes Q]$

$⟨P⟩\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢[P]$

There is no right-focus rule for $\mathbf{0}$.

Positive inversion is generated by

$\mathrm{\Gamma },N;\mathrm{\Omega }⊢U$

$\mathrm{\Gamma };\downarrow N,\mathrm{\Omega }⊢U$

$\mathrm{\Gamma };\mathbf{0},\mathrm{\Omega }⊢U$

$\mathrm{\Gamma };P,\mathrm{\Omega }⊢U$$\mathrm{\Gamma };Q,\mathrm{\Omega }⊢U$

$\mathrm{\Gamma };P\vee Q,\mathrm{\Omega }⊢U$

$\mathrm{\Gamma };\mathrm{\Omega }⊢U$

$\mathrm{\Gamma };{\mathbf{1}}^{+},\mathrm{\Omega }⊢U$

$\mathrm{\Gamma };P,Q,\mathrm{\Omega }⊢U$

$\mathrm{\Gamma };P\otimes Q,\mathrm{\Omega }⊢U$

$\mathrm{\Gamma },⟨p^{+}⟩;\mathrm{\Omega }⊢U$

$\mathrm{\Gamma };p^{+},\mathrm{\Omega }⊢U$

Negative right inversion is generated by

$\mathrm{\Gamma };\cdot ⊢P$

$\mathrm{\Gamma };\cdot ⊢\uparrow P$

$\mathrm{\Gamma };P⊢N$

$\mathrm{\Gamma };\cdot ⊢P\Rightarrow N$

$\mathrm{\Gamma };\cdot ⊢{\mathbf{1}}^{-}$

$\mathrm{\Gamma };\cdot ⊢N$$\mathrm{\Gamma };\cdot ⊢M$

$\mathrm{\Gamma };\cdot ⊢⟨p^{-}⟩$

$\mathrm{\Gamma };\cdot ⊢p^{-}$

The phase rules and left-focus rules are

$\mathrm{\Gamma }⊢[P]$

$\mathrm{\Gamma };\cdot ⊢P$

$\mathrm{\Gamma };P⊢U$

$\mathrm{\Gamma };[\uparrow P]⊢U$

$\mathrm{\Gamma };[N]⊢⟨N⟩$

$\mathrm{\Gamma },N;[N]⊢U$

$\mathrm{\Gamma },N;\cdot ⊢U$

$\mathrm{\Gamma };[N]⊢U$

$\mathrm{\Gamma }⊢[P]$$\mathrm{\Gamma };[N]⊢U$

$\mathrm{\Gamma };[P\Rightarrow N]⊢U$

$\mathrm{\Gamma };[M]⊢U$

No rule left-focuses ${\mathbf{1}}^{-}$. Final sequents suspend only atoms; compound suspensions occur only inside focal substitution and identity expansion. The focal-substitution metarules are admissible, rather than constructors of the focused derivability judgments:

$\mathrm{\Gamma }⊢[P]$$\mathrm{\Gamma },⟨P⟩;L⊢U$

$\mathrm{\Gamma };L⊢U$

$\mathrm{\Gamma };L⊢⟨N⟩$$\mathrm{\Gamma };[N]⊢U$

$\mathrm{\Gamma };L⊢U$