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: ↓P (shift down): positive to negative ↑N (shift up): negative to positive

Symbols.

Symbol	Unicode	Name	Meaning
[ ]	—	Focus	Focused formula
↑	U+2191	Shift up	Neg to pos
↓	U+2193	Shift down	Pos to neg
;	—	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.