From 2c5b5fa504acd7ec9f0d04dc362084a6735d2f31 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 19 Jun 2026 16:44:47 -0700 Subject: [PATCH] refactor(Semantics/Degree): retire degree-property family + relationalGQ --- Linglib/Core/Order/Comparison.lean | 8 + Linglib/Semantics/Degree/DirectedMeasure.lean | 24 +- Linglib/Semantics/Degree/Predicate.lean | 230 ++++++------------ Linglib/Semantics/Entailment/Extremum.lean | 34 +-- Linglib/Semantics/Measurement/Basic.lean | 6 +- Linglib/Semantics/Numerals/Basic.lean | 105 ++++---- Linglib/Studies/FoxHackl2006Numerals.lean | 13 +- Linglib/Typology/Numeral/Basic.lean | 2 +- 8 files changed, 174 insertions(+), 248 deletions(-) diff --git a/Linglib/Core/Order/Comparison.lean b/Linglib/Core/Order/Comparison.lean index 60fae9d13..287f0986b 100644 --- a/Linglib/Core/Order/Comparison.lean +++ b/Linglib/Core/Order/Comparison.lean @@ -88,6 +88,14 @@ def Comparison.over {E α : Type*} [Preorder α] x ∈ c.over μ n ↔ c.rel (μ x) n := by simp [Comparison.over] +instance Comparison.relDecidable {α : Type*} [Preorder α] [DecidableEq α] [DecidableLE α] + [DecidableLT α] (c : Comparison) (a n : α) : Decidable (c.rel a n) := by + cases c <;> simp only [Comparison.rel, ge_iff_le, gt_iff_lt] <;> infer_instance + +instance Comparison.overDecidable {E α : Type*} [Preorder α] [DecidableEq α] [DecidableLE α] + [DecidableLT α] (c : Comparison) (μ : E → α) (n : α) (x : E) : Decidable (x ∈ c.over μ n) := + decidable_of_iff _ (Comparison.mem_over c μ n x).symm + /-- **Class A/B is interval-endpoint membership.** A non-strict comparison (bare `=`, Class B `≥`/`≤`) keeps the boundary `n`; a strict one (Class A `>`/`<`) drops it — the whole Class A/B distinction diff --git a/Linglib/Semantics/Degree/DirectedMeasure.lean b/Linglib/Semantics/Degree/DirectedMeasure.lean index dbb116647..a583fabd0 100644 --- a/Linglib/Semantics/Degree/DirectedMeasure.lean +++ b/Linglib/Semantics/Degree/DirectedMeasure.lean @@ -16,8 +16,8 @@ degree-domain constructors and epistemic threshold semantics. - `DirectedMeasure`: the bundled measure structure. - `DirectedMeasure.IsLicensed`: endpoint-based licensing via `Boundedness.IsLicensed`. - `DirectedMeasure.degreeProperty`: the degree property derived from - `direction` (`atLeastDeg` positive, `atMostDeg` negative); its maximal - informativity is characterized in `Semantics/Entailment/Extremum.lean`. + `direction` (`Comparison.ge.over` positive, `Comparison.le.over` negative); its + maximal informativity is characterized in `Semantics/Entailment/Extremum.lean`. - `DirectedMeasure.numeral`, `DirectedMeasure.adjective`: Kennedy-style numeral and gradable-adjective domains. @@ -49,10 +49,10 @@ open Core.Order Common algebraic core of the `numeral`/`adjective` domain constructors and epistemic thresholds (`epistemicAsDirectedMeasure`, on - `DirectedMeasure ℚ (E × (W → Bool))`). The degree property (`atLeastDeg` - for positive, `atMostDeg` for negative) is derived from `direction`, not - stored — per [lassiter-goodman-2017], the binary direction choice is the - fundamental parameter. -/ + `DirectedMeasure ℚ (E × (W → Bool))`). The degree property + (`Comparison.ge.over` for positive, `Comparison.le.over` for negative) is + derived from `direction`, not stored — per [lassiter-goodman-2017], the + binary direction choice is the fundamental parameter. -/ structure DirectedMeasure (D : Type*) [LinearOrder D] (E : Type*) extends ComparativeScale D where /-- Measure function: maps entities to degrees on the scale -/ μ : E → D @@ -75,14 +75,14 @@ def IsLicensed (dm : DirectedMeasure D E) : Prop := dm.boundedness.IsLicensed instance (dm : DirectedMeasure D E) : Decidable dm.IsLicensed := inferInstanceAs (Decidable dm.boundedness.IsLicensed) -/-- The degree property derived from the measure's direction: `atLeastDeg` - for positive scales (tall, likely), `atMostDeg` for negative ones +/-- The degree property derived from the measure's direction: `Comparison.ge.over` + for positive scales (tall, likely), `Comparison.le.over` for negative ones (short, unlikely). The derivation the structure docstring promises: `direction` is the stored parameter, the property follows. -/ -def degreeProperty (dm : DirectedMeasure D E) : D → E → Prop := +def degreeProperty (dm : DirectedMeasure D E) : D → Set E := match dm.direction with - | .positive => atLeastDeg dm.μ - | .negative => atMostDeg dm.μ + | .positive => Comparison.ge.over dm.μ + | .negative => Comparison.le.over dm.μ end DirectedMeasure @@ -102,7 +102,7 @@ variable {α : Type*} [LinearOrder α] {W : Type*} /-- [kennedy-2015] numeral domain: "at least n" over cardinality. Closed scale (ℕ well-ordered) → always licensed. - Type-shift to exact = MIP applied to atLeastDeg. -/ + Type-shift to exact = MIP applied to `Comparison.ge.over`. -/ def numeral (μ : W → α) : DirectedMeasure α W := { boundedness := .closed, μ := μ } diff --git a/Linglib/Semantics/Degree/Predicate.lean b/Linglib/Semantics/Degree/Predicate.lean index 869f0abfb..85fc69629 100644 --- a/Linglib/Semantics/Degree/Predicate.lean +++ b/Linglib/Semantics/Degree/Predicate.lean @@ -9,21 +9,22 @@ import Linglib.Core.Order.Comparison # Core/Scales/Predicate.lean — degree predicates + monotonicity [fox-2007] [kennedy-2015] [geurts-nouwen-2007] [nouwen-2010] [partee-1987] -Predicate transformers and degree-relative comparison primitives, parameterized -by a measure function `μ : W → α`: +Predicate transformers over a measure function `μ : W → α`: - `IsUpwardMonotone` / `IsDownwardMonotone` / `IsConstant` / `AdmitsOptimum` -- `eqDeg` / `atLeastDeg` / `moreThanDeg` / `atMostDeg` / `lessThanDeg` (Fox 2007 §2) -- `relationalGQ` (unified Kennedy 2015 GQ denotation) - `typeLower` (Partee 1987 existential lowering) -- Anti-Horn-scale lemmas (general) +- monotonicity / anti-Horn-scale lemmas about the `Core.Order.Comparison.over` + degree predicates (general) + +The five degree predicates ("exactly", "at least", "more than", "at most", +"less than") are `Core.Order.Comparison.{eq,ge,gt,le,lt}.over μ` directly: the +reified `Core.Order.Comparison` IS the canonical scale-comparison primitive, so +there is no separate named family. `c.over μ n` is a `Set W`; `w ∈ c.over μ n ↔ +c.rel (μ w) n` (`Comparison.mem_over`), and `c.rel` unfolds to the order +relation per case. This file is part of the Phase A decomposition of the legacy `Core/Scales/Scale.lean` dumping ground (master plan v4). - -`relationalGQ` stays here as the canonical scale-comparison primitive: it is -domain-general (numerals, measure phrases, and gradable comparatives all reduce -to it), and the reified `Core.Order.Comparison` interprets into it. -/ namespace Semantics.Degree @@ -118,55 +119,37 @@ theorem open_notLicensed : ¬ Boundedness.open_.IsLicensed := id -- § 6. Degree Properties ([fox-2007] §2) -- ════════════════════════════════════════════════════ -/-! ### Degree properties for comparison relations +/-! ### Degree properties as `Comparison.over` -Five degree properties covering all comparison relations, parameterized by -a measure function `μ : W → α`. These are the building blocks for the named -numeral meanings (`Semantics.Numerals.atLeastMeaning` etc.) and degree -question semantics. +The five degree predicates covering all comparison relations are +`Core.Order.Comparison.{eq,ge,gt,le,lt}.over μ` directly — there is no separate +named family. `c.over μ d : Set W`, with `w ∈ c.over μ d ↔ c.rel (μ w) d` +(`Comparison.mem_over`). These are the building blocks for the named numeral +meanings (`Semantics.Numerals.atLeastMeaning` etc.) and degree question +semantics. -- `atLeastDeg`: closed `≥`, always has max⊨ -- `moreThanDeg`: open `>`, fails on dense scales -- `eqDeg`: equality `=`, trivially has max⊨ -- `atMostDeg`: closed `≤` -- `lessThanDeg`: open `<` +- `Comparison.ge.over μ`: closed `≥`, always has max⊨ +- `Comparison.gt.over μ`: open `>`, fails on dense scales +- `Comparison.eq.over μ`: equality `=`, trivially has max⊨ +- `Comparison.le.over μ`: closed `≤` +- `Comparison.lt.over μ`: open `<` The key divergence: on ℕ, `>` collapses to `≥` with successor, so both have `HasMaxInf`. On dense scales, `>` yields an open set with no max⊨. This is the UDM prediction ([fox-2007] §2). -/ -/-- Degree property for "exactly d": the measure at w equals d. -/ -abbrev eqDeg {W : Type*} (μ : W → α) : α → W → Prop := - Comparison.eq.over μ - -/-- Degree property for "at least d": the measure at w meets or exceeds d. -/ -abbrev atLeastDeg {W : Type*} (μ : W → α) : α → W → Prop := - Comparison.ge.over μ - -/-- Degree property for "more than d": the measure strictly exceeds d. -/ -abbrev moreThanDeg {W : Type*} (μ : W → α) : α → W → Prop := - Comparison.gt.over μ - -/-- Degree property for "at most d": the measure at w is at most d. -/ -abbrev atMostDeg {W : Type*} (μ : W → α) : α → W → Prop := - Comparison.le.over μ - -/-- Degree property for "less than d": the measure is strictly less than d. -/ -abbrev lessThanDeg {W : Type*} (μ : W → α) : α → W → Prop := - Comparison.lt.over μ - /-- "At least" is downward monotone: weaker thresholds are easier to satisfy. -/ -theorem atLeastDeg_downMono {W : Type*} (μ : W → α) : IsDownwardMonotone (atLeastDeg μ) := +theorem geOver_downMono {W : Type*} (μ : W → α) : IsDownwardMonotone (Comparison.ge.over μ) := fun _ _ hxy _ hy => le_trans hxy hy /-- "More than" is downward monotone: weaker thresholds are easier to satisfy. -/ -theorem moreThanDeg_downMono {W : Type*} (μ : W → α) : IsDownwardMonotone (moreThanDeg μ) := +theorem gtOver_downMono {W : Type*} (μ : W → α) : IsDownwardMonotone (Comparison.gt.over μ) := fun _ _ hxy _ hy => lt_of_le_of_lt hxy hy /-- On ℕ, `>` collapses to `≥` with successor: "more than m" ↔ "at least m+1". This is the discrete equivalence that density breaks. -/ -theorem moreThan_eq_atLeast_succ {W : Type*} (μ : W → ℕ) (m : ℕ) (w : W) : - moreThanDeg μ m w ↔ atLeastDeg μ (m + 1) w := +theorem gtOver_eq_geOver_succ {W : Type*} (μ : W → ℕ) (m : ℕ) (w : W) : + w ∈ Comparison.gt.over μ m ↔ w ∈ Comparison.ge.over μ (m + 1) := Iff.rfl /-! IsMaxInf-flavored consequences of these degree predicates @@ -184,7 +167,7 @@ theorem moreThan_eq_atLeast_succ {W : Type*} (μ : W → ℕ) (m : ℕ) (w : W) [partee-1987]'s BE + iota + existential closure, applied to a degree property: from an exact reading `exact d w` ("the measure equals `d`"), existentially close to `∃ d' ≥ d, exact d' w`. On any reflexive linear -order this collapses to `atLeastDeg μ d w` — witness `d' := μ w`. +order this collapses to `Comparison.ge.over μ d w` — witness `d' := μ w`. This is the formal content of [kennedy-2015]'s "de-Fregean" derivation of the lower-bound numeral reading from the exact reading. The collapse @@ -196,108 +179,32 @@ generalizes Numeral type-shifting to arbitrary scales. -/ def typeLower {W : Type*} (exact : α → W → Prop) (d : α) (w : W) : Prop := ∃ d', d' ≥ d ∧ exact d' w -/-- **Type-shift collapse**: `typeLower (eqDeg μ) = atLeastDeg μ`. -/ -theorem typeLower_eqDeg_iff {W : Type*} (μ : W → α) (d : α) (w : W) : - typeLower (eqDeg μ) d w ↔ atLeastDeg μ d w := by +/-- **Type-shift collapse**: existentially lowering the exact property + `Comparison.eq.over μ` yields the lower-bound property `Comparison.ge.over μ`. -/ +theorem typeLower_eqOver_iff {W : Type*} (μ : W → α) (d : α) (w : W) : + typeLower (fun d' w => w ∈ Comparison.eq.over μ d') d w ↔ w ∈ Comparison.ge.over μ d := by + simp only [Comparison.mem_over, Comparison.rel, typeLower, ge_iff_le] refine ⟨?_, fun h => ⟨μ w, h, rfl⟩⟩ rintro ⟨d', hd', heq⟩ - -- heq : eqDeg μ d' w unfolds to μ w = d' - have heq' : μ w = d' := heq - show μ w ≥ d - exact heq'.symm ▸ hd' - -instance atLeastDeg.decidable {W : Type*} [DecidableLE α] (μ : W → α) - (d : α) (w : W) : Decidable (atLeastDeg μ d w) := - inferInstanceAs (Decidable (d ≤ μ w)) - -instance atMostDeg.decidable {W : Type*} [DecidableLE α] (μ : W → α) - (d : α) (w : W) : Decidable (atMostDeg μ d w) := - inferInstanceAs (Decidable (μ w ≤ d)) - -instance moreThanDeg.decidable {W : Type*} [DecidableLT α] (μ : W → α) - (d : α) (w : W) : Decidable (moreThanDeg μ d w) := - inferInstanceAs (Decidable (d < μ w)) - -instance lessThanDeg.decidable {W : Type*} [DecidableLT α] (μ : W → α) - (d : α) (w : W) : Decidable (lessThanDeg μ d w) := - inferInstanceAs (Decidable (μ w < d)) - -instance eqDeg.decidable {W : Type*} [DecidableEq α] (μ : W → α) - (d : α) (w : W) : Decidable (eqDeg μ d w) := - inferInstanceAs (Decidable (μ w = d)) - -instance typeLower_eqDeg.decidable {W : Type*} (μ : W → α) (d : α) (w : W) : - Decidable (typeLower (eqDeg μ) d w) := - decidable_of_iff _ (typeLower_eqDeg_iff μ d w).symm + exact heq.symm ▸ hd' -- ════════════════════════════════════════════════════ -- § 6d. [kennedy-2015]'s De-Fregean GQ -- ════════════════════════════════════════════════════ -/-! ## A unified GQ denotation parameterized by the comparison relation +/-! ## A unified GQ denotation via `Core.Order.Comparison` [kennedy-2015] proposes a single denotation for modified and unmodified numerals: `λP. max{d | #P ≥ d} REL m`, where the only parameter distinguishing surface forms is the relation `REL ∈ {=, ≥, >, ≤, <}`. -Specialised to a property of the form `atLeastDeg μ`, the maximum degree -satisfying `atLeastDeg μ d w` is `μ w` itself, so Kennedy's denotation -collapses to `rel (μ w) m` — captured here as `relationalGQ rel μ m w`. - -The five existing degree properties (`eqDeg`, `atLeastDeg`, `moreThanDeg`, -`atMostDeg`, `lessThanDeg`) are definitionally `relationalGQ` instantiated at -the corresponding relation. The Class A vs Class B distinction -([geurts-nouwen-2007], [nouwen-2010]) collapses to a structural -property of `rel`: Class B ↔ `IsRefl α rel`; Class A ↔ `IsIrrefl α rel`. - -This is the canonical comparison primitive of the scale substrate; the reified -`Core.Order.Comparison` (in `Comparison.lean`) selects which `rel` to use. -/ - -/-- Kennedy's unified GQ denotation: `(rel) (μ w) d`. The five named degree - properties are definitionally equal to instantiations of this. -/ -def relationalGQ {W : Type*} (rel : α → α → Prop) (μ : W → α) (d : α) (w : W) : Prop := - rel (μ w) d - -/-- Specialisation to `(· = ·)` recovers `eqDeg`. -/ -theorem relationalGQ_eq_eqDeg {W : Type*} (μ : W → α) : - relationalGQ (· = ·) μ = eqDeg μ := rfl - -/-- Specialisation to `(· ≥ ·)` recovers `atLeastDeg`. -/ -theorem relationalGQ_ge_eq_atLeastDeg {W : Type*} (μ : W → α) : - relationalGQ (· ≥ ·) μ = atLeastDeg μ := rfl - -/-- Specialisation to `(· > ·)` recovers `moreThanDeg`. -/ -theorem relationalGQ_gt_eq_moreThanDeg {W : Type*} (μ : W → α) : - relationalGQ (· > ·) μ = moreThanDeg μ := rfl - -/-- Specialisation to `(· ≤ ·)` recovers `atMostDeg`. -/ -theorem relationalGQ_le_eq_atMostDeg {W : Type*} (μ : W → α) : - relationalGQ (· ≤ ·) μ = atMostDeg μ := rfl - -/-- Specialisation to `(· < ·)` recovers `lessThanDeg`. -/ -theorem relationalGQ_lt_eq_lessThanDeg {W : Type*} (μ : W → α) : - relationalGQ (· < ·) μ = lessThanDeg μ := rfl - -omit [LinearOrder α] in -/-- **Class B inclusion at the boundary** (general). If `rel` is reflexive, - Kennedy's GQ holds at any world `w` whose measure equals the boundary `d`. - Specialised to numerals: "at least 3" / "at most 3" hold at `w = 3`. -/ -theorem relationalGQ_refl_at_boundary {W : Type*} {rel : α → α → Prop} - [Std.Refl rel] (μ : W → α) {d : α} {w : W} (h : μ w = d) : - relationalGQ rel μ d w := by - show rel (μ w) d - rw [h]; exact Std.Refl.refl _ - -omit [LinearOrder α] in -/-- **Class A exclusion at the boundary** (general). If `rel` is irreflexive, - Kennedy's GQ fails at any world `w` whose measure equals the boundary `d`. - Specialised to numerals: "more than 3" / "fewer than 3" fail at `w = 3`. -/ -theorem relationalGQ_irrefl_at_boundary {W : Type*} {rel : α → α → Prop} - [Std.Irrefl rel] (μ : W → α) {d : α} {w : W} (h : μ w = d) : - ¬ relationalGQ rel μ d w := by - intro hk - have hdd : rel d d := h ▸ (hk : rel (μ w) d) - exact (Std.Irrefl.irrefl (r := rel) d) hdd +Specialised to a property of the form `Comparison.ge.over μ`, the maximum degree +satisfying `Comparison.ge.over μ d w` is `μ w` itself, so Kennedy's denotation +collapses to `c.rel (μ w) m` — i.e. `w ∈ c.over μ m` (`Comparison.mem_over`). +The reified `Core.Order.Comparison` (in `Comparison.lean`) IS this canonical +comparison primitive; it selects which `rel`/`interval` to use, and the Class +A vs Class B distinction ([geurts-nouwen-2007], [nouwen-2010]) is its +`Comparison.boundary_mem` (non-strict comparisons keep the endpoint). -/ -- ════════════════════════════════════════════════════ -- § 6e. Anti-Horn-Scale Lemmas (general) @@ -313,53 +220,62 @@ downward monotonicity. Kennedy's unified GQ accommodates both modifier directions without needing a Horn scale at all. The lemmas below state the failure-of-monotonicity and weakness-vs-exact -results purely in terms of `eqDeg` / `atLeastDeg` / `moreThanDeg` — -independent of any specific scale. The Nat-specific results in -`Semantics/Numerals/Basic.lean` are immediate corollaries. -/ +results purely in terms of `Comparison.{eq,ge,gt}.over` — independent of any +specific scale. The Nat-specific results in `Semantics/Numerals/Basic.lean` +are immediate corollaries. -/ /-- "More than `d`" and "exactly `d`" are disjoint (general). -/ -theorem moreThanDeg_disjoint_eqDeg {W : Type*} (μ : W → α) (d : α) (w : W) : - ¬ (eqDeg μ d w ∧ moreThanDeg μ d w) := by +theorem gtOver_disjoint_eqOver {W : Type*} (μ : W → α) (d : α) (w : W) : + ¬ (w ∈ Comparison.eq.over μ d ∧ w ∈ Comparison.gt.over μ d) := by + simp only [Comparison.mem_over, Comparison.rel, gt_iff_lt] rintro ⟨h₁, h₂⟩ exact lt_irrefl d (h₁ ▸ h₂) /-- "Less than `d`" and "exactly `d`" are disjoint (general). -/ -theorem lessThanDeg_disjoint_eqDeg {W : Type*} (μ : W → α) (d : α) (w : W) : - ¬ (eqDeg μ d w ∧ lessThanDeg μ d w) := by +theorem ltOver_disjoint_eqOver {W : Type*} (μ : W → α) (d : α) (w : W) : + ¬ (w ∈ Comparison.eq.over μ d ∧ w ∈ Comparison.lt.over μ d) := by + simp only [Comparison.mem_over, Comparison.rel] rintro ⟨h₁, h₂⟩ exact lt_irrefl d (h₁ ▸ h₂) /-- Bare exact meaning entails "at least" (general half of Class B inclusion). -/ -theorem eqDeg_imp_atLeastDeg {W : Type*} (μ : W → α) (d : α) (w : W) : - eqDeg μ d w → atLeastDeg μ d w := fun h => h ▸ le_refl _ +theorem eqOver_imp_geOver {W : Type*} (μ : W → α) (d : α) (w : W) : + w ∈ Comparison.eq.over μ d → w ∈ Comparison.ge.over μ d := by + simp only [Comparison.mem_over, Comparison.rel, ge_iff_le] + exact fun h => h ▸ le_refl _ /-- Bare exact meaning entails "at most" (general; symmetric to above). -/ -theorem eqDeg_imp_atMostDeg {W : Type*} (μ : W → α) (d : α) (w : W) : - eqDeg μ d w → atMostDeg μ d w := fun h => h ▸ le_refl _ +theorem eqOver_imp_leOver {W : Type*} (μ : W → α) (d : α) (w : W) : + w ∈ Comparison.eq.over μ d → w ∈ Comparison.le.over μ d := by + simp only [Comparison.mem_over, Comparison.rel] + exact fun h => h ▸ le_refl _ /-- "At least `d`" is strictly weaker than "exactly `d`" (general). Given a witness world `w` with `μ w = d'` where `d < d'`, "at least `d`" holds but "exactly `d`" fails. -/ -theorem atLeastDeg_strictly_weaker_than_eqDeg {W : Type*} (μ : W → α) +theorem geOver_strictly_weaker_than_eqOver {W : Type*} (μ : W → α) {d d' : α} (hlt : d < d') {w : W} (hμ : μ w = d') : - atLeastDeg μ d w ∧ ¬ eqDeg μ d w := by + w ∈ Comparison.ge.over μ d ∧ w ∉ Comparison.eq.over μ d := by + simp only [Comparison.mem_over, Comparison.rel, ge_iff_le] refine ⟨?_, ?_⟩ - · show μ w ≥ d; rw [hμ]; exact le_of_lt hlt - · show ¬ μ w = d; rw [hμ]; exact ne_of_gt hlt + · rw [hμ]; exact le_of_lt hlt + · rw [hμ]; exact ne_of_gt hlt -/-- Exact `eqDeg` is **not upward-monotone** (general). Given two distinct +/-- Exact equality is **not upward-monotone** (general). Given two distinct boundary values `d ≤ d'` and a witness world with `μ w = d`, the universal "if exact at `d` then exact at `d'`" fails — `μ w` cannot equal both. -/ -theorem eqDeg_not_upward_monotone {W : Type*} (μ : W → α) +theorem eqOver_not_upward_monotone {W : Type*} (μ : W → α) {d d' : α} (hne : d ≠ d') (hle : d ≤ d') {w : W} (hμ : μ w = d) : - ¬ ∀ x y, x ≤ y → eqDeg μ x w → eqDeg μ y w := by + ¬ ∀ x y, x ≤ y → w ∈ Comparison.eq.over μ x → w ∈ Comparison.eq.over μ y := by + simp only [Comparison.mem_over, Comparison.rel] intro h exact hne ((h d d' hle hμ).symm.trans hμ).symm -/-- Exact `eqDeg` is **not downward-monotone** (general). Symmetric to above. -/ -theorem eqDeg_not_downward_monotone {W : Type*} (μ : W → α) +/-- Exact equality is **not downward-monotone** (general). Symmetric to above. -/ +theorem eqOver_not_downward_monotone {W : Type*} (μ : W → α) {d d' : α} (hne : d ≠ d') (hle : d' ≤ d) {w : W} (hμ : μ w = d) : - ¬ ∀ x y, y ≤ x → eqDeg μ x w → eqDeg μ y w := by + ¬ ∀ x y, y ≤ x → w ∈ Comparison.eq.over μ x → w ∈ Comparison.eq.over μ y := by + simp only [Comparison.mem_over, Comparison.rel] intro h exact hne ((h d d' hle hμ).symm.trans hμ).symm @@ -377,10 +293,10 @@ theorem distinct_no_universal_witness {α : Type*} (k₁ k₂ : α) (hne : k₁ -- ════════════════════════════════════════════════════ /-- "At most" is upward monotone: larger thresholds are easier to satisfy. -/ -theorem atMostDeg_upMono {W : Type*} (μ : W → α) : IsUpwardMonotone (atMostDeg μ) := +theorem leOver_upMono {W : Type*} (μ : W → α) : IsUpwardMonotone (Comparison.le.over μ) := fun _ _ hxy _ hy => le_trans hy hxy -/-! IsMaxInf-flavored consequences of `atMostDeg` (`atMost_hasMaxInf`, +/-! IsMaxInf-flavored consequences of "at most" (`atMost_hasMaxInf`, `isMaxInf_atMost_iff_eq`) live in `Semantics/Entailment/Extremum.lean`. -/ diff --git a/Linglib/Semantics/Entailment/Extremum.lean b/Linglib/Semantics/Entailment/Extremum.lean index 0116c7679..12d7fca9b 100644 --- a/Linglib/Semantics/Entailment/Extremum.lean +++ b/Linglib/Semantics/Entailment/Extremum.lean @@ -60,6 +60,7 @@ not their primary formulation. namespace Entailment open Semantics.Degree +open Core.Order (Comparison) variable {α : Type*} [LinearOrder α] -- ════════════════════════════════════════════════════ @@ -133,11 +134,10 @@ def MIP_LicensedDown {W : Type*} (P : α → W → Prop) : Prop := -- § 4. Degree-predicate IsMaxInf characterizations -- ════════════════════════════════════════════════════ -/-! Migrated from `Core/Scales/Scale.lean`: applications of `IsMaxInf` to - the canonical degree predicates `atLeastDeg`, `moreThanDeg`, `atMostDeg` - (defined in Scale.lean, monotonicity proven there). The pure scale - theory stays in Scale.lean; the IsMaxInf-flavored consequences live - here as a downstream entailment-theoretic application. -/ +/-! Applications of `IsMaxInf` to the canonical degree predicates + `Comparison.{ge,gt,le}.over` (defined in `Core/Order/Comparison.lean`, + monotonicity in `Semantics/Degree/Predicate.lean`). The IsMaxInf-flavored + consequences live here as a downstream entailment-theoretic application. -/ /-- "At least d" always has a maximally informative element: d₀ = μ(w). @@ -149,7 +149,7 @@ def MIP_LicensedDown {W : Type*} (P : α → W → Prop) : Prop := of scale density: the `≥` relation creates a closed set with a natural maximum at the true value. -/ theorem atLeast_hasMaxInf {W : Type*} (μ : W → α) (w : W) : - HasMaxInf (atLeastDeg μ) w := + HasMaxInf (Comparison.ge.over μ) w := ⟨μ w, le_refl _, fun _ hd _ hw' => le_trans hd hw'⟩ /-- **Implicature asymmetry** ([fox-2007], [fox-hackl-2006]): @@ -163,7 +163,7 @@ theorem atLeast_hasMaxInf {W : Type*} (μ : W → α) (w : W) : possible world. -/ theorem moreThan_noMaxInf {W : Type*} [DenselyOrdered α] (μ : W → α) (hSurj : Function.Surjective μ) (w : W) : - ¬ HasMaxInf (moreThanDeg μ) w := by + ¬ HasMaxInf (Comparison.gt.over μ) w := by intro ⟨d₀, hd₀, hent⟩ obtain ⟨d', hd₀d', hd'w⟩ := DenselyOrdered.dense d₀ (μ w) hd₀ obtain ⟨m, hd₀m, hmd'⟩ := DenselyOrdered.dense d₀ d' hd₀d' @@ -177,7 +177,7 @@ theorem moreThan_noMaxInf {W : Type*} [DenselyOrdered α] (μ : W → α) actually used in the proof. -/ theorem isMaxInf_atLeast_of_hit {W : Type*} (μ : W → α) (m : α) (w : W) (hHit : ∃ w', μ w' = m) : - IsMaxInf (atLeastDeg μ) m w ↔ μ w = m := by + IsMaxInf (Comparison.ge.over μ) m w ↔ μ w = m := by constructor · intro ⟨hge, hent⟩ obtain ⟨w_m, hw_m⟩ := hHit @@ -192,13 +192,13 @@ theorem isMaxInf_atLeast_of_hit {W : Type*} (μ : W → α) (m : α) (w : W) equals m, under full surjectivity. Corollary of `isMaxInf_atLeast_of_hit`. -/ theorem isMaxInf_atLeast_iff_eq {W : Type*} (μ : W → α) (m : α) (w : W) (hSurj : Function.Surjective μ) : - IsMaxInf (atLeastDeg μ) m w ↔ μ w = m := + IsMaxInf (Comparison.ge.over μ) m w ↔ μ w = m := isMaxInf_atLeast_of_hit μ m w (hSurj m) /-- On ℕ, "more than m" has `HasMaxInf`: the discrete collapse rescues maximality. Contrast with `moreThan_noMaxInf`: on dense scales, `HasMaxInf` fails. -/ theorem moreThan_nat_hasMaxInf {W : Type*} (μ : W → ℕ) (w : W) - (hw : moreThanDeg μ 0 w) : HasMaxInf (moreThanDeg μ) w := by + (hw : w ∈ Comparison.gt.over μ 0) : HasMaxInf (Comparison.gt.over μ) w := by refine ⟨μ w - 1, ?_, fun d hd w' hw' => ?_⟩ · have : μ w > 0 := hw; show μ w > μ w - 1; omega · have : μ w' > μ w - 1 := hw'; have : μ w > d := hd; show μ w' > d; omega @@ -206,7 +206,7 @@ theorem moreThan_nat_hasMaxInf {W : Type*} (μ : W → ℕ) (w : W) /-- "At most d" always has a maximally informative element: d₀ = μ(w). Symmetric to `atLeast_hasMaxInf`. -/ theorem atMost_hasMaxInf {W : Type*} (μ : W → α) (w : W) : - HasMaxInf (atMostDeg μ) w := + HasMaxInf (Comparison.le.over μ) w := ⟨μ w, le_refl _, fun _ hd _ hw' => le_trans hw' hd⟩ /-- **Kennedy / [rouillard-2026] bridge**: `IsMaxInf` of "at most d" at @@ -215,7 +215,7 @@ theorem atMost_hasMaxInf {W : Type*} (μ : W → α) (w : W) : just as it does from "at least". -/ theorem isMaxInf_atMost_iff_eq {W : Type*} (μ : W → α) (m : α) (w : W) (hSurj : Function.Surjective μ) : - IsMaxInf (atMostDeg μ) m w ↔ μ w = m := by + IsMaxInf (Comparison.le.over μ) m w ↔ μ w = m := by constructor · intro ⟨hle, hent⟩ obtain ⟨w_m, hw_m⟩ := hSurj m @@ -238,21 +238,21 @@ theorem isMaxInf_atMost_iff_eq {W : Type*} (μ : W → α) (m : α) (w : W) /-- MIP derives exact meaning from "at least" (Kennedy's direction). -/ theorem mip_atLeast_is_exact {W : Type*} (μ : W → α) (m : α) (w : W) (hSurj : Function.Surjective μ) : - IsMaxInf (atLeastDeg μ) m w ↔ eqDeg μ m w := - isMaxInf_atLeast_iff_eq μ m w hSurj + IsMaxInf (Comparison.ge.over μ) m w ↔ w ∈ Comparison.eq.over μ m := by + rw [isMaxInf_atLeast_iff_eq μ m w hSurj, Comparison.mem_over, Comparison.rel] /-- MIP derives exact meaning from "at most" (Rouillard's direction). -/ theorem mip_atMost_is_exact {W : Type*} (μ : W → α) (m : α) (w : W) (hSurj : Function.Surjective μ) : - IsMaxInf (atMostDeg μ) m w ↔ eqDeg μ m w := - isMaxInf_atMost_iff_eq μ m w hSurj + IsMaxInf (Comparison.le.over μ) m w ↔ w ∈ Comparison.eq.over μ m := by + rw [isMaxInf_atMost_iff_eq μ m w hSurj, Comparison.mem_over, Comparison.rel] /-- The MIP is direction-invariant: "at least" and "at most" yield the same exact meaning under maximal informativity. Kennedy's type-shift and Rouillard's MIP are literally the same operation. -/ theorem mip_direction_invariant {W : Type*} (μ : W → α) (m : α) (w : W) (hSurj : Function.Surjective μ) : - IsMaxInf (atLeastDeg μ) m w ↔ IsMaxInf (atMostDeg μ) m w := by + IsMaxInf (Comparison.ge.over μ) m w ↔ IsMaxInf (Comparison.le.over μ) m w := by rw [mip_atLeast_is_exact μ m w hSurj, mip_atMost_is_exact μ m w hSurj] /-! ### The bundled form: `DirectedMeasure.degreeProperty` diff --git a/Linglib/Semantics/Measurement/Basic.lean b/Linglib/Semantics/Measurement/Basic.lean index ad392e0d0..6530da3ce 100644 --- a/Linglib/Semantics/Measurement/Basic.lean +++ b/Linglib/Semantics/Measurement/Basic.lean @@ -317,7 +317,7 @@ realization (`∃ e, μ(e) = n`) rather than full surjectivity. Mass nouns realize every n ∈ ℚ≥0 (rice is uniformly divisible by hypothesis); count nouns realize only n ∈ ℕ. -/ -open Semantics.Degree (atLeastDeg) +open Core.Order (Comparison) open Entailment (IsMaxInf HasMaxInf) /-- For a measure function μ on ℚ: when n is realized by some entity, the @@ -328,14 +328,14 @@ Bridges Scontras's exact measure-term meaning with the `max{n | ...} = n` form of Kennedy's de-Fregean analysis. -/ theorem scontras_kennedy_dense {E : Type*} (μ : MeasureFn E) (n : ℚ) (x : E) (hHit : ∃ e, μ.apply e = n) : - IsMaxInf (atLeastDeg μ.apply) n x ↔ μ.apply x = n := + IsMaxInf (Comparison.ge.over μ.apply) n x ↔ μ.apply x = n := Entailment.isMaxInf_atLeast_of_hit μ.apply n x hHit /-- For a cardinality function on ℕ: same point-realization equivalence. *Formalization-internal observation* — see the prose above. -/ theorem scontras_kennedy_card {E : Type*} (cardFn : E → ℕ) (n : ℕ) (x : E) (hHit : ∃ e, cardFn e = n) : - IsMaxInf (atLeastDeg cardFn) n x ↔ cardFn x = n := + IsMaxInf (Comparison.ge.over cardFn) n x ↔ cardFn x = n := Entailment.isMaxInf_atLeast_of_hit cardFn n x hHit -- ============================================================================ diff --git a/Linglib/Semantics/Numerals/Basic.lean b/Linglib/Semantics/Numerals/Basic.lean index 57d3b397e..55b839708 100644 --- a/Linglib/Semantics/Numerals/Basic.lean +++ b/Linglib/Semantics/Numerals/Basic.lean @@ -14,10 +14,10 @@ import Mathlib.Order.Interval.Set.Basic The numeral surface forms ("three", "more than three", "at least three", "at most three", "fewer than three") are five `Nat`-instantiations of [kennedy-2015]'s unified de-Fregean GQ -`λP. max{d | #P ≥ d} REL m`, captured in `Semantics.Degree.relationalGQ`. Each named -meaning is the corresponding `Semantics.Degree.{...}Deg id` specialization, and so -inherits the scale infrastructure (maximal informativity, monotonicity, -density) by construction. +`λP. max{d | #P ≥ d} REL m`, captured by `Core.Order.Comparison.over`. Each named +meaning is the corresponding `Core.Order.Comparison.{eq,gt,lt,ge,le}.over id` +specialization, and so inherits the scale infrastructure (maximal informativity, +monotonicity, density) by construction. The only theory disagreement is the bare-numeral semantics: @@ -28,14 +28,13 @@ The only theory disagreement is the bare-numeral semantics: Modified numerals are theory-independent — everyone agrees "more than 3" means `> 3`. The Class A / Class B distinction ([geurts-nouwen-2007], -[nouwen-2010]) reduces to reflexivity vs irreflexivity of the modifier's -underlying relation; see `Semantics.Degree.relationalGQ_refl_at_boundary` and -`Semantics.Degree.relationalGQ_irrefl_at_boundary`. +[nouwen-2010]) reduces to whether the modifier's comparison keeps its +interval endpoint; see `Core.Order.Comparison.boundary_mem`. ## Sections 1. Modifier classification (Class A/B, Bound direction) -2. Numeral meaning functions (5 `def`s over `Semantics.Degree.{...}Deg id`) +2. Numeral meaning functions (5 `def`s over `Core.Order.Comparison.{...}.over id`) 3. `BareNumeral`; `Comparison` interpretation (`Entry.denoteUnder`) 4. Alternative sets (Kennedy §4.1) 5. Class A/B corollaries, anti-Horn-scale corollaries @@ -59,15 +58,18 @@ numerals — a descriptive split due to [nouwen-2010]. Truth-conditionally the split is the reflexive/irreflexive boundary behavior: Class A EXCLUDES the bare-numeral world, Class B INCLUDES it (Class B iff the -underlying relation is reflexive; see `Semantics.Degree.relationalGQ_refl_at_boundary` -and `Core.Order.Comparison.boundary_mem`). The further claim that this predicts +comparison's interval keeps its endpoint; see +`Core.Order.Comparison.boundary_mem`). The further claim that this predicts a *categorical* ignorance-implicature pattern (Class B carries ignorance, Class A not) is contested: [schwarz-buccola-hamilton-2012] show *at most* and *up to* dissociate (so "Class B" is not one class), and [cremers-coppock-dotlacil-roelofsen-2022] find the ignorance contrast graded and QUD-dependent rather than categorical; [enguehard-2018] derives comparative-numeral inferences from granularity scales rather than from the -strict/non-strict relation type. -/ +strict/non-strict relation type. + +Truth-conditionally the split is `Core.Order.Comparison.boundary_mem` (the +non-strict comparison's interval keeps its endpoint). -/ inductive ModifierClass where | classA -- strict: >, < | classB -- non-strict: ≥, ≤ @@ -87,31 +89,31 @@ inductive BoundDirection where -- ============================================================================ /-! Five named meanings — one per surface form. Each is the `id`-instantiation -of the corresponding `Semantics.Degree` degree property. They capture +of the corresponding `Core.Order.Comparison.over` degree property. They capture [kennedy-2015]'s ⟦modifier m⟧ = λP. max{d | #P ≥ d} REL m where `n` plays the role of `max{d | #P ≥ d}` and `m` is the numeral. `bareMeaning` is the exact (Kennedy) reading; the lower-bound (Horn) reading -of bare numerals is `atLeastMeaning`. Grounding in `Semantics.Degree` makes the -density predictions (`atLeastDeg_downMono`, `moreThan_noMaxInf`, +of bare numerals is `atLeastMeaning`. Grounding in `Comparison.over` makes the +density predictions (`geOver_downMono`, `moreThan_noMaxInf`, `atLeast_hasMaxInf`, etc.) hold by construction. -/ /-- Bare numeral meaning (exact reading): `n = m`. -/ -def bareMeaning : Nat → Nat → Prop := Semantics.Degree.eqDeg id +def bareMeaning : Nat → Nat → Prop := fun m n => n ∈ Core.Order.Comparison.eq.over id m /-- "More than `m`": `n > m`. -/ -def moreThanMeaning : Nat → Nat → Prop := Semantics.Degree.moreThanDeg id +def moreThanMeaning : Nat → Nat → Prop := fun m n => n ∈ Core.Order.Comparison.gt.over id m /-- "Fewer than `m`": `n < m`. -/ -def fewerThanMeaning : Nat → Nat → Prop := Semantics.Degree.lessThanDeg id +def fewerThanMeaning : Nat → Nat → Prop := fun m n => n ∈ Core.Order.Comparison.lt.over id m /-- "At least `m`": `n ≥ m`. -/ -def atLeastMeaning : Nat → Nat → Prop := Semantics.Degree.atLeastDeg id +def atLeastMeaning : Nat → Nat → Prop := fun m n => n ∈ Core.Order.Comparison.ge.over id m /-- "At most `m`": `n ≤ m`. -/ -def atMostMeaning : Nat → Nat → Prop := Semantics.Degree.atMostDeg id +def atMostMeaning : Nat → Nat → Prop := fun m n => n ∈ Core.Order.Comparison.le.over id m @[simp] theorem bareMeaning_def (m n : Nat) : bareMeaning m n ↔ n = m := Iff.rfl @[simp] theorem moreThanMeaning_def (m n : Nat) : moreThanMeaning m n ↔ n > m := Iff.rfl @@ -164,19 +166,19 @@ instance : ToString BareNumeral where /-- Denotation of a numeral word `e`: the predicate over cardinalities it is true of, under a choice of bare-numeral semantics (`bareMeaning` exact vs. `atLeastMeaning` lower-bound — only the bare `.eq` form consults `bare`; the - four modified forms are theory-independent `relationalGQ` denotations). A + four modified forms are theory-independent `Comparison.over` denotations). A method on the numeral object, mirroring `PersonalPronoun.denote`. -/ def _root_.Numeral.Entry.denoteUnder (e : Numeral.Entry) (bare : Nat → Nat → Prop) : Nat → Prop := match e.comparison with | .eq => bare e.argument - | c => Semantics.Degree.relationalGQ c.rel id e.argument + | c => fun n => n ∈ c.over id e.argument instance (e : Numeral.Entry) (bare : Nat → Nat → Prop) [∀ m n, Decidable (bare m n)] (n : Nat) : Decidable (e.denoteUnder bare n) := by obtain ⟨_, c, _⟩ := e cases c <;> - simp only [Numeral.Entry.denoteUnder, Core.Order.Comparison.rel, Semantics.Degree.relationalGQ] <;> + simp only [Numeral.Entry.denoteUnder] <;> infer_instance /-- The bare-world meaning of a *modified* numeral word (`comparison ≠ .eq`) is @@ -187,8 +189,8 @@ theorem _root_.Numeral.Entry.denoteUnder_boundary (e : Numeral.Entry) (bare : Na e.denoteUnder bare e.argument ↔ e.argument ∈ e.comparison.interval e.argument := by obtain ⟨_, c, _⟩ := e cases c <;> - simp_all [Numeral.Entry.denoteUnder, Core.Order.Comparison.interval, - Semantics.Degree.relationalGQ, Core.Order.Comparison.rel] + simp_all [Numeral.Entry.denoteUnder, Core.Order.Comparison.over, + Core.Order.Comparison.interval] -- ============================================================================ -- Section 4: Alternative Set ([kennedy-2015] §4.1) @@ -232,41 +234,41 @@ theorem classB_includes_bare_world (e : Numeral.Entry) (bare : Nat → Nat → P exact h /-- Bare numeral pointwise entails "at least `m`" — the `id`-specialization - of `Semantics.Degree.eqDeg_imp_atLeastDeg`. -/ + of `Semantics.Degree.eqOver_imp_geOver`. -/ theorem classB_entailed_by_bare (m n : Nat) : bareMeaning m n → atLeastMeaning m n := - Semantics.Degree.eqDeg_imp_atLeastDeg id m n + Semantics.Degree.eqOver_imp_geOver id m n /-- Exact bare numerals are not upward-monotone: the `id`-specialization of - `Semantics.Degree.eqDeg_not_upward_monotone` (witness `d = 3`, `d' = 4`). -/ + `Semantics.Degree.eqOver_not_upward_monotone` (witness `d = 3`, `d' = 4`). -/ theorem bare_not_upward_monotone : ¬ ∀ m m' n, m ≤ m' → bareMeaning m n → bareMeaning m' n := by intro h - exact Semantics.Degree.eqDeg_not_upward_monotone (W := Nat) id (d := 3) (d' := 4) + exact Semantics.Degree.eqOver_not_upward_monotone (W := Nat) id (d := 3) (d' := 4) (by decide) (by decide) (w := 3) rfl (fun x y hxy hex => h x y 3 hxy hex) /-- Bare numerals are not downward-monotone either, so they fail the Horn-scale criterion in both directions. The `id`-specialization of - `Semantics.Degree.eqDeg_not_downward_monotone`. -/ + `Semantics.Degree.eqOver_not_downward_monotone`. -/ theorem bare_not_downward_monotone : ¬ ∀ m m' n, m' ≤ m → bareMeaning m n → bareMeaning m' n := by intro h - exact Semantics.Degree.eqDeg_not_downward_monotone (W := Nat) id (d := 3) (d' := 2) + exact Semantics.Degree.eqOver_not_downward_monotone (W := Nat) id (d := 3) (d' := 2) (by decide) (by decide) (w := 3) rfl (fun x y hyx hex => h x y 3 hyx hex) /-- "At least `m`" is strictly weaker than "bare `m`" — the `id`-specialization - of `Semantics.Degree.atLeastDeg_strictly_weaker_than_eqDeg` (witness `d' = m+1`). -/ + of `Semantics.Degree.geOver_strictly_weaker_than_eqOver` (witness `d' = m+1`). -/ theorem atLeast_strictly_weaker_than_bare (m : Nat) : atLeastMeaning m (m + 1) ∧ ¬ bareMeaning m (m + 1) := - Semantics.Degree.atLeastDeg_strictly_weaker_than_eqDeg id (Nat.lt_succ_self m) (w := m + 1) rfl + Semantics.Degree.geOver_strictly_weaker_than_eqOver id (Nat.lt_succ_self m) (w := m + 1) rfl /-- "More than `m`" and "bare `m`" have disjoint denotations — the - `id`-specialization of `Semantics.Degree.moreThanDeg_disjoint_eqDeg`. -/ + `id`-specialization of `Semantics.Degree.gtOver_disjoint_eqOver`. -/ theorem moreThan_disjoint_from_bare (m n : Nat) : ¬ (bareMeaning m n ∧ moreThanMeaning m n) := - Semantics.Degree.moreThanDeg_disjoint_eqDeg id m n + Semantics.Degree.gtOver_disjoint_eqOver id m n -- ============================================================================ -- Section 6: Type-Shifting ([kennedy-2015] §3.1) @@ -275,18 +277,19 @@ theorem moreThan_disjoint_from_bare (m n : Nat) : /-! ## De-Fregean type-shifting: exact → lower-bound The general operation `Semantics.Degree.typeLower` (`∃ d' ≥ d, exact d' w`) and -its collapse `typeLower_eqDeg_iff : typeLower (eqDeg μ) d w ↔ atLeastDeg μ d w` -live in `Core/Scales/Scale.lean`. Numerals are the `id`-instantiation: -`typeLower bareMeaning m n ↔ atLeastMeaning m n` follows by definitional -unfolding (`bareMeaning ≡ eqDeg id`, `atLeastMeaning ≡ atLeastDeg id`). +its collapse `typeLower_eqOver_iff` (existentially lowering `Comparison.eq.over μ` +yields `Comparison.ge.over μ`) live in `Semantics/Degree/Predicate.lean`. +Numerals are the `id`-instantiation: `typeLower bareMeaning m n ↔ atLeastMeaning m n` +follows by definitional unfolding (`bareMeaning ≡ Comparison.eq.over id`, +`atLeastMeaning ≡ Comparison.ge.over id`). The general theorem `Semantics.Degree.distinct_no_universal_witness` rules out the alternative universal-closure reading of Partee's iota. -/ -/-- The numeral instantiation of `Semantics.Degree.typeLower_eqDeg_iff`. -/ +/-- The numeral instantiation of `Semantics.Degree.typeLower_eqOver_iff`. -/ theorem typeLower_bareMeaning_iff (m n : Nat) : Semantics.Degree.typeLower bareMeaning m n ↔ atLeastMeaning m n := - Semantics.Degree.typeLower_eqDeg_iff id m n + Semantics.Degree.typeLower_eqOver_iff id m n -- ============================================================================ -- Section 7: EXH–Type-Shift Duality ([spector-2013] §6.2 vs [kennedy-2015]) @@ -336,7 +339,7 @@ connects B&N's quantifier view (type ⟨⟨e,t⟩,⟨e,t⟩,t⟩) to the Kennedy maximality view (type ⟨d,t⟩). -/ section GQTBridge -open Classical Intensional Quantification +open Classical Core.Logic.Intensional Quantification /-- GQT "at least `n`" agrees with `atLeastMeaning` on intersection cardinality. -/ theorem gqt_atLeast_agrees {α : Type*} [Fintype α] @@ -365,12 +368,11 @@ end GQTBridge The lexical numeral object (`Core.Order.Comparison`, `Numeral.Entry`) is owned by `Typology/Numeral/Basic.lean`; this section is the *semantics* side — it imports -that object and provides its `relationalGQ` denotation, mirroring how +that object and provides its `Comparison.over` denotation, mirroring how `Semantics/Reference/PronounDenotation.lean` denotes the `PersonalPronoun` object. -The denotation is **by construction** a `Semantics.Degree.relationalGQ`, so every lemma -about `relationalGQ` transfers to every numeral entry. `Comparison.rel` lives in -`Semantics.Degree`; `Entry.denoteUnder` (the cardinal, theory-parameterized reading) is -in Section 3. -/ +The denotation is **by construction** a `Core.Order.Comparison.over`, so every lemma +about `Comparison.over` transfers to every numeral entry. `Entry.denoteUnder` (the +cardinal, theory-parameterized reading) is in Section 3. -/ /-- Denotation of a numeral entry against a measure `μ : E → α` and a magnitude `m`: [kennedy-2015]'s de-Fregean GQ `λx. REL (μ x) m`. The measure and @@ -378,7 +380,7 @@ in Section 3. -/ `α = ℕ`. -/ def _root_.Numeral.Entry.denote {E α : Type*} [LinearOrder α] (e : Numeral.Entry) (μ : E → α) (m : α) : E → Prop := - Semantics.Degree.relationalGQ e.comparison.rel μ m + e.comparison.over μ m /-- Bare cardinal denotation: count with `μ = id` and the entry's own argument. -/ def _root_.Numeral.Entry.denoteCard (e : Numeral.Entry) : Nat → Prop := @@ -397,13 +399,12 @@ theorem denoteCard_eq_atLeastMeaning (e : Numeral.Entry) (h : e.comparison = .ge /-- **Class A/B boundary behaviour, free for every numeral entry.** At an entity whose measure equals the magnitude, the numeral holds iff its comparison is non-strict (bare `=`, Class B `≥`/`≤`) and fails for the strict Class A - comparisons (`>`/`<`). Inherited from `relationalGQ`, no per-entry proof. -/ + comparisons (`>`/`<`). Inherited from `Comparison.over`, no per-entry proof. -/ theorem denote_at_boundary {E α : Type*} [LinearOrder α] (e : Numeral.Entry) (μ : E → α) (m : α) {x : E} (h : μ x = m) : e.denote μ m x ↔ ¬ e.comparison.isStrict := by - obtain ⟨_, c, _⟩ := e - cases c <;> - simp [Numeral.Entry.denote, Core.Order.Comparison.rel, Core.Order.Comparison.isStrict, - Semantics.Degree.relationalGQ, h] + show x ∈ e.comparison.over μ m ↔ ¬ e.comparison.isStrict + rw [Core.Order.Comparison.mem_over, ← Core.Order.Comparison.mem_interval, h, + Core.Order.Comparison.boundary_mem] end Semantics.Numerals diff --git a/Linglib/Studies/FoxHackl2006Numerals.lean b/Linglib/Studies/FoxHackl2006Numerals.lean index 2734226f8..103e31e77 100644 --- a/Linglib/Studies/FoxHackl2006Numerals.lean +++ b/Linglib/Studies/FoxHackl2006Numerals.lean @@ -16,7 +16,7 @@ density predictions. ## Bridge Structure The named numeral meanings (`atLeastMeaning`, `moreThanMeaning`, ...) are -`abbrev`s over `Semantics.Degree.{atLeastDeg, moreThanDeg, ...} id` in +`def`s over `Core.Order.Comparison.{ge, gt, ...}.over id` in `Semantics/Numerals/Basic.lean` §2 — the connection holds by construction, no bridge lemma needed. @@ -36,6 +36,7 @@ namespace FoxHackl2006Numerals open Semantics.Degree open Entailment open Semantics.Numerals +open Core.Order (Comparison) -- ════════════════════════════════════════════════════ -- § 1. HasMaxInf for "at least" (any scale) @@ -44,12 +45,12 @@ open Semantics.Numerals /-- "At least n" always has a maximally informative element. Instantiated on ℕ with `id` as the measure function. -/ theorem atLeast_has_maxInf_at_3 : - HasMaxInf (atLeastDeg (α := ℕ) id) 3 := + HasMaxInf (Comparison.ge.over (α := ℕ) id) 3 := atLeast_hasMaxInf id 3 /-- Generalized: "at least n" has max⊨ at every world n. -/ theorem atLeast_has_maxInf_general (n : ℕ) : - HasMaxInf (atLeastDeg (α := ℕ) id) n := + HasMaxInf (Comparison.ge.over (α := ℕ) id) n := atLeast_hasMaxInf id n -- ════════════════════════════════════════════════════ @@ -62,8 +63,8 @@ theorem atLeast_has_maxInf_general (n : ℕ) : Contrast with `moreThan_noMaxInf` on dense scales: no rescue there. -/ theorem moreThan_has_maxInf_nat : - HasMaxInf (moreThanDeg (α := ℕ) id) 3 := - moreThan_nat_hasMaxInf id 3 (show moreThanDeg id 0 3 from by decide) + HasMaxInf (Comparison.gt.over (α := ℕ) id) 3 := + moreThan_nat_hasMaxInf id 3 (show (3 : ℕ) ∈ Comparison.gt.over id 0 from by decide) -- ════════════════════════════════════════════════════ -- § 3. MIP Derives Exact Meaning @@ -73,7 +74,7 @@ theorem moreThan_has_maxInf_nat : This is the MIP derivation of exact meaning from lower-bound semantics: [kennedy-2015]'s "de-Fregean" type-shift IS the MIP. -/ theorem mip_derives_exact (m n : ℕ) : - IsMaxInf (atLeastDeg (α := ℕ) id) m n ↔ n = m := + IsMaxInf (Comparison.ge.over (α := ℕ) id) m n ↔ n = m := isMaxInf_atLeast_iff_eq id m n Function.surjective_id -- ════════════════════════════════════════════════════ diff --git a/Linglib/Typology/Numeral/Basic.lean b/Linglib/Typology/Numeral/Basic.lean index 6abbd75e3..a98677362 100644 --- a/Linglib/Typology/Numeral/Basic.lean +++ b/Linglib/Typology/Numeral/Basic.lean @@ -13,7 +13,7 @@ The comparison vocabulary itself is **not** numeral-specific — it is the share degree-comparison primitive `Core.Order.Comparison` (also used by measure phrases and gradable comparatives, per [kennedy-2015], [rett-2014]); this file just records that a numeral *entry* carries one. The denotation (the -`relationalGQ`-based meaning, the Kennedy-vs-Horn bare-form choice) lives in +`Comparison.over`-based meaning, the Kennedy-vs-Horn bare-form choice) lives in `Semantics/Numerals/`, which imports this object — the same object/denotation split as `Syntax/Pronoun/Basic.lean` vs. `Semantics/Reference/PronounDenotation.lean`. The WALS typological survey