Hoeksema (1983): Negative Polarity and the Comparative

@cite{hoeksema-1983}

The asymmetry

@cite{hoeksema-1983} (NLLT 1: 403–434) advances a Boolean-algebraic account of comparatives that distinguishes two distinctly typed than-arguments, each with a different polarity-environment signature. The empirical hook is that English / Dutch comparatives sometimes license NPIs and sometimes do not — the type distinction predicts which.

• NP-comparative [Adj-er than NP] (§3.6, Eq 22): the than-argument is a generalized quantifier; ⟦than NP⟧ : Set (Set U) → Set U is a Boolean homomorphism. By Fact 3 it is monotone increasing in its GQ argument, and (§3.6) not a negative polarity environment. Surface NPIs in "than NP" arise (by hypothesis) from a covert clausal source.

• S-comparative [Adj-er than S] (§3.8, Def 7): the than-clause ranges over degrees; ⟦than S⟧ : Set D → Set U is anti-additive but not a Boolean homomorphism, hence an NPI environment by Zwarts.

Formalization

npComparativeGQ is mathlib's CompleteLatticeHom.setPreimage applied to a threshold function npThreshold μ y = {x | μ x < μ y}. All Boolean-algebra preservation properties — finite ∩/∪/ᶜ/⊤/⊥ and arbitrary sSup/sInf (strengthening Hoeksema's finitary claim) — are inherited from the bundled hom via the standard mathlib map_inf / map_sup / map_compl / map_top / map_bot / OrderHomClass.mono API. BoundedLatticeHomClass.toBiheytingHomClass gives complement preservation for free on BooleanAlgebra → BooleanAlgebra homs.

The S-comparative sComparative (originally @cite{hoeksema-1983} §3.8 Def 7) and its anti-additivity (Fact 4) live in Theories/Semantics/Degree/Comparative.lean as the natural generalization of comparativeSem from a binary comparator to a degree-set comparator. This file imports them from there.

Hoeksema's algebraic spine: Definitions 4–8 and Facts 1–4

The §3 algebraic content is formalized in five layers:

• Definition 4 (IsOrderingPreserving): the abstract property μ b < μ a ↔ a ∈ f Q_b, where Q_b = {X | b ∈ X} is the principal ultrafilter at b (principalUltrafilter).
• Definition 7/8 (sComparative in Theories/Semantics/Degree/Comparative.lean): the S-comparative as a set-of-degrees operator.
• Fact 1 (fact1_agree_on_atoms): two >-preserving functions coincide on every principal ultrafilter — a one-line chain of the Definition 4 biconditionals.
• Fact 2 (fact2_unique_from_atoms): a CompleteLatticeHom on Set (Set Entity) → Set Entity is determined by its values on the principal-ultrafilter generators Q_b. Combined with Fact 1, this gives npComparativeGQ_uniqueness: two >-preserving complete Boolean homs are equal.
• Fact 3 (npComparativeGQ_monotone): every Boolean hom is monotone increasing — disqualifies the NP-comparative as a Ladusaw NPI environment.
• Fact 4 (sComparative_isAntiAdditive in Theories/Semantics/Degree/Comparative.lean, cited from IsAntiAdditive.antitone in AntiAdditivity.lean): every anti-additive function is antitone — hence the S-comparative qualifies as an NPI environment.
• §3.9 NP↔S equivalence (npComparativeGQ_principal_eq_sComparative_singleton): on principal ultrafilters / singleton degree sets, the two constructions deliver the same predicate.

Registry connection

The licensing-context registry Core/Lexical/PolarityItem.lean records this paper's central asymmetry as a structural invariant:

• .comparativeNP has signature .mono (Boolean hom is monotone, not DE)
• .comparativeS has signature .antiAdd

The comparativeNP_signature_monotone and comparativeS_signature_anti_additive theorems below witness the agreement between this study file's mathematical statements and the registry's classification, by rfl.

NP-comparative as Boolean homomorphism (§3.6, Eq 22)

