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: ↓P: shift positive P to negative (delay). ↑N: shift negative N to positive (force).

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	Delay
↑	U+2191	Up-shift	Force
[·]	—	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.