From b30f8df15d43b3eab2b5ddac4f445eb69b30b695 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 19 Jun 2026 16:29:14 -0700 Subject: [PATCH] refactor(Semantics/Degree): delete reducible duplicate names --- .../Attitudes/EpistemicThreshold.lean | 18 +++--- Linglib/Semantics/Degree/Abstraction.lean | 56 +++++++------------ Linglib/Semantics/Degree/Basic.lean | 41 ++++---------- Linglib/Semantics/Degree/Granularity.lean | 23 ++------ 4 files changed, 47 insertions(+), 91 deletions(-) diff --git a/Linglib/Semantics/Attitudes/EpistemicThreshold.lean b/Linglib/Semantics/Attitudes/EpistemicThreshold.lean index 2e919c8e3..55c70c42f 100644 --- a/Linglib/Semantics/Attitudes/EpistemicThreshold.lean +++ b/Linglib/Semantics/Attitudes/EpistemicThreshold.lean @@ -41,7 +41,7 @@ against a threshold (Table 1(a)): The threshold semantics is structurally identical to the positive form of gradable adjectives: - ⟦tall⟧(x) = height(x) ≥ θ_tall (Degree/Basic.positiveSem) + ⟦tall⟧(x) = height(x) ≥ θ_tall (the ≥-threshold condition) ⟦believes⟧(A, φ) = Pr(A, φ) ≥ θ_bel (meetsThreshold) Both are instances of the same degree-threshold architecture: a measure @@ -190,7 +190,7 @@ variable {E W : Type*} This is the single mechanism underlying all epistemic vocabulary. `believes`, `knows`, `certain`, `must`, `might` are all instances. - Structurally identical to `Degree.positiveSem μ θ x`: both are + Structurally identical to the degree-semantic ≥-threshold condition `measure(entity) ≥ threshold`. -/ def meetsThreshold (cr : AgentCredence E W) (θ : ℚ) (a : E) (φ : (W → Bool)) : Prop := @@ -449,7 +449,7 @@ The structural analogy between adjective degree semantics ([kennedy-2007], [lassiter-goodman-2017]) and epistemic threshold semantics: both are instances of `μ(entity) ≥ θ`. The threshold semantics makes this precise: - ⟦tall⟧(x) = height(x) ≥ θ_tall (Degree.positiveSem) + ⟦tall⟧(x) = height(x) ≥ θ_tall (the ≥-threshold condition) ⟦believes⟧(A, φ) = Pr(A, φ) ≥ θ_bel (meetsThreshold) Both are instances of `μ(entity) ≥ θ`. The epistemic scale is the @@ -492,15 +492,15 @@ def epistemicAsDirectedMeasure (cr : AgentCredence E W) (_entry : EpistemicEntry μ := fun ⟨a, φ⟩ => cr a φ boundedness := epistemicBoundedness -/-- The degree-threshold identity: `meetsThreshold` is `positiveSem` - instantiated on the epistemic scale. +/-- The degree-threshold identity: `meetsThreshold` is the ≥-threshold + condition `θ ≤ μ(entity)` with credence as the measure function. This is the formal statement that epistemic threshold semantics IS - degree semantics with credence as the measure function. -/ -theorem meetsThreshold_eq_positiveSem (cr : AgentCredence E W) (θ : ℚ) + degree semantics (the positive-form `Comparison.ge.over μ θ` + condition) with credence as the measure function. -/ +theorem meetsThreshold_eq_threshold (cr : AgentCredence E W) (θ : ℚ) (a : E) (φ : (W → Bool)) : - meetsThreshold cr θ a φ ↔ - Semantics.Degree.positiveSem (fun (p : E × (W → Bool)) => cr p.1 p.2) θ (a, φ) := by + meetsThreshold cr θ a φ ↔ θ ≤ cr a φ := by rfl /-- The epistemic scale is licensed: closed → admits absolute standards. diff --git a/Linglib/Semantics/Degree/Abstraction.lean b/Linglib/Semantics/Degree/Abstraction.lean index 342d41e0a..215bcd6a9 100644 --- a/Linglib/Semantics/Degree/Abstraction.lean +++ b/Linglib/Semantics/Degree/Abstraction.lean @@ -34,9 +34,9 @@ and intensional verbs. ## Order-Theoretic Foundations Heim's maximality operator `IsMaxDeg` is Mathlib's `IsGreatest`. -The matrix predicate `λd. μ(a) ≥ d` and [kennedy-1999]'s -`posExt μ a` are both the principal downset `Set.Iic (μ a)` — the -same mathematical object arrived at from different linguistic +Heim's matrix degree predicate `λd. μ(a) ≥ d` is [kennedy-1999]'s +`posExt μ a` — the principal downset `Set.Iic (μ a)`, the same +mathematical object arrived at from different linguistic motivations. The scope collapse theorems factor through the degree image `μ '' {x | R x}`, connecting to `gc_sSup_Iic` under `ConditionallyCompleteLattice`. @@ -74,45 +74,29 @@ theorem isMaxDeg_iff_isGreatest {D : Type*} [LE D] (P : DegreePredicate D) (d : IsMaxDeg P d ↔ IsGreatest {d' | P d'} d := ⟨fun ⟨h1, h2⟩ => ⟨h1, h2⟩, fun ⟨h1, h2⟩ => ⟨h1, h2⟩⟩ -/-- The matrix degree predicate for "A is d-tall": λd. μ(A) ≥ d. -/ -def matrixPredicate {Entity D : Type*} [Preorder D] - (μ : Entity → D) (a : Entity) : DegreePredicate D := - fun d => μ a ≥ d - /-- The than-clause degree predicate for "B is d-tall": λd. μ(B) ≥ d. -/ def thanClausePredicate {Entity D : Type*} [Preorder D] (μ : Entity → D) (b : Entity) : DegreePredicate D := fun d => μ b ≥ d --- ─── Matrix Predicate = posExt = Iic ────────────── +-- ─── posExt = Iic: Heim's matrix predicate ────────── -- --- Heim's matrix predicate and Kennedy's positive extent --- are the same mathematical object — the principal downset --- (Mathlib's Set.Iic): +-- Heim's matrix degree predicate λd. μ(a) ≥ d and Kennedy's +-- positive extent are the same mathematical object — the +-- principal downset (Mathlib's Set.Iic): -- --- Heim: matrixPredicate μ a = λd. μ(a) ≥ d --- Kennedy: posExt μ a = {d | d ≤ μ a} --- = Set.Iic (μ a) - -/-- Matrix predicate membership = `Set.Iic` membership. -/ -theorem matrixPredicate_mem_iff_Iic {Entity D : Type*} [Preorder D] - (μ : Entity → D) (a : Entity) (d : D) : - matrixPredicate μ a d ↔ d ∈ Set.Iic (μ a) := Iff.rfl - -/-- Matrix predicate membership = `posExt` membership - ([kennedy-1999]). -/ -theorem matrixPredicate_mem_iff_posExt {Entity D : Type*} [Preorder D] - (μ : Entity → D) (a : Entity) (d : D) : - matrixPredicate μ a d ↔ d ∈ posExt μ a := Iff.rfl +-- [kennedy-1999]: posExt μ a = {d | d ≤ μ a} = Set.Iic (μ a) +-- +-- so Heim's scope theory is stated directly on `posExt`. -/-- The maximum of a monotone predicate λd. μ(a) ≥ d is μ(a) itself. +/-- The maximum of the positive extent λd. μ(a) ≥ d is μ(a) itself. This grounds the Heim–Kennedy equivalence: max{d: tall(a,d)} = μ(a). This is Mathlib's `isGreatest_Iic` — the greatest element of `{d | d ≤ μ(a)}` is `μ(a)` — specialized to degree semantics. -/ -theorem isMaxDeg_matrixPredicate {Entity D : Type*} [LinearOrder D] +theorem isMaxDeg_posExt {Entity D : Type*} [LinearOrder D] (μ : Entity → D) (a : Entity) : - IsMaxDeg (matrixPredicate μ a) (μ a) := + IsMaxDeg (posExt μ a) (μ a) := (isMaxDeg_iff_isGreatest _ _).mpr isGreatest_Iic -- ════════════════════════════════════════════════════ @@ -131,11 +115,11 @@ def IsMonotoneAdj {Entity D : Type*} [Preorder D] (adj : D → Entity → Prop) : Prop := ∀ (x : Entity) (d d' : D), adj d x → d' ≤ d → adj d' x -/-- `matrixPredicate μ a` is always monotone (by construction). -/ -theorem matrixPredicate_monotone {Entity D : Type*} [Preorder D] +/-- `posExt μ a` is always downward-closed (by construction). -/ +theorem posExt_downwardClosed {Entity D : Type*} [Preorder D] (μ : Entity → D) (a : Entity) : - ∀ (d d' : D), matrixPredicate μ a d → d' ≤ d → - matrixPredicate μ a d' := by + ∀ (d d' : D), posExt μ a d → d' ≤ d → + posExt μ a d' := by intro d d' hd hle exact le_trans hle hd @@ -304,9 +288,9 @@ theorem heim_extensional_equivalence {Entity D : Type*} [LinearOrder D] -- -- The antonymy biconditional (Extent.lean § 7) is the -- statement that posExt and negExt form an antitone Galois --- connection on (Set D, ⊆). Since matrixPredicate = posExt, --- Heim's scope theory is built on the same Galois connection --- that grounds Kennedy's antonymy: +-- connection on (Set D, ⊆). Heim's matrix degree predicate is +-- `posExt`, so his scope theory is built on the same Galois +-- connection that grounds Kennedy's antonymy: -- -- posExt μ a ⊆ posExt μ b ↔ negExt μ b ⊆ negExt μ a -- ↔ μ a ≤ μ b diff --git a/Linglib/Semantics/Degree/Basic.lean b/Linglib/Semantics/Degree/Basic.lean index b0f625593..2c2776507 100644 --- a/Linglib/Semantics/Degree/Basic.lean +++ b/Linglib/Semantics/Degree/Basic.lean @@ -3,15 +3,15 @@ import Linglib.Semantics.Degree.Defs /-! # Degree Semantics: Positive-Form Semantics -Positive-form semantic operations on the types declared in `Defs.lean`, -plus threshold-comparison predicates on the concrete `Degree max` / -`Threshold max` carriers [kennedy-2007] [heim-2001] -[kennedy-mcnally-2005]. Kennedy 2007's interpretive economy lives -in the sibling `Kennedy.lean`. +Threshold-comparison predicates on the concrete `Degree max` / +`Threshold max` carriers declared in `Defs.lean` [kennedy-2007] +[heim-2001] [kennedy-mcnally-2005]. The abstract positive-form +predicate `μ(x) ≥ θ` is just `Comparison.ge.over μ θ` — used directly +where needed. Kennedy 2007's interpretive economy lives in the sibling +`Kennedy.lean`. ## Main definitions -* `positiveSem` — abstract positive-form predicate `μ(x) ≥ θ` * `positiveMeaning`, `negativeMeaning`, `antonymMeaning` — concrete threshold-comparison predicates on `Degree max` / `Threshold max` @@ -21,34 +21,17 @@ in the sibling `Kennedy.lean`. ## Relationship to `Gradability.Basic` -This module uses abstract types (`Entity D : Type*` with `LinearOrder D`) -for framework-level theorems. `Gradability.Basic` uses concrete -`Degree max := Fin (max + 1)` for computation in RSA models and Fragment -entries. The two serve different clients: this module is imported by -`Degree/Comparative.lean` and other framework siblings; `Gradability.Basic` -is imported by `Fragments/English/` and gradability `Studies/` files. +This module's concrete `Degree max := Fin (max + 1)` predicates serve +computation in RSA models and Fragment entries. `Gradability.Basic` +serves the same clients; this module is imported by +`Degree/Comparative.lean` and other framework siblings, while +`Gradability.Basic` is imported by `Fragments/English/` and gradability +`Studies/` files. -/ namespace Semantics.Degree open Semantics.Degree (Degree Threshold) -section Abstract - -variable {Entity D : Type*} [LinearOrder D] - -/-- The positive (unmarked) form of a gradable adjective: -"Kim is tall" is true iff `μ(Kim) ≥ θ` for a contextual standard `θ`. - -This is the common core across Kennedy and Heim: -* Kennedy: `⟦tall⟧ = λd.λx. height(x) ≥ d`, with `θ = pos(tall)` -* Heim: `⟦tall⟧ = λx. height(x) ≥ θ_c` - -Klein's approach is different: "tall" is true relative to a comparison -class, with no degree parameter. -/ -def positiveSem (μ : Entity → D) (θ : D) (x : Entity) : Prop := - μ x ≥ θ - -end Abstract /-! ### Concrete threshold-based meanings diff --git a/Linglib/Semantics/Degree/Granularity.lean b/Linglib/Semantics/Degree/Granularity.lean index c0cb47250..150a0a626 100644 --- a/Linglib/Semantics/Degree/Granularity.lean +++ b/Linglib/Semantics/Degree/Granularity.lean @@ -99,21 +99,6 @@ end GranularityFunction variable {D : Type*} [LinearOrder D] -/-- Equative at granularity interval: "as Adj as d_c". - - Paper eq. (45): ⟦as...as d_c⟧^g = λGλx.∃d[d > inf(g(d_c)) ∧ G(d)(x)]. - - For upward-monotone G (e.g., tall, where G(d)(x) iff μ(x) ≥ d), - the existential reduces to μ_x > inf(g(d_c)). -/ -def eqAt (gi : GranInterval D) (μ_x : D) : Prop := μ_x > gi.lo - -/-- Comparative at granularity interval: "Adj-er than d_c". - - Paper eq. (49): ⟦er/more than d_c⟧^g = λGλx.∃d[d > sup(g(d_c)) ∧ G(d)(x)]. - - For upward-monotone G, the existential reduces to μ_x > sup(g(d_c)). -/ -def compAt (gi : GranInterval D) (μ_x : D) : Prop := μ_x > gi.hi - -- ════════════════════════════════════════════════════ -- § 2. Entailment Reversal -- ════════════════════════════════════════════════════ @@ -133,20 +118,24 @@ The proofs are one-liners: transitivity of `<` and `≤`. -/ /-- Equatives: finer grain (larger lo) entails coarser grain (smaller lo). + The equative "as Adj as d_c" (eq. 45) at grain cell `gi`, for + upward-monotone G, reduces to `μ_x > gi.lo` (the cell's infimum). If μ_x exceeds the fine-grain infimum, it a fortiori exceeds the coarse-grain infimum (which is smaller). -/ theorem eq_fine_entails_coarse (gi₁ gi₂ : GranInterval D) (hlo : gi₂.lo ≤ gi₁.lo) - (μ_x : D) (h : eqAt gi₁ μ_x) : eqAt gi₂ μ_x := + (μ_x : D) (h : μ_x > gi₁.lo) : μ_x > gi₂.lo := lt_of_le_of_lt hlo h /-- Comparatives: coarser grain (larger hi) entails finer grain (smaller hi). + The comparative "Adj-er than d_c" (eq. 49) at grain cell `gi`, for + upward-monotone G, reduces to `μ_x > gi.hi` (the cell's supremum). If μ_x exceeds the coarse-grain supremum, it a fortiori exceeds the fine-grain supremum (which is smaller). -/ theorem comp_coarse_entails_fine (gi₁ gi₂ : GranInterval D) (hhi : gi₁.hi ≤ gi₂.hi) - (μ_x : D) (h : compAt gi₂ μ_x) : compAt gi₁ μ_x := + (μ_x : D) (h : μ_x > gi₂.hi) : μ_x > gi₁.hi := lt_of_le_of_lt hhi h -- ════════════════════════════════════════════════════