From 0488ec3e0cbbac30a5c4a6e2018dea35a92dede7 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 29 May 2026 17:34:34 -0700 Subject: [PATCH 1/8] refactor(Studies): move PIP framework from Semantics into KeshetAbney2024 --- Linglib.lean | 12 ++++++------ Linglib/Studies/AbneyKeshet2025.lean | 8 ++++---- Linglib/Studies/KeshetAbney2024.lean | 10 +++++----- .../PIP => Studies/KeshetAbney2024}/Basic.lean | 4 ++-- .../PIP => Studies/KeshetAbney2024}/Bridges.lean | 14 +++++++------- .../KeshetAbney2024}/Composition.lean | 6 +++--- .../KeshetAbney2024}/Connectives.lean | 8 ++++---- .../PIP => Studies/KeshetAbney2024}/Expr.lean | 6 +++--- .../PIP => Studies/KeshetAbney2024}/Felicity.lean | 6 +++--- 9 files changed, 37 insertions(+), 37 deletions(-) rename Linglib/{Semantics/PIP => Studies/KeshetAbney2024}/Basic.lean (99%) rename Linglib/{Semantics/PIP => Studies/KeshetAbney2024}/Bridges.lean (98%) rename Linglib/{Semantics/PIP => Studies/KeshetAbney2024}/Composition.lean (99%) rename Linglib/{Semantics/PIP => Studies/KeshetAbney2024}/Connectives.lean (98%) rename Linglib/{Semantics/PIP => Studies/KeshetAbney2024}/Expr.lean (99%) rename Linglib/{Semantics/PIP => Studies/KeshetAbney2024}/Felicity.lean (99%) diff --git a/Linglib.lean b/Linglib.lean index 836de2ab4..864972495 100644 --- a/Linglib.lean +++ b/Linglib.lean @@ -2082,12 +2082,12 @@ import Linglib.Studies.Charlow2021.UpdateTheoretic import Linglib.Studies.Charlow2021.HigherOrder import Linglib.Studies.Charlow2021.SubtypePolymorphism import Linglib.Studies.Charlow2021.PostSuppositional -import Linglib.Semantics.PIP.Basic -import Linglib.Semantics.PIP.Bridges -import Linglib.Semantics.PIP.Composition -import Linglib.Semantics.PIP.Connectives -import Linglib.Semantics.PIP.Expr -import Linglib.Semantics.PIP.Felicity +import Linglib.Studies.KeshetAbney2024.Basic +import Linglib.Studies.KeshetAbney2024.Bridges +import Linglib.Studies.KeshetAbney2024.Composition +import Linglib.Studies.KeshetAbney2024.Connectives +import Linglib.Studies.KeshetAbney2024.Expr +import Linglib.Studies.KeshetAbney2024.Felicity import Linglib.Semantics.Dynamic.PLA.Basic import Linglib.Semantics.Dynamic.PLA.Belief import Linglib.Semantics.Dynamic.PLA.DeepTheorems diff --git a/Linglib/Studies/AbneyKeshet2025.lean b/Linglib/Studies/AbneyKeshet2025.lean index 4ff7e277a..8832b151d 100644 --- a/Linglib/Studies/AbneyKeshet2025.lean +++ b/Linglib/Studies/AbneyKeshet2025.lean @@ -1,5 +1,5 @@ -import Linglib.Semantics.PIP.Composition -import Linglib.Semantics.PIP.Bridges +import Linglib.Studies.KeshetAbney2024.Composition +import Linglib.Studies.KeshetAbney2024.Bridges import Linglib.Studies.KeshetAbney2024 import Mathlib.Data.Set.Basic import Mathlib.Data.Fintype.Basic @@ -34,8 +34,8 @@ anaphora, modal subordination, and the exists/sigma bridge. namespace AbneyKeshet2025 -open Semantics.PIP -open Semantics.PIP.Bridges (single plural setEvery_eq_pipEvery) +open KeshetAbney2024.PIP +open KeshetAbney2024.PIP.Bridges (single plural setEvery_eq_pipEvery) -- ============================================================ diff --git a/Linglib/Studies/KeshetAbney2024.lean b/Linglib/Studies/KeshetAbney2024.lean index eea1f65a3..eaa87378a 100644 --- a/Linglib/Studies/KeshetAbney2024.lean +++ b/Linglib/Studies/KeshetAbney2024.lean @@ -1,6 +1,6 @@ -import Linglib.Semantics.PIP.Bridges -import Linglib.Semantics.PIP.Connectives -import Linglib.Semantics.PIP.Felicity +import Linglib.Studies.KeshetAbney2024.Bridges +import Linglib.Studies.KeshetAbney2024.Connectives +import Linglib.Studies.KeshetAbney2024.Felicity import Linglib.Semantics.Dynamic.Connectives.Defs import Linglib.Semantics.Dynamic.Connectives.Assignment import Linglib.Phenomena.Anaphora.DonkeyAnaphora @@ -46,9 +46,9 @@ finite models with `decide` verification. namespace KeshetAbney2024 -open Semantics.PIP +open KeshetAbney2024.PIP open Semantics.Dynamic.Core (IVar ICDRTAssignment Entity IContext) --- `BAccessRel` is re-exported by `Semantics.PIP` (opened above); +-- `BAccessRel` is re-exported by `KeshetAbney2024.PIP` (opened above); -- `BRefl` / `kripkeEval` were Bool-internal modal infrastructure that has -- been replaced by the Prop-valued `Refl`/`boxR` API in -- `Core.Logic.Intensional` and isn't needed here. diff --git a/Linglib/Semantics/PIP/Basic.lean b/Linglib/Studies/KeshetAbney2024/Basic.lean similarity index 99% rename from Linglib/Semantics/PIP/Basic.lean rename to Linglib/Studies/KeshetAbney2024/Basic.lean index e7c091b68..5723aea25 100644 --- a/Linglib/Semantics/PIP/Basic.lean +++ b/Linglib/Studies/KeshetAbney2024/Basic.lean @@ -45,7 +45,7 @@ external/local variable distinction) are faithfully preserved. -/ -namespace Semantics.PIP +namespace KeshetAbney2024.PIP open Semantics.Dynamic.Core @@ -330,4 +330,4 @@ theorem summation_nonempty {W E : Type*} ⟨gw.1, gw.2, h, rfl⟩ -end Semantics.PIP +end KeshetAbney2024.PIP diff --git a/Linglib/Semantics/PIP/Bridges.lean b/Linglib/Studies/KeshetAbney2024/Bridges.lean similarity index 98% rename from Linglib/Semantics/PIP/Bridges.lean rename to Linglib/Studies/KeshetAbney2024/Bridges.lean index 0a69d0bc8..d9a42ffac 100644 --- a/Linglib/Semantics/PIP/Bridges.lean +++ b/Linglib/Studies/KeshetAbney2024/Bridges.lean @@ -1,7 +1,7 @@ -import Linglib.Semantics.PIP.Expr -import Linglib.Semantics.PIP.Felicity -import Linglib.Semantics.PIP.Connectives -import Linglib.Semantics.PIP.Composition +import Linglib.Studies.KeshetAbney2024.Expr +import Linglib.Studies.KeshetAbney2024.Felicity +import Linglib.Studies.KeshetAbney2024.Connectives +import Linglib.Studies.KeshetAbney2024.Composition import Linglib.Semantics.Presupposition.Basic import Linglib.Semantics.Quantification.Quantifier import Linglib.Semantics.Plurality.Algebra @@ -35,9 +35,9 @@ the Brasoveanu equivalence (which requires a non-trivial model theory argument). -/ -namespace Semantics.PIP.Bridges +namespace KeshetAbney2024.PIP.Bridges -open Semantics.PIP +open KeshetAbney2024.PIP open Semantics.Dynamic.Core (IVar ICDRTAssignment Entity IContext) open Core.Logic.Intensional.Logic (frameConditions) @@ -461,4 +461,4 @@ theorem static_neg_agrees_dynamic {W E : Type*} exact ⟨fun ⟨_, hneg⟩ => hneg, fun hneg => ⟨hd, hneg⟩⟩ -end Semantics.PIP.Bridges +end KeshetAbney2024.PIP.Bridges diff --git a/Linglib/Semantics/PIP/Composition.lean b/Linglib/Studies/KeshetAbney2024/Composition.lean similarity index 99% rename from Linglib/Semantics/PIP/Composition.lean rename to Linglib/Studies/KeshetAbney2024/Composition.lean index fb0784ccf..57d41be47 100644 --- a/Linglib/Semantics/PIP/Composition.lean +++ b/Linglib/Studies/KeshetAbney2024/Composition.lean @@ -1,4 +1,4 @@ -import Linglib.Semantics.PIP.Expr +import Linglib.Studies.KeshetAbney2024.Expr import Mathlib.Data.Fintype.Basic /-! @@ -24,7 +24,7 @@ value (type t). It is therefore defined externally from the `PIPExprF` inductive type and connected to it via bridge theorems. -/ -namespace Semantics.PIP +namespace KeshetAbney2024.PIP -- ============================================================ @@ -410,4 +410,4 @@ theorem sigmaEval_labelDef_subordination (α : FLabel) (φ ψ : D → PIPExprF W end Subordination -end Semantics.PIP +end KeshetAbney2024.PIP diff --git a/Linglib/Semantics/PIP/Connectives.lean b/Linglib/Studies/KeshetAbney2024/Connectives.lean similarity index 98% rename from Linglib/Semantics/PIP/Connectives.lean rename to Linglib/Studies/KeshetAbney2024/Connectives.lean index 55ac2cb4b..f62146bbc 100644 --- a/Linglib/Semantics/PIP/Connectives.lean +++ b/Linglib/Studies/KeshetAbney2024/Connectives.lean @@ -1,4 +1,4 @@ -import Linglib.Semantics.PIP.Basic +import Linglib.Studies.KeshetAbney2024.Basic import Linglib.Core.Logic.Intensional.RestrictedModality import Mathlib.Data.Fintype.Basic @@ -24,14 +24,14 @@ PIP's modals are generalized quantifiers over worlds (paper Section 2.5): - MIGHT^β_w(W₁, W₂) ≜ SOME(β_w ∩ W₁, W₂) - MUST^β_w(W₁, W₂) ≜ EVERY(β_w ∩ W₁, W₂) -Our encoding parameterizes by an accessibility relation (`Semantics.PIP.BAccessRel`, +Our encoding parameterizes by an accessibility relation (`KeshetAbney2024.PIP.BAccessRel`, equivalent to a Kratzer modal base β) and quantifies over accessible worlds. The grounding theorem `must_truth_agrees_boxR` proves that PIP's `must` produces the same truth conditions as `Core.Logic.Intensional.boxR`. -/ -namespace Semantics.PIP +namespace KeshetAbney2024.PIP open Semantics.Dynamic.Core @@ -415,4 +415,4 @@ theorem forall_eq_neg_exists_neg {W E : Type*} (v : IVar) (domain : Set E) forall_ v domain body = negation (exists_ v domain (negation body)) := rfl -end Semantics.PIP +end KeshetAbney2024.PIP diff --git a/Linglib/Semantics/PIP/Expr.lean b/Linglib/Studies/KeshetAbney2024/Expr.lean similarity index 99% rename from Linglib/Semantics/PIP/Expr.lean rename to Linglib/Studies/KeshetAbney2024/Expr.lean index cee99da84..c515e9e7a 100644 --- a/Linglib/Semantics/PIP/Expr.lean +++ b/Linglib/Studies/KeshetAbney2024/Expr.lean @@ -1,4 +1,4 @@ -import Linglib.Semantics.PIP.Basic +import Linglib.Studies.KeshetAbney2024.Basic import Mathlib.Data.Set.Basic import Mathlib.Data.Fintype.Basic @@ -38,7 +38,7 @@ label definitions are tautologies that float freely, this function collects all `X ≡ φ` definitions regardless of their structural position. -/ -namespace Semantics.PIP +namespace KeshetAbney2024.PIP /-- A finite domain of individuals for PIP quantifier evaluation. -/ class FiniteDomain (D : Type*) where @@ -241,4 +241,4 @@ theorem felicitousF_must (R : BAccessRel W) (φ : PIPExprF W D) (w : W) : end Properties -end Semantics.PIP +end KeshetAbney2024.PIP diff --git a/Linglib/Semantics/PIP/Felicity.lean b/Linglib/Studies/KeshetAbney2024/Felicity.lean similarity index 99% rename from Linglib/Semantics/PIP/Felicity.lean rename to Linglib/Studies/KeshetAbney2024/Felicity.lean index abef57033..cf524a0c2 100644 --- a/Linglib/Semantics/PIP/Felicity.lean +++ b/Linglib/Studies/KeshetAbney2024/Felicity.lean @@ -1,4 +1,4 @@ -import Linglib.Semantics.PIP.Expr +import Linglib.Studies.KeshetAbney2024.Expr import Mathlib.Data.Fintype.Basic /-! @@ -55,7 +55,7 @@ world and assignment consistent with γ. -/ -namespace Semantics.PIP.Felicity +namespace KeshetAbney2024.PIP.Felicity variable {W : Type*} @@ -464,4 +464,4 @@ theorem sigma_body_felicitous_iff (body : D → PIPExprF W D) (w : W) : end FullFelicity -end Semantics.PIP.Felicity +end KeshetAbney2024.PIP.Felicity From dff450f2f5e0a4e8d020b2241589d51335cfcf5f Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 29 May 2026 17:40:45 -0700 Subject: [PATCH 2/8] refactor(Studies/KeshetAbney2024): make PIPExprF evaluators Prop-native --- Linglib/Studies/KeshetAbney2024/Expr.lean | 76 +++++++++++------------ 1 file changed, 38 insertions(+), 38 deletions(-) diff --git a/Linglib/Studies/KeshetAbney2024/Expr.lean b/Linglib/Studies/KeshetAbney2024/Expr.lean index c515e9e7a..54c723d04 100644 --- a/Linglib/Studies/KeshetAbney2024/Expr.lean +++ b/Linglib/Studies/KeshetAbney2024/Expr.lean @@ -1,4 +1,5 @@ import Linglib.Studies.KeshetAbney2024.Basic +import Linglib.Core.Logic.Intensional.Defs import Mathlib.Data.Set.Basic import Mathlib.Data.Fintype.Basic @@ -40,6 +41,8 @@ all `X ≡ φ` definitions regardless of their structural position. namespace KeshetAbney2024.PIP +open Core.Logic.Intensional (AccessRel boxR diamondR) + /-- A finite domain of individuals for PIP quantifier evaluation. -/ class FiniteDomain (D : Type*) where elements : List D @@ -62,7 +65,7 @@ constructors extend it to the full system. -/ inductive PIPExprF (W : Type*) (D : Type*) where /-- Atomic predicate: P_w(x₁, ..., xₙ). Always felicitous. -/ - | pred (p : W → Bool) + | pred (p : W → Prop) /-- Conjunction: φ ∧ ψ. Felicity is asymmetric (Karttunen). -/ | conj (φ ψ : PIPExprF W D) /-- Negation: ¬φ. Felicity passes through. -/ @@ -72,7 +75,7 @@ inductive PIPExprF (W : Type*) (D : Type*) where /-- Implication: φ → ψ. -/ | impl (φ ψ : PIPExprF W D) /-- Presupposition: φ|ψ. Assert φ, presuppose ψ. -/ - | presup (φ : PIPExprF W D) (ψ : W → Bool) + | presup (φ : PIPExprF W D) (ψ : W → Prop) /-- Existential quantification: ∃x.φ (paper item 43). `body` takes a domain element and returns a formula. -/ | exists_ (body : D → PIPExprF W D) @@ -84,10 +87,10 @@ inductive PIPExprF (W : Type*) (D : Type*) where | labelDef (label : FLabel) (φ : PIPExprF W D) /-- Modal necessity: □_R φ (paper item 28, MUST). Universal quantification over R-accessible worlds. -/ - | must (R : BAccessRel W) (φ : PIPExprF W D) + | must (R : AccessRel W) (φ : PIPExprF W D) /-- Modal possibility: ◇_R φ (paper item 28, MIGHT). Existential quantification over R-accessible worlds. -/ - | might (R : BAccessRel W) (φ : PIPExprF W D) + | might (R : AccessRel W) (φ : PIPExprF W D) -- ============================================================ @@ -104,21 +107,19 @@ standard first-order quantification over domains and worlds. Requires `[Fintype D]` for quantifier evaluation and `[Fintype W]` for modal evaluation. -/ -noncomputable def PIPExprF.truth {W D : Type*} [FiniteDomain D] [Fintype W] : - PIPExprF W D → (W → Bool) +def PIPExprF.truth {W D : Type*} : + PIPExprF W D → (W → Prop) | .pred p => p - | .conj φ ψ => λ w => φ.truth w && ψ.truth w - | .neg φ => λ w => (φ.truth w).not - | .disj φ ψ => λ w => φ.truth w || ψ.truth w - | .impl φ ψ => λ w => (φ.truth w).not || ψ.truth w + | .conj φ ψ => λ w => φ.truth w ∧ ψ.truth w + | .neg φ => λ w => ¬ φ.truth w + | .disj φ ψ => λ w => φ.truth w ∨ ψ.truth w + | .impl φ ψ => λ w => φ.truth w → ψ.truth w | .presup φ _ψ => φ.truth - | .exists_ body => λ w => FiniteDomain.elements.any (λ d => (body d).truth w) - | .forall_ body => λ w => FiniteDomain.elements.all (λ d => (body d).truth w) + | .exists_ body => λ w => ∃ d, (body d).truth w + | .forall_ body => λ w => ∀ d, (body d).truth w | .labelDef _label φ => φ.truth -- label defs are tautological wrt truth - | .must R φ => λ w => - (((Finset.univ : Finset W).toList.filter (R w))).all φ.truth - | .might R φ => λ w => - (((Finset.univ : Finset W).toList.filter (R w))).any φ.truth + | .must R φ => boxR R φ.truth + | .might R φ => diamondR R φ.truth -- ============================================================ @@ -139,32 +140,30 @@ The universal quantification in the quantifier/modal felicity clauses is the key insight: an expression is felicitous only if its presuppositions are met for EVERY possible witness/world, not just some. -/ -noncomputable def PIPExprF.felicitous {W D : Type*} [FiniteDomain D] [Fintype W] : - PIPExprF W D → (W → Bool) - -- F(P(α₁,...,αₙ)) = true (atoms are always felicitous) - | .pred _ => λ _ => true +def PIPExprF.felicitous {W D : Type*} : + PIPExprF W D → (W → Prop) + -- F(P(α₁,...,αₙ)) = ⊤ (atoms are always felicitous) + | .pred _ => λ _ => True -- F(φ ∧ ψ) iff Fφ ∧ (φ → Fψ) [Karttunen's asymmetric conjunction] - | .conj φ ψ => λ w => φ.felicitous w && ((φ.truth w).not || ψ.felicitous w) + | .conj φ ψ => λ w => φ.felicitous w ∧ (φ.truth w → ψ.felicitous w) -- F(¬φ) iff Fφ | .neg φ => φ.felicitous -- F(φ ∨ ψ) iff Fφ ∧ (¬φ → Fψ) - | .disj φ ψ => λ w => φ.felicitous w && (φ.truth w || ψ.felicitous w) + | .disj φ ψ => λ w => φ.felicitous w ∧ (¬ φ.truth w → ψ.felicitous w) -- F(φ → ψ) iff Fφ ∧ (φ → Fψ) - | .impl φ ψ => λ w => φ.felicitous w && ((φ.truth w).not || ψ.felicitous w) + | .impl φ ψ => λ w => φ.felicitous w ∧ (φ.truth w → ψ.felicitous w) -- F(φ|ψ) iff Fφ ∧ ψ [presupposition must hold] - | .presup φ ψ => λ w => φ.felicitous w && ψ w + | .presup φ ψ => λ w => φ.felicitous w ∧ ψ w -- F(∃xφ) iff ∀x.Fφ [felicity universal over witnesses, item 43] - | .exists_ body => λ w => FiniteDomain.elements.all (λ d => (body d).felicitous w) + | .exists_ body => λ w => ∀ d, (body d).felicitous w -- F(∀xφ) iff ∀x.Fφ - | .forall_ body => λ w => FiniteDomain.elements.all (λ d => (body d).felicitous w) + | .forall_ body => λ w => ∀ d, (body d).felicitous w -- F(X≡φ) iff Fφ [labels don't affect felicity] | .labelDef _label φ => φ.felicitous -- F(□φ) iff ∀w'.Fφ [item 47: felicity universal over accessible worlds] - | .must R φ => λ w => - (((Finset.univ : Finset W).toList.filter (R w))).all φ.felicitous + | .must R φ => boxR R φ.felicitous -- F(◇φ) iff ∀w'.Fφ [item 47: felicity universal, NOT existential] - | .might R φ => λ w => - (((Finset.univ : Finset W).toList.filter (R w))).all φ.felicitous + | .might R φ => boxR R φ.felicitous -- ============================================================ @@ -201,22 +200,22 @@ def PIPExprF.labelDefs {W D : Type*} : PIPExprF W D → List (FLabel × PIPExprF section Properties -variable {W D : Type*} [FiniteDomain D] [Fintype W] +variable {W D : Type*} /-- F(¬φ) iff Fφ — negation preserves felicity. -/ theorem felicitousF_neg (φ : PIPExprF W D) (w : W) : (PIPExprF.neg φ).felicitous w = φ.felicitous w := rfl /-- F(φ|ψ) iff Fφ ∧ ψ(w) — presupposition must hold. -/ -theorem felicitousF_presup (φ : PIPExprF W D) (ψ : W → Bool) (w : W) : - (PIPExprF.presup φ ψ).felicitous w = (φ.felicitous w && ψ w) := rfl +theorem felicitousF_presup (φ : PIPExprF W D) (ψ : W → Prop) (w : W) : + (PIPExprF.presup φ ψ).felicitous w = (φ.felicitous w ∧ ψ w) := rfl /-- F(X≡φ) iff Fφ — label definitions don't affect felicity. -/ theorem felicitousF_labelDef (α : FLabel) (φ : PIPExprF W D) (w : W) : (PIPExprF.labelDef α φ).felicitous w = φ.felicitous w := rfl /-- Presupposition truth-independence: φ|ψ is true iff φ is true. -/ -theorem presupF_truth_independent (φ : PIPExprF W D) (ψ : W → Bool) (w : W) : +theorem presupF_truth_independent (φ : PIPExprF W D) (ψ : W → Prop) (w : W) : (PIPExprF.presup φ ψ).truth w = φ.truth w := rfl /-- Label definitions are truth-transparent: X≡φ is true iff φ is true. -/ @@ -226,17 +225,18 @@ theorem labelDef_truth_transparent (α : FLabel) (φ : PIPExprF W D) (w : W) : /-- Conjunction felicity is asymmetric (Karttunen). -/ theorem felicitousF_conj (φ ψ : PIPExprF W D) (w : W) : (PIPExprF.conj φ ψ).felicitous w = - (φ.felicitous w && ((φ.truth w).not || ψ.felicitous w)) := rfl + (φ.felicitous w ∧ (φ.truth w → ψ.felicitous w)) := rfl /-- Existential felicity is universal over witnesses. -/ theorem felicitousF_exists (body : D → PIPExprF W D) (w : W) : (PIPExprF.exists_ body).felicitous w = - FiniteDomain.elements.all (λ d => (body d).felicitous w) := rfl + (∀ d, (body d).felicitous w) := rfl /-- Modal necessity felicity is universal over accessible worlds. -/ -theorem felicitousF_must (R : BAccessRel W) (φ : PIPExprF W D) (w : W) : +theorem felicitousF_must (R : AccessRel W) (φ : PIPExprF W D) + (w : W) : (PIPExprF.must R φ).felicitous w = - (((Finset.univ : Finset W).toList.filter (R w))).all φ.felicitous := rfl + boxR R φ.felicitous w := rfl end Properties From 946e9d27c14eb180ec2aa624dcee4a1a2da5db92 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 29 May 2026 17:56:14 -0700 Subject: [PATCH 3/8] refactor(Studies/KeshetAbney2024): Prop-native PIP framework, consume boxR/diamondR --- Linglib/Studies/KeshetAbney2024/Basic.lean | 23 +- .../Studies/KeshetAbney2024/Composition.lean | 146 +++++------- .../Studies/KeshetAbney2024/Connectives.lean | 84 +++---- Linglib/Studies/KeshetAbney2024/Felicity.lean | 218 ++++++++---------- 4 files changed, 191 insertions(+), 280 deletions(-) diff --git a/Linglib/Studies/KeshetAbney2024/Basic.lean b/Linglib/Studies/KeshetAbney2024/Basic.lean index 5723aea25..f8504b9ee 100644 --- a/Linglib/Studies/KeshetAbney2024/Basic.lean +++ b/Linglib/Studies/KeshetAbney2024/Basic.lean @@ -49,17 +49,6 @@ namespace KeshetAbney2024.PIP open Semantics.Dynamic.Core -/-- Local Bool-valued accessibility for PIP's computational modal evaluation. - PIP's modal operators use Bool predicates throughout for `List.all`/`List.any` - computation; this is not the parallel-universe pattern (we are not shadowing - Prop infrastructure with Bool versions), it is a legitimate Bool-internal - framework over which PIP's discourse-update operators compute. The Prop-valued - `Core.Logic.Intensional.AccessRel` is the canonical type for - Kripke-style modal logic; PIP needs the Bool variant for its `List.all`/`List.any` - truth-value pipeline. Lifted to Prop via `fun a b => R a b = true` when bridging - to `boxR`/`diamondR`. -/ -abbrev BAccessRel (W : Type*) := W → W → Bool - -- ============================================================ -- Formula Labels @@ -88,7 +77,7 @@ structure Description (W : Type*) (E : Type*) where /-- The variable being described -/ var : IVar /-- The constraining predicate (per assignment and world) -/ - predicate : ICDRTAssignment W E → W → Bool + predicate : ICDRTAssignment W E → W → Prop -- ============================================================ @@ -211,7 +200,7 @@ In PIP, presuppositions are used for: 2. Pronominal anaphora (presupposes antecedent is accessible) -/ def presuppose {W E : Type*} - (pred : ICDRTAssignment W E → W → Bool) : PUpdate W E := + (pred : ICDRTAssignment W E → W → Prop) : PUpdate W E := λ d => d.mapInfo (λ c => { gw ∈ c | pred gw.1 gw.2 }) @@ -256,7 +245,7 @@ assignments may bind different entities to the same variable, and truth requires the predicate to hold across all of them. -/ def pluralTruth {W E : Type*} - (c : IContext W E) (w : W) (pred : ICDRTAssignment W E → W → Bool) : Prop := + (c : IContext W E) (w : W) (pred : ICDRTAssignment W E → W → Prop) : Prop := ∀ g, (g, w) ∈ c → pred g w @@ -308,8 +297,8 @@ This is a core PIP operation (paper items 25–27), not study-specific. GQ arguments in PIP take two summation terms: restrictor and scope. -/ def summationFiltered {W E : Type*} (c : IContext W E) (v : IVar) - (φ : ICDRTAssignment W E → W → Bool) : Set (Entity E) := - { e | ∃ g w, (g, w) ∈ c ∧ φ g w = true ∧ g.indiv v w = e } + (φ : ICDRTAssignment W E → W → Prop) : Set (Entity E) := + { e | ∃ g w, (g, w) ∈ c ∧ φ g w ∧ g.indiv v w = e } /-- Summation without filtering: collects all values of variable v. -/ def summationValues {W E : Type*} (c : IContext W E) (v : IVar) : Set (Entity E) := @@ -318,7 +307,7 @@ def summationValues {W E : Type*} (c : IContext W E) (v : IVar) : Set (Entity E) /-- Unfiltered summation equals trivially filtered summation. -/ theorem summationValues_eq_trivial_filter {W E : Type*} (c : IContext W E) (v : IVar) : - summationValues c v = summationFiltered c v (λ _ _ => true) := by + summationValues c v = summationFiltered c v (λ _ _ => True) := by ext e; simp [summationValues, summationFiltered] /-- Any assignment in a non-empty context contributes to summation. -/ diff --git a/Linglib/Studies/KeshetAbney2024/Composition.lean b/Linglib/Studies/KeshetAbney2024/Composition.lean index 57d41be47..f0fcb46b5 100644 --- a/Linglib/Studies/KeshetAbney2024/Composition.lean +++ b/Linglib/Studies/KeshetAbney2024/Composition.lean @@ -26,6 +26,8 @@ type and connected to it via bridge theorems. namespace KeshetAbney2024.PIP +open Core.Logic.Intensional (AccessRel boxR diamondR) + -- ============================================================ -- §1: Sigma Evaluation (paper's Σ operator and ZF expansion) @@ -33,7 +35,7 @@ namespace KeshetAbney2024.PIP section Sigma -variable {W D : Type*} [FiniteDomain D] [Fintype W] +variable {W D : Type*} /-- Sigma evaluation: Σxφ = {d ∈ D | ⟦φ(d)⟧^w = 1}. @@ -48,85 +50,62 @@ performs the same collection on the dynamic `IContext` level. Agreement between the two is part of the static↔dynamic correspondence. -/ def sigmaEval (body : D → PIPExprF W D) (w : W) : Set D := - { d | (body d).truth w = true } + { d | (body d).truth w } @[simp] theorem sigmaEval_mem (body : D → PIPExprF W D) (w : W) (d : D) : - d ∈ sigmaEval body w ↔ (body d).truth w = true := + d ∈ sigmaEval body w ↔ (body d).truth w := Iff.rfl /-- ∃xφ is true iff the sigma set is nonempty. -/ theorem exists_iff_sigma_nonempty (body : D → PIPExprF W D) (w : W) : - (PIPExprF.exists_ body).truth w = true ↔ (sigmaEval body w).Nonempty := by - simp only [PIPExprF.truth, sigmaEval, Set.Nonempty, Set.mem_setOf_eq] - constructor - · intro h - rw [List.any_eq_true] at h - obtain ⟨d, _, hd⟩ := h - exact ⟨d, hd⟩ - · intro ⟨d, hd⟩ - rw [List.any_eq_true] - exact ⟨d, FiniteDomain.complete d, hd⟩ + (PIPExprF.exists_ body).truth w ↔ (sigmaEval body w).Nonempty := + Iff.rfl /-- ∀xφ is true iff every individual is in the sigma set. -/ theorem forall_iff_sigma_univ (body : D → PIPExprF W D) (w : W) : - (PIPExprF.forall_ body).truth w = true ↔ sigmaEval body w = Set.univ := by - simp only [PIPExprF.truth, sigmaEval, Set.eq_univ_iff_forall, Set.mem_setOf_eq] - constructor - · intro h d - rw [List.all_eq_true] at h - exact h d (FiniteDomain.complete d) - · intro h - rw [List.all_eq_true] - intro d _ - exact h d + (PIPExprF.forall_ body).truth w ↔ sigmaEval body w = Set.univ := by + rw [Set.eq_univ_iff_forall]; rfl /-- Σx(φ ∧ ψ) = Σxφ ∩ Σxψ. -/ theorem sigmaEval_conj (φ ψ : D → PIPExprF W D) (w : W) : sigmaEval (λ d => PIPExprF.conj (φ d) (ψ d)) w = sigmaEval φ w ∩ sigmaEval ψ w := by ext d - simp only [sigmaEval, Set.mem_setOf_eq, Set.mem_inter_iff] - show ((φ d).truth w && (ψ d).truth w) = true ↔ (φ d).truth w = true ∧ (ψ d).truth w = true - simp only [Bool.and_eq_true] + simp only [sigmaEval, Set.mem_setOf_eq, Set.mem_inter_iff, PIPExprF.truth] /-- Σx(φ ∨ ψ) = Σxφ ∪ Σxψ. -/ theorem sigmaEval_disj (φ ψ : D → PIPExprF W D) (w : W) : sigmaEval (λ d => PIPExprF.disj (φ d) (ψ d)) w = sigmaEval φ w ∪ sigmaEval ψ w := by ext d - simp only [sigmaEval, Set.mem_setOf_eq, Set.mem_union] - show ((φ d).truth w || (ψ d).truth w) = true ↔ (φ d).truth w = true ∨ (ψ d).truth w = true - simp only [Bool.or_eq_true] + simp only [sigmaEval, Set.mem_setOf_eq, Set.mem_union, PIPExprF.truth] /-- Σx(¬φ) = (Σxφ)ᶜ. -/ theorem sigmaEval_neg (φ : D → PIPExprF W D) (w : W) : sigmaEval (λ d => PIPExprF.neg (φ d)) w = (sigmaEval φ w)ᶜ := by ext d - simp only [sigmaEval, Set.mem_setOf_eq, Set.mem_compl_iff] - show (!(φ d).truth w) = true ↔ ¬((φ d).truth w = true) - cases (φ d).truth w <;> simp + simp only [sigmaEval, Set.mem_setOf_eq, Set.mem_compl_iff, PIPExprF.truth] /-- Σx(⊤) = D (everything satisfies a tautology). -/ theorem sigmaEval_true (w : W) : - sigmaEval (D := D) (λ _ => PIPExprF.pred (λ _ => true)) w = Set.univ := by - ext d; simp only [sigmaEval, Set.mem_setOf_eq, Set.mem_univ, iff_true]; rfl + sigmaEval (D := D) (λ _ => PIPExprF.pred (λ _ => True)) w = Set.univ := by + ext d; simp only [sigmaEval, Set.mem_setOf_eq, Set.mem_univ, iff_true, PIPExprF.truth] /-- Σx(⊥) = ∅ (nothing satisfies a contradiction). -/ theorem sigmaEval_false (w : W) : - sigmaEval (D := D) (λ _ => PIPExprF.pred (λ _ => false)) w = ∅ := by - ext d; simp only [sigmaEval, Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false]; exact - Bool.false_ne_true + sigmaEval (D := D) (λ _ => PIPExprF.pred (λ _ => False)) w = ∅ := by + ext d + simp only [sigmaEval, Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false, PIPExprF.truth, + not_false_iff] /-- Label definitions are truth-transparent for sigma. -/ theorem sigmaEval_labelDef (α : FLabel) (φ : D → PIPExprF W D) (w : W) : - sigmaEval (λ d => PIPExprF.labelDef α (φ d)) w = sigmaEval φ w := by - ext d; show (φ d).truth w = true ↔ (φ d).truth w = true; exact Iff.rfl + sigmaEval (λ d => PIPExprF.labelDef α (φ d)) w = sigmaEval φ w := rfl /-- Presuppositions are truth-transparent for sigma. -/ -theorem sigmaEval_presup (φ : D → PIPExprF W D) (ψ : W → Bool) (w : W) : - sigmaEval (λ d => PIPExprF.presup (φ d) ψ) w = sigmaEval φ w := by - ext d; show (φ d).truth w = true ↔ (φ d).truth w = true; exact Iff.rfl +theorem sigmaEval_presup (φ : D → PIPExprF W D) (ψ : W → Prop) (w : W) : + sigmaEval (λ d => PIPExprF.presup (φ d) ψ) w = sigmaEval φ w := rfl end Sigma @@ -181,18 +160,18 @@ theorem gq_duality (R S : Set α) : -- Sigma bridge: connecting set-based GQs to PIPExprF quantifiers -variable {W D : Type*} [FiniteDomain D] [Fintype W] +variable {W D : Type*} /-- EVERY over sigma sets ↔ pointwise universal implication. -/ theorem setEvery_sigma (body_R body_S : D → PIPExprF W D) (w : W) : setEvery (sigmaEval body_R w) (sigmaEval body_S w) ↔ - ∀ d, (body_R d).truth w = true → (body_S d).truth w = true := by + ∀ d, (body_R d).truth w → (body_S d).truth w := by simp [setEvery, Set.subset_def, sigmaEval] /-- SOME over sigma sets ↔ pointwise existential conjunction. -/ theorem setSome_sigma (body_R body_S : D → PIPExprF W D) (w : W) : setSome (sigmaEval body_R w) (sigmaEval body_S w) ↔ - ∃ d, (body_R d).truth w = true ∧ (body_S d).truth w = true := by + ∃ d, (body_R d).truth w ∧ (body_S d).truth w := by simp [setSome, Set.Nonempty, sigmaEval] end GQ @@ -213,7 +192,7 @@ Three-argument necessity: the modal base β restricted by W₁ is included in W₂. When W₁ = ⊤, reduces to β ⊆ W₂. The modal base β corresponds to `accessRelToBase R w` for an -`BAccessRel W` from `Core.Logic.Intensional`. `PIP.Connectives.must` +`AccessRel W` from `Core.Logic.Intensional`. `PIP.Connectives.must` provides the dynamic implementation; `must_truth_iff_mustBase` below bridges the static `PIPExprF.must` to this set-based formulation. Cf. `Semantics.Modality.Kratzer.simpleNecessity` for the @@ -258,37 +237,25 @@ theorem modal_duality (β W₁ W₂ : Set W) : exact gq_duality (β ∩ W₁) W₂ /-- Convert an accessibility relation to a modal base at world w. -/ -def accessRelToBase (R : BAccessRel W) (w : W) : Set W := - { w' | R w w' = true } - -/-- `PIPExprF.must R φ` truth agrees with three-argument `mustBase`. -/ -theorem must_truth_iff_mustBase {D : Type*} [FiniteDomain D] [Fintype W] - (R : BAccessRel W) (φ : PIPExprF W D) (w : W) : - (PIPExprF.must R φ).truth w = true ↔ - mustBase (accessRelToBase R w) Set.univ { w' | φ.truth w' = true } := by - simp only [mustBase, accessRelToBase, Set.inter_univ, Set.subset_def, Set.mem_setOf_eq] - constructor - · intro h w' hw' - exact List.all_eq_true.mp h w' (List.mem_filter.mpr ⟨Finset.mem_toList.mpr (Finset.mem_univ w'), hw'⟩) - · intro h - apply List.all_eq_true.mpr - intro w' hw' - exact h w' (List.mem_filter.mp hw').2 +def accessRelToBase (R : AccessRel W) (w : W) : Set W := + { w' | R w w' } + +/-- `PIPExprF.must R φ` truth agrees with three-argument `mustBase`. + Direct, since `must` truth is `boxR` and `mustBase` is set inclusion. -/ +theorem must_truth_iff_mustBase {D : Type*} + (R : AccessRel W) (φ : PIPExprF W D) (w : W) : + (PIPExprF.must R φ).truth w ↔ + mustBase (accessRelToBase R w) Set.univ { w' | φ.truth w' } := by + simp only [mustBase, accessRelToBase, Set.inter_univ, Set.subset_def, Set.mem_setOf_eq, + PIPExprF.truth, boxR] /-- `PIPExprF.might R φ` truth agrees with three-argument `mightBase`. -/ -theorem might_truth_iff_mightBase {D : Type*} [FiniteDomain D] [Fintype W] - (R : BAccessRel W) (φ : PIPExprF W D) (w : W) : - (PIPExprF.might R φ).truth w = true ↔ - mightBase (accessRelToBase R w) Set.univ { w' | φ.truth w' = true } := by +theorem might_truth_iff_mightBase {D : Type*} + (R : AccessRel W) (φ : PIPExprF W D) (w : W) : + (PIPExprF.might R φ).truth w ↔ + mightBase (accessRelToBase R w) Set.univ { w' | φ.truth w' } := by simp only [mightBase, accessRelToBase, Set.inter_univ, Set.Nonempty, - Set.mem_inter_iff, Set.mem_setOf_eq] - constructor - · intro h - obtain ⟨w', hw'_mem, hw'_sat⟩ := List.any_eq_true.mp h - exact ⟨w', (List.mem_filter.mp hw'_mem).2, hw'_sat⟩ - · intro ⟨w', hw'R, hw'φ⟩ - apply List.any_eq_true.mpr - exact ⟨w', List.mem_filter.mpr ⟨Finset.mem_toList.mpr (Finset.mem_univ w'), hw'R⟩, hw'φ⟩ + Set.mem_inter_iff, Set.mem_setOf_eq, PIPExprF.truth, diamondR] end ThreeArgModals @@ -306,7 +273,7 @@ FX (↑f): lift a thematic-role predicate into a formula modifier. ↑f = λφλx. f(x) ∧ φ (base case, when f : ⟨e, t⟩) -Given a predicate `f : D → W → Bool` (e.g., AGENT, PATIENT), +Given a predicate `f : D → W → Prop` (e.g., AGENT, PATIENT), `fxApply f φ x` conjoins `f(x)` with formula `φ`, producing a restricted variable: x is constrained to satisfy both `f` and `φ`. @@ -319,27 +286,24 @@ Cf. `Semantics.ArgumentStructure.ThematicRel` for the general Davidsonian role type `Entity → Event → Prop`; FX is PIP's mechanism for composing such roles with restricted variables. -/ -def fxApply (f : D → W → Bool) (φ : W → Bool) (x : D) : W → Bool := - λ w => f x w && φ w +def fxApply (f : D → W → Prop) (φ : W → Prop) (x : D) : W → Prop := + λ w => f x w ∧ φ w /-- FX entails the role predicate. -/ -theorem fxApply_entails_role (f : D → W → Bool) (φ : W → Bool) (x : D) (w : W) - (h : fxApply f φ x w = true) : f x w = true := by - simp only [fxApply, Bool.and_eq_true] at h; exact h.1 +theorem fxApply_entails_role (f : D → W → Prop) (φ : W → Prop) (x : D) (w : W) + (h : fxApply f φ x w) : f x w := h.1 /-- FX entails the formula body. -/ -theorem fxApply_entails_body (f : D → W → Bool) (φ : W → Bool) (x : D) (w : W) - (h : fxApply f φ x w = true) : φ w = true := by - simp only [fxApply, Bool.and_eq_true] at h; exact h.2 +theorem fxApply_entails_body (f : D → W → Prop) (φ : W → Prop) (x : D) (w : W) + (h : fxApply f φ x w) : φ w := h.2 /-- Iterated FX accumulates assertions: ↑g(↑f(φ))(x) = g(x) ∧ f(x) ∧ φ. -/ -theorem fxApply_twice (f g : D → W → Bool) (φ : W → Bool) (x : D) (w : W) : - fxApply g (fxApply f φ x) x w = (g x w && f x w && φ w) := by - simp [fxApply, Bool.and_assoc] +theorem fxApply_twice (f g : D → W → Prop) (φ : W → Prop) (x : D) (w : W) : + fxApply g (fxApply f φ x) x w = (g x w ∧ f x w ∧ φ w) := rfl -/-- FX with tautological formula: ↑f(⊤)(x) = f(x). -/ -theorem fxApply_true (f : D → W → Bool) (x : D) (w : W) : - fxApply f (λ _ => true) x w = f x w := by +/-- FX with tautological formula: ↑f(⊤)(x) ↔ f(x). -/ +theorem fxApply_true (f : D → W → Prop) (x : D) (w : W) : + fxApply f (λ _ => True) x w ↔ f x w := by simp [fxApply] end FX @@ -378,11 +342,11 @@ denotation = `sigmaEval` by the paper's own analysis. section Subordination -variable {W D : Type*} [FiniteDomain D] [Fintype W] +variable {W D : Type*} /-- Sigma is monotone: stronger body conditions produce smaller sets. -/ theorem sigma_monotone (φ ψ : D → PIPExprF W D) (w : W) - (h : ∀ d, (ψ d).truth w = true → (φ d).truth w = true) : + (h : ∀ d, (ψ d).truth w → (φ d).truth w) : sigmaEval ψ w ⊆ sigmaEval φ w := λ _ hd => h _ hd diff --git a/Linglib/Studies/KeshetAbney2024/Connectives.lean b/Linglib/Studies/KeshetAbney2024/Connectives.lean index f62146bbc..69a5d68e7 100644 --- a/Linglib/Studies/KeshetAbney2024/Connectives.lean +++ b/Linglib/Studies/KeshetAbney2024/Connectives.lean @@ -24,7 +24,7 @@ PIP's modals are generalized quantifiers over worlds (paper Section 2.5): - MIGHT^β_w(W₁, W₂) ≜ SOME(β_w ∩ W₁, W₂) - MUST^β_w(W₁, W₂) ≜ EVERY(β_w ∩ W₁, W₂) -Our encoding parameterizes by an accessibility relation (`KeshetAbney2024.PIP.BAccessRel`, +Our encoding parameterizes by an accessibility relation (`KeshetAbney2024.PIP.AccessRel`, equivalent to a Kratzer modal base β) and quantifies over accessible worlds. The grounding theorem `must_truth_agrees_boxR` proves that PIP's `must` produces the same truth conditions as `Core.Logic.Intensional.boxR`. @@ -34,6 +34,7 @@ produces the same truth conditions as `Core.Logic.Intensional.boxR`. namespace KeshetAbney2024.PIP open Semantics.Dynamic.Core +open Core.Logic.Intensional (AccessRel boxR diamondR boxR_T) variable {W E : Type*} @@ -46,7 +47,7 @@ variable {W E : Type*} Atomic predicate: filters the info state to pairs satisfying the predicate. Labels are preserved. -/ -def atom (pred : ICDRTAssignment W E → W → Bool) : PUpdate W E := +def atom (pred : ICDRTAssignment W E → W → Prop) : PUpdate W E := λ d => d.mapInfo (λ c => { gw ∈ c | pred gw.1 gw.2 }) /-- @@ -115,7 +116,7 @@ negation and modal operators. This is what enables: - Paycheck pronouns: "John spent his paycheck. Bill saved it." -/ def existsLabeled (α : FLabel) (v : IVar) (domain : Set E) - (bodyPred : ICDRTAssignment W E → W → Bool) + (bodyPred : ICDRTAssignment W E → W → Prop) (body : PUpdate W E) : PUpdate W E := λ d => let extended : IContext W E := @@ -163,18 +164,18 @@ would produce no accessible-world pairs for universal modals to check, making must/would vacuously satisfied and losing the modal subordination mechanism. -/ -def modalExpand (c : IContext W E) (access : BAccessRel W) : IContext W E := - c ∪ { gw | ∃ w₀, (gw.1, w₀) ∈ c ∧ access w₀ gw.2 = true } +def modalExpand (c : IContext W E) (access : AccessRel W) : IContext W E := + c ∪ { gw | ∃ w₀, (gw.1, w₀) ∈ c ∧ access w₀ gw.2 } /-- Modal expansion includes all original pairs. -/ -theorem modalExpand_superset (c : IContext W E) (access : BAccessRel W) : +theorem modalExpand_superset (c : IContext W E) (access : AccessRel W) : c ⊆ modalExpand c access := by intro x hx; left; exact hx /-- Modal expansion adds accessible-world pairs. -/ -theorem modalExpand_adds_accessible (c : IContext W E) (access : BAccessRel W) +theorem modalExpand_adds_accessible (c : IContext W E) (access : AccessRel W) (g : ICDRTAssignment W E) (w₀ w₁ : W) - (hc : (g, w₀) ∈ c) (hacc : access w₀ w₁ = true) : + (hc : (g, w₀) ∈ c) (hacc : access w₀ w₁) : (g, w₁) ∈ modalExpand c access := by right; exact ⟨w₀, hc, hacc⟩ @@ -197,13 +198,13 @@ subordination work: "A wolf might come in" introduces the wolf (local) under the modal's world quantification (external). The wolf's descriptive content (via the label) is accessible in subsequent discourse. -/ -def must (access : BAccessRel W) (allWorlds : List W) +def must (access : AccessRel W) (allWorlds : List W) (body : PUpdate W E) : PUpdate W E := λ d => let bodyResult := body { d with info := modalExpand d.info access } let result : IContext W E := { gw ∈ d.info | - ∀ w₁ ∈ allWorlds, access gw.2 w₁ = true → (gw.1, w₁) ∈ bodyResult.info } + ∀ w₁ ∈ allWorlds, access gw.2 w₁ → (gw.1, w₁) ∈ bodyResult.info } -- Labels from the body propagate outward { info := result, labels := bodyResult.labels } @@ -216,13 +217,13 @@ Modal possibility (might): existential quantification over accessible worlds. Like `must`, the body is evaluated on an expanded context (via `modalExpand`) and the world variable is external. -/ -def might (access : BAccessRel W) (allWorlds : List W) +def might (access : AccessRel W) (allWorlds : List W) (body : PUpdate W E) : PUpdate W E := λ d => let bodyResult := body { d with info := modalExpand d.info access } let result : IContext W E := { gw ∈ d.info | - ∃ w₁ ∈ allWorlds, access gw.2 w₁ = true ∧ (gw.1, w₁) ∈ bodyResult.info } + ∃ w₁ ∈ allWorlds, access gw.2 w₁ ∧ (gw.1, w₁) ∈ bodyResult.info } { info := result, labels := bodyResult.labels } /-- @@ -233,7 +234,7 @@ In the paper's modal subordination analysis, "It would eat you first" is analyzed as MUST with the same accessibility relation from "might" in the preceding sentence. So `would` = `must` with the inherited modal base. -/ -def would (access : BAccessRel W) (allWorlds : List W) +def would (access : AccessRel W) (allWorlds : List W) (body : PUpdate W E) : PUpdate W E := must access allWorlds body @@ -263,12 +264,12 @@ Labels survive modal operators. Labels registered inside a modal scope propagate to the outer discourse state. This is what enables modal subordination. -/ -theorem labels_survive_must (access : BAccessRel W) (allWorlds : List W) +theorem labels_survive_must (access : AccessRel W) (allWorlds : List W) (body : PUpdate W E) (desc : Description W E) (h : (body { d with info := modalExpand d.info access }).labels.lookup α = some desc) : (must access allWorlds body d).labels.lookup α = some desc := h -theorem labels_survive_might (access : BAccessRel W) (allWorlds : List W) +theorem labels_survive_might (access : AccessRel W) (allWorlds : List W) (body : PUpdate W E) (desc : Description W E) (h : (body { d with info := modalExpand d.info access }).labels.lookup α = some desc) : (might access allWorlds body d).labels.lookup α = some desc := h @@ -280,36 +281,23 @@ end Properties -- Grounding: PIP modals ↔ Core.Logic.Intensional.boxR/diamondR -- ============================================================ -open Core.Logic.Intensional (boxR diamondR boxR_T) - -/-- Lift a Bool-valued accessibility to its Prop-valued equivalent. -/ -private def liftR {W : Type*} (R : BAccessRel W) : W → W → Prop := - fun a b => R a b = true - -/-- Lift a Bool-valued world predicate to its Prop-valued equivalent. -/ -private def liftP {W : Type*} (p : W → Bool) : W → Prop := - fun w => p w = true - /-- PIP's `must` produces the same truth conditions as `Core.Logic.Intensional.boxR`. Specifically: a pair (g, w₀) survives `must R allWorlds (atom p)` iff -`boxR R (fun w => p g w = true) w₀` — the body predicate holds at -all R-accessible worlds. This connects PIP's discourse-update modals to the -standard Kripke semantics used throughout `Semantics/Modality/`. +`boxR R (p g) w₀` — the body predicate holds at all R-accessible worlds. +This connects PIP's discourse-update modals to the standard Kripke semantics +used throughout `Semantics/Modality/`. Since accessibility is now the +project-canonical Prop-valued `AccessRel`, the identity is direct — no lift. -/ theorem must_truth_agrees_boxR [Fintype W] - (R : BAccessRel W) (p : ICDRTAssignment W E → W → Bool) + (R : AccessRel W) (p : ICDRTAssignment W E → W → Prop) (d : Discourse W E) (g : ICDRTAssignment W E) (w₀ : W) (hd : (g, w₀) ∈ d.info) : ((g, w₀) ∈ (must R (Finset.univ : Finset W).toList (atom p) d).info) ↔ - boxR (liftR R) (liftP (p g)) w₀ := by + boxR R (p g) w₀ := by constructor - · intro ⟨_, h⟩ - intro v hRv - have hmem : v ∈ (Finset.univ : Finset W).toList.filter (R w₀) := by - simp only [List.mem_filter] - exact ⟨Finset.mem_toList.mpr (Finset.mem_univ v), hRv⟩ + · intro ⟨_, h⟩ v hRv have := h v (Finset.mem_toList.mpr (Finset.mem_univ v)) hRv unfold atom Discourse.mapInfo at this exact this.2 @@ -317,18 +305,17 @@ theorem must_truth_agrees_boxR [Fintype W] refine ⟨hd, ?_⟩ intro w₁ _hw₁ hacc unfold atom Discourse.mapInfo - refine ⟨modalExpand_adds_accessible d.info R g w₀ w₁ hd hacc, ?_⟩ - exact hbox w₁ hacc + exact ⟨modalExpand_adds_accessible d.info R g w₀ w₁ hd hacc, hbox w₁ hacc⟩ /-- PIP's `might` agrees with `diamondR`. -/ theorem might_truth_agrees_diamondR [Fintype W] - (R : BAccessRel W) (p : ICDRTAssignment W E → W → Bool) + (R : AccessRel W) (p : ICDRTAssignment W E → W → Prop) (d : Discourse W E) (g : ICDRTAssignment W E) (w₀ : W) (hd : (g, w₀) ∈ d.info) : ((g, w₀) ∈ (might R (Finset.univ : Finset W).toList (atom p) d).info) ↔ - diamondR (liftR R) (liftP (p g)) w₀ := by + diamondR R (p g) w₀ := by constructor · intro ⟨_, w₁, _, hacc, hmem⟩ unfold atom Discourse.mapInfo at hmem @@ -340,24 +327,23 @@ theorem might_truth_agrees_diamondR [Fintype W] /-- Realistic modal base (T axiom) for PIP: if R is reflexive and `must R (atom p)` -holds at (g, w₀), then p g w₀ = true. +holds at (g, w₀), then `p g w₀`. This derives PIP's key insight — must allows anaphora because a realistic modal base guarantees the description holds at the evaluation world — from `Core.Logic.Intensional.boxR_T`. -/ theorem must_realistic_of_refl [Fintype W] - (R : BAccessRel W) [Std.Refl (liftR R)] - (p : ICDRTAssignment W E → W → Bool) + (R : AccessRel W) [Std.Refl R] + (p : ICDRTAssignment W E → W → Prop) (d : Discourse W E) (g : ICDRTAssignment W E) (w₀ : W) (hd : (g, w₀) ∈ d.info) (hmust : (g, w₀) ∈ (must R (Finset.univ : Finset W).toList (atom p) d).info) : - p g w₀ = true := - boxR_T (liftR R) (liftP (p g)) w₀ - ((must_truth_agrees_boxR R p d g w₀ hd).mp hmust) + p g w₀ := + boxR_T R (p g) w₀ ((must_truth_agrees_boxR R p d g w₀ hd).mp hmust) /-- -Pointwise realistic base: if R w₀ w₀ = true and must holds at w₀, +Pointwise realistic base: if `R w₀ w₀` and must holds at w₀, the body predicate holds at w₀. This is the version that applies to non-globally-reflexive relations @@ -365,11 +351,11 @@ This is the version that applies to non-globally-reflexive relations @cite{kratzer-1991}'s realistic modal base without requiring global reflexivity. -/ theorem must_realistic_at [Fintype W] - (R : BAccessRel W) (p : ICDRTAssignment W E → W → Bool) + (R : AccessRel W) (p : ICDRTAssignment W E → W → Prop) (d : Discourse W E) (g : ICDRTAssignment W E) (w₀ : W) - (hRefl_at : R w₀ w₀ = true) + (hRefl_at : R w₀ w₀) (hmust : (g, w₀) ∈ (must R (Finset.univ : Finset W).toList (atom p) d).info) : - p g w₀ = true := by + p g w₀ := by obtain ⟨_, h⟩ := hmust have := h w₀ (Finset.mem_toList.mpr (Finset.mem_univ w₀)) hRefl_at unfold atom Discourse.mapInfo at this diff --git a/Linglib/Studies/KeshetAbney2024/Felicity.lean b/Linglib/Studies/KeshetAbney2024/Felicity.lean index cf524a0c2..75b125623 100644 --- a/Linglib/Studies/KeshetAbney2024/Felicity.lean +++ b/Linglib/Studies/KeshetAbney2024/Felicity.lean @@ -57,6 +57,8 @@ world and assignment consistent with γ. namespace KeshetAbney2024.PIP.Felicity +open Core.Logic.Intensional (AccessRel boxR diamondR) + variable {W : Type*} @@ -81,7 +83,7 @@ and correctly implements the F operator for items 41–42, 44–45c. -/ inductive PIPExpr (W : Type*) where /-- Atomic predicate: P_w(x₁, ..., xₙ). Always felicitous. -/ - | pred (p : W → Bool) + | pred (p : W → Prop) /-- Conjunction: φ ∧ ψ. Felicity is asymmetric (Karttunen). -/ | conj (φ ψ : PIPExpr W) /-- Negation: ¬φ. Felicity passes through. -/ @@ -91,7 +93,7 @@ inductive PIPExpr (W : Type*) where /-- Implication: φ → ψ. -/ | impl (φ ψ : PIPExpr W) /-- Presupposition: φ|ψ. Assert φ, presuppose ψ. -/ - | presup (φ : PIPExpr W) (ψ : W → Bool) + | presup (φ : PIPExpr W) (ψ : W → Prop) -- ============================================================ @@ -104,12 +106,12 @@ Truth evaluation for PIP expressions. PIP truth conditions are classical: presuppositions play no role in determining truth values. φ|ψ is true iff φ is true. -/ -def PIPExpr.truth : PIPExpr W → (W → Bool) +def PIPExpr.truth : PIPExpr W → (W → Prop) | .pred p => p - | .conj φ ψ => λ w => φ.truth w && ψ.truth w - | .neg φ => λ w => (φ.truth w).not - | .disj φ ψ => λ w => φ.truth w || ψ.truth w - | .impl φ ψ => λ w => (φ.truth w).not || ψ.truth w + | .conj φ ψ => λ w => φ.truth w ∧ ψ.truth w + | .neg φ => λ w => ¬ φ.truth w + | .disj φ ψ => λ w => φ.truth w ∨ ψ.truth w + | .impl φ ψ => λ w => φ.truth w → ψ.truth w | .presup φ _ψ => φ.truth -- presupposition doesn't affect truth @@ -125,19 +127,19 @@ F determines whether a PIP expression is felicitous (well-defined) relative to a world w. Every failure of F traces to a presupposition violation. -/ -def PIPExpr.felicitous : PIPExpr W → (W → Bool) - -- F(P(α₁,...,αₙ)) = true (atoms are always felicitous) - | .pred _ => λ _ => true +def PIPExpr.felicitous : PIPExpr W → (W → Prop) + -- F(P(α₁,...,αₙ)) = ⊤ (atoms are always felicitous) + | .pred _ => λ _ => True -- F(φ ∧ ψ) iff Fφ ∧ (φ → Fψ) [Karttunen's asymmetric conjunction] - | .conj φ ψ => λ w => φ.felicitous w && ((φ.truth w).not || ψ.felicitous w) + | .conj φ ψ => λ w => φ.felicitous w ∧ (φ.truth w → ψ.felicitous w) -- F(¬φ) iff Fφ | .neg φ => φ.felicitous -- F(φ ∨ ψ) iff Fφ ∧ (¬φ → Fψ) - | .disj φ ψ => λ w => φ.felicitous w && (φ.truth w || ψ.felicitous w) + | .disj φ ψ => λ w => φ.felicitous w ∧ (¬ φ.truth w → ψ.felicitous w) -- F(φ → ψ) iff Fφ ∧ (φ → Fψ) - | .impl φ ψ => λ w => φ.felicitous w && ((φ.truth w).not || ψ.felicitous w) + | .impl φ ψ => λ w => φ.felicitous w ∧ (φ.truth w → ψ.felicitous w) -- F(φ|ψ) iff Fφ ∧ ψ [presupposition must hold] - | .presup φ ψ => λ w => φ.felicitous w && ψ w + | .presup φ ψ => λ w => φ.felicitous w ∧ ψ w -- ============================================================ @@ -149,34 +151,33 @@ theorem felicitous_neg (φ : PIPExpr W) (w : W) : (PIPExpr.neg φ).felicitous w = φ.felicitous w := rfl /-- F(φ|ψ) iff Fφ ∧ ψ(w) (paper item 41) -/ -theorem felicitous_presup (φ : PIPExpr W) (ψ : W → Bool) (w : W) : - (PIPExpr.presup φ ψ).felicitous w = (φ.felicitous w && ψ w) := rfl +theorem felicitous_presup (φ : PIPExpr W) (ψ : W → Prop) (w : W) : + (PIPExpr.presup φ ψ).felicitous w = (φ.felicitous w ∧ ψ w) := rfl /-- Presupposition truth-independence: φ|ψ is true iff φ is true -/ -theorem presup_truth_independent (φ : PIPExpr W) (ψ : W → Bool) (w : W) : +theorem presup_truth_independent (φ : PIPExpr W) (ψ : W → Prop) (w : W) : (PIPExpr.presup φ ψ).truth w = φ.truth w := rfl /-- Conjunction felicity is asymmetric (paper item 42, @cite{karttunen-1973}): the first conjunct can satisfy presuppositions of the second. -/ theorem felicitous_conj (φ ψ : PIPExpr W) (w : W) : (PIPExpr.conj φ ψ).felicitous w = - (φ.felicitous w && ((φ.truth w).not || ψ.felicitous w)) := rfl + (φ.felicitous w ∧ (φ.truth w → ψ.felicitous w)) := rfl /-- If the first conjunct is true and both are felicitous, the conjunction is felicitous. -/ theorem felicitous_conj_of_both (φ ψ : PIPExpr W) (w : W) - (hFφ : φ.felicitous w = true) - (hFψ : ψ.felicitous w = true) : - (PIPExpr.conj φ ψ).felicitous w = true := by - unfold PIPExpr.felicitous - rw [hFφ, hFψ]; simp + (hFφ : φ.felicitous w) + (hFψ : ψ.felicitous w) : + (PIPExpr.conj φ ψ).felicitous w := + ⟨hFφ, fun _ => hFψ⟩ /-- If the first conjunct is false, its felicity suffices for the conjunction. -/ theorem felicitous_conj_of_false_first (φ ψ : PIPExpr W) (w : W) - (hFφ : φ.felicitous w = true) - (hTφ : φ.truth w = false) : - (PIPExpr.conj φ ψ).felicitous w = true := by - rw [felicitous_conj, hFφ, hTφ]; simp + (hFφ : φ.felicitous w) + (hTφ : ¬ φ.truth w) : + (PIPExpr.conj φ ψ).felicitous w := + ⟨hFφ, fun ht => absurd ht hTφ⟩ -- ============================================================ @@ -189,8 +190,8 @@ felicity conditions are met at every world in the context set. This captures the paper's item 40: F(Σw(φ₁ ∧ ... ∧ φₙ)) -/ -def discourseFelicitous (φ : PIPExpr W) (contextSet : W → Bool) : Prop := - ∀ w, contextSet w = true → φ.felicitous w = true +def discourseFelicitous (φ : PIPExpr W) (contextSet : W → Prop) : Prop := + ∀ w, contextSet w → φ.felicitous w /-- Incremental felicity: adding sentence ψ to a felicitous discourse φ @@ -199,7 +200,7 @@ requires that ψ's presuppositions are met whenever φ is true. This captures the paper's item 51: ∀wxy(γ → Fφ) -/ def incrementallyFelicitous (γ ψ : PIPExpr W) : Prop := - ∀ w, γ.truth w = true → ψ.felicitous w = true + ∀ w, γ.truth w → ψ.felicitous w -- ============================================================ @@ -213,8 +214,8 @@ A pronoun presupposes that its denotation is non-empty (and singular for singular pronouns). In PIP, this is modeled as a presupposition on the summation term: SINGLE(Σxφ). -/ -def singlePresup (denotation : W → Bool) : PIPExpr W := - .presup (.pred (λ _ => true)) denotation +def singlePresup (denotation : W → Prop) : PIPExpr W := + .presup (.pred (λ _ => True)) denotation /-- Might blocks anaphora: might(φ) does not guarantee that the @@ -226,15 +227,14 @@ introduced by φ will have an empty denotation at w, causing presupposition failure. -/ theorem might_blocks_anaphora - (φ_accessible : W → Bool) -- φ holds at some accessible worlds - (pronoun_presup : W → Bool) -- pronoun presupposes entity exists + (φ_accessible : W → Prop) -- φ holds at some accessible worlds + (pronoun_presup : W → Prop) -- pronoun presupposes entity exists (w : W) - (h_might : φ_accessible w = false) -- φ doesn't hold at w itself - (h_presup_needs : pronoun_presup w = φ_accessible w) : - (singlePresup pronoun_presup).felicitous w = false := by - unfold singlePresup - show (true && pronoun_presup w) = false - rw [h_presup_needs, h_might]; rfl + (h_might : ¬ φ_accessible w) -- φ doesn't hold at w itself + (h_presup_needs : pronoun_presup w ↔ φ_accessible w) : + ¬ (singlePresup pronoun_presup).felicitous w := by + intro hfel + exact h_might (h_presup_needs.mp hfel.2) /-- Must allows anaphora: if must(φ) is true at w (with a realistic @@ -242,15 +242,13 @@ modal base), then φ holds at w (since w is accessible from itself). The pronoun's presupposition is satisfied. -/ theorem must_allows_anaphora - (φ_everywhere : W → Bool) -- φ holds at all accessible worlds - (pronoun_presup : W → Bool) -- pronoun presupposes entity exists + (φ_everywhere : W → Prop) -- φ holds at all accessible worlds + (pronoun_presup : W → Prop) -- pronoun presupposes entity exists (w : W) - (h_must_realistic : φ_everywhere w = true) -- realistic: w is accessible from w - (h_presup_follows : pronoun_presup w = φ_everywhere w) : - (singlePresup pronoun_presup).felicitous w = true := by - unfold singlePresup - show (true && pronoun_presup w) = true - rw [h_presup_follows, h_must_realistic]; rfl + (h_must_realistic : φ_everywhere w) -- realistic: w is accessible from w + (h_presup_follows : pronoun_presup w ↔ φ_everywhere w) : + (singlePresup pronoun_presup).felicitous w := + ⟨trivial, h_presup_follows.mpr h_must_realistic⟩ -- ============================================================ @@ -287,29 +285,21 @@ This section derives: section FullFelicity -variable {W D : Type*} [FiniteDomain D] [Fintype W] +variable {W D : Type*} -- ======== Prop-level iff characterizations ======== /-- F(∃xφ) iff ∀d, F(φ(d)) — existential felicity is universal - over the domain (item 39d). -/ + over the domain (item 39d). Holds by definition. -/ theorem existsF_felicitous_iff (body : D → PIPExprF W D) (w : W) : - (PIPExprF.exists_ body).felicitous w = true ↔ - ∀ d, (body d).felicitous w = true := by - simp only [PIPExprF.felicitous] - constructor - · intro h d; exact List.all_eq_true.mp h d (FiniteDomain.complete d) - · intro h; exact List.all_eq_true.mpr (λ d _ => h d) + (PIPExprF.exists_ body).felicitous w ↔ ∀ d, (body d).felicitous w := + Iff.rfl -/-- F(∀xφ) iff ∀d, F(φ(d)) (item 35). -/ +/-- F(∀xφ) iff ∀d, F(φ(d)) (item 35). Holds by definition. -/ theorem forallF_felicitous_iff (body : D → PIPExprF W D) (w : W) : - (PIPExprF.forall_ body).felicitous w = true ↔ - ∀ d, (body d).felicitous w = true := by - simp only [PIPExprF.felicitous] - constructor - · intro h d; exact List.all_eq_true.mp h d (FiniteDomain.complete d) - · intro h; exact List.all_eq_true.mpr (λ d _ => h d) + (PIPExprF.forall_ body).felicitous w ↔ ∀ d, (body d).felicitous w := + Iff.rfl /-- ∃ and ∀ have identical felicity clauses — both project universally. The difference is only in truth conditions (∃ vs ∀). -/ @@ -317,34 +307,21 @@ theorem existsF_forallF_felicity_agree (body : D → PIPExprF W D) (w : W) : (PIPExprF.exists_ body).felicitous w = (PIPExprF.forall_ body).felicitous w := rfl -/-- F(□_R φ) iff φ is felicitous at every R-accessible world. -/ -theorem mustF_felicitous_iff (R : BAccessRel W) (φ : PIPExprF W D) (w : W) : - (PIPExprF.must R φ).felicitous w = true ↔ - ∀ w', R w w' = true → φ.felicitous w' = true := by - simp only [PIPExprF.felicitous] - constructor - · intro h w' hw' - exact List.all_eq_true.mp h w' - (List.mem_filter.mpr ⟨Finset.mem_toList.mpr (Finset.mem_univ w'), hw'⟩) - · intro h - exact List.all_eq_true.mpr (λ w' hw' => h w' (List.mem_filter.mp hw').2) +/-- F(□_R φ) iff φ is felicitous at every R-accessible world. + Holds by definition (`must` felicity is `boxR`). -/ +theorem mustF_felicitous_iff (R : AccessRel W) (φ : PIPExprF W D) (w : W) : + (PIPExprF.must R φ).felicitous w ↔ ∀ w', R w w' → φ.felicitous w' := + Iff.rfl /-- F(◇_R φ) iff φ is felicitous at every R-accessible world. Truth is existential for ◇ but felicity is universal for both. -/ -theorem mightF_felicitous_iff (R : BAccessRel W) (φ : PIPExprF W D) (w : W) : - (PIPExprF.might R φ).felicitous w = true ↔ - ∀ w', R w w' = true → φ.felicitous w' = true := by - simp only [PIPExprF.felicitous] - constructor - · intro h w' hw' - exact List.all_eq_true.mp h w' - (List.mem_filter.mpr ⟨Finset.mem_toList.mpr (Finset.mem_univ w'), hw'⟩) - · intro h - exact List.all_eq_true.mpr (λ w' hw' => h w' (List.mem_filter.mp hw').2) +theorem mightF_felicitous_iff (R : AccessRel W) (φ : PIPExprF W D) (w : W) : + (PIPExprF.might R φ).felicitous w ↔ ∀ w', R w w' → φ.felicitous w' := + Iff.rfl /-- □ and ◇ have identical felicity clauses — both project universally. The asymmetry between must and might is in truth, not felicity. -/ -theorem mustF_mightF_felicity_agree (R : BAccessRel W) (φ : PIPExprF W D) (w : W) : +theorem mustF_mightF_felicity_agree (R : AccessRel W) (φ : PIPExprF W D) (w : W) : (PIPExprF.must R φ).felicitous w = (PIPExprF.might R φ).felicitous w := rfl @@ -365,21 +342,19 @@ Mathematically, this is `forall_and_right` (Mathlib): the presupposition ψ doesn't vary with d, so it factors out of `∀d, (F(φ(d)) ∧ ψ)`. -/ theorem existsF_presup_factored [Nonempty D] - (φ : D → PIPExprF W D) (ψ : W → Bool) (w : W) : - (PIPExprF.exists_ (λ d => PIPExprF.presup (φ d) ψ)).felicitous w = true ↔ - (∀ d, (φ d).felicitous w = true) ∧ ψ w = true := by - rw [existsF_felicitous_iff] - simp only [PIPExprF.felicitous, Bool.and_eq_true] + (φ : D → PIPExprF W D) (ψ : W → Prop) (w : W) : + (PIPExprF.exists_ (λ d => PIPExprF.presup (φ d) ψ)).felicitous w ↔ + (∀ d, (φ d).felicitous w) ∧ ψ w := by + simp only [PIPExprF.felicitous] exact forall_and_right _ _ /-- Factored projection through ∀ — identical to ∃ since both have the same felicity clause. -/ theorem forallF_presup_factored [Nonempty D] - (φ : D → PIPExprF W D) (ψ : W → Bool) (w : W) : - (PIPExprF.forall_ (λ d => PIPExprF.presup (φ d) ψ)).felicitous w = true ↔ - (∀ d, (φ d).felicitous w = true) ∧ ψ w = true := by - rw [forallF_felicitous_iff] - simp only [PIPExprF.felicitous, Bool.and_eq_true] + (φ : D → PIPExprF W D) (ψ : W → Prop) (w : W) : + (PIPExprF.forall_ (λ d => PIPExprF.presup (φ d) ψ)).felicitous w ↔ + (∀ d, (φ d).felicitous w) ∧ ψ w := by + simp only [PIPExprF.felicitous] exact forall_and_right _ _ /-- @@ -392,23 +367,21 @@ No `Nonempty` hypothesis needed: ψ varies with w', so this is a direct instance of `∀x, (P x ∧ Q x) ↔ (∀x, P x) ∧ (∀x, Q x)`. -/ theorem mustF_presup_factored - (R : BAccessRel W) (φ : PIPExprF W D) (ψ : W → Bool) (w : W) : - (PIPExprF.must R (PIPExprF.presup φ ψ)).felicitous w = true ↔ - (∀ w', R w w' = true → φ.felicitous w' = true) ∧ - (∀ w', R w w' = true → ψ w' = true) := by - rw [mustF_felicitous_iff] - simp only [PIPExprF.felicitous, Bool.and_eq_true] + (R : AccessRel W) (φ : PIPExprF W D) (ψ : W → Prop) (w : W) : + (PIPExprF.must R (PIPExprF.presup φ ψ)).felicitous w ↔ + (∀ w', R w w' → φ.felicitous w') ∧ + (∀ w', R w w' → ψ w') := by + simp only [PIPExprF.felicitous, boxR] exact ⟨fun h => ⟨fun w' hw' => (h w' hw').1, fun w' hw' => (h w' hw').2⟩, fun ⟨h1, h2⟩ w' hw' => ⟨h1 w' hw', h2 w' hw'⟩⟩ /-- Factored projection through ◇ — identical structure to □. -/ theorem mightF_presup_factored - (R : BAccessRel W) (φ : PIPExprF W D) (ψ : W → Bool) (w : W) : - (PIPExprF.might R (PIPExprF.presup φ ψ)).felicitous w = true ↔ - (∀ w', R w w' = true → φ.felicitous w' = true) ∧ - (∀ w', R w w' = true → ψ w' = true) := by - rw [mightF_felicitous_iff] - simp only [PIPExprF.felicitous, Bool.and_eq_true] + (R : AccessRel W) (φ : PIPExprF W D) (ψ : W → Prop) (w : W) : + (PIPExprF.might R (PIPExprF.presup φ ψ)).felicitous w ↔ + (∀ w', R w w' → φ.felicitous w') ∧ + (∀ w', R w w' → ψ w') := by + simp only [PIPExprF.felicitous, boxR] exact ⟨fun h => ⟨fun w' hw' => (h w' hw').1, fun w' hw' => (h w' hw').2⟩, fun ⟨h1, h2⟩ w' hw' => ⟨h1 w' hw', h2 w' hw'⟩⟩ @@ -418,34 +391,34 @@ theorem mightF_presup_factored /-- Presupposition extraction through ∃: if ∃x(φ(x)|ψ) is felicitous, then ψ holds. Follows from the factored form by projecting `.2`. -/ theorem existsF_presup_projection - (φ : D → PIPExprF W D) (ψ : W → Bool) (w : W) (d : D) - (hF : (PIPExprF.exists_ (λ d => PIPExprF.presup (φ d) ψ)).felicitous w = true) : - ψ w = true := + (φ : D → PIPExprF W D) (ψ : W → Prop) (w : W) (d : D) + (hF : (PIPExprF.exists_ (λ d => PIPExprF.presup (φ d) ψ)).felicitous w) : + ψ w := haveI : Nonempty D := ⟨d⟩ (existsF_presup_factored φ ψ w).mp hF |>.2 /-- Presupposition extraction through ∀. -/ theorem forallF_presup_projection - (φ : D → PIPExprF W D) (ψ : W → Bool) (w : W) (d : D) - (hF : (PIPExprF.forall_ (λ d => PIPExprF.presup (φ d) ψ)).felicitous w = true) : - ψ w = true := + (φ : D → PIPExprF W D) (ψ : W → Prop) (w : W) (d : D) + (hF : (PIPExprF.forall_ (λ d => PIPExprF.presup (φ d) ψ)).felicitous w) : + ψ w := haveI : Nonempty D := ⟨d⟩ (forallF_presup_factored φ ψ w).mp hF |>.2 /-- Presupposition extraction through □ at an accessible world. -/ theorem mustF_presup_at_accessible - (R : BAccessRel W) (φ : PIPExprF W D) (ψ : W → Bool) (w w' : W) - (hR : R w w' = true) - (hF : (PIPExprF.must R (PIPExprF.presup φ ψ)).felicitous w = true) : - ψ w' = true := + (R : AccessRel W) (φ : PIPExprF W D) (ψ : W → Prop) (w w' : W) + (hR : R w w') + (hF : (PIPExprF.must R (PIPExprF.presup φ ψ)).felicitous w) : + ψ w' := (mustF_presup_factored R φ ψ w).mp hF |>.2 w' hR /-- Presupposition extraction through ◇ at an accessible world. -/ theorem mightF_presup_at_accessible - (R : BAccessRel W) (φ : PIPExprF W D) (ψ : W → Bool) (w w' : W) - (hR : R w w' = true) - (hF : (PIPExprF.might R (PIPExprF.presup φ ψ)).felicitous w = true) : - ψ w' = true := + (R : AccessRel W) (φ : PIPExprF W D) (ψ : W → Prop) (w w' : W) + (hR : R w w') + (hF : (PIPExprF.might R (PIPExprF.presup φ ψ)).felicitous w) : + ψ w' := (mightF_presup_factored R φ ψ w).mp hF |>.2 w' hR @@ -457,8 +430,7 @@ theorem mightF_presup_at_accessible (Composition.lean) takes the same body type `D → PIPExprF W D` as `∃`, sigma felicity reduces to existential felicity. -/ theorem sigma_body_felicitous_iff (body : D → PIPExprF W D) (w : W) : - (∀ d, (body d).felicitous w = true) ↔ - (PIPExprF.exists_ body).felicitous w = true := + (∀ d, (body d).felicitous w) ↔ (PIPExprF.exists_ body).felicitous w := (existsF_felicitous_iff body w).symm end FullFelicity From 487131bda9f8e1db64fe99f06cda3c994b9e9f4c Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 29 May 2026 17:59:28 -0700 Subject: [PATCH 4/8] refactor(Studies/KeshetAbney2024): collapse PIP bridges onto Prop-native Core --- Linglib/Studies/KeshetAbney2024/Bridges.lean | 71 +++++++------------- 1 file changed, 25 insertions(+), 46 deletions(-) diff --git a/Linglib/Studies/KeshetAbney2024/Bridges.lean b/Linglib/Studies/KeshetAbney2024/Bridges.lean index d9a42ffac..8b0aead04 100644 --- a/Linglib/Studies/KeshetAbney2024/Bridges.lean +++ b/Linglib/Studies/KeshetAbney2024/Bridges.lean @@ -39,6 +39,7 @@ namespace KeshetAbney2024.PIP.Bridges open KeshetAbney2024.PIP open Semantics.Dynamic.Core (IVar ICDRTAssignment Entity IContext) +open Core.Logic.Intensional (AccessRel boxR diamondR) open Core.Logic.Intensional.Logic (frameConditions) @@ -69,23 +70,11 @@ and `felicitous` as `presup`. -/ theorem pip_felicity_agrees_with_andFilter {W : Type*} (φ ψ : Felicity.PIPExpr W) (w : W) : - ((Felicity.PIPExpr.conj φ ψ).felicitous w = true) ↔ + (Felicity.PIPExpr.conj φ ψ).felicitous w ↔ (Semantics.Presupposition.PrProp.andFilter - (({ presup w := φ.felicitous w = true, assertion w := φ.truth w = true } : Semantics.Presupposition.PrProp _)) - (({ presup w := ψ.felicitous w = true, assertion w := ψ.truth w = true } : Semantics.Presupposition.PrProp _))).presup w := by - simp only [Felicity.PIPExpr.felicitous, Semantics.Presupposition.PrProp.andFilter, - Bool.and_eq_true, Bool.or_eq_true] - constructor - · intro ⟨h1, h2⟩ - exact ⟨h1, fun ht => by - rcases h2 with h | h - · exact absurd ht (by simp [Bool.not_eq_true'] at h; rw [h]; decide) - · exact h⟩ - · intro ⟨h1, h2⟩ - refine ⟨h1, ?_⟩ - by_cases ht : φ.truth w = true - · exact Or.inr (h2 ht) - · simp [Bool.not_eq_true, ht] + (({ presup w := φ.felicitous w, assertion w := φ.truth w } : Semantics.Presupposition.PrProp _)) + (({ presup w := ψ.felicitous w, assertion w := ψ.truth w } : Semantics.Presupposition.PrProp _))).presup w := + Iff.rfl /-- PIP's negation felicity agrees with `PrProp.neg`: both preserve the @@ -93,10 +82,10 @@ presupposition/felicity of the negated expression unchanged. -/ theorem pip_felicity_agrees_with_neg {W : Type*} (φ : Felicity.PIPExpr W) (w : W) : - ((Felicity.PIPExpr.neg φ).felicitous w = true) ↔ + (Felicity.PIPExpr.neg φ).felicitous w ↔ (Semantics.Presupposition.PrProp.neg - (({ presup w := φ.felicitous w = true, assertion w := φ.truth w = true } : Semantics.Presupposition.PrProp _))).presup w := by - simp only [Felicity.PIPExpr.felicitous, Semantics.Presupposition.PrProp.neg] + (({ presup w := φ.felicitous w, assertion w := φ.truth w } : Semantics.Presupposition.PrProp _))).presup w := + Iff.rfl /-- PIP's implication felicity agrees with `PrProp.impFilter`. @@ -108,23 +97,11 @@ the antecedent can satisfy the consequent's presupposition. -/ theorem pip_felicity_agrees_with_impFilter {W : Type*} (φ ψ : Felicity.PIPExpr W) (w : W) : - ((Felicity.PIPExpr.impl φ ψ).felicitous w = true) ↔ + (Felicity.PIPExpr.impl φ ψ).felicitous w ↔ (Semantics.Presupposition.PrProp.impFilter - (({ presup w := φ.felicitous w = true, assertion w := φ.truth w = true } : Semantics.Presupposition.PrProp _)) - (({ presup w := ψ.felicitous w = true, assertion w := ψ.truth w = true } : Semantics.Presupposition.PrProp _))).presup w := by - simp only [Felicity.PIPExpr.felicitous, Semantics.Presupposition.PrProp.impFilter, - Bool.and_eq_true, Bool.or_eq_true] - constructor - · intro ⟨h1, h2⟩ - exact ⟨h1, fun ht => by - rcases h2 with h | h - · exact absurd ht (by simp [Bool.not_eq_true'] at h; rw [h]; decide) - · exact h⟩ - · intro ⟨h1, h2⟩ - refine ⟨h1, ?_⟩ - by_cases ht : φ.truth w = true - · exact Or.inr (h2 ht) - · simp [Bool.not_eq_true, ht] + (({ presup w := φ.felicitous w, assertion w := φ.truth w } : Semantics.Presupposition.PrProp _)) + (({ presup w := ψ.felicitous w, assertion w := ψ.truth w } : Semantics.Presupposition.PrProp _))).presup w := + Iff.rfl /-- PIP's disjunction felicity agrees with a one-sided filtering disjunction: @@ -132,9 +109,12 @@ PIP's disjunction felicity agrees with a one-sided filtering disjunction: -/ theorem pip_felicity_agrees_with_orFilter {W : Type*} (φ ψ : Felicity.PIPExpr W) (w : W) : - ((Felicity.PIPExpr.disj φ ψ).felicitous w = true) ↔ - (φ.felicitous w = true ∧ (φ.truth w = true ∨ ψ.felicitous w = true)) := by - simp only [Felicity.PIPExpr.felicitous, Bool.and_eq_true, Bool.or_eq_true] + (Felicity.PIPExpr.disj φ ψ).felicitous w ↔ + (φ.felicitous w ∧ (φ.truth w ∨ ψ.felicitous w)) := by + simp only [Felicity.PIPExpr.felicitous] + constructor + · rintro ⟨h1, h2⟩; exact ⟨h1, (Classical.em (φ.truth w)).imp id h2⟩ + · rintro ⟨h1, h2⟩; exact ⟨h1, fun hn => h2.resolve_left hn⟩ -- ============================================================ @@ -399,13 +379,12 @@ The composition: `mustBase (accessRelToBase R w) ⊤ {w' | φ w' = true}` ↔ `boxR (fun a b => R a b = true) (fun w' => φ w' = true) w`. Both express "the body holds at every R-accessible world from w". -/ -theorem mustBase_agrees_boxR {W D : Type*} [FiniteDomain D] [Fintype W] - (R : BAccessRel W) (φ : PIPExprF W D) (w : W) : - mustBase (accessRelToBase R w) Set.univ { w' | φ.truth w' = true } ↔ - Core.Logic.Intensional.boxR - (fun a b => R a b = true) (fun w' => φ.truth w' = true) w := by +theorem mustBase_agrees_boxR {W D : Type*} + (R : AccessRel W) (φ : PIPExprF W D) (w : W) : + mustBase (accessRelToBase R w) Set.univ { w' | φ.truth w' } ↔ + boxR R φ.truth w := by simp only [mustBase, accessRelToBase, Set.inter_univ, Set.subset_def, - Set.mem_setOf_eq, Core.Logic.Intensional.boxR] + Set.mem_setOf_eq, boxR] -- ============================================================ @@ -440,9 +419,9 @@ iff the static truth value is true. TODO: Full proof requires reasoning about `Set.sep` over singleton IContext. -/ theorem static_atom_agrees_dynamic {W E : Type*} - (p : ICDRTAssignment W E → W → Bool) (g : ICDRTAssignment W E) (w : W) + (p : ICDRTAssignment W E → W → Prop) (g : ICDRTAssignment W E) (w : W) (d : Discourse W E) (hd : (g, w) ∈ d.info) : - (g, w) ∈ (atom p d).info ↔ p g w = true := by + (g, w) ∈ (atom p d).info ↔ p g w := by unfold atom Discourse.mapInfo exact ⟨fun ⟨_, hp⟩ => hp, fun hp => ⟨hd, hp⟩⟩ From f0485eb9d3fc86410f8a952e136a69ea64d288f3 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 29 May 2026 18:32:50 -0700 Subject: [PATCH 5/8] refactor(Studies/KeshetAbney2024): Prop-native analysis files (Bool removed) --- Linglib/Studies/AbneyKeshet2025.lean | 124 ++++++++------- Linglib/Studies/KeshetAbney2024.lean | 217 +++++++++++++-------------- 2 files changed, 174 insertions(+), 167 deletions(-) diff --git a/Linglib/Studies/AbneyKeshet2025.lean b/Linglib/Studies/AbneyKeshet2025.lean index 8832b151d..40ee303f4 100644 --- a/Linglib/Studies/AbneyKeshet2025.lean +++ b/Linglib/Studies/AbneyKeshet2025.lean @@ -69,31 +69,34 @@ section SigmaFinite /-- Farmer predicate: true for alice and bob. -/ def farmerBody : Ent → PIPExprF W1 Ent - | .alice | .bob => .pred (λ _ => true) - | .spot | .rex => .pred (λ _ => false) + | .alice | .bob => .pred (λ _ => True) + | .spot | .rex => .pred (λ _ => False) /-- Donkey predicate: true for spot and rex. -/ def donkeyBody : Ent → PIPExprF W1 Ent - | .spot | .rex => .pred (λ _ => true) - | .alice | .bob => .pred (λ _ => false) + | .spot | .rex => .pred (λ _ => True) + | .alice | .bob => .pred (λ _ => False) /-- Alice is a farmer (in the sigma set). -/ -theorem sigma_farmer_alice : Ent.alice ∈ sigmaEval farmerBody W1.w0 := rfl +theorem sigma_farmer_alice : Ent.alice ∈ sigmaEval farmerBody W1.w0 := by + simp [sigmaEval, farmerBody, donkeyBody, PIPExprF.truth] /-- Bob is a farmer. -/ -theorem sigma_farmer_bob : Ent.bob ∈ sigmaEval farmerBody W1.w0 := rfl +theorem sigma_farmer_bob : Ent.bob ∈ sigmaEval farmerBody W1.w0 := by + simp [sigmaEval, farmerBody, donkeyBody, PIPExprF.truth] /-- Spot is not a farmer. -/ -theorem sigma_farmer_not_spot : Ent.spot ∉ sigmaEval farmerBody W1.w0 := Bool.false_ne_true +theorem sigma_farmer_not_spot : Ent.spot ∉ sigmaEval farmerBody W1.w0 := by simp [sigmaEval, farmerBody, donkeyBody, PIPExprF.truth] /-- Rex is not a farmer. -/ -theorem sigma_farmer_not_rex : Ent.rex ∉ sigmaEval farmerBody W1.w0 := Bool.false_ne_true +theorem sigma_farmer_not_rex : Ent.rex ∉ sigmaEval farmerBody W1.w0 := by simp [sigmaEval, farmerBody, donkeyBody, PIPExprF.truth] /-- Spot is a donkey. -/ -theorem sigma_donkey_spot : Ent.spot ∈ sigmaEval donkeyBody W1.w0 := rfl +theorem sigma_donkey_spot : Ent.spot ∈ sigmaEval donkeyBody W1.w0 := by + simp [sigmaEval, farmerBody, donkeyBody, PIPExprF.truth] /-- Alice is not a donkey. -/ -theorem sigma_donkey_not_alice : Ent.alice ∉ sigmaEval donkeyBody W1.w0 := Bool.false_ne_true +theorem sigma_donkey_not_alice : Ent.alice ∉ sigmaEval donkeyBody W1.w0 := by simp [sigmaEval, farmerBody, donkeyBody, PIPExprF.truth] end SigmaFinite @@ -119,7 +122,7 @@ theorem sigma_disj_farmer_donkey : /-- Verify: the farmer∧donkey intersection is empty. -/ theorem farmer_donkey_disjoint (d : Ent) : d ∉ sigmaEval (λ d => PIPExprF.conj (farmerBody d) (donkeyBody d)) W1.w0 := by - cases d <;> exact Bool.false_ne_true + cases d <;> rintro ⟨h1, h2⟩ <;> first | exact h1 | exact h2 end SigmaAlgebra @@ -132,8 +135,8 @@ section GQSigma /-- "Bought a donkey" predicate: alice and bob each bought one. -/ def boughtDonkeyBody : Ent → PIPExprF W1 Ent - | .alice | .bob => .pred (λ _ => true) - | .spot | .rex => .pred (λ _ => false) + | .alice | .bob => .pred (λ _ => True) + | .spot | .rex => .pred (λ _ => False) /-- EVERY(Σf farmer, Σf (farmer ∧ boughtDonkey)) — via `setEvery`. @@ -150,10 +153,10 @@ theorem every_farmer_bought_donkey : -- d ∈ sigmaEval farmerBody means (farmerBody d).truth w0 = true -- For alice and bob, boughtDonkeyBody also returns true cases d with - | alice => rfl - | bob => rfl - | spot => exact absurd hd Bool.false_ne_true - | rex => exact absurd hd Bool.false_ne_true + | alice => exact ⟨trivial, trivial⟩ + | bob => exact ⟨trivial, trivial⟩ + | spot => exact hd.elim + | rex => exact hd.elim /-- SOME(Σf donkey, Σf farmerBody) — no donkey is a farmer. @@ -163,10 +166,10 @@ theorem no_donkey_is_farmer : ¬setSome (sigmaEval donkeyBody W1.w0) (sigmaEval farmerBody W1.w0) := by intro ⟨d, hd, hf⟩ cases d with - | alice => exact absurd hd Bool.false_ne_true - | bob => exact absurd hd Bool.false_ne_true - | spot => exact absurd hf Bool.false_ne_true - | rex => exact absurd hf Bool.false_ne_true + | alice => exact hd.elim + | bob => exact hd.elim + | spot => exact hf.elim + | rex => exact hf.elim end GQSigma @@ -193,11 +196,12 @@ theorem farmer_buyer_subordination : /-- All farmer-buyers are indeed farmers (pointwise verification). -/ theorem farmer_buyer_alice : - Ent.alice ∈ sigmaEval (λ d => PIPExprF.conj (farmerBody d) (boughtDonkeyBody d)) W1.w0 := rfl + Ent.alice ∈ sigmaEval (λ d => PIPExprF.conj (farmerBody d) (boughtDonkeyBody d)) W1.w0 := by + simp [sigmaEval, farmerBody, boughtDonkeyBody, PIPExprF.truth] theorem farmer_buyer_spot_excluded : - Ent.spot ∉ sigmaEval (λ d => PIPExprF.conj (farmerBody d) (boughtDonkeyBody d)) W1.w0 := - Bool.false_ne_true + Ent.spot ∉ sigmaEval (λ d => PIPExprF.conj (farmerBody d) (boughtDonkeyBody d)) W1.w0 := by + rintro ⟨h, _⟩; exact h end Subordination @@ -209,17 +213,17 @@ end Subordination section ExistsSigma /-- ∃x(farmer(x)) is true (at least one farmer exists). -/ -theorem exists_farmer : (PIPExprF.exists_ farmerBody).truth W1.w0 = true := by decide +theorem exists_farmer : (PIPExprF.exists_ farmerBody).truth W1.w0 := ⟨.alice, trivial⟩ /-- The sigma bridge: ∃x(farmer(x)) ↔ nonempty sigma set. -/ theorem exists_farmer_bridge : - (PIPExprF.exists_ farmerBody).truth W1.w0 = true ↔ + (PIPExprF.exists_ farmerBody).truth W1.w0 ↔ (sigmaEval farmerBody W1.w0).Nonempty := exists_iff_sigma_nonempty farmerBody W1.w0 /-- ∀x(farmer(x)) is false (donkeys are not farmers). -/ theorem forall_farmer_false : - (PIPExprF.forall_ farmerBody).truth W1.w0 = false := by decide + ¬ (PIPExprF.forall_ farmerBody).truth W1.w0 := fun h => h .spot end ExistsSigma @@ -245,16 +249,18 @@ handled by `PIP.Bridges.plural`. /-- Both alice and bob are in the sigma set — exhaustive, not a single witness. -/ theorem strong_donkey_alice : Ent.alice ∈ sigmaEval - (λ d => PIPExprF.conj (farmerBody d) (boughtDonkeyBody d)) W1.w0 := rfl + (λ d => PIPExprF.conj (farmerBody d) (boughtDonkeyBody d)) W1.w0 := by + simp [sigmaEval, farmerBody, boughtDonkeyBody, PIPExprF.truth] theorem strong_donkey_bob : Ent.bob ∈ sigmaEval - (λ d => PIPExprF.conj (farmerBody d) (boughtDonkeyBody d)) W1.w0 := rfl + (λ d => PIPExprF.conj (farmerBody d) (boughtDonkeyBody d)) W1.w0 := by + simp [sigmaEval, farmerBody, boughtDonkeyBody, PIPExprF.truth] /-- The sigma set has 2+ elements → plural presupposition satisfied. -/ theorem strong_donkey_plural : plural (sigmaEval (λ d => PIPExprF.conj (farmerBody d) (boughtDonkeyBody d)) W1.w0) := - ⟨.alice, .bob, Ent.noConfusion, rfl, rfl⟩ + ⟨.alice, .bob, by decide, ⟨trivial, trivial⟩, ⟨trivial, trivial⟩⟩ end StrongDonkey @@ -266,31 +272,31 @@ end StrongDonkey section FXRoles /-- AGENT role predicate: alice and bob are agents. -/ -def agentRole : Ent → W1 → Bool - | .alice, _ | .bob, _ => true - | .spot, _ | .rex, _ => false +def agentRole : Ent → W1 → Prop + | .alice, _ | .bob, _ => True + | .spot, _ | .rex, _ => False /-- PATIENT role predicate: spot and rex are patients. -/ -def patientRole : Ent → W1 → Bool - | .spot, _ | .rex, _ => true - | .alice, _ | .bob, _ => false +def patientRole : Ent → W1 → Prop + | .spot, _ | .rex, _ => True + | .alice, _ | .bob, _ => False -def buyEvent : W1 → Bool := λ _ => true +def buyEvent : W1 → Prop := λ _ => True /-- ↑AGENT(buy)(alice) = true — alice is an agent of buying. -/ -theorem fx_agent_alice : fxApply agentRole buyEvent Ent.alice W1.w0 = true := by decide +theorem fx_agent_alice : fxApply agentRole buyEvent Ent.alice W1.w0 := ⟨trivial, trivial⟩ /-- ↑AGENT(buy)(spot) = false — spot is not an agent. -/ -theorem fx_agent_spot : fxApply agentRole buyEvent Ent.spot W1.w0 = false := by decide +theorem fx_agent_spot : ¬ fxApply agentRole buyEvent Ent.spot W1.w0 := fun h => h.1 /-- Iterated FX: ↑PATIENT(↑AGENT(buy))(spot) = false — agent fails for spot. -/ theorem fx_double_spot : - fxApply patientRole (fxApply agentRole buyEvent Ent.spot) Ent.spot W1.w0 = false := by decide + ¬ fxApply patientRole (fxApply agentRole buyEvent Ent.spot) Ent.spot W1.w0 := fun h => h.2.1 /-- ↑PATIENT(↑AGENT(buy))(alice, alice) — decomposes by fxApply_twice. -/ theorem fx_double_decomposes : fxApply patientRole (fxApply agentRole buyEvent Ent.alice) Ent.alice W1.w0 = - (patientRole Ent.alice W1.w0 && agentRole Ent.alice W1.w0 && buyEvent W1.w0) := + (patientRole Ent.alice W1.w0 ∧ agentRole Ent.alice W1.w0 ∧ buyEvent W1.w0) := fxApply_twice agentRole patientRole buyEvent Ent.alice W1.w0 end FXRoles @@ -322,9 +328,9 @@ already quantified over, not formulas with free variables. /-- Diorama predicate: d1 and d2 are dioramas. -/ def dioramaBody : Ent → PIPExprF W1 Ent - | .spot => .pred (λ _ => true) -- spot = "diorama d1" - | .rex => .pred (λ _ => true) -- rex = "diorama d2" - | .alice | .bob => .pred (λ _ => false) + | .spot => .pred (λ _ => True) -- spot = "diorama d1" + | .rex => .pred (λ _ => True) -- rex = "diorama d2" + | .alice | .bob => .pred (λ _ => False) /-- "Made" relation parameterized by maker (external free variable x): @@ -332,9 +338,9 @@ alice made spot (d1), bob made rex (d2). -/ def madeBody (maker : Ent) : Ent → PIPExprF W1 Ent | d => .pred (λ _ => match maker, d with - | .alice, .spot => true -- alice made d1 - | .bob, .rex => true -- bob made d2 - | _, _ => false) + | .alice, .spot => True -- alice made d1 + | .bob, .rex => True -- bob made d2 + | _, _ => False) /-- Paycheck body: `D ≡ DIORAMA([d]) ∧ MADE(x, d)` with x as free variable. @@ -345,17 +351,19 @@ def paycheckBody (maker : Ent) (d : Ent) : PIPExprF W1 Ent := /-- When x = alice, ΣdD = {spot} (alice's diorama). -/ theorem paycheck_alice_spot : - Ent.spot ∈ sigmaEval (paycheckBody .alice) W1.w0 := rfl + Ent.spot ∈ sigmaEval (paycheckBody .alice) W1.w0 := by + simp [sigmaEval, paycheckBody, dioramaBody, madeBody, PIPExprF.truth] theorem paycheck_alice_not_rex : - Ent.rex ∉ sigmaEval (paycheckBody .alice) W1.w0 := Bool.false_ne_true + Ent.rex ∉ sigmaEval (paycheckBody .alice) W1.w0 := by simp [sigmaEval, paycheckBody, dioramaBody, madeBody, PIPExprF.truth] /-- When x = bob, ΣdD = {rex} (bob's diorama). -/ theorem paycheck_bob_rex : - Ent.rex ∈ sigmaEval (paycheckBody .bob) W1.w0 := rfl + Ent.rex ∈ sigmaEval (paycheckBody .bob) W1.w0 := by + simp [sigmaEval, paycheckBody, dioramaBody, madeBody, PIPExprF.truth] theorem paycheck_bob_not_spot : - Ent.spot ∉ sigmaEval (paycheckBody .bob) W1.w0 := Bool.false_ne_true + Ent.spot ∉ sigmaEval (paycheckBody .bob) W1.w0 := by simp [sigmaEval, paycheckBody, dioramaBody, madeBody, PIPExprF.truth] /-- The paycheck property: the sigma set varies with the external free @@ -372,14 +380,16 @@ theorem paycheck_varies : /-- Each maker's sigma set is a singleton — satisfying the SG presupposition. -/ theorem paycheck_alice_single : - single (sigmaEval (paycheckBody .alice) W1.w0) := - ⟨.spot, Set.eq_singleton_iff_unique_mem.mpr - ⟨rfl, fun d hd => by cases d <;> first | rfl | exact absurd hd Bool.false_ne_true⟩⟩ + single (sigmaEval (paycheckBody .alice) W1.w0) := by + refine ⟨.spot, ?_⟩ + ext d + cases d <;> simp [sigmaEval, paycheckBody, dioramaBody, madeBody, PIPExprF.truth] theorem paycheck_bob_single : - single (sigmaEval (paycheckBody .bob) W1.w0) := - ⟨.rex, Set.eq_singleton_iff_unique_mem.mpr - ⟨rfl, fun d hd => by cases d <;> first | rfl | exact absurd hd Bool.false_ne_true⟩⟩ + single (sigmaEval (paycheckBody .bob) W1.w0) := by + refine ⟨.rex, ?_⟩ + ext d + cases d <;> simp [sigmaEval, paycheckBody, dioramaBody, madeBody, PIPExprF.truth] end PaycheckPronouns diff --git a/Linglib/Studies/KeshetAbney2024.lean b/Linglib/Studies/KeshetAbney2024.lean index eaa87378a..2ce8bf3ef 100644 --- a/Linglib/Studies/KeshetAbney2024.lean +++ b/Linglib/Studies/KeshetAbney2024.lean @@ -48,10 +48,7 @@ namespace KeshetAbney2024 open KeshetAbney2024.PIP open Semantics.Dynamic.Core (IVar ICDRTAssignment Entity IContext) --- `BAccessRel` is re-exported by `KeshetAbney2024.PIP` (opened above); --- `BRefl` / `kripkeEval` were Bool-internal modal infrastructure that has --- been replaced by the Prop-valued `Refl`/`boxR` API in --- `Core.Logic.Intensional` and isn't needed here. +open Core.Logic.Intensional (AccessRel) open Phenomena.Anaphora @@ -82,16 +79,16 @@ def αWolf : FLabel := ⟨0⟩ def vWolf : IVar := ⟨0⟩ /-- Epistemic accessibility from actual world. -/ -def sAccess : BAccessRel SWorld - | .actual, .wolfIn => true - | .actual, .noWolf => true - | _, _ => false +def sAccess : AccessRel SWorld + | .actual, .wolfIn => True + | .actual, .noWolf => True + | _, _ => False -def isWolf (g : ICDRTAssignment SWorld SEntity) (w : SWorld) : Bool := - g.indiv vWolf w == .some .wolf +def isWolf (g : ICDRTAssignment SWorld SEntity) (w : SWorld) : Prop := + g.indiv vWolf w = .some .wolf -def comesIn (g : ICDRTAssignment SWorld SEntity) (w : SWorld) : Bool := - g.indiv vWolf w == .some .wolf && w == .wolfIn +def comesIn (g : ICDRTAssignment SWorld SEntity) (w : SWorld) : Prop := + g.indiv vWolf w = .some .wolf ∧ w = .wolfIn /-- "A wolf might come in." (paper item 59a) @@ -104,7 +101,7 @@ def stoneSentence1 : PUpdate SWorld SEntity := might sAccess sWorlds (existsLabeled αWolf vWolf {.wolf} isWolf - (atom (λ g w => isWolf g w && comesIn g w))) + (atom (λ g w => isWolf g w ∧ comesIn g w))) /-- After "A wolf might come in", the label αWolf is registered. -/ theorem stone_label_registered (d : Discourse SWorld SEntity) @@ -123,7 +120,7 @@ def stoneSentence2 : PUpdate SWorld SEntity := conj (retrieveDef αWolf) (would sAccess sWorlds - (atom (λ g w => g.indiv vWolf w != .star))) + (atom (λ g w => g.indiv vWolf w ≠ .star))) def stoneDiscourse : PUpdate SWorld SEntity := conj stoneSentence1 stoneSentence2 @@ -154,14 +151,14 @@ private theorem g_wolf_in_sentence1 : · exact Set.mem_univ _ · refine ⟨SWorld.wolfIn, ?_, ?_, ?_⟩ · simp [sWorlds] - · rfl + · trivial · unfold existsLabeled atom Discourse.mapInfo constructor · refine ⟨g₀_stone, SEntity.wolf, ?_, ?_, ?_⟩ · left; exact Set.mem_univ _ · rfl · rfl - · rfl + · exact ⟨rfl, rfl, rfl⟩ private theorem g_wolf_in_retrieve : (g_wolf, SWorld.actual) ∈ (retrieveDef αWolf (stoneSentence1 stone_d₀)).info := by @@ -169,7 +166,7 @@ private theorem g_wolf_in_retrieve : simp only [stoneSentence1, might, modalExpand, existsLabeled, atom, Discourse.mapInfo, LabelStore.register, LabelStore.lookup, αWolf, vWolf, isWolf] - refine ⟨g_wolf_in_sentence1, ?_, ?_⟩ <;> decide + refine ⟨g_wolf_in_sentence1, ?_, ?_⟩ <;> first | rfl | decide | trivial /-- End-to-end test: Stone's discourse is consistent on a concrete model. @@ -188,7 +185,9 @@ theorem stone_discourse_consistent : unfold atom Discourse.mapInfo constructor · right; exact ⟨SWorld.actual, g_wolf_in_retrieve, hacc⟩ - · rfl + · intro h + have h1 : g_wolf.indiv vWolf w₁ = .some .wolf := rfl + rw [h1] at h; exact absurd h (by decide) /-- Negative test: unbound wolf variable is rejected. -/ theorem stone_discourse_rejects_unbound : @@ -222,11 +221,11 @@ inductive BEntity where def αBath : FLabel := ⟨1⟩ def vBath : IVar := ⟨1⟩ -def isBathroom (g : ICDRTAssignment BWorld BEntity) (w : BWorld) : Bool := - g.indiv vBath w == .some .bathroom +def isBathroom (g : ICDRTAssignment BWorld BEntity) (w : BWorld) : Prop := + g.indiv vBath w = .some .bathroom -def isUpstairs (g : ICDRTAssignment BWorld BEntity) (w : BWorld) : Bool := - g.indiv vBath w == .some .bathroom && w == .bath +def isUpstairs (g : ICDRTAssignment BWorld BEntity) (w : BWorld) : Prop := + g.indiv vBath w = .some .bathroom ∧ w = .bath /-- "Either there's no bathroom, or it's upstairs." (paper item 92b) @@ -326,11 +325,11 @@ inductive PWorld where deriving DecidableEq, Repr, Inhabited /-- Relational paycheck predicate: depends on both paycheck and possessor. -/ -def isPaycheckOf (g : ICDRTAssignment PWorld PEntity) (w : PWorld) : Bool := +def isPaycheckOf (g : ICDRTAssignment PWorld PEntity) (w : PWorld) : Prop := match g.indiv vPaycheck w, g.indiv vPossessor w with - | .some .johnsPaycheck, .some .john => true - | .some .billsPaycheck, .some .bill => true - | _, _ => false + | .some .johnsPaycheck, .some .john => True + | .some .billsPaycheck, .some .bill => True + | _, _ => False /-- Re-evaluation yields Bill's paycheck when possessor = Bill. -/ theorem paycheck_needs_descriptions : @@ -340,7 +339,7 @@ theorem paycheck_needs_descriptions : else if v == vPossessor then .some .bill else .star prop := λ _ => ∅ } - isPaycheckOf g .w0 = true := by decide + isPaycheckOf g .w0 := by trivial end Paycheck @@ -556,14 +555,14 @@ def ibWorlds : List IBWorld := [.actual, .burgerW] def αBurger : FLabel := ⟨10⟩ def vBurger : IVar := ⟨10⟩ -def ibAccess : BAccessRel IBWorld - | .actual, .actual => true - | .actual, .burgerW => true - | _, _ => false +def ibAccess : AccessRel IBWorld + | .actual, .actual => True + | .actual, .burgerW => True + | _, _ => False /-- World-dependent predicate: burger exists only at burgerW. -/ -def isBurgerAt (g : ICDRTAssignment IBWorld IBEntity) (w : IBWorld) : Bool := - g.indiv vBurger w == .some .burger && w == .burgerW +def isBurgerAt (g : ICDRTAssignment IBWorld IBEntity) (w : IBWorld) : Prop := + g.indiv vBurger w = .some .burger ∧ w = .burgerW def burgerSentence : PUpdate IBWorld IBEntity := might ibAccess ibWorlds @@ -580,10 +579,8 @@ theorem burger_label_registered (d : Discourse IBWorld IBEntity) : /-- The burger description fails at actual — presupposition failure. -/ theorem burger_desc_fails_at_actual : ∀ g : ICDRTAssignment IBWorld IBEntity, - isBurgerAt g .actual = false := by - intro g; unfold isBurgerAt - have : (IBWorld.actual == IBWorld.burgerW) = false := by decide - simp [this] + ¬ isBurgerAt g .actual := by + intro g h; exact absurd h.2 (by decide) instance : Fintype IBWorld where elems := {.actual, .burgerW} @@ -600,11 +597,11 @@ confirming that the blocking mechanism is about description content, not accessibility structure. -/ theorem burger_desc_world_dependent : - isBurgerAt + ¬ isBurgerAt { indiv := λ _ _ => .some .burger, prop := λ _ => ∅ } - .actual = false ∧ - ibAccess .actual .actual = true := - ⟨rfl, rfl⟩ + .actual ∧ + ibAccess .actual .actual := + ⟨fun h => absurd h.2 (by decide), trivial⟩ end IntensionalBurger @@ -639,14 +636,14 @@ def αAnimal : FLabel := ⟨11⟩ def vAnimal : IVar := ⟨11⟩ /-- Realistic epistemic: actual accessible from itself. -/ -def iaAccess : BAccessRel IAWorld - | .actual, .actual => true - | .actual, .shedW => true - | _, _ => false +def iaAccess : AccessRel IAWorld + | .actual, .actual => True + | .actual, .shedW => True + | _, _ => False /-- World-INdependent predicate: holds at ALL worlds. -/ -def isAnimalInShed (g : ICDRTAssignment IAWorld IAEntity) (w : IAWorld) : Bool := - g.indiv vAnimal w == .some .animal +def isAnimalInShed (g : ICDRTAssignment IAWorld IAEntity) (w : IAWorld) : Prop := + g.indiv vAnimal w = .some .animal def animalSentence : PUpdate IAWorld IAEntity := must iaAccess iaWorlds @@ -662,8 +659,8 @@ theorem animal_label_registered (d : Discourse IAWorld IAEntity) : theorem animal_desc_succeeds : ∀ (g : ICDRTAssignment IAWorld IAEntity) (w : IAWorld), - g.indiv vAnimal w == .some .animal → isAnimalInShed g w = true := by - intro g w h; simp [isAnimalInShed, h] + g.indiv vAnimal w = .some .animal → isAnimalInShed g w := by + intro g w h; exact h instance : Fintype IAWorld where elems := {.actual, .shedW} @@ -678,7 +675,7 @@ description predicate holds at .actual. This is the Kripke-semantic grounding of why must enables intensional anaphora. -/ theorem animal_must_realistic : - iaAccess .actual .actual = true := rfl + iaAccess .actual .actual := trivial end IntensionalAnimal @@ -720,17 +717,17 @@ def αMA : FLabel := ⟨12⟩ def vMA : IVar := ⟨12⟩ /-- Realistic epistemic: actual accessible from itself, plus two alternatives. -/ -def maAccess : BAccessRel MAWorld - | .actual, _ => true - | _, _ => false +def maAccess : AccessRel MAWorld + | .actual, _ => True + | _, _ => False /-- World-dependent predicate: different animal in each world. -/ -def isAnimalInShedMA (g : ICDRTAssignment MAWorld MAEntity) (w : MAWorld) : Bool := +def isAnimalInShedMA (g : ICDRTAssignment MAWorld MAEntity) (w : MAWorld) : Prop := match g.indiv vMA w, w with - | .some .cat, .actual => true - | .some .dog, .shedW1 => true - | .some .raccoon, .shedW2 => true - | _, _ => false + | .some .cat, .actual => True + | .some .dog, .shedW1 => True + | .some .raccoon, .shedW2 => True + | _, _ => False /-- At the actual world, only one entity satisfies the description. -/ private def maG (e : MAEntity) : ICDRTAssignment MAWorld MAEntity := @@ -739,33 +736,33 @@ private def maG (e : MAEntity) : ICDRTAssignment MAWorld MAEntity := /-- At actual, only cat satisfies the description (SINGLE). -/ theorem ma_single_at_actual : - isAnimalInShedMA (maG .cat) .actual = true ∧ - isAnimalInShedMA (maG .dog) .actual = false ∧ - isAnimalInShedMA (maG .raccoon) .actual = false := - ⟨rfl, rfl, rfl⟩ + isAnimalInShedMA (maG .cat) .actual ∧ + ¬ isAnimalInShedMA (maG .dog) .actual ∧ + ¬ isAnimalInShedMA (maG .raccoon) .actual := + ⟨trivial, id, id⟩ /-- Different entities satisfy the description at different worlds. -/ theorem ma_different_animals_per_world : isAnimalInShedMA { indiv := λ v _w => if v == vMA then .some .cat else .star - prop := λ _ => ∅ } .actual = true ∧ + prop := λ _ => ∅ } .actual ∧ isAnimalInShedMA { indiv := λ v _w => if v == vMA then .some .dog else .star - prop := λ _ => ∅ } .shedW1 = true ∧ + prop := λ _ => ∅ } .shedW1 ∧ isAnimalInShedMA { indiv := λ v _w => if v == vMA then .some .raccoon else .star - prop := λ _ => ∅ } .shedW2 = true := by - exact ⟨rfl, rfl, rfl⟩ + prop := λ _ => ∅ } .shedW2 := + ⟨trivial, trivial, trivial⟩ /-- Cross-world summation yields PLURAL — Stone/Brasoveanu would incorrectly predict plurality here since they sum across all accessible worlds. Different animals satisfy the description at different worlds: cat at actual, dog at shedW1. -/ theorem ma_cross_world_plural : - isAnimalInShedMA (maG .cat) .actual = true ∧ - isAnimalInShedMA (maG .dog) .shedW1 = true ∧ + isAnimalInShedMA (maG .cat) .actual ∧ + isAnimalInShedMA (maG .dog) .shedW1 ∧ MAEntity.cat ≠ MAEntity.dog := - ⟨rfl, rfl, by decide⟩ + ⟨trivial, trivial, by decide⟩ end MultiAnimal @@ -803,16 +800,16 @@ def αWinner : FLabel := ⟨20⟩ def vWinner : IVar := ⟨20⟩ /-- Epistemic: speaker considers all outcomes possible. -/ -def pcAccess : BAccessRel PCWorld - | .actual, _ => true - | _, _ => false +def pcAccess : AccessRel PCWorld + | .actual, _ => True + | _, _ => False /-- World-dependent predicate: winner only at resolution worlds. -/ -def isWinner (g : ICDRTAssignment PCWorld PCEntity) (w : PCWorld) : Bool := +def isWinner (g : ICDRTAssignment PCWorld PCEntity) (w : PCWorld) : Prop := match g.indiv vWinner w, w with - | .some .alice, .aliceWins => true - | .some .bob, .bobWins => true - | _, _ => false + | .some .alice, .aliceWins => True + | .some .bob, .bobWins => True + | _, _ => False /-- "There may already be a winner." -/ def candidateSentence : PUpdate PCWorld PCEntity := @@ -864,9 +861,9 @@ Since the pronoun's existential presupposition (paper item 9) requires the description to hold at the evaluation world, might fails and must succeeds. -/ theorem pip_intensional_anaphora_contrast : - (∀ g : ICDRTAssignment IBWorld IBEntity, isBurgerAt g .actual = false) ∧ + (∀ g : ICDRTAssignment IBWorld IBEntity, ¬ isBurgerAt g .actual) ∧ (∀ (g : ICDRTAssignment IAWorld IAEntity) (w : IAWorld), - g.indiv vAnimal w == .some .animal → isAnimalInShed g w = true) := + g.indiv vAnimal w = .some .animal → isAnimalInShed g w) := ⟨burger_desc_fails_at_actual, animal_desc_succeeds⟩ /-- Labels are registered in BOTH cases — the asymmetry is about @@ -880,12 +877,12 @@ theorem labels_registered_in_both_cases : /-- Static felicity operator F distinguishes might from must. -/ theorem felicity_might_blocks : - (Felicity.singlePresup (W := IBWorld) (λ w => w == .burgerW)).felicitous .actual = false := by - decide + ¬ (Felicity.singlePresup (W := IBWorld) (λ w => w = .burgerW)).felicitous .actual := by + intro h; exact absurd h.2 (by decide) theorem felicity_must_allows : - (Felicity.singlePresup (W := IAWorld) (λ _ => true)).felicitous .actual = true := by - decide + (Felicity.singlePresup (W := IAWorld) (λ _ => True)).felicitous .actual := by + exact ⟨trivial, trivial⟩ -- ============================================================ @@ -951,12 +948,12 @@ itself must hold there. -/ theorem intensional_anaphora_is_T_axiom : -- Must's accessibility is reflexive at actual - iaAccess .actual .actual = true ∧ + iaAccess .actual .actual ∧ -- Might's accessibility is ALSO reflexive at actual - ibAccess .actual .actual = true ∧ + ibAccess .actual .actual ∧ -- But the burger description fails at actual (world-dependent) - (∀ g : ICDRTAssignment IBWorld IBEntity, isBurgerAt g .actual = false) := - ⟨animal_must_realistic, rfl, burger_desc_fails_at_actual⟩ + (∀ g : ICDRTAssignment IBWorld IBEntity, ¬ isBurgerAt g .actual) := + ⟨animal_must_realistic, trivial, burger_desc_fails_at_actual⟩ -- ============================================================ @@ -1161,29 +1158,29 @@ def αDonkey : FLabel := ⟨30⟩ def vFarmer : IVar := ⟨30⟩ def vDonkey : IVar := ⟨31⟩ -def isFarmer (g : ICDRTAssignment DWorld DEntity) (w : DWorld) : Bool := +def isFarmer (g : ICDRTAssignment DWorld DEntity) (w : DWorld) : Prop := match g.indiv vFarmer w with - | .some .farmer1 | .some .farmer2 => true - | _ => false + | .some .farmer1 | .some .farmer2 => True + | _ => False -def isDonkey (g : ICDRTAssignment DWorld DEntity) (w : DWorld) : Bool := +def isDonkey (g : ICDRTAssignment DWorld DEntity) (w : DWorld) : Prop := match g.indiv vDonkey w with - | .some .donkey1 | .some .donkey2 => true - | _ => false + | .some .donkey1 | .some .donkey2 => True + | _ => False /-- Ownership: farmer1 owns donkey1, farmer2 owns donkey2. -/ -def owns (g : ICDRTAssignment DWorld DEntity) (w : DWorld) : Bool := +def owns (g : ICDRTAssignment DWorld DEntity) (w : DWorld) : Prop := match g.indiv vFarmer w, g.indiv vDonkey w with - | .some .farmer1, .some .donkey1 => true - | .some .farmer2, .some .donkey2 => true - | _, _ => false + | .some .farmer1, .some .donkey1 => True + | .some .farmer2, .some .donkey2 => True + | _, _ => False /-- Beating: every farmer who owns a donkey beats it. -/ -def beats (g : ICDRTAssignment DWorld DEntity) (w : DWorld) : Bool := +def beats (g : ICDRTAssignment DWorld DEntity) (w : DWorld) : Prop := match g.indiv vFarmer w, g.indiv vDonkey w with - | .some .farmer1, .some .donkey1 => true - | .some .farmer2, .some .donkey2 => true - | _, _ => false + | .some .farmer1, .some .donkey1 => True + | .some .farmer2, .some .donkey2 => True + | _, _ => False /-- "Every farmer who owns a donkey beats it." @@ -1200,7 +1197,7 @@ def donkeySentence : PUpdate DWorld DEntity := (conj (existsLabeled αDonkey vDonkey {.donkey1, .donkey2} isDonkey - (atom (λ g w => isDonkey g w && owns g w))) + (atom (λ g w => isDonkey g w ∧ owns g w))) (conj (retrieveDef αDonkey) (atom beats)))) @@ -1257,17 +1254,17 @@ def αWitch : FLabel := ⟨40⟩ def vWitch : IVar := ⟨40⟩ /-- Hob's doxastic accessibility: Hob believes from actual to hobBelief. -/ -def hobAccess : BAccessRel HNWorld - | .actual, .hobBelief => true - | _, _ => false +def hobAccess : AccessRel HNWorld + | .actual, .hobBelief => True + | _, _ => False /-- Nob's bouletic accessibility: Nob wonders from actual to nobWonder. -/ -def nobAccess : BAccessRel HNWorld - | .actual, .nobWonder => true - | _, _ => false +def nobAccess : AccessRel HNWorld + | .actual, .nobWonder => True + | _, _ => False -def isWitch (g : ICDRTAssignment HNWorld HNEntity) (w : HNWorld) : Bool := - g.indiv vWitch w == .some .witch +def isWitch (g : ICDRTAssignment HNWorld HNEntity) (w : HNWorld) : Prop := + g.indiv vWitch w = .some .witch /-- Hob's belief: "a witch blighted his mare" -/ def hobBelief : PUpdate HNWorld HNEntity := @@ -1281,7 +1278,7 @@ def nobWonder : PUpdate HNWorld HNEntity := conj (retrieveDef αWitch) (might nobAccess hnWorlds - (atom (λ g w => g.indiv vWitch w != .star))) + (atom (λ g w => g.indiv vWitch w ≠ .star))) /-- The full Hob-Nob discourse. -/ def hobNobDiscourse : PUpdate HNWorld HNEntity := From 2d8053fc1be8774c6b13c3330016372e4fa7ecbc Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 29 May 2026 18:39:36 -0700 Subject: [PATCH 6/8] docs(Studies/KeshetAbney2024): refresh docstrings for Prop-native PIP --- Linglib/Studies/AbneyKeshet2025.lean | 2 +- Linglib/Studies/KeshetAbney2024.lean | 16 +++++++------- Linglib/Studies/KeshetAbney2024/Basic.lean | 2 +- Linglib/Studies/KeshetAbney2024/Bridges.lean | 22 ++++++++++---------- 4 files changed, 21 insertions(+), 21 deletions(-) diff --git a/Linglib/Studies/AbneyKeshet2025.lean b/Linglib/Studies/AbneyKeshet2025.lean index 40ee303f4..73a2a57e3 100644 --- a/Linglib/Studies/AbneyKeshet2025.lean +++ b/Linglib/Studies/AbneyKeshet2025.lean @@ -150,7 +150,7 @@ theorem every_farmer_bought_donkey : (sigmaEval farmerBody W1.w0) (sigmaEval (λ d => PIPExprF.conj (farmerBody d) (boughtDonkeyBody d)) W1.w0) := by intro d hd - -- d ∈ sigmaEval farmerBody means (farmerBody d).truth w0 = true + -- d ∈ sigmaEval farmerBody means (farmerBody d).truth w0 holds -- For alice and bob, boughtDonkeyBody also returns true cases d with | alice => exact ⟨trivial, trivial⟩ diff --git a/Linglib/Studies/KeshetAbney2024.lean b/Linglib/Studies/KeshetAbney2024.lean index 2ce8bf3ef..be7766ca0 100644 --- a/Linglib/Studies/KeshetAbney2024.lean +++ b/Linglib/Studies/KeshetAbney2024.lean @@ -36,11 +36,11 @@ conditions, uniformly explains: ## Architecture This study file imports: -- **Theory**: `Semantics/PIP/` (PIP mechanism) +- **Framework**: the PIP mechanism in `Studies/KeshetAbney2024/` - **Data**: `Phenomena/Anaphora/` (theory-neutral judgments) -and proves that PIP's predictions match the empirical data via worked -finite models with `decide` verification. +and proves that PIP's predictions match the empirical data on worked +finite models. -/ @@ -588,11 +588,11 @@ instance : Fintype IBWorld where /-- Might blocks anaphora NOT because of non-reflexive access, but because the -burger **description** is world-dependent: `isBurgerAt g .actual = false` +burger **description** is world-dependent: `¬ isBurgerAt g .actual` for all g (burger_desc_fails_at_actual). Even with a reflexive modal base, the description Σb(BURGER_w([b])) is empty at .actual — no burger there. -The accessibility IS reflexive at .actual (ibAccess .actual .actual = true), +The accessibility IS reflexive at .actual (ibAccess .actual .actual), confirming that the blocking mechanism is about description content, not accessibility structure. -/ @@ -820,8 +820,8 @@ def candidateSentence : PUpdate PCWorld PCEntity := /-- The winner description is empty at the actual world — no winner declared yet. -/ theorem winner_desc_empty_at_actual : ∀ g : ICDRTAssignment PCWorld PCEntity, - isWinner g .actual = false := by - intro g; simp [isWinner] + ¬ isWinner g .actual := by + intro g h; exact h /-- Contrast with Stone/Brasoveanu: the entities EXIST in the actual world @@ -831,7 +831,7 @@ DESCRIPTION yields nothing at actual → infelicitous. -/ theorem candidates_exist_but_description_fails : ({.alice, .bob} : Set PCEntity).Nonempty ∧ - (∀ g : ICDRTAssignment PCWorld PCEntity, isWinner g .actual = false) := + (∀ g : ICDRTAssignment PCWorld PCEntity, ¬ isWinner g .actual) := ⟨⟨.alice, Set.mem_insert _ _⟩, winner_desc_empty_at_actual⟩ /-- The label is registered (the mechanism works), but the description diff --git a/Linglib/Studies/KeshetAbney2024/Basic.lean b/Linglib/Studies/KeshetAbney2024/Basic.lean index f8504b9ee..4ed400af7 100644 --- a/Linglib/Studies/KeshetAbney2024/Basic.lean +++ b/Linglib/Studies/KeshetAbney2024/Basic.lean @@ -237,7 +237,7 @@ def retrieveDef {W E : Type*} (α : FLabel) : PUpdate W E := /-- PIP truth relative to a world and a plural context. -A predicate P holds at world w in context c iff P(g, w) = true +A predicate P holds at world w in context c iff P(g, w) for ALL assignments g paired with w in c. This "plural" evaluation is what gives PIP its power: different diff --git a/Linglib/Studies/KeshetAbney2024/Bridges.lean b/Linglib/Studies/KeshetAbney2024/Bridges.lean index 8b0aead04..f92bcdd97 100644 --- a/Linglib/Studies/KeshetAbney2024/Bridges.lean +++ b/Linglib/Studies/KeshetAbney2024/Bridges.lean @@ -305,10 +305,10 @@ theorem properPlural_implies_plural {α : Type*} {a b : α} PIP's must allows anaphora because of a **realistic modal base** (@cite{kratzer-1991}): the evaluation world w* is accessible from -itself (R w* w* = true). This is exactly the T axiom (`□p → p`, +itself (`R w* w*`). This is exactly the T axiom (`□p → p`, frame condition: reflexivity). -The `must_truth_agrees_kripkeEval` and `must_realistic_of_refl` +The `must_truth_agrees_boxR` and `must_realistic_of_refl` theorems in `Connectives.lean` already prove this correspondence. This section classifies PIP's modal operators in the lattice of normal modal logics from `Core.Logic.Intensional`. @@ -329,9 +329,9 @@ theorem pip_anaphora_requires_T : /-- A reflexive accessibility relation satisfies Logic.T's frame condition. -Stated for the Prop-valued `AccessRel`/`IsReflexive`/`frameConditions` API in -`Core.Logic.Intensional`. To apply this to a PIP -`BAccessRel R`, lift via `liftR R = fun a b => R a b = true`. +Stated for the Prop-valued `AccessRel`/`Std.Refl`/`frameConditions` API in +`Core.Logic.Intensional` — the same accessibility type PIP's modal +operators now use directly. -/ theorem reflexive_satisfies_T {W : Type*} (R : Core.Logic.Intensional.AccessRel W) [hRefl : Std.Refl R] : @@ -362,21 +362,21 @@ This is structurally identical to @cite{kratzer-1991}'s analysis where: The formal connection is established via `Core.Logic.Intensional.boxR`: `must_truth_agrees_boxR` (in Connectives.lean) proves that PIP's `must R allWorlds (atom p)` produces the same truth conditions as -`boxR (liftR R) (liftP (p g))`. +`boxR R (p g)`. Direct import of `Semantics/Modality/Kratzer/` is not possible because Kratzer's implementation is monomorphic over `World4`. The -correspondence is structural (via `BAccessRel` ≅ `ModalBase`) rather +correspondence is structural (via `AccessRel` ≅ `ModalBase`) rather than definitional. -/ /-- Full Kratzer bridge: PIP's three-argument `mustBase` agrees with -`boxR` when the modal base comes from a BAccessRel and the restriction +`boxR` when the modal base comes from an `AccessRel` and the restriction is tautological. -The composition: `mustBase (accessRelToBase R w) ⊤ {w' | φ w' = true}` ↔ -`boxR (fun a b => R a b = true) (fun w' => φ w' = true) w`. Both express +The composition: `mustBase (accessRelToBase R w) ⊤ {w' | φ.truth w'}` ↔ +`boxR R φ.truth w`. Both express "the body holds at every R-accessible world from w". -/ theorem mustBase_agrees_boxR {W D : Type*} @@ -412,7 +412,7 @@ a substantial model-theoretic argument. We mark these with `sorry`. Static atom truth agrees with dynamic `atom` filtering. For an atomic predicate p, `PIPExprF.pred p` has truth value `p w`, -and `atom p` filters the info state to pairs where `p g w = true`. +and `atom p` filters the info state to pairs where `p g w`. When the info state is a singleton, the dynamic update is non-empty iff the static truth value is true. From 7f2d271cef51a1a63d1ab0c2e1c2ca0d47f1c3d5 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 29 May 2026 18:40:13 -0700 Subject: [PATCH 7/8] fix(Studies/KeshetAbney2024): reduce isWinner match via simp in winner_desc_empty --- Linglib/Studies/KeshetAbney2024.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Linglib/Studies/KeshetAbney2024.lean b/Linglib/Studies/KeshetAbney2024.lean index be7766ca0..6ec2ada8f 100644 --- a/Linglib/Studies/KeshetAbney2024.lean +++ b/Linglib/Studies/KeshetAbney2024.lean @@ -821,7 +821,7 @@ def candidateSentence : PUpdate PCWorld PCEntity := theorem winner_desc_empty_at_actual : ∀ g : ICDRTAssignment PCWorld PCEntity, ¬ isWinner g .actual := by - intro g h; exact h + intro g; simp [isWinner] /-- Contrast with Stone/Brasoveanu: the entities EXIST in the actual world From d49e7e37096b16d61ff5f1fd540560d1fcdff948 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 29 May 2026 18:58:05 -0700 Subject: [PATCH 8/8] refactor(Studies/KeshetAbney2024): consume Core GQ, drop vacuous lemma, fix cites --- Linglib/Studies/AbneyKeshet2025.lean | 4 +- Linglib/Studies/KeshetAbney2024.lean | 4 +- Linglib/Studies/KeshetAbney2024/Bridges.lean | 145 +++++------------- Linglib/Studies/KeshetAbney2024/Expr.lean | 16 +- Linglib/Studies/KeshetAbney2024/Felicity.lean | 14 +- blog/references.bib | 4 +- 6 files changed, 63 insertions(+), 124 deletions(-) diff --git a/Linglib/Studies/AbneyKeshet2025.lean b/Linglib/Studies/AbneyKeshet2025.lean index 73a2a57e3..3d26af0ed 100644 --- a/Linglib/Studies/AbneyKeshet2025.lean +++ b/Linglib/Studies/AbneyKeshet2025.lean @@ -35,7 +35,7 @@ anaphora, modal subordination, and the exists/sigma bridge. namespace AbneyKeshet2025 open KeshetAbney2024.PIP -open KeshetAbney2024.PIP.Bridges (single plural setEvery_eq_pipEvery) +open KeshetAbney2024.PIP.Bridges (single plural) -- ============================================================ @@ -143,7 +143,7 @@ EVERY(Σf farmer, Σf (farmer ∧ boughtDonkey)) — via `setEvery`. "Every farmer bought a donkey" modeled as: the set of farmers is a subset of the set of farmer-buyers. This connects to the GQ bridge -in `Bridges.lean` via `setEvery_eq_pipEvery`. +in `Bridges.lean` via `setEvery_eq_every_sem`. -/ theorem every_farmer_bought_donkey : setEvery diff --git a/Linglib/Studies/KeshetAbney2024.lean b/Linglib/Studies/KeshetAbney2024.lean index 6ec2ada8f..f9966255d 100644 --- a/Linglib/Studies/KeshetAbney2024.lean +++ b/Linglib/Studies/KeshetAbney2024.lean @@ -166,7 +166,9 @@ private theorem g_wolf_in_retrieve : simp only [stoneSentence1, might, modalExpand, existsLabeled, atom, Discourse.mapInfo, LabelStore.register, LabelStore.lookup, αWolf, vWolf, isWolf] - refine ⟨g_wolf_in_sentence1, ?_, ?_⟩ <;> first | rfl | decide | trivial + refine ⟨g_wolf_in_sentence1, ?_, ?_⟩ + · decide -- (g_wolf.indiv vWolf actual).isSome + · rfl -- isWolf g_wolf actual (= g_wolf.indiv vWolf actual = some wolf) /-- End-to-end test: Stone's discourse is consistent on a concrete model. diff --git a/Linglib/Studies/KeshetAbney2024/Bridges.lean b/Linglib/Studies/KeshetAbney2024/Bridges.lean index f92bcdd97..3e7c5eedf 100644 --- a/Linglib/Studies/KeshetAbney2024/Bridges.lean +++ b/Linglib/Studies/KeshetAbney2024/Bridges.lean @@ -3,6 +3,7 @@ import Linglib.Studies.KeshetAbney2024.Felicity import Linglib.Studies.KeshetAbney2024.Connectives import Linglib.Studies.KeshetAbney2024.Composition import Linglib.Semantics.Presupposition.Basic +import Linglib.Core.Logic.Quantification.Basic import Linglib.Semantics.Quantification.Quantifier import Linglib.Semantics.Plurality.Algebra import Mathlib.Data.Fintype.Basic @@ -29,10 +30,12 @@ companion paper (@cite{abney-keshet-2025}) are in `PIP.Composition`. ## Design Each section is self-contained: it imports what it needs and states -the correspondence as a theorem or definition. The presupposition and -modal bridges are proved; the static↔dynamic bridge uses `sorry` for -the Brasoveanu equivalence (which requires a non-trivial model theory -argument). +the correspondence as a theorem or definition. The presupposition, +modal, and static↔dynamic bridges are all proved (atomic and negation +cases for the last); the *full* Brasoveanu model-equivalence — a +bijection between PIP models and ICDRT information states — is a +non-trivial model-theoretic argument left as future work, not +formalized here. -/ namespace KeshetAbney2024.PIP.Bridges @@ -133,102 +136,38 @@ are sets (extensional GQs). The GQ type `(α → Prop) → (α → Prop) → Pro is the predicate-based version. -/ -/-- PIP's EVERY as a GQ: ∀x, R(x) → S(x) (= set inclusion). -/ -def pipEvery {α : Type*} : Core.Quantification.GQ α := - λ R S => ∀ x, R x → S x - -/-- PIP's SOME as a GQ: ∃x, R(x) ∧ S(x) (= non-empty intersection). -/ -def pipSome {α : Type*} : Core.Quantification.GQ α := - λ R S => ∃ x, R x ∧ S x - -/-- PIP's EVERY is conservative: EVERY(R, S) ↔ EVERY(R, R ∩ S). -/ -theorem pipEvery_conservative {α : Type*} : - Core.Quantification.Conservative (pipEvery (α := α)) := by - intro R S - simp only [pipEvery] - constructor - · intro h x hR; exact ⟨hR, h x hR⟩ - · intro h x hR; exact (h x hR).2 - -/-- PIP's EVERY is scope-upward-monotone (right upward monotone). -/ -theorem pipEvery_scope_upward_mono {α : Type*} : - Core.Quantification.ScopeUpwardMono (pipEvery (α := α)) := by - intro R S S' hSS' h x hR - exact hSS' x (h x hR) - -/-- PIP's SOME is conservative: SOME(R, S) ↔ SOME(R, R ∩ S). -/ -theorem pipSome_conservative {α : Type*} : - Core.Quantification.Conservative (pipSome (α := α)) := by - intro R S - simp only [pipSome] - constructor - · intro ⟨x, hR, hS⟩; exact ⟨x, hR, ⟨hR, hS⟩⟩ - · intro ⟨x, hR, _, hS⟩; exact ⟨x, hR, hS⟩ - -/-- PIP's SOME is scope-upward-monotone (right upward monotone). -/ -theorem pipSome_scope_upward_mono {α : Type*} : - Core.Quantification.ScopeUpwardMono (pipSome (α := α)) := by - intro R S S' hSS' ⟨x, hR, hS⟩ - exact ⟨x, hR, hSS' x hS⟩ - --- Bridge: set-based GQs (Composition.lean) ↔ predicate-based GQ - /-- -`setEvery` from `PIP.Composition` agrees with `pipEvery` (and hence `every_sem`). - -Both express universal GQ as set inclusion / pointwise implication. -This bridge lets `setEvery` inherit all `GQ` property proofs -(conservativity, monotonicity) from `pipEvery_conservative` etc. +`setEvery` (from `PIP.Composition`, = set inclusion `R ⊆ S`) agrees with +`Core.Quantification.every_sem` (= `∀ x, R x → S x`). + +This is the genuine, load-bearing bridge: `setEvery` is `Set`-typed while +`every_sem` is predicate-typed (defeq, but the binder annotations differ, +so a named lemma earns its keep). PIP's set-GQ therefore *consumes* Core's +quantifier theory directly — conservativity, the Zwarts monotonicity +hierarchy, duality — with no PIP-local re-derivation. -/ -theorem setEvery_eq_pipEvery {α : Type*} (R S : Set α) : - setEvery R S ↔ pipEvery R S := +theorem setEvery_eq_every_sem {α : Type*} (R S : Set α) : + setEvery R S ↔ Core.Quantification.every_sem R S := ⟨fun h x hx => h hx, fun h x hx => h x hx⟩ -/-- -`setSome` from `PIP.Composition` agrees with `pipSome` (and hence `some_sem`). --/ -theorem setSome_eq_pipSome {α : Type*} (R S : Set α) : - setSome R S ↔ pipSome R S := +/-- `setSome` agrees with `Core.Quantification.some_sem`. -/ +theorem setSome_eq_some_sem {α : Type*} (R S : Set α) : + setSome R S ↔ Core.Quantification.some_sem R S := ⟨fun ⟨x, hx⟩ => ⟨x, hx.1, hx.2⟩, fun ⟨x, hr, hs⟩ => ⟨x, hr, hs⟩⟩ -/-- -Conservativity of `setEvery` derived from the GQ proof. --/ +/-- Conservativity of `setEvery`, inherited from + `Core.Quantification.every_conservative` (not re-proved). -/ theorem setEvery_conservative' {α : Type*} (R S : Set α) : setEvery R S ↔ setEvery R (R ∩ S) := by - rw [setEvery_eq_pipEvery, setEvery_eq_pipEvery] - exact pipEvery_conservative R S + rw [setEvery_eq_every_sem, setEvery_eq_every_sem] + exact Core.Quantification.every_conservative R S -/-- -Conservativity of `setSome` derived from the GQ proof. --/ +/-- Conservativity of `setSome`, inherited from + `Core.Quantification.some_conservative` (not re-proved). -/ theorem setSome_conservative' {α : Type*} (R S : Set α) : setSome R S ↔ setSome R (R ∩ S) := by - rw [setSome_eq_pipSome, setSome_eq_pipSome] - exact pipSome_conservative R S - --- Bridge: PIP's GQ ↔ model-theoretic GQ from Quantifier.lean - -/-- -PIP's EVERY is definitionally equal to `every_sem` from `Quantifier.lean`. - -This closes the full bridge chain: - `setEvery R S` ↔ `pipEvery R S` = `every_sem m R S` - -All GQ property proofs in Quantifier.lean (duality, monotonicity, -Zwarts monotonicity hierarchy, quantity invariance, etc.) apply -directly to PIP's quantifiers. --/ -theorem pipEvery_eq_every_sem {α : Type*} : - (pipEvery : Core.Quantification.GQ α) = - Semantics.Quantification.Quantifier.every_sem := rfl - -/-- -PIP's SOME is definitionally equal to `some_sem` from `Quantifier.lean`. --/ -theorem pipSome_eq_some_sem {α : Type*} : - (pipSome : Core.Quantification.GQ α) = - Semantics.Quantification.Quantifier.some_sem := rfl + rw [setSome_eq_some_sem, setSome_eq_some_sem] + exact Core.Quantification.some_conservative R S -- ============================================================ @@ -314,17 +253,15 @@ This section classifies PIP's modal operators in the lattice of normal modal logics from `Core.Logic.Intensional`. -/ -/-- -PIP's anaphora-enabling modality requires at least Logic.T. - -The might/must asymmetry for intensional anaphora reduces to whether -the accessibility relation satisfies the T axiom (reflexivity). Must -with a reflexive R guarantees the description holds at the evaluation -world; might with a non-reflexive R does not. +/-! +PIP's anaphora-enabling modality needs the **T axiom** (reflexivity): a +realistic modal base guarantees the description holds at the evaluation +world. The content of that claim is carried by `reflexive_satisfies_T` +below (reflexivity ⟹ T's frame condition) together with +`Connectives.must_realistic_of_refl` (which consumes `Std.Refl R` to +derive `p g w₀`). A bare `K ≤ T` lemma would be vacuous — `K = ⊥` — so +it is intentionally omitted. -/ -theorem pip_anaphora_requires_T : - Core.Logic.Intensional.Logic.K ≤ Core.Logic.Intensional.Logic.T := - Core.Logic.Intensional.Logic.K_bot ▸ OrderBot.bot_le _ /-- A reflexive accessibility relation satisfies Logic.T's frame condition. @@ -399,13 +336,13 @@ in `Basic.lean` / `Connectives.lean` encodes PIP as a dynamic update system over `IContext W E`. @cite{brasoveanu-2010} shows the equivalence between plural predicate calculi and dynamic plural logics. -The following theorems state that the static system (`PIPExprF.truth`) +The following theorems prove that the static system (`PIPExprF.truth`) and the dynamic encoding (`PUpdate` operators) compute the same thing -for atomic formulas, conjunction, negation, and presupposition. +for the atomic and negation cases (the proofs are complete). -Full proof of the Brasoveanu equivalence requires establishing a -bijection between PIP models and ICDRT information states, which is -a substantial model-theoretic argument. We mark these with `sorry`. +The *full* Brasoveanu equivalence requires establishing a bijection +between PIP models and ICDRT information states — a substantial +model-theoretic argument left as future work, not formalized here. -/ /-- diff --git a/Linglib/Studies/KeshetAbney2024/Expr.lean b/Linglib/Studies/KeshetAbney2024/Expr.lean index 54c723d04..48bfaf67b 100644 --- a/Linglib/Studies/KeshetAbney2024/Expr.lean +++ b/Linglib/Studies/KeshetAbney2024/Expr.lean @@ -76,19 +76,19 @@ inductive PIPExprF (W : Type*) (D : Type*) where | impl (φ ψ : PIPExprF W D) /-- Presupposition: φ|ψ. Assert φ, presuppose ψ. -/ | presup (φ : PIPExprF W D) (ψ : W → Prop) - /-- Existential quantification: ∃x.φ (paper item 43). + /-- Existential quantification: ∃x.φ. `body` takes a domain element and returns a formula. -/ | exists_ (body : D → PIPExprF W D) - /-- Universal quantification: ∀x.φ (paper item 43). + /-- Universal quantification: ∀x.φ. `body` takes a domain element and returns a formula. -/ | forall_ (body : D → PIPExprF W D) /-- Formula label definition: X ≡ φ (paper item 17.3). Tautological — always true. Registers the label for later retrieval. -/ | labelDef (label : FLabel) (φ : PIPExprF W D) - /-- Modal necessity: □_R φ (paper item 28, MUST). + /-- Modal necessity: □_R φ (MUST). Universal quantification over R-accessible worlds. -/ | must (R : AccessRel W) (φ : PIPExprF W D) - /-- Modal possibility: ◇_R φ (paper item 28, MIGHT). + /-- Modal possibility: ◇_R φ (MIGHT). Existential quantification over R-accessible worlds. -/ | might (R : AccessRel W) (φ : PIPExprF W D) @@ -133,8 +133,8 @@ Extends the propositional fragment with: - F(∃xφ) iff ∀x.Fφ — felicity is universal over witnesses (item 43) - F(∀xφ) iff ∀x.Fφ — felicity is universal over witnesses (item 43) - F(X≡φ) iff Fφ — labels don't affect felicity -- F(□φ) iff ∀w'.Fφ — felicity universal over accessible worlds (item 47) -- F(◇φ) iff ∀w'.Fφ — felicity universal over accessible worlds (item 47) +- F(□φ) iff ∀w'.Fφ — felicity universal over accessible worlds +- F(◇φ) iff ∀w'.Fφ — felicity universal over accessible worlds The universal quantification in the quantifier/modal felicity clauses is the key insight: an expression is felicitous only if its presuppositions @@ -160,9 +160,9 @@ def PIPExprF.felicitous {W D : Type*} : | .forall_ body => λ w => ∀ d, (body d).felicitous w -- F(X≡φ) iff Fφ [labels don't affect felicity] | .labelDef _label φ => φ.felicitous - -- F(□φ) iff ∀w'.Fφ [item 47: felicity universal over accessible worlds] + -- F(□φ) iff ∀w'.Fφ [felicity universal over accessible worlds] | .must R φ => boxR R φ.felicitous - -- F(◇φ) iff ∀w'.Fφ [item 47: felicity universal, NOT existential] + -- F(◇φ) iff ∀w'.Fφ [felicity universal, NOT existential] | .might R φ => boxR R φ.felicitous diff --git a/Linglib/Studies/KeshetAbney2024/Felicity.lean b/Linglib/Studies/KeshetAbney2024/Felicity.lean index 75b125623..825246164 100644 --- a/Linglib/Studies/KeshetAbney2024/Felicity.lean +++ b/Linglib/Studies/KeshetAbney2024/Felicity.lean @@ -20,7 +20,7 @@ This file provides: `PIPExprF W D` in `Expr.lean` is the **full** PIP expression type with quantifiers (`∃x`, `∀x`), modals (`□`, `◇`), and label definitions. It defines its own `truth` and `felicitous` functions covering all -constructors, including the quantifier felicity clauses (items 35, 39d). +constructors, including the quantifier and modal felicity clauses. The propositional `PIPExpr W` here is the restriction to `D = Empty`. ## The F Operator (Propositional) @@ -37,7 +37,7 @@ This file covers the propositional fragment (items 40–42, 44–45c): The full quantifier/modal clauses are in `PIPExprF.felicitous` (`Expr.lean`): - F(∃xφ) iff ∀x.Fφ — felicity universal over witnesses (item 43) -- F(□φ) iff ∀w'.Fφ — felicity universal over accessible worlds (item 47) +- F(□φ) iff ∀w'.Fφ — felicity universal over accessible worlds The asymmetric conjunction clause (Karttunen's insight) allows the first conjunct to satisfy presuppositions of the second. This is what makes @@ -268,8 +268,8 @@ universally as usual. This asymmetry is PIP's mechanism for presupposition projection. The felicity clauses (in `PIPExprF.felicitous`): -- F(∃xφ) = ∀x.Fφ — universal over witnesses (item 39d) -- F(∀xφ) = ∀x.Fφ — (item 35) +- F(∃xφ) = ∀x.Fφ — universal over witnesses (universal over the domain) +- F(∀xφ) = ∀x.Fφ — (same felicity clause as ∃) - F(□φ) = ∀w'.Fφ — universal over accessible worlds - F(◇φ) = ∀w'.Fφ — ALSO universal (truth differs: existential) @@ -291,12 +291,12 @@ variable {W D : Type*} -- ======== Prop-level iff characterizations ======== /-- F(∃xφ) iff ∀d, F(φ(d)) — existential felicity is universal - over the domain (item 39d). Holds by definition. -/ + over the domain (universal over the domain). Holds by definition. -/ theorem existsF_felicitous_iff (body : D → PIPExprF W D) (w : W) : (PIPExprF.exists_ body).felicitous w ↔ ∀ d, (body d).felicitous w := Iff.rfl -/-- F(∀xφ) iff ∀d, F(φ(d)) (item 35). Holds by definition. -/ +/-- F(∀xφ) iff ∀d, F(φ(d)) (same felicity clause as ∃). Holds by definition. -/ theorem forallF_felicitous_iff (body : D → PIPExprF W D) (w : W) : (PIPExprF.forall_ body).felicitous w ↔ ∀ d, (body d).felicitous w := Iff.rfl @@ -422,7 +422,7 @@ theorem mightF_presup_at_accessible (mightF_presup_factored R φ ψ w).mp hF |>.2 w' hR --- ======== Sigma body felicity (item 39f) ======== +-- ======== Sigma body felicity (sigma body felicity) ======== /-- Sigma body felicity: for Σxφ to appear felicitously in a discourse, φ must be felicitous for every witness d. This is item (39f) in the diff --git a/blog/references.bib b/blog/references.bib index e47b466fe..d90862fc4 100644 --- a/blog/references.bib +++ b/blog/references.bib @@ -12330,7 +12330,7 @@ @article{keshet-abney-2024 subfield = {semantics/dynamic}, validated = {true}, role = {formalized}, - sources = {Semantics/Dynamic/Systems/PIP/Basic.lean;Semantics/Dynamic/Systems/PIP/Connectives.lean;Semantics/Dynamic/Systems/PIP/Phenomena.lean;Phenomena/Anaphora/Bridge/PIPAnaphora.lean} + sources = {Studies/KeshetAbney2024.lean;Studies/KeshetAbney2024/Basic.lean;Studies/KeshetAbney2024/Expr.lean;Studies/KeshetAbney2024/Felicity.lean;Studies/KeshetAbney2024/Connectives.lean;Studies/KeshetAbney2024/Bridges.lean} } @article{abney-keshet-2025, author = {Abney, Steven and Keshet, Ezra}, @@ -12344,7 +12344,7 @@ @article{abney-keshet-2025 subfield = {semantics/dynamic}, validated = {true}, role = {formalized}, - sources = {Semantics/PIP/Composition.lean} + sources = {Studies/AbneyKeshet2025.lean;Studies/KeshetAbney2024/Composition.lean} } @article{lewis-1979, author = {Lewis, David},