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 (Dyckhoff): focused intuitionistic logic. 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
[ ]	—	Focus	Focused formula
↑	U+2191	Up-shift	Pos to neg: ↑A⁺ is negative
↓	U+2193	Down-shift	Neg to pos: ↓A⁻ is positive
;	—	Zone	Left/right context

Metatheory. Focused completeness: every proof has focused form. Deterministic asynchronous phase. Cut-free focused proofs. Proof irrelevance for negative. Correspondence to call-by-value/name.

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

Limitations. Polarity choice affects search. Atoms need assignment. Extensions to full dependent types complex. Implementation requires discipline.