Semantic Negation: Unified Foundations #

This module unifies the scattered negation semantics in linglib into a coherent architecture with three layers:

NegOp — a semantic negation operator bundling involution + antitonicity, with standardNeg (pnot) as the canonical instance
DEStrength ↔ PolarityLicensing bridge — the entailment hierarchy (weak DE / anti-additive / anti-morphic) determines the polarity licensing profile, connecting the Prop-based semantic properties in Theories.Semantics.Entailment to the Bool-valued empirical classification in Core.Negation
Scoped vs unscoped negation — a negation operator that retains scope into a domain preserves its semantic properties; when scope is blocked (e.g., by phase transfer), it loses antitonicity and hence licensing ability

Dependencies #

Core.Negation — framework-agnostic classification types (ENType, ENStrength, PolarityClass, PolarityLicensing) with Mathlib lattice instances
Mathlib.Data.Set.Basic — set complement (pᶜ) replaces the old Core.Semantics.Proposition.pnot
Core.Logic.NaturalLogic — DEStrength (weak/antiAdditive/antiMorphic), strengthSufficient
Theories.Semantics.Entailment.Polarity — IsDE = Antitone, IsUE = Monotone, pnot_isDownwardEntailing
Theories.Semantics.Entailment.AntiAdditivity — IsAntiAdditive, IsAntiMorphic, pnot_isAntiMorphic, licensesWeakNPI, licensesStrongNPI

source

structure Semantics.Negation.NegOp (W : Type u_1) :

Type u_1

A semantic negation operator on decidable propositions over worlds W.

Bundles a function with its two defining properties:

Involution: ¬¬p = p (double negation elimination)
Antitonicity: p ≤ q → ¬q ≤ ¬p (downward entailment)

Standard sentential negation (pnot) satisfies both. Expletive negation that has lost its scope may fail antitonicity — it is then no longer a NegOp in this sense.

TODO: NegOp should operate on Set W not W → Bool — separate cleanup pass per the Bool→Prop migration. The whole structure (and boolPnot, standardNeg, isAntiAdditive, isAntiMorphic) lives in the Bool layer and is out of scope for the current Prop' → Set migration.

op : (W → Bool) → W → Bool
The negation function on decidable propositions.
involutive : Function.Involutive self.op
Involutive: applying negation twice is the identity.
antitone : Antitone self.op
Antitone: reverses the entailment ordering (= DE).

Instances For

source

def Semantics.Negation.standardNeg (W : Type u_1) :

NegOp W

Standard sentential negation (pnot) is the canonical NegOp.

It satisfies involution (pnot_pnot), antitonicity (pnot_antitone), and additionally anti-morphism (De Morgan).

Equations

Semantics.Negation.standardNeg W = { op := Semantics.Negation.boolPnot✝ W, involutive := ⋯, antitone := ⋯ }

Instances For

source

def Semantics.Negation.NegOp.isAntiAdditive (n : NegOp Entailment.World) :

Prop

A NegOp is anti-additive if it distributes ∨ to ∧: ¬(A ∨ B) = ¬A ∧ ¬B (De Morgan, part 1). Stated directly on the W → Bool-typed operator.

Equations

n.isAntiAdditive = ∀ (p q : Semantics.Entailment.World → Bool) (w : Semantics.Entailment.World), n.op (fun (w : Semantics.Entailment.World) => p w || q w) w = (n.op p w && n.op q w)

Instances For

source

def Semantics.Negation.NegOp.isAntiMorphic (n : NegOp Entailment.World) :

Prop

A NegOp is anti-morphic if it is anti-additive AND distributes ∧ to ∨: ¬(A ∧ B) = ¬A ∨ ¬B (De Morgan, part 2). This is the full De Morgan property — the characteristic signature of negation in the entailment hierarchy.

Equations

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

Instances For

source

theorem Semantics.Negation.standardNeg_isAntiAdditive :

(standardNeg Entailment.World).isAntiAdditive

Standard negation is anti-additive (De Morgan part 1).

source

theorem Semantics.Negation.standardNeg_isAntiMorphic :

(standardNeg Entailment.World).isAntiMorphic

Standard negation is anti-morphic (full De Morgan).

The entailment hierarchy determines polarity licensing #

The Bool-valued PolarityLicensing profile in Core.Negation is a consequence of the Prop-based entailment properties in Theories.Semantics.Entailment:

DEStrength	Semantic property	Licenses	Profile
weak	`Antitone`	weak NPIs, N-words	`weakENProfile`
antiAdditive	`IsAntiAdditive`	+ strong NPIs, ¬also	`standardNegProfile`
antiMorphic	`IsAntiMorphic`	all (= standard neg)	`standardNegProfile`
(none)	¬ `Antitone`	nothing	`strongENProfile`

The anti-additive and anti-morphic levels both yield standardNegProfile because notAlsoConj and N-word licensing track anti-additivity, not anti-morphism (@cite{chierchia-2013} §1.4.3, @cite{icard-2012}).

source

def Semantics.Negation.deToPolarityLicensing :

Core.NaturalLogic.DEStrength → Phenomena.Negation.ExpletiveNegation.PolarityLicensing

Map DE strength to its empirical polarity licensing profile.

This is the central bridge: the semantic entailment hierarchy determines the Bool-valued licensing table.

Equations

Instances For

source

theorem Semantics.Negation.de_licensing_monotone (d₁ d₂ : Core.NaturalLogic.DEStrength) :

Core.NaturalLogic.strengthSufficient d₂ d₁ = true → deToPolarityLicensing d₁ ≤ deToPolarityLicensing d₂

The bridge is monotone: stronger DE → more licensing in the lattice.

source

theorem Semantics.Negation.weak_de_licensing :

deToPolarityLicensing Core.NaturalLogic.DEStrength.weak = Phenomena.Negation.ExpletiveNegation.weakENProfile

Weak DE licenses exactly weak NPIs and N-words.

source

theorem Semantics.Negation.antiAdditive_de_licensing :

deToPolarityLicensing Core.NaturalLogic.DEStrength.antiAdditive = Phenomena.Negation.ExpletiveNegation.standardNegProfile

Anti-additive DE licenses all polarity classes (= standard negation).

source

theorem Semantics.Negation.antiMorphic_de_licensing :

deToPolarityLicensing Core.NaturalLogic.DEStrength.antiMorphic = Phenomena.Negation.ExpletiveNegation.standardNegProfile

Anti-morphic DE licenses all polarity classes (= standard negation).

EN strength as presence/absence of DE #

The two-valued ENStrength classification collapses the three-level DE hierarchy into a binary:

ENStrength.weak = the negation retains at least weak DE (≥ DEStrength.weak)
ENStrength.strong = the negation has lost all DE properties

This is @cite{greco-2020}'s core claim: the weak/strong EN distinction reduces to whether negation retains its downward-entailing property.

source

def Semantics.Negation.deToENStrength :

Core.NaturalLogic.DEStrength → Phenomena.Negation.ExpletiveNegation.ENStrength

Map DE strength to EN strength: any DE at all → weak EN.

Equations

Instances For

source

def Semantics.Negation.enStrengthToLicensing :

Phenomena.Negation.ExpletiveNegation.ENStrength → Phenomena.Negation.ExpletiveNegation.PolarityLicensing

The licensing profile associated with an EN strength.

Weak EN retains at least weakENProfile (the minimum licensing from any DE context). Strong EN has strongENProfile (= ⊥, no licensing).

Equations

Instances For

source

theorem Semantics.Negation.enStrength_licensing_antitone (s₁ s₂ : Phenomena.Negation.ExpletiveNegation.ENStrength) :

s₁ ≤ s₂ → enStrengthToLicensing s₂ ≤ enStrengthToLicensing s₁

enStrengthToLicensing is antitone: stronger EN → less licensing.

This captures the inverse relationship: EN "strength" means strength of expletiveness, not strength of licensing. A stronger EN is more expletive, hence licenses less.

EN type determines EN strength #

The position-based ENType (high/low, @cite{rett-2026}) determines the polarity-based ENStrength (strong/weak, @cite{greco-2020}):

Low EN (truth-conditional, TP-area) → weak EN (retains polarity)
High EN (non-truth-conditional, CP-area) → strong EN (loses polarity)

This bridge connects the two orthogonal classifications.

source

def Semantics.Negation.enTypeToStrength :

Phenomena.Negation.ExpletiveNegation.ENType → Phenomena.Negation.ExpletiveNegation.ENStrength

Map EN type to EN strength.

Equations

Instances For

source

theorem Semantics.Negation.low_is_weak :

enTypeToStrength Phenomena.Negation.ExpletiveNegation.ENType.low = Phenomena.Negation.ExpletiveNegation.ENStrength.weak

Low EN is weak EN.

source

theorem Semantics.Negation.high_is_strong :

enTypeToStrength Phenomena.Negation.ExpletiveNegation.ENType.high = Phenomena.Negation.ExpletiveNegation.ENStrength.strong

High EN is strong EN.

source

def Semantics.Negation.enTypeToLicensing (t : Phenomena.Negation.ExpletiveNegation.ENType) :

Phenomena.Negation.ExpletiveNegation.PolarityLicensing

The composite bridge: ENType → ENStrength → PolarityLicensing.

Equations

Semantics.Negation.enTypeToLicensing t = Semantics.Negation.enStrengthToLicensing (Semantics.Negation.enTypeToStrength t)

Instances For

source

theorem Semantics.Negation.low_en_weak_licensing :

enTypeToLicensing Phenomena.Negation.ExpletiveNegation.ENType.low = Phenomena.Negation.ExpletiveNegation.weakENProfile

Low EN has at least weak licensing.

source

theorem Semantics.Negation.high_en_no_licensing :

enTypeToLicensing Phenomena.Negation.ExpletiveNegation.ENType.high = Phenomena.Negation.ExpletiveNegation.strongENProfile

High EN has no licensing (= ⊥).

Scope determines semantic property survival #

A NegOp that can scope into a domain retains all its semantic properties (involution, antitonicity, anti-morphism). When scope is blocked — e.g., by phase transfer in the Minimalist framework — the operator can no longer reverse entailment over that domain's propositions.

The connection to EN classification:

Scoped negation (TP-area merge) → retains Antitone → ENType.low → ENStrength.weak → weakENProfile
Unscoped negation (CP-area merge, vP transferred) → loses Antitone → ENType.high → ENStrength.strong → strongENProfile = ⊥

This is the full derivation chain: merge position → scope access → semantic property survival → entailment strength → polarity licensing.

source

def Semantics.Negation.scopeToENType (canScopeIntoVP : Bool) :

Phenomena.Negation.ExpletiveNegation.ENType

Classify negation by scope access.

A negation with scope into the propositional domain is low EN (truth-conditional). A negation without scope is high EN (non-truth-conditional).

Equations