The Zwarts strength hierarchies

[Zwa98] [Ica12] [Lad80]

The polarity-facing quotient of the natural-logic signature system: the DE hierarchy weak < antiAdditive < antiMorphic and its UE dual as linear orders, the bridge maps reading strength off an Signature's projection behavior, and DEStrength.HoldsFor, the semantic content of each level (weak = Antitone, antiAdditive = IsAntiAdditive, antiMorphic = IsAntiMorphic), downward closed along the chain (HoldsFor.of_le).

Main declarations

• DEStrength, UEStrength — the Zwarts hierarchies.
• DEStrength.HoldsFor — the semantic content of a strength level.
• Signature.toDEStrength, Signature.toUEStrength — the signature → strength bridge maps.
• NaturalLogic.de_signature_licenses_weak_npi, NaturalLogic.strong_npi_requires_antiadditive — the Ladusaw/Zwarts licensing connections.

The hierarchies

inductive Polarity.DEStrength : Type

The three levels of the DE hierarchy ([Zwa98]): weak is plain DE (licenses weak NPIs: ever, any), antiAdditive adds ∨→∧ distributivity (licenses strong NPIs: lift a finger), and antiMorphic adds ∧→∨ distributivity (= negation).

• weak : DEStrength
• antiAdditive : DEStrength
• antiMorphic : DEStrength

@[instance_reducible]

instance Polarity.instDecidableEqDEStrength : DecidableEq DEStrength

Equations

• Polarity.instDecidableEqDEStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Polarity.instReprDEStrength : Repr DEStrength

Equations

• Polarity.instReprDEStrength = { reprPrec := Polarity.instReprDEStrength.repr }

def Polarity.instReprDEStrength.repr : DEStrength → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Polarity.instReprDEStrength.repr Polarity.DEStrength.weak prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Polarity.DEStrength.weak")).group prec✝

def Polarity.DEStrength.toNat : DEStrength → ℕ

Rank in the Zwarts chain weak < antiAdditive < antiMorphic.

Equations

• Polarity.DEStrength.weak.toNat = 0
• Polarity.DEStrength.antiAdditive.toNat = 1
• Polarity.DEStrength.antiMorphic.toNat = 2

theorem Polarity.DEStrength.toNat_injective : Function.Injective toNat

@[instance_reducible]

instance Polarity.instLinearOrderDEStrength : LinearOrder DEStrength

The Zwarts DE hierarchy as the linear order weak < antiAdditive < antiMorphic — the carrier of the canonical zwartsScale (Semantics/Polarity/Licensing.lean); other theories of NPI strength supply other ordered carriers.

Equations

• Polarity.instLinearOrderDEStrength = LinearOrder.lift' Polarity.DEStrength.toNat Polarity.DEStrength.toNat_injective

inductive Polarity.UEStrength : Type

The three levels of the UE hierarchy (dual of DEStrength): weak is plain UE (monotone), multiplicative adds ∧-distributivity, additive ∨-distributivity (strongest).

• weak : UEStrength
• multiplicative : UEStrength
• additive : UEStrength

@[instance_reducible]

instance Polarity.instDecidableEqUEStrength : DecidableEq UEStrength

Equations

• Polarity.instDecidableEqUEStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Polarity.instReprUEStrength.repr : UEStrength → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Polarity.instReprUEStrength.repr Polarity.UEStrength.weak prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Polarity.UEStrength.weak")).group prec✝

@[instance_reducible]

instance Polarity.instReprUEStrength : Repr UEStrength

Equations

• Polarity.instReprUEStrength = { reprPrec := Polarity.instReprUEStrength.repr }

The Zwarts hierarchy semantically

def Polarity.DEStrength.HoldsFor {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (s : DEStrength) (f : α → β) : Prop

The semantic content of a DEStrength level for a context function ([Ica12] §4, after Zwarts): weak is antitonicity, antiAdditive the anti-additivity equation, antiMorphic the full anti-morphism — few is weak-only, no anti-additive, not anti-morphic.

Equations

• Polarity.DEStrength.weak.HoldsFor f = Antitone f
• Polarity.DEStrength.antiAdditive.HoldsFor f = IsAntiAdditive f
• Polarity.DEStrength.antiMorphic.HoldsFor f = IsAntiMorphic f

theorem Polarity.DEStrength.HoldsFor.of_le {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] {f : α → β} {s₁ s₂ : DEStrength} (h : s₁ ≤ s₂) (hf : s₂.HoldsFor f) : s₁.HoldsFor f

Strength facts are downward closed along the Zwarts chain weak < antiAdditive < antiMorphic: a function holding a level holds every weaker one.

Signature → strength bridge maps

def NaturalLogic.Signature.toDEStrength (φ : Signature) : Option Polarity.DEStrength

The DE strength a signature realizes, derived from project: a signature is DE iff it reverses forward entailment; within the DE side, anti-additivity is detected by the ∨→∧ swap on cover and anti-morphism additionally by the ∧→∨ swap on alternation. none for UE-side signatures.

Equations

• One or more equations did not get rendered due to their size.

def NaturalLogic.Signature.toUEStrength (φ : Signature) : Option Polarity.UEStrength

The UE strength a signature realizes, derived from project: a signature is UE iff it preserves forward entailment; additivity is ∨-preservation on cover, multiplicativity ∧-preservation on alternation. none for DE-side signatures.

Equations

• One or more equations did not get rendered due to their size.

theorem NaturalLogic.de_signature_licenses_weak_npi (σ : Signature) : σ.toContextPolarity = ContextPolarity.downward → σ.toDEStrength.isSome = true

Any DE-side signature licenses weak NPIs ([Lad80]): a signature whose context polarity is downward carries a DE strength.

theorem NaturalLogic.strong_npi_requires_antiadditive (σ : Signature) : σ.toDEStrength = some Polarity.DEStrength.antiAdditive ∨ σ.toDEStrength = some Polarity.DEStrength.antiMorphic → σ.toContextPolarity = ContextPolarity.downward

Anti-additive or stronger signatures sit on the DE side: the strong NPI licensors (antiAdd, antiAddMult) are downward contexts — but plain anti and antiMult only reach weak.