Polarized Logic

Origin. Girard introduced polarity (1991, 1993). Andreoli: focusing (1992). Laurent: polarized linear logic (2002). Formulas have polarity: positive (synchronous) or negative (asynchronous). Controls proof search. Foundation for focused proof systems.

Models. Synchronous vs asynchronous behavior. Positive formulas: demand immediate action (output). Negative formulas: allow delayed action (input). Focusing: proof search discipline based on polarity. Eliminates don't-care nondeterminism.

Formalism.

Polarities: Positive (synchronous): ⊗, ⊕, 1, 0, ∃, ! Negative (asynchronous): ⅋, &, ⊥, ⊤, ∀, ?

Focusing: Positive phase: decompose positive formulas (must continue). Negative phase: decompose negative formulas (can pause). Focus: choose positive formula and decompose fully.

Shifts: ↑A⁺: shifts a positive formula up into the negatives — ↑A⁺ is negative. ↓A⁻: shifts a negative formula down into the positives — ↓A⁻ is positive.

Each shift belongs to the polarity it produces, not the one it consumes: the polarized grammar puts ↑A⁺ among the negative formulas and ↓A⁻ among the positive ones (Girard 1991). The names come from picturing the negative layer above the positive. Computationally ↓ is the thunk — a suspended computation packaged as a value, hence the delay — and ↑ is the returner, a computation that yields a value.

Focused sequent calculus: Γ; Δ ⊢ [A]: focus on A (positive). Γ; Δ ⊢ A: no focus (inversion). Γ; Δ; [A] ⊢ C: focused hypothesis.

Inversion: Negative formulas: apply rules invertibly (any order). Positive formulas: require commitment (focus).

Call-by-name vs call-by-value: Polarity relates to evaluation strategy. Positive = values (CBV), Negative = computations (CBN).

Polarized classical logic (LKp): Classical logic with explicit polarity. De Morgan dual exchanges polarity.

Symbols.

Metatheory. Girard introduced polarity in LC (1991) to fix a specific defect: cut elimination in LK is not confluent, since the same cut reduces to different normal forms depending on which side is taken first, and the semantic version of the collapse is Joyal's lemma — a cartesian closed category with an involutive negation is a preorder — so classical proofs admit no naive denotation. Assigning polarities and inserting shifts breaks the symmetry and makes reduction deterministic. Danos, Joinet and Schellinx (1997) showed the two ways of breaking it are the calculi LKQ and LKT, which correspond under continuation-passing translation to call-by-value and call-by-name evaluation. Laurent (2002) isolated polarized linear logic LLP, showed Girard's translations of classical logic land inside it, and gave polarized proof nets with a confluent cut elimination. Andreoli's focalization is the proof-search face of the same structure and Levy's call-by-push-value its programming-language face.

Applies to. Proof search. Logic programming (uniform proofs). Type systems. Compilation (CPS, CBV). Game semantics. Linear logic programming.

Limitations. Polarity is imposed on the logic rather than discovered in it: a classical formula admits many polarizations, they are logically equivalent but proof-theoretically distinct, and nothing in the logic selects one — which is why LKQ and LKT both exist and assign different normal forms to the same classical theorem. Canonicity is therefore relative to a polarization, and the identity of classical proofs is fixed only after that choice is made. Shifts are what determinism requires: one must be inserted at every change of polarity, so polarized formulas are strictly larger than the formulas they polarize. The account is propositional in the first instance — extending polarity to dependent types, where a type may mention a term computed during a positive phase, has no settled treatment. And polarity constrains the shape of proofs, not their size, so it yields no complexity gain.

© 2026 Lingenic LLC