Polarity Operators

[Lak90] [TH26]

The two semantic operators that polarity heads spell out, as bare functions on (W → Prop) propositions:

• affirm — identity (the affirmative Σ operator of [Lak90]).
• neg — pointwise propositional negation.

This module is deliberately syntax-free: no UPOS, no head structure, no "PolarityHead" packaging. Those notions belong at the syntax-semantics interface or in fragment-level entries that pair a semantic operator with its syntactic realization. The semantics layer only owns the operator.

Equational simp lemmas (affirm_eq_id, neg_apply, neg_neg) make the operators transparent to downstream reasoning.

def Semantics.Polarity.affirm (W : Type u) : (W → Prop) → W → Prop

Affirmative polarity operator — identity on propositions ([Lak90]'s Σ).

Equations

• Semantics.Polarity.affirm W = id

def Semantics.Polarity.neg (W : Type u) : (W → Prop) → W → Prop

Negative polarity operator — pointwise propositional negation ([Lak90]'s NEG).

Equations

• Semantics.Polarity.neg W p w = ¬p w

@[simp]

theorem Semantics.Polarity.affirm_eq_id (W : Type u) : affirm W = id

@[simp]

theorem Semantics.Polarity.affirm_apply {W : Type u} (p : W → Prop) : affirm W p = p

@[simp]

theorem Semantics.Polarity.neg_apply {W : Type u} (p : W → Prop) (w : W) : neg W p w ↔ ¬p w

theorem Semantics.Polarity.neg_neg {W : Type u} (p : W → Prop) (w : W) : neg W (neg W p) w ↔ p w

neg is an involution (up to propositional extensionality).