Focusing

Origin. Andreoli (1992) for linear logic. Organizes proof search phases. Synchronous vs asynchronous connectives. Eliminates don't-care nondeterminism. Foundation for modern proof search.

Models. Connectives classified by polarity. Positive: synchronous (must choose). Negative: asynchronous (no choice). Focused proofs: maximal inversion phases. Completeness: focused proofs suffice.

Formalism.

Polarity assignment: Positive: ⊕, ⊗, 1, 0, ∃, atoms (by convention) Negative: &, ⅋, ⊤, ⊥, ∀, negated atoms

Asynchronous phase: Decompose negative formulas eagerly. No backtracking needed. Γ; A, B, Δ ⊢ [C] ─────────────────── A&B Γ; A & B, Δ ⊢ [C]

Synchronous phase: Choose one positive formula. Decompose until negative encountered. Γ; · ⊢ [A] ────────────── focus Γ; · ⊢ A

Judgment forms: Γ; Δ ⊢ [A]: focusing on A (synchronous) Γ; Δ ⊢ A: inversion phase (asynchronous)

Blur/Focus transitions: Focus: select positive formula to focus on. Blur: encounter negative, return to inversion.

Intuitionistic focusing: Left and right focus zones. LJT (Herbelin), LJF (Liang and Miller): focused intuitionistic systems. Derives decision procedures.

Polarized connectives: ↑A⁺ (up-shift): takes a positive formula and yields a negative one. ↓A⁻ (down-shift): takes a negative formula and yields a positive one.

The arrows are named for a vertical picture with the negative layer above the positive: ↑ lifts a positive into the negative layer, ↓ drops a negative into the positive layer (Girard 1991). So the polarized grammar reads A⁻ ::= A⁺ ⊃ B⁻ | A⁻ & B⁻ | ⊤ | P⁻ | ↑A⁺ A⁺ ::= A⁺ ⊕ B⁺ | 0 | A⁺ ⊗ B⁺ | 1 | P⁺ | ↓A⁻ with each shift appearing among the formulas of the polarity it produces, not the one it consumes. Shifts are inserted exactly where polarity changes, which is what makes the phase boundaries explicit in the syntax.

Under Curry–Howard this is call-by-push-value: positives are value types, negatives are computation types, ↑ is the returner F (a computation producing a value) and ↓ is the thunk U (a suspended computation used as a value).

Symbols.

Symbol	Unicode	Name	Meaning
↑	U+2191	Upwards arrow / Up-shift	↑A⁺ is negative: lifts a positive into the negative layer
↓	U+2193	Downwards arrow / Down-shift	↓A⁻ is positive: drops a negative into the positive layer
⁺, ⁻	U+207A, U+207B	Superscript plus, minus	Polarity annotation on a formula
⊗	U+2297	Tensor	Positive conjunction
⊕	U+2295	Plus	Positive disjunction
&	U+0026	Ampersand / With	Negative conjunction; its rule is invertible
⅋	U+214B	Par	Negative disjunction
⊤, ⊥	U+22A4, U+22A5	Top, Bottom	Negative units
⊃	U+2283	Superset of / Implication	Negative implication of the polarized grammar
∀	U+2200	Universal quantifier	Negative: decomposed in the inversion phase
∃	U+2203	Existential quantifier	Positive: requires a committed choice of witness
[ ]	U+005B, U+005D	Square brackets / Focus	Enclose the formula currently under focus
;	U+003B	Semicolon / Zone separator	Divides the zones of a focused sequent
Γ, Δ	U+0393, U+0394	Gamma, Delta	Unfocused contexts on either side of the semicolon

Metatheory. Andreoli (1992) proved the focalization theorem for linear logic: every provable sequent has a focused proof, so restricting search to alternating inversion and focusing phases loses no provability while discarding the don't-care nondeterminism of rule ordering. The asynchronous phase is confluent because the negative rules are invertible; the genuine choice lives in the synchronous phase, and focusing confines it there. Liang and Miller (2009) carried the theorem to classical and intuitionistic logic with the systems LKF and LJF, and showed that the polarity assigned to atoms is a free parameter — different uniform assignments reproduce goal-directed backward chaining and resolution-style forward chaining inside a single calculus — which Chaudhuri, Pfenning and Price (2008) made precise for the inverse method. Under Curry–Howard the discipline is Levy's call-by-push-value, with positives as values, negatives as computations, and the shifts as the thunk and returner.

Applies to. Proof search. Logic programming. Type theory (call-by-push-value). Theorem provers. Certified proof search.

Limitations. Focusing removes the nondeterminism of rule ordering and nothing more: which positive formula to focus on is don't-know nondeterminism and survives untouched, so a focused calculus shrinks the search space without making search decidable or subexponential. Polarity assignment is a free parameter with a real cost — different assignments yield proofs of different sizes, and no procedure selects the best one for a given goal. A bipole can be arbitrarily large, so one focused phase is an unbounded macro-step; that is what makes focused proofs compact and also what makes their cost hard to account for. And focalization is not inherited: it has been proved logic by logic — linear, classical, intuitionistic, then particular modal and substructural systems — while dependent type theory, where a type may mention a term produced inside a phase, has no settled focused presentation.