def Hoeksema1983.npThreshold {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (y : Entity) : Set Entity

The threshold function underlying the NP-comparative: npThreshold μ y is the set of individuals y is taller than under measure μ. The NP-comparative GQ is the set-preimage operator induced by this function (npComparativeGQ); Hoeksema Fact 1 (uniqueness) is the injectivity of this assignment, supplied by Core.Order.setPreimage_injective.

Equations

• Hoeksema1983.npThreshold μ y = {x : Entity | μ x < μ y}

def Hoeksema1983.npComparativeGQ {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) : CompleteLatticeHom (Set (Set Entity)) (Set Entity)

@cite{hoeksema-1983} Eq (22): the NP-comparative as a function on generalized quantifiers, packaged as the bundled mathlib CompleteLatticeHom.setPreimage (npThreshold μ).

npComparativeGQ μ Q y holds iff the property "is shorter than y" (npThreshold μ y) is one of the properties picked out by the GQ Q. All Boolean-algebra preservation properties — finite ∩/∪/ᶜ/⊤/⊥ and arbitrary sSup/sInf (stronger than Hoeksema's finitary statement) — are inherited from the bundled hom via the standard mathlib map_* API.

Equations

• Hoeksema1983.npComparativeGQ μ = CompleteLatticeHom.setPreimage (Hoeksema1983.npThreshold μ)

Hoeksema Fact 3: monotonicity, and the §3.6 corollary

theorem Hoeksema1983.npComparativeGQ_monotone {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) : Monotone ⇑(npComparativeGQ μ)

@cite{hoeksema-1983} Fact 3: the GQ NP-comparative is monotone increasing in its GQ argument. Inherited from the bundled hom's OrderHomClass.

theorem Hoeksema1983.npComparativeGQ_map_compl {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (Q : Set (Set Entity)) : (npComparativeGQ μ) Qᶜ = ((npComparativeGQ μ) Q)ᶜ

@cite{hoeksema-1983} Eq (22), complement clause: complement preservation on the NP-comparative GQ, via mathlib's automatic BiheytingHomClass instance for BooleanAlgebra → BooleanAlgebra BoundedLatticeHoms.

theorem Hoeksema1983.npComparativeGQ_antitone_iff_constant_on_chains {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) : Antitone ⇑(npComparativeGQ μ) ↔ ∀ (Q₁ Q₂ : Set (Set Entity)), Q₁ ⊆ Q₂ → (npComparativeGQ μ) Q₁ = (npComparativeGQ μ) Q₂

@cite{hoeksema-1983} §3.6: the NP-comparative is not downward- entailing on any nontrivial domain. We state the contrapositive: if the GQ NP-comparative were antitone, then for Q ⊆ Q' it would map to npComparativeGQ μ Q' ⊆ npComparativeGQ μ Q — combined with the Fact 3 monotonicity going the other way, it would force equality on every comparable pair. This is the formal content of "monotone increasing ≠ downward-entailing", which is what disqualifies NP-comparative as an NPI environment under Ladusaw monotonicity.

Threshold uniqueness for the NP-comparative GQ

A specialization of the Hoeksema atom-uniqueness story to the
`npComparativeGQ` family: distinct measures induce distinct GQs.
Adjacent to but not literally @cite{hoeksema-1983} Fact 1 (which is
stated for arbitrary `>`-preserving functions; see below). 

theorem Hoeksema1983.npComparativeGQ_injective_in_threshold {Entity : Type u_1} {D : Type u_2} [Preorder D] {μ₁ μ₂ : Entity → D} : npComparativeGQ μ₁ = npComparativeGQ μ₂ ↔ npThreshold μ₁ = npThreshold μ₂

The NP-comparative GQ uniquely determines its underlying threshold function. Two scales μ₁, μ₂ produce the same NP-comparative GQ iff they induce the same "things-y-is-taller-than" set for every y. Proof by atom-decomposition (probe at singletons), packaged as Core.Order.setPreimage_injective.

Definition 4: >-preserving functions on quantifiers

@cite{hoeksema-1983} Definition 4 isolates the abstract property
that distinguishes a comparative GQ-to-predicate operator from an
arbitrary one. The principal ultrafilter `Q_b = {X | b ∈ X}` is the
GQ denotation of the proper name `b`; `f` *preserves* `>` iff for
every pair `a, b`, `μ b < μ a` is equivalent to `a ∈ f Q_b`
(`f Q_b ∈ Q_a` in Hoeksema's exact phrasing). 

def Hoeksema1983.principalUltrafilter {Entity : Type u_1} (b : Entity) : Set (Set Entity)

The principal ultrafilter at an individual: the GQ denotation of a proper name b. Hoeksema's Q_b.

Equations

• Hoeksema1983.principalUltrafilter b = {X : Set Entity | b ∈ X}

def Hoeksema1983.IsOrderingPreserving {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (f : Set (Set Entity) → Set Entity) : Prop

@cite{hoeksema-1983} Definition 4: f preserves > iff for every pair a, b, μ b < μ a ↔ a ∈ f Q_b.

Equations

• Hoeksema1983.IsOrderingPreserving μ f = ∀ (a b : Entity), μ b < μ a ↔ a ∈ f (Hoeksema1983.principalUltrafilter b)

theorem Hoeksema1983.npComparativeGQ_preserves_ordering {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) : IsOrderingPreserving μ ⇑(npComparativeGQ μ)

The NP-comparative GQ preserves > in the sense of @cite{hoeksema-1983} Definition 4. Combined with npComparativeGQ_monotone (Fact 3), this is the precise sense in which [[Adj-er than]] is the GQ-level comparative operator.

Fact 1: any two >-preserving functions agree on every atom

theorem Hoeksema1983.fact1_agree_on_atoms {Entity : Type u_1} {D : Type u_2} [Preorder D] {μ : Entity → D} {f g : Set (Set Entity) → Set Entity} (hf : IsOrderingPreserving μ f) (hg : IsOrderingPreserving μ g) (b : Entity) : f (principalUltrafilter b) = g (principalUltrafilter b)

@cite{hoeksema-1983} Fact 1: any two functions on quantifiers that both preserve > (Definition 4) coincide on every principal ultrafilter Q_b. The proof is a direct chain of the two IsOrderingPreserving biconditionals — both sides reduce to μ b < μ a.

Fact 2: Boolean-hom uniqueness from agreement on principal ultrafilters

Hoeksema's Fact 2 strengthens Fact 1: two complete-lattice Boolean
homomorphisms on `Set (Set Entity) → Set Entity` that agree on every
principal ultrafilter `Q_b` are equal. The proof reduces every
`Q : Set (Set Entity)` to the `iSup` of its singleton members, each of
which is the `iInf` of `Q_a` for `a ∈ Y` and `Q_aᶜ` for `a ∉ Y`.
The hom commutes with `iSup`, `iInf`, `inf`, and `compl`.

The two bridge lemmas (`singleton_eq_iInf_principalUltrafilter`,
`eq_iSup_singletons`) state the atom representation directly with
`⨅`/`⨆` so the consumer (`fact2_unique_from_atoms`) chains with
`map_iInf₂` / `map_iSup₂` without any `⋂ → ⨅` bridging step. 

theorem Hoeksema1983.singleton_eq_iInf_principalUltrafilter {Entity : Type u_1} (X : Set Entity) : {X} = (⨅ a ∈ X, principalUltrafilter a) ⊓ ⨅ (a : Entity), ⨅ (_ : a ∉ X), (principalUltrafilter a)ᶜ

Atom representation of a singleton in Set (Set Entity): {X} = (⨅_{a ∈ X} Q_a) ⊓ (⨅_{a ∉ X} Q_aᶜ). Stated with ⨅/⊓ rather than ⋂/∩ so that consumers chain directly with map_iInf₂ / map_inf.

theorem Hoeksema1983.eq_iSup_singletons {Entity : Type u_1} (Q : Set (Set Entity)) : Q = ⨆ Y ∈ Q, {Y}

Any Q : Set (Set Entity) is the ⨆ of its singleton members. Stated with ⨆ rather than ⋃ so that the consumer (fact2_unique_from_atoms) chains directly with map_iSup₂.

theorem Hoeksema1983.fact2_unique_from_atoms {Entity : Type u_1} (f g : CompleteLatticeHom (Set (Set Entity)) (Set Entity)) (hagree : ∀ (b : Entity), f (principalUltrafilter b) = g (principalUltrafilter b)) : f = g

@cite{hoeksema-1983} Fact 2: a CompleteLatticeHom on Set (Set Entity) → Set Entity is determined by its values on the principal-ultrafilter generators Q_b. The proof composes eq_iSup_singletons (every Q is a ⨆ of singletons), singleton_eq_iInf_principalUltrafilter (every singleton is an atomic ⨅ of Q_a's and Q_aᶜ's), and the standard mathlib hom API (map_iSup₂, map_iInf₂, map_inf, map_compl).

The mathematical content — "a CompleteLatticeHom on Set (Set α) → Set α is determined by its values on principal-set generators" — is generic and would PR cleanly to Mathlib/Order/Hom/CompleteLattice.lean as a strengthening of the existing pointwise @[ext] lemma.

theorem Hoeksema1983.npComparativeGQ_uniqueness {Entity : Type u_1} {D : Type u_2} [Preorder D] {μ : Entity → D} (f g : CompleteLatticeHom (Set (Set Entity)) (Set Entity)) (hf : IsOrderingPreserving μ ⇑f) (hg : IsOrderingPreserving μ ⇑g) : f = g

Combining Fact 1 and Fact 2: two >-preserving complete-lattice homomorphisms (Definition 4) on Set (Set Entity) → Set Entity are equal. Hoeksema's strongest uniqueness statement: the threshold function determines the comparative GQ entirely.

§3.9: NP-comparative on principal ultrafilter ≡ S-comparative on singleton

theorem Hoeksema1983.npComparativeGQ_principal_eq_sComparative_singleton {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (b : Entity) : (npComparativeGQ μ) (principalUltrafilter b) = Semantics.Degree.Comparative.sComparative μ {μ b}

@cite{hoeksema-1983} §3.9 (Eq. 44): the NP-comparative applied to a principal ultrafilter Q_b (the GQ denotation of a proper name) coincides with the S-comparative applied to the singleton degree set {μ b}. Both reduce to "is taller than b" — explaining the empirical equivalence of "I am bigger than you" (NP-form) and "I am bigger than you are" (S-form), Hoeksema's Eq. 44a–b.

Connection to the licensing-context registry

theorem Hoeksema1983.comparativeNP_signature_monotone : (Semantics.Polarity.Licensing.contextProperties Features.LicensingContext.comparativeNP).signature = Core.NaturalLogic.EntailmentSig.mono

The .comparativeNP registry slot is monotone, matching npComparativeGQ_monotone. This is the registry-level encoding of Hoeksema's central asymmetry: the NP-comparative is monotone increasing and therefore not an NPI environment.

theorem Hoeksema1983.comparativeS_signature_anti_additive : (Semantics.Polarity.Licensing.contextProperties Features.LicensingContext.comparativeS).signature = Core.NaturalLogic.EntailmentSig.antiAdd

The .comparativeS registry slot is anti-additive, matching sComparative_isAntiAdditive.

theorem Hoeksema1983.both_comparatives_cite_hoeksema : "hoeksema-1983" ∈ (Semantics.Polarity.Licensing.contextProperties Features.LicensingContext.comparativeNP).citations ∧ "hoeksema-1983" ∈ (Semantics.Polarity.Licensing.contextProperties Features.LicensingContext.comparativeS).citations

Both registry slots cite Hoeksema 1983, anchoring the registry's classification to this study file.