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.

Symbol	Unicode	Name	Meaning
⊗	U+2297	Tensor	Positive conjunction
⅋	U+214B	Par	Negative disjunction
⊕	U+2295	Plus	Positive disjunction
&	—	With	Negative conjunction
↓	U+2193	Down-shift	Neg to pos: ↓A⁻ is positive (thunk)
↑	U+2191	Up-shift	Pos to neg: ↑A⁺ is negative (returner)
[·]	—	Focus	Focused formula

Metatheory. Focusing is complete (no loss of proofs). Cut-elimination preserves focusing. Polarized proofs canonical representatives. Relates to call-by-name/value. Polarity determines focusing strategy.

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

Limitations. Adds complexity to logic. Shift operators require care. Not standard presentation. Multiple polarization choices. Tool support limited. Research-oriented.