From b71db81f4b3bc0f4782e44f6b9daa547339f7974 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 19 Jun 2026 16:54:17 -0700 Subject: [PATCH] refactor(Semantics/Degree): retire clausalComparison for overSet --- Linglib/Semantics/Degree/Comparative.lean | 113 +++++++----------- .../Semantics/Entailment/AntiAdditivity.lean | 2 +- Linglib/Studies/BhattPancheva2004.lean | 15 +-- Linglib/Studies/Gajewski2011.lean | 12 +- Linglib/Studies/Hoeksema1983.lean | 33 +++-- Linglib/Studies/VonFintel1999.lean | 8 +- 6 files changed, 79 insertions(+), 104 deletions(-) diff --git a/Linglib/Semantics/Degree/Comparative.lean b/Linglib/Semantics/Degree/Comparative.lean index 0ec7ccf40..00ea7dfe8 100644 --- a/Linglib/Semantics/Degree/Comparative.lean +++ b/Linglib/Semantics/Degree/Comparative.lean @@ -9,11 +9,14 @@ import Linglib.Core.Order.Comparison [rett-2026] [schwarzschild-2008] [von-stechow-1984] [hoeksema-1983] Comparative semantics shared across all degree frameworks: the binary -`comparativeSem` / `equativeSem`, the set-of-degrees generalization -`clausalComparison`, antonymy as scale reversal, and downward-entailingness of -*than*-clauses. All three are the measure-pullback predications of the reified -`Core.Order.Comparison` (`over` at a point standard, `overSet` at a set standard); -`clausalComparison_eq_overSet` / `comparativeSem_positive_eq_over` make that an identity. +`comparativeSem` / `equativeSem`, antonymy as scale reversal, and +downward-entailingness of *than*-clauses. Both binary comparators are +measure-pullback predications of the reified `Core.Order.Comparison` +(`over` at a point standard, `overSet` at a set standard); +`comparativeSem_positive_eq_over` makes that an identity. The set-of-degrees +S-comparative ([hoeksema-1983]) *is* `Comparison.gt.overSet μ` directly — there is +no separate clausal-comparison definition; its properties are stated about `overSet` +here (anti-additivity) and reuse the `Comparison.overSet`/`over` API for the rest. Framework-specific content for [rett-2026] (MAX, ambidirectionality, manner implicature) lives in `Studies/Rett2026.lean`; [hoeksema-1983]'s polarity-asymmetry consumers in `Studies/Hoeksema1983.lean`. @@ -22,13 +25,13 @@ consumers in `Studies/Hoeksema1983.lean`. * `comparativeSem` / `equativeSem` — "A is Adj-er / as-Adj-as B" via a directed measure on a scale. -* `clausalComparison` — set-of-degrees comparative ([hoeksema-1983]), anti-additive in - its standard (`clausalComparison_isAntiAdditive`): the algebraic source of +* `gtOverSet_isAntiAdditive` — the S-comparative `Comparison.gt.overSet μ` + ([hoeksema-1983]) is anti-additive in its standard: the algebraic source of *than*-clause NPI licensing. -* `mem_clausalComparison_iff_subset_Iio` / `clausalComparison_singleton` — the set-of-degrees - comparative as `Set.Iio` interval inclusion (strict mirror of mathlib's - `mem_upperBounds_iff_subset_Iic`), collapsing to the binary comparator at a singleton. -* `clausalComparison_eq_singleton_of_isGreatest` — a than-clause with a greatest degree +* `mem_gtOverSet_iff_subset_Iio` — the set-of-degrees comparative as `Set.Iio` + interval inclusion (strict mirror of mathlib's `mem_upperBounds_iff_subset_Iic`), + collapsing to the binary comparator at a singleton via `Comparison.overSet_singleton`. +* `gtOverSet_eq_singleton_of_isGreatest` — a than-clause with a greatest degree reduces to that degree ([bhatt-pancheva-2004], order-theoretic form). * `taller_shorter_antonymy` — antonymy is argument swap plus direction reversal. * `comparative_iff_posExt_ssubset` — comparison as extent inclusion ([kennedy-1999]). @@ -118,72 +121,43 @@ end Boundary /-! ### Set-of-degrees comparative -The S-comparative `clausalComparison` ([hoeksema-1983] §3.8 Def 7) generalizes -`comparativeSem` from a single standard to an arbitrary degree-set standard. -It needs only `[Preorder D]`. -/ +The S-comparative ([hoeksema-1983] §3.8 Def 7) generalizes `comparativeSem` from a +single standard to an arbitrary degree-set standard. It *is* `Comparison.gt.overSet μ` +(`μ ⁻¹' strictUpperBounds Δ`) — the strict-`>` set-standard predication of +`Core.Order.Comparison` — not a separate definition; the binary comparator is its +singleton case (`Comparison.overSet_singleton`). The properties below are stated +about `Comparison.gt.overSet μ` directly. Needs only `[Preorder D]`. -/ section SetOfDegrees variable {Entity D : Type*} [Preorder D] -/-- S-comparative on a set of degrees ([hoeksema-1983] §3.8 Def 7): -`y ∈ clausalComparison μ Δ` iff `μ y` strictly exceeds every degree in `Δ`. The -than-clause supplies the degree set `Δ` (typically existentially closed). -/ -def clausalComparison (μ : Entity → D) (Δ : Set D) : Set Entity := - fun y => ∀ d ∈ Δ, d < μ y - -/-- **Grounding**: the set-of-degrees comparative is the strict-`>` *set-standard* -predication of `Core.Order.Comparison` (`μ ⁻¹' strictUpperBounds Δ`) — the -fundamental object, with the binary comparator its singleton case -(`Comparison.overSet_singleton`). True by `rfl`: this is not a reinvention. -/ -theorem clausalComparison_eq_overSet (μ : Entity → D) (Δ : Set D) : - clausalComparison μ Δ = Comparison.gt.overSet μ Δ := - rfl - -/-- The set-of-degrees comparative as a strict-interval inclusion: `y` clears the -than-clause iff every standard degree lies strictly below `μ y`. Strict mirror of -mathlib's `mem_upperBounds_iff_subset_Iic`; both faces are `Iff.rfl` siblings. -/ -theorem mem_clausalComparison_iff_subset_Iio (μ : Entity → D) (Δ : Set D) (y : Entity) : - y ∈ clausalComparison μ Δ ↔ Δ ⊆ Set.Iio (μ y) := +/-- The set-of-degrees comparative `Comparison.gt.overSet μ` ([hoeksema-1983]) as a +strict-interval inclusion: `y` clears the than-clause iff every standard degree lies +strictly below `μ y`. Strict mirror of mathlib's `mem_upperBounds_iff_subset_Iic`; +both faces are `Iff.rfl` siblings. -/ +theorem mem_gtOverSet_iff_subset_Iio (μ : Entity → D) (Δ : Set D) (y : Entity) : + y ∈ Comparison.gt.overSet μ Δ ↔ Δ ⊆ Set.Iio (μ y) := Iff.rfl -/-- A than-clause whose denotation is the single degree `d` reduces to the binary -comparator `d < μ y`. Strict mirror of mathlib's -`upperBounds_singleton : upperBounds {a} = Ici a`. -/ -theorem clausalComparison_singleton (μ : Entity → D) (d : D) : - clausalComparison μ {d} = {y | d < μ y} := by - ext y - refine ⟨fun h => h d rfl, ?_⟩ - intro h x hx - rw [Set.mem_singleton_iff] at hx - rw [hx] - exact h - -/-- [hoeksema-1983] Fact 4: the S-comparative is anti-additive in its -set-of-degrees argument — the algebraic source of NPI licensing in clausal -*than*-comparatives. -/ -theorem clausalComparison_isAntiAdditive (μ : Entity → D) : - Entailment.IsAntiAdditive (clausalComparison μ) := +/-- [hoeksema-1983] Fact 4: the S-comparative `Comparison.gt.overSet μ` is +anti-additive in its set-of-degrees argument — the algebraic source of NPI licensing +in clausal *than*-comparatives. -/ +theorem gtOverSet_isAntiAdditive (μ : Entity → D) : + Entailment.IsAntiAdditive (Comparison.gt.overSet μ) := Entailment.isAntiAdditive_forall_mem (fun d y => d < μ y) -/-- Atomic specialization: at the singleton `{μ b}`, S-comparative membership -reduces to the binary "taller than `b`" relation. Corollary of -`clausalComparison_singleton`. -/ -theorem clausalComparison_atomic (μ : Entity → D) (a b : Entity) : - a ∈ clausalComparison μ {μ b} ↔ μ b < μ a := by - simp only [clausalComparison_singleton, Set.mem_setOf_eq] - /-- **Reduction lemma** ([bhatt-pancheva-2004] §3, order-theoretic form): the -S-comparative is determined by the *greatest* element of its degree-set -argument. Needs neither linearity nor density — only `[Preorder D]` and the +S-comparative `Comparison.gt.overSet μ` is determined by the *greatest* element of its +degree-set argument. Needs neither linearity nor density — only `[Preorder D]` and the `IsGreatest` witness. -/ -theorem clausalComparison_eq_singleton_of_isGreatest (μ : Entity → D) {Δ : Set D} +theorem gtOverSet_eq_singleton_of_isGreatest (μ : Entity → D) {Δ : Set D} {m : D} (hm : IsGreatest Δ m) : - clausalComparison μ Δ = clausalComparison μ ({m} : Set D) := by + Comparison.gt.overSet μ Δ = Comparison.gt.overSet μ ({m} : Set D) := by ext y refine ⟨fun h d hd => ?_, fun h d hd => ?_⟩ · rw [Set.mem_singleton_iff] at hd - exact hd ▸ h m hm.1 - · exact lt_of_le_of_lt (hm.2 hd) (h m rfl) + exact hd ▸ h hm.1 + · exact lt_of_le_of_lt (hm.2 hd) (h rfl) end SetOfDegrees @@ -207,12 +181,13 @@ extent complementarity rather than being stipulated. -/ section Extent variable {Entity D : Type*} [LinearOrder D] -/-- Bridge: the atomic S-comparative coincides with the binary `comparativeSem` -on a `LinearOrder`. The set-of-degrees schema strictly generalizes the binary -comparator. -/ -theorem clausalComparison_atomic_eq_comparativeSem (μ : Entity → D) (a b : Entity) : - a ∈ clausalComparison μ {μ b} ↔ comparativeSem μ a b .positive := - clausalComparison_atomic μ a b +/-- Bridge: the atomic S-comparative `Comparison.gt.overSet μ {μ b}` coincides with +the binary `comparativeSem` on a `LinearOrder`. The set-of-degrees schema strictly +generalizes the binary comparator, collapsing at a singleton via +`Comparison.overSet_singleton`. -/ +theorem gtOverSet_atomic_eq_comparativeSem (μ : Entity → D) (a b : Entity) : + a ∈ Comparison.gt.overSet μ {μ b} ↔ comparativeSem μ a b .positive := by + rw [Comparison.overSet_singleton, ← comparativeSem_positive_eq_over] /-- "A is taller than B" iff A's positive extent strictly contains B's ([kennedy-1999]). Bridges the point comparison to `posExt_ssubset_iff`. -/ diff --git a/Linglib/Semantics/Entailment/AntiAdditivity.lean b/Linglib/Semantics/Entailment/AntiAdditivity.lean index b683b6ed6..c8909fd9b 100644 --- a/Linglib/Semantics/Entailment/AntiAdditivity.lean +++ b/Linglib/Semantics/Entailment/AntiAdditivity.lean @@ -232,7 +232,7 @@ end Bridges section ToyWitnesses /-- Any function of the form `fun X y => ∀ x ∈ X, P x y` is anti-additive in -`X`. `npComparative` and `clausalComparison` ([hoeksema-1983]) instantiate this +`X`. `npComparative` and `Comparison.gt.overSet` ([hoeksema-1983]) instantiate this with `P x y := μ x < μ y` and `P d y := d < μ y` respectively. -/ theorem isAntiAdditive_forall_mem {α β : Type*} (P : α → β → Prop) : IsAntiAdditive (fun (X : Set α) (y : β) => ∀ x ∈ X, P x y) := by diff --git a/Linglib/Studies/BhattPancheva2004.lean b/Linglib/Studies/BhattPancheva2004.lean index db9bf98be..7e57bd30d 100644 --- a/Linglib/Studies/BhattPancheva2004.lean +++ b/Linglib/Studies/BhattPancheva2004.lean @@ -74,7 +74,8 @@ open Minimalist.DegreeMovement ScopeBinding IsHeimKennedy not_isHeimKennedy_QP_above_bound_DegP isHeimKennedy_no_dependency isHeimKennedy_dependency_requires_high_DegP williams_scope_correlation williams_exempt_when_no_binding) -open Semantics.Degree (clausalComparison clausalComparison_eq_singleton_of_isGreatest) +open Core.Order (Comparison) +open Semantics.Degree (gtOverSet_eq_singleton_of_isGreatest) open Semantics.Degree.ThanClause (thanClauseDenotation thanClauseMax thanClauseMax_isGreatest) open Typology.PolarityItem (LicensingContext) open Semantics.Polarity.Licensing (contextProperties) @@ -154,14 +155,14 @@ theorem bp_hkc_matches_heim_intensional_data : /-- B&P's clausal-source than-clause denotation `{d | d ≤ μ b}` collapses to the singleton `{μ b}` when fed to the S-comparative. - Direct corollary of `clausalComparison_eq_singleton_of_isGreatest` + Direct corollary of `gtOverSet_eq_singleton_of_isGreatest` instantiated at the than-clause's greatest element (the standard's measure). -/ theorem thanClause_reduces_to_max {D : Type*} [Preorder D] (μ : Entity → D) (b : Entity) : - clausalComparison μ (thanClauseDenotation μ b) = - clausalComparison μ ({μ b} : Set D) := - clausalComparison_eq_singleton_of_isGreatest μ (thanClauseMax_isGreatest μ b) + Comparison.gt.overSet μ (thanClauseDenotation μ b) = + Comparison.gt.overSet μ ({μ b} : Set D) := + gtOverSet_eq_singleton_of_isGreatest μ (thanClauseMax_isGreatest μ b) /-- Combining [hoeksema-1983] §3.9 (the principal-ultrafilter / singleton-degree-set equivalence) with the B&P reduction: @@ -172,8 +173,8 @@ theorem thanClause_reduces_to_max theorem npGQ_principal_eq_sComp_thanClause {D : Type*} [Preorder D] (μ : Entity → D) (b : Entity) : npComparativeGQ μ (principalUltrafilter b) = - clausalComparison μ (thanClauseDenotation μ b) := by - rw [npComparativeGQ_principal_eq_clausalComparison_singleton, + Comparison.gt.overSet μ (thanClauseDenotation μ b) := by + rw [npComparativeGQ_principal_eq_gtOverSet_singleton, ← thanClause_reduces_to_max] -- ════════════════════════════════════════════════════ diff --git a/Linglib/Studies/Gajewski2011.lean b/Linglib/Studies/Gajewski2011.lean index fcb6bf814..05edfd5dd 100644 --- a/Linglib/Studies/Gajewski2011.lean +++ b/Linglib/Studies/Gajewski2011.lean @@ -53,7 +53,7 @@ with "DE + scalar endpoint" (Conjecture 48). Gajewski's headline empirical claim made `decide`-checkable over the Fragment registry. - Hoeksema S-comparative SAA bridge - (`bridge_hoeksema_clausalComparison_strawsonAA`) — the positive test case + (`bridge_hoeksema_gtOverSet_strawsonAA`) — the positive test case for Gajewski's framework: classically AA → strong NPIs predicted ✓. ## §4 framework — both halves now in skeleton @@ -472,7 +472,7 @@ context-dependent truncation à la Chierchia 2004 axiom (i)). Deferred. - [crnic-2014] challenges Strawson-based analyses with a non-monotonicity reanalysis; engages directly with this paper. - [hoeksema-1983] S-comparative is anti-additive (per - `bridge_hoeksema_clausalComparison_strawsonDE` in VonFintel1999) — hence, + `bridge_hoeksema_gtOverSet_strawsonDE` in VonFintel1999) — hence, per the Zwarts-classical theory, predicted to license strong NPIs. Empirically borne out (Hoeksema's data). -/ @@ -604,19 +604,19 @@ theorem only_satisfies_condition2_no_alts (x : World → Prop) : /-! ## Hoeksema S-comparative — the positive test case [hoeksema-1983]'s S-comparative is *classically* anti-additive -(`Semantics/Degree/Comparative.lean::clausalComparison_isAntiAdditive`), +(`Semantics/Degree/Comparative.lean::gtOverSet_isAntiAdditive`), hence by `antiAdditive_implies_strawsonAA` it is also Strawson-AA. This is the **positive test** for Gajewski's framework: an AA operator licenses strong NPIs (Hoeksema's data confirms — "Mary is taller than anyone is", "in years"-style strong NPIs grammatical in than-S comparatives). Contrast vF's recalcitrants which are SAA-but-not-AA and hence don't license strong NPIs. -/ -theorem bridge_hoeksema_clausalComparison_strawsonAA +theorem bridge_hoeksema_gtOverSet_strawsonAA {Entity D : Type*} [Preorder D] (μ : Entity → D) (defined : Set D → Entity → Prop) : - IsStrawsonAntiAdditive (Semantics.Degree.clausalComparison μ) defined := + IsStrawsonAntiAdditive (Core.Order.Comparison.gt.overSet μ) defined := antiAdditive_implies_strawsonAA _ - (Semantics.Degree.clausalComparison_isAntiAdditive μ) _ + (Semantics.Degree.gtOverSet_isAntiAdditive μ) _ /-! ## Strong-NPI registry consistency diff --git a/Linglib/Studies/Hoeksema1983.lean b/Linglib/Studies/Hoeksema1983.lean index 2e1b77252..1f9d27e47 100644 --- a/Linglib/Studies/Hoeksema1983.lean +++ b/Linglib/Studies/Hoeksema1983.lean @@ -42,11 +42,11 @@ and arbitrary `sSup`/`sInf` (strengthening Hoeksema's finitary claim) gives complement preservation for free on `BooleanAlgebra → BooleanAlgebra` homs. -The S-comparative `clausalComparison` (originally [hoeksema-1983] §3.8 -Def 7) and its anti-additivity (Fact 4) live in -`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. +The S-comparative is `Core.Order.Comparison.gt.overSet μ` (originally +[hoeksema-1983] §3.8 Def 7); its anti-additivity (Fact 4, +`gtOverSet_isAntiAdditive`) lives in `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 @@ -54,7 +54,7 @@ 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** (`clausalComparison` in +- **Definition 7/8** (`Comparison.gt.overSet μ`, from `Semantics/Degree/Comparative.lean`): the S-comparative as a set-of-degrees operator. - **Fact 1** (`fact1_agree_on_atoms`): two `>`-preserving functions @@ -68,12 +68,12 @@ The §3 algebraic content is formalized in five layers: - **Fact 3** (`npComparativeGQ_monotone`): every Boolean hom is monotone increasing — disqualifies the NP-comparative as a Ladusaw NPI environment. -- **Fact 4** (`clausalComparison_isAntiAdditive` in +- **Fact 4** (`gtOverSet_isAntiAdditive` in `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_clausalComparison_singleton`): +- **§3.9 NP↔S equivalence** (`npComparativeGQ_principal_eq_gtOverSet_singleton`): on principal ultrafilters / singleton degree sets, the two constructions deliver the same predicate. @@ -95,8 +95,8 @@ namespace Hoeksema1983 open Semantics.Polarity.Licensing open Entailment -open Semantics.Degree (clausalComparison clausalComparison_isAntiAdditive - clausalComparison_atomic) +open Core.Order (Comparison) +open Semantics.Degree (gtOverSet_isAntiAdditive gtOverSet_atomic_eq_comparativeSem) open Typology.PolarityItem (LicensingContext) open Semantics.Polarity.Licensing (contextProperties) @@ -317,14 +317,13 @@ theorem npComparativeGQ_uniqueness {μ : Entity → D} 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. -/ -theorem npComparativeGQ_principal_eq_clausalComparison_singleton +theorem npComparativeGQ_principal_eq_gtOverSet_singleton (μ : Entity → D) (b : Entity) : - npComparativeGQ μ (principalUltrafilter b) = clausalComparison μ {μ b} := by + npComparativeGQ μ (principalUltrafilter b) = Comparison.gt.overSet μ {μ b} := by ext a - unfold npComparativeGQ principalUltrafilter clausalComparison npThreshold - simp only [CompleteLatticeHom.coe_setPreimage, Set.mem_preimage, - Set.mem_setOf_eq, Set.mem_singleton_iff] - refine ⟨fun h d hd => hd ▸ h, fun h => h (μ b) rfl⟩ + unfold npComparativeGQ principalUltrafilter npThreshold + simp only [CompleteLatticeHom.coe_setPreimage, Set.mem_preimage, Set.mem_setOf_eq, + Comparison.overSet_singleton, Comparison.mem_over, Comparison.rel, gt_iff_lt] /-! ## Connection to the licensing-context registry -/ @@ -336,7 +335,7 @@ theorem comparativeNP_signature_monotone : (contextProperties .comparativeNP).strawsonSignature = .mono := rfl /-- The `.comparativeS` registry slot is anti-additive, matching - `clausalComparison_isAntiAdditive`. -/ + `gtOverSet_isAntiAdditive`. -/ theorem comparativeS_signature_anti_additive : (contextProperties .comparativeS).strawsonSignature = .antiAdd := rfl diff --git a/Linglib/Studies/VonFintel1999.lean b/Linglib/Studies/VonFintel1999.lean index 61c3b8f59..6413148f8 100644 --- a/Linglib/Studies/VonFintel1999.lean +++ b/Linglib/Studies/VonFintel1999.lean @@ -491,18 +491,18 @@ theorem bridge_lahiri_glad_settle_overgeneration : /-- **Hoeksema's S-comparative is anti-additive, hence trivially Strawson-DE.** [hoeksema-1983] proves the S-comparative anti-additive - (`Semantics.Degree.clausalComparison_isAntiAdditive`); the + (`Semantics.Degree.gtOverSet_isAntiAdditive`); the inheritance chain AA → DE → Strawson-DE makes the bridge automatic. This places the S-comparative in the same Strawson-DE class as [von-fintel-1999]'s recalcitrants, but with the additional classical AA backing — meaning S-comparatives license *strong* NPIs too (whereas vF's `only` only licenses weak NPIs). -/ -theorem bridge_hoeksema_clausalComparison_strawsonDE +theorem bridge_hoeksema_gtOverSet_strawsonDE {Entity D : Type*} [Preorder D] (μ : Entity → D) (defined : Set D → Entity → Prop) : - IsStrawsonDE (Semantics.Degree.clausalComparison μ) defined := + IsStrawsonDE (Core.Order.Comparison.gt.overSet μ) defined := antitone_implies_strawsonDE _ - (Semantics.Degree.clausalComparison_isAntiAdditive μ).antitone defined + (Semantics.Degree.gtOverSet_isAntiAdditive μ).antitone defined end VonFintel1999