From 1de50ebbbf47affc5a3987cb420e31838f17a078 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 29 May 2026 21:17:05 -0700 Subject: [PATCH] refactor(Discourse/CommonGround): rename CG to root-level CommonGround --- Linglib/Dialogue/Brandom.lean | 4 +- Linglib/Dialogue/CommitmentSpace.lean | 48 ++-- Linglib/Dialogue/CredenceThreshold.lean | 6 +- Linglib/Dialogue/DisjunctiveUpdate.lean | 2 +- Linglib/Dialogue/DistributionalCG.lean | 20 +- Linglib/Dialogue/FarkasBruce.lean | 16 +- Linglib/Dialogue/Gunlogson.lean | 6 +- Linglib/Dialogue/KOS/Basic.lean | 8 +- Linglib/Dialogue/KOS/Defs.lean | 2 +- Linglib/Dialogue/ReasonableInference.lean | 4 +- Linglib/Dialogue/Stalnaker.lean | 28 +-- Linglib/Discourse/Commitment/Basic.lean | 4 +- Linglib/Discourse/Commitment/Frame.lean | 2 +- Linglib/Discourse/Commitment/Table.lean | 12 +- Linglib/Discourse/CommonGround.lean | 116 ++++----- Linglib/Discourse/Scoreboard.lean | 24 +- Linglib/Discourse/SpeechAct/Update.lean | 2 +- Linglib/Features/Topic.lean | 6 +- Linglib/Fragments/Mandarin/Predicates.lean | 2 +- Linglib/Fragments/Marathi/Particles.lean | 4 +- Linglib/Phenomena/Assertion/Compare.lean | 2 +- Linglib/Phenomena/Dialogue/Basic.lean | 2 +- Linglib/Phenomena/Verum/Basic.lean | 2 +- Linglib/Pragmatics/Expressives/Basic.lean | 8 +- Linglib/Pragmatics/RSA/Incremental.lean | 2 +- Linglib/Semantics/Attitudes/Doxastic.lean | 18 +- Linglib/Semantics/Attitudes/Parasitic.lean | 2 +- .../Semantics/Comparison/Metalinguistic.lean | 6 +- Linglib/Semantics/Composition/Glue.lean | 6 +- Linglib/Semantics/Conditionals/Stalnaker.lean | 2 +- .../Dynamic/Effects/Probability.lean | 2 +- .../Semantics/Dynamic/Postsupposition.lean | 4 +- Linglib/Semantics/Lexical/VerbEntry.lean | 2 +- Linglib/Semantics/Modality/BiasedPQ.lean | 26 +- .../Semantics/Modality/EpistemicLogic.lean | 9 +- Linglib/Semantics/Modality/Kernel.lean | 2 +- .../Presupposition/Accommodation.lean | 2 +- .../Presupposition/BeliefEmbedding.lean | 2 +- Linglib/Semantics/Presupposition/Context.lean | 4 +- .../Presupposition/LocalContext.lean | 2 +- .../Presupposition/TonhauserDerivation.lean | 2 +- .../Presupposition/TriggerTypology.lean | 6 +- .../Semantics/TypeTheoretic/Discourse.lean | 14 +- Linglib/Studies/Anderson2021.lean | 228 +++++++++--------- Linglib/Studies/Beaver2001/Basic.lean | 4 +- Linglib/Studies/Clark1983.lean | 58 ++--- Linglib/Studies/CohenKrifka2014.lean | 14 +- Linglib/Studies/CohnGordonEtAl2019.lean | 8 +- Linglib/Studies/CondoravdiLauer2012.lean | 6 +- .../Studies/DelPinalBassiSauerland2024.lean | 2 +- Linglib/Studies/Enguehard2024.lean | 2 +- Linglib/Studies/Faller2019.lean | 2 +- Linglib/Studies/FarkasBruce2010.lean | 6 +- Linglib/Studies/Ginzburg2012.lean | 18 +- Linglib/Studies/Glass2025.lean | 20 +- Linglib/Studies/Heim1992Projection.lean | 2 +- Linglib/Studies/Hohle1992.lean | 2 +- Linglib/Studies/Karttunen1973.lean | 2 +- Linglib/Studies/KayFillmore1999.lean | 8 +- Linglib/Studies/Krifka2015.lean | 32 +-- Linglib/Studies/MartinezVera2026.lean | 6 +- Linglib/Studies/MaticNikolaeva2018.lean | 12 +- Linglib/Studies/Ney2026.lean | 70 +++--- Linglib/Studies/PullumGazdar1982.lean | 4 +- Linglib/Studies/QingGoodmanLassiter2016.lean | 24 +- Linglib/Studies/RitchieSchiller2024.lean | 2 +- Linglib/Studies/Roberts2023.lean | 4 +- Linglib/Studies/RomeroHan2004.lean | 50 ++-- Linglib/Studies/RonderosEtAl2024.lean | 2 +- Linglib/Studies/Rudin2025.lean | 2 +- Linglib/Studies/Schlenker2009.lean | 2 +- Linglib/Studies/SeeligerRepp2018.lean | 10 +- Linglib/Studies/SolstadBott2024.lean | 2 +- Linglib/Studies/Stakov2026Typology.lean | 2 +- Linglib/Studies/Stalnaker1975.lean | 4 +- Linglib/Studies/VanDerLeer2026.lean | 4 +- Linglib/Studies/Wang2025.lean | 90 +++---- .../Studies/GoldbergShirtz2025.lean | 6 +- Linglib/Typology/PolarityMarking.lean | 2 +- 79 files changed, 572 insertions(+), 583 deletions(-) diff --git a/Linglib/Dialogue/Brandom.lean b/Linglib/Dialogue/Brandom.lean index 2bb968d6e..4e2e2d424 100644 --- a/Linglib/Dialogue/Brandom.lean +++ b/Linglib/Dialogue/Brandom.lean @@ -37,7 +37,7 @@ inferential role. namespace Dialogue.Brandom open Discourse.Commitment (CommitmentSlate) -open Discourse.CommonGround (ContextSet CG) +open CommonGround (ContextSet) -- ════════════════════════════════════════════════════ -- § 1. Normative Status @@ -220,7 +220,7 @@ theorem scorekeepers_can_disagree : -- § 7. HasContextSet instance -- ════════════════════════════════════════════════════ -open Discourse.CommonGround in +open CommonGround in /-- Brandom states project to a context set via `effectiveContextSet` (the lossy Brandom → Stalnaker projection: intersection of all self-attributed commitments). The lossy projection is the price of diff --git a/Linglib/Dialogue/CommitmentSpace.lean b/Linglib/Dialogue/CommitmentSpace.lean index e6d89eded..1d5ddde25 100644 --- a/Linglib/Dialogue/CommitmentSpace.lean +++ b/Linglib/Dialogue/CommitmentSpace.lean @@ -10,7 +10,7 @@ import Linglib.Discourse.SpeechAct.Update @cite{krifka-2015} @cite{cohen-krifka-2014} Krifka's commitment-space framework: the discourse state is a tree — the -root (√C) is the current CG holding speaker-indexed commitments `S⊢φ`, +root (√C) is the current CommonGround holding speaker-indexed commitments `S⊢φ`, and continuations are proposed future states from questions. - Assertion narrows every state with `commit speaker φ`. @@ -27,11 +27,11 @@ the commitment/belief separation (lying, hedging). ## Speaker indexing The paper's central primitive is the Frege turnstile `S⊢φ` (p. 332): -assertion is responsibility-undertaking, so what enters the CG is +assertion is responsibility-undertaking, so what enters the CommonGround is "speaker S is committed to the truth of φ", not bare φ. The substrate uses `Discourse.Commitment.IndexedCommitment` to model this — the root holds indexed commitments, projected to a flat context set via -`IndexedCommitment.toCommitment` for the CG-as-set view. +`IndexedCommitment.toCommitment` for the CommonGround-as-set view. ## Sibling files @@ -54,7 +54,7 @@ Out of scope (would need substrate extensions): - **Time-indexed commitments** (Lauer 2013 PB/PEP carry a `t` index): the substrate has no time index; `rejectFirst` is the closest proxy for rescission. True time-indexed commitment dynamics need a separate layer. -- **Anderson 2021 distributional CG**: requires `weight_nonneg` on the +- **Anderson 2021 distributional CommonGround**: requires `weight_nonneg` on the per-world weight. Hosting Anderson via `CommitmentSpace W ℝ` would need an `[OrderedAddCommMonoid G]` constraint or an Anderson wrapper — current substrate does not enforce non-negativity. @@ -75,7 +75,7 @@ open Discourse.Commitment (CommitmentSlate IndexedCommitment IndexedWeightedCommitment CommitmentForce HasSupport CommitmentGrade) open Discourse (DiscourseRole) -open Discourse.CommonGround (ContextSet) +open CommonGround (ContextSet) open Semantics.Mood (IllocutionaryMood) -- ════════════════════════════════════════════════════ @@ -125,10 +125,10 @@ abbrev KAgent := DiscourseRole - Reject: prune a continuation (= return to `{√C}` disjunct). The tree structure captures the assertion/question asymmetry: - assertions modify the root (the CG changes), while questions only - add continuations (the CG is preserved until acceptance). -/ + assertions modify the root (the CommonGround changes), while questions only + add continuations (the CommonGround is preserved until acceptance). -/ structure CommitmentSpace (W : Type*) (G : Type*) where - /-- Root commitment state √C: indexed commitments currently in the CG. + /-- Root commitment state √C: indexed commitments currently in the CommonGround. The grade type `G` lets the same shape host binary (G = Prop), distributional (G = ℝ), or credence-bounded (G = ℚ) commitments. -/ root : List (IndexedWeightedCommitment W G) @@ -165,7 +165,7 @@ def assert (cs : CommitmentSpace W G) (committer : DiscourseRole) `C + ?φ = {√C} ∪ (C + S₂⊢φ)` - The root stays unchanged (CG preserved). A new continuation is added + The root stays unchanged (CommonGround preserved). A new continuation is added where the addressee has committed to `weight`. Existing continuations are also extended by the addressee-commitment. The committer is hardcoded to `.addressee` per Krifka's discussion of (30), p. 337: @@ -213,13 +213,13 @@ instance : DecidablePred (@hasNoOpenContinuations W G) := fun cs => by cases conts <;> (unfold hasNoOpenContinuations; infer_instance) /-- Accept the first continuation: it becomes the new root. - The CG is updated to the accepted proposal's content. -/ + The CommonGround is updated to the accepted proposal's content. -/ def acceptFirst : CommitmentSpace W G → CommitmentSpace W G | ⟨_, c :: rest⟩ => ⟨c, rest⟩ | cs => cs /-- Reject the first continuation: prune it. - The CG is unchanged; the proposal is discarded. -/ + The CommonGround is unchanged; the proposal is discarded. -/ def rejectFirst : CommitmentSpace W G → CommitmentSpace W G | ⟨r, _ :: rest⟩ => ⟨r, rest⟩ | cs => cs @@ -249,7 +249,7 @@ def denegate (actMarker : IndexedWeightedCommitment W G → Prop) continuations := cs.continuations.filter (fun cont => decide (¬ ∃ ic ∈ cont, actMarker ic)) } -/-- Denegation preserves the root (CG unchanged) — Krifka 2015 p. 330: +/-- Denegation preserves the root (CommonGround unchanged) — Krifka 2015 p. 330: "denegation does not change the root of the commitment space, but prunes its legal developments." -/ @[simp] @@ -449,13 +449,13 @@ theorem assert_in_root (cs : CommitmentSpace W Prop) (s : DiscourseRole) IndexedCommitment.commit s φ ∈ (cs.assert s φ).root := by simp only [assert, IndexedCommitment.commit, List.mem_cons, true_or] -/-- Monopolar question preserves the root (CG unchanged). -/ +/-- Monopolar question preserves the root (CommonGround unchanged). -/ @[simp] theorem monopolarQuestion_preserves_root (cs : CommitmentSpace W G) (weight : W → G) : (cs.monopolarQuestion weight).root = cs.root := rfl -/-- Bipolar question preserves the root (CG unchanged). -/ +/-- Bipolar question preserves the root (CommonGround unchanged). -/ @[simp] theorem bipolarQuestion_preserves_root [CommitmentGrade G] (cs : CommitmentSpace W G) (φ : W → G) : @@ -467,7 +467,7 @@ end CommitmentSpace commitment space (tree). The commitment space tracks the shared discourse structure: what's in - the CG (root) and what's been proposed (continuations). Per-agent + the CommonGround (root) and what's been proposed (continuations). Per-agent slates track individual public commitments, enabling the commitment/belief separation central to Krifka's theory. -/ structure KrifkaState (W : Type*) where @@ -475,7 +475,7 @@ structure KrifkaState (W : Type*) where speakerCS : CommitmentSlate W /-- Addressee's individual commitment slate. -/ addresseeCS : CommitmentSlate W - /-- Shared commitment space (tree): CG + proposed updates. + /-- Shared commitment space (tree): CommonGround + proposed updates. Binary specialisation `CommitmentSpace W Prop` of the polymorphic `CommitmentSpace W G`. Future graded-state extensions (Lauer-credence, Anderson-distributional) belong in a separate @@ -528,7 +528,7 @@ def negatedQuestionLow (s : KrifkaState W) (φ : W → Prop) : KrifkaState W := def negatedQuestionHigh (s : KrifkaState W) (φ : W → Prop) : KrifkaState W := { s with space := s.space.negatedQuestionHigh φ } -/-- Accept the first continuation: it becomes the new CG root. -/ +/-- Accept the first continuation: it becomes the new CommonGround root. -/ def acceptContinuation (s : KrifkaState W) : KrifkaState W := { s with space := s.space.acceptFirst } @@ -536,7 +536,7 @@ def acceptContinuation (s : KrifkaState W) : KrifkaState W := def rejectContinuation (s : KrifkaState W) : KrifkaState W := { s with space := s.space.rejectFirst } -/-- Context set: from the commitment space root (= CG), via +/-- Context set: from the commitment space root (= CommonGround), via `IndexedCommitment.toCommitment` projection. -/ def contextSet (s : KrifkaState W) : ContextSet W := s.space.toContextSet @@ -566,12 +566,12 @@ theorem commitment_closure {W : Type*} (s : KrifkaState W) (p : W → Prop) IndexedCommitment.commit committer p :: s.space.root := by cases committer <;> rfl -/-- Questions don't change the CG: the root is preserved. -/ +/-- Questions don't change the CommonGround: the root is preserved. -/ theorem monopolarQuestion_preserves_cg {W : Type*} (s : KrifkaState W) (p : W → Prop) : (s.monopolarQuestion p).space.root = s.space.root := rfl /-- Question then accept ≈ assert (on the root): accepting a monopolar - question's sole continuation yields the same CG as the addressee + question's sole continuation yields the same CommonGround as the addressee directly asserting φ. This connects the two modes of updating: direct assertion (committer @@ -756,22 +756,22 @@ end KrifkaState -- § 5. HasContextSet Instances -- ════════════════════════════════════════════════════ -open Discourse.CommonGround in +open CommonGround in /-- A polymorphic commitment space projects to a context set via its root, using the `[HasSupport G]` typeclass's `support` projection. Recovers the binary case at `G = Prop` definitionally (via `support := id` in - the `Prop` instance). Anderson 2021's distributional CG (`G = ℝ`) + the `Prop` instance). Anderson 2021's distributional CommonGround (`G = ℝ`) becomes a consumer via `HasSupport ℝ` provided in `Anderson2021.lean`. -/ instance {W G : Type*} [HasSupport G] : HasContextSet (CommitmentSpace W G) W where toContextSet := CommitmentSpace.toContextSet -open Discourse.CommonGround in +open CommonGround in /-- A Krifka state projects to a context set via the commitment space root. -/ instance {W : Type*} : HasContextSet (KrifkaState W) W where toContextSet := KrifkaState.contextSet -open Discourse.CommonGround in +open CommonGround in /-- KrifkaState context set agrees with CommitmentSpace context set. -/ theorem krifkaState_contextSet_eq_space {W : Type*} (s : KrifkaState W) : HasContextSet.toContextSet s = HasContextSet.toContextSet s.space := rfl diff --git a/Linglib/Dialogue/CredenceThreshold.lean b/Linglib/Dialogue/CredenceThreshold.lean index 7d0bec986..4e83eb356 100644 --- a/Linglib/Dialogue/CredenceThreshold.lean +++ b/Linglib/Dialogue/CredenceThreshold.lean @@ -41,7 +41,7 @@ substrate-supported elsewhere: maps to the rationality parameter Closest to Stalnaker in structure (no explicit commitment/belief -separation), but adds a probabilistic dimension that the bare CG +separation), but adds a probabilistic dimension that the bare CommonGround model lacks. -/ @@ -49,7 +49,7 @@ model lacks. namespace Dialogue.CredenceThreshold open Discourse.Commitment (CommitmentSlate) -open Discourse.CommonGround (ContextSet) +open CommonGround (ContextSet) -- ════════════════════════════════════════════════════ -- § 1. Credence Functions @@ -166,7 +166,7 @@ theorem always_stable {W : Type*} (s : State W) : -- HasContextSet instance -- ════════════════════════════════════════════════════ -open Discourse.CommonGround in +open CommonGround in /-- Credence-threshold states project to a context set via the asserted-list intersection (`contextSet`). The credence + threshold machinery gates *which* assertions can occur; once asserted, the diff --git a/Linglib/Dialogue/DisjunctiveUpdate.lean b/Linglib/Dialogue/DisjunctiveUpdate.lean index b3410ee5b..9bab25940 100644 --- a/Linglib/Dialogue/DisjunctiveUpdate.lean +++ b/Linglib/Dialogue/DisjunctiveUpdate.lean @@ -58,7 +58,7 @@ sequential update = single conjunctive update — apply directly. namespace Dialogue.DisjunctiveUpdate -open Discourse.CommonGround (ContextSet) +open CommonGround (ContextSet) open Semantics.Dynamic.ParameterizedUpdate diff --git a/Linglib/Dialogue/DistributionalCG.lean b/Linglib/Dialogue/DistributionalCG.lean index 54a64a3a4..f8e25e13f 100644 --- a/Linglib/Dialogue/DistributionalCG.lean +++ b/Linglib/Dialogue/DistributionalCG.lean @@ -11,7 +11,7 @@ import Linglib.Dialogue.CommitmentSpace A non-negative real-valued weight function over worlds, refining @cite{stalnaker-2002}'s sharp set-membership context set with graded -plausibility. The probabilistic counterpart of `Discourse.CommonGround.CG W`. +plausibility. The probabilistic counterpart of `CommonGround W`. ## Substrate role @@ -43,7 +43,7 @@ frameworks. namespace Dialogue -open Discourse.CommonGround (ContextSet HasContextSet) +open CommonGround (ContextSet HasContextSet) open Discourse (DiscourseRole) open Discourse.Commitment (HasSupport IndexedWeightedCommitment CommitmentForce) @@ -54,7 +54,7 @@ open Discourse.Commitment (HasSupport IndexedWeightedCommitment CommitmentForce) /-- A distributional common ground: a non-negative weight function over worlds (@cite{anderson-2021}). The probabilistic counterpart of @cite{stalnaker-2002}'s context set — instead of - a sharp membership predicate (`W → Prop`), the CG assigns graded + a sharp membership predicate (`W → Prop`), the CommonGround assigns graded plausibility (`W → ℝ`). -/ structure DistributionalCG (W : Type*) where weight : W → ℝ @@ -64,7 +64,7 @@ namespace DistributionalCG variable {W : Type*} -/-- Uniform distributional CG: all worlds equally plausible (empty CG). -/ +/-- Uniform distributional CommonGround: all worlds equally plausible (empty CommonGround). -/ noncomputable def uniform : DistributionalCG W where weight _ := 1 weight_nonneg _ := le_of_lt one_pos @@ -75,7 +75,7 @@ noncomputable def uniform : DistributionalCG W where def toContextSet (cg : DistributionalCG W) : ContextSet W := λ w => 0 < cg.weight w -/-- Uniform distributional CG maps to the trivial context set. -/ +/-- Uniform distributional CommonGround maps to the trivial context set. -/ theorem uniform_toContextSet : (uniform : DistributionalCG W).toContextSet = ContextSet.trivial := by funext w @@ -91,7 +91,7 @@ theorem zero_weight_excluded (cg : DistributionalCG W) (w : W) end DistributionalCG -/-- A distributional CG projects to a context set: worlds with +/-- A distributional CommonGround projects to a context set: worlds with positive weight. -/ instance {W : Type*} : HasContextSet (DistributionalCG W) W where toContextSet := DistributionalCG.toContextSet @@ -102,7 +102,7 @@ instance {W : Type*} : HasContextSet (DistributionalCG W) W where /-- `[HasSupport ℝ]` instance for distributional CGs. `support g := 0 < g` matches Anderson's "world has positive weight - iff in CG" projection (cf. `DistributionalCG.toContextSet`). + iff in CommonGround" projection (cf. `DistributionalCG.toContextSet`). Provides ONLY `HasSupport ℝ`, NOT `CommitmentGrade ℝ`: the latter would require the involution law on `complement`, which fails on @@ -114,7 +114,7 @@ instance : HasSupport ℝ where -- § 3. Bridge to polymorphic CommitmentSpace W ℝ -- ════════════════════════════════════════════════════ -/-- Bridge: a distributional CG embeds into a commitment space at +/-- Bridge: a distributional CommonGround embeds into a commitment space at `G = ℝ`. The speaker's distributional weights become a single `commit speaker .doxastic weight` entry in the root. @@ -129,10 +129,10 @@ noncomputable def DistributionalCG.toCommitmentSpace {W : Type*} root := [IndexedWeightedCommitment.commit .speaker .doxastic cg.weight] continuations := [] -/-- Bridge theorem: the support of a distributional CG equals the +/-- Bridge theorem: the support of a distributional CommonGround equals the `toContextSet` projection of the bridged commitment space. Demonstrates that the polymorphic substrate at `G = ℝ` - faithfully captures Anderson's distributional CG when projected + faithfully captures Anderson's distributional CommonGround when projected to its support. -/ theorem DistributionalCG.toCommitmentSpace_support {W : Type*} (cg : DistributionalCG W) (w : W) : diff --git a/Linglib/Dialogue/FarkasBruce.lean b/Linglib/Dialogue/FarkasBruce.lean index 7aeaf56f6..2295b724c 100644 --- a/Linglib/Dialogue/FarkasBruce.lean +++ b/Linglib/Dialogue/FarkasBruce.lean @@ -43,7 +43,7 @@ properties — `assert_adds_to_dcS`, `assert_preserves_cg`, namespace Dialogue.FarkasBruce -open Discourse.CommonGround +open CommonGround /-- @@ -124,7 +124,7 @@ def empty : DiscourseState W := ⟨[], [], [], []⟩ /-- Convert common ground to a ContextSet (worlds where all cg props hold). -Bridges to the existing `Discourse.CommonGround` infrastructure as the +Bridges to the existing `CommonGround` infrastructure as the fold-intersection of the cg list. -/ def toContextSet (ds : DiscourseState W) : ContextSet W := @@ -251,17 +251,17 @@ def acceptTop (ds : DiscourseState W) : DiscourseState W := /-- -Convert the common ground component to a `CG` structure. +Convert the common ground component to a `CommonGround` structure. -/ -def toCG (ds : DiscourseState W) : CG W := +def toCG (ds : DiscourseState W) : CommonGround W := { propositions := ds.cg } /-- -Create a discourse state from a `CG` structure. +Create a discourse state from a `CommonGround` structure. -Sets cg, dcS, and dcL all to the CG propositions (everyone agrees). +Sets cg, dcS, and dcL all to the CommonGround propositions (everyone agrees). -/ -def fromCG (cg : CG W) : DiscourseState W := +def fromCG (cg : CommonGround W) : DiscourseState W := { dcS := cg.propositions dcL := cg.propositions cg := cg.propositions @@ -341,7 +341,7 @@ end DiscourseState -- HasContextSet instance -- ════════════════════════════════════════════════════ -open Discourse.CommonGround in +open CommonGround in /-- F&B states project to a context set via `cg`-only intersection (`toContextSet`). Note: this projection deliberately ignores `dcS`/`dcL` and `table` — F&B's whole point is that assertion diff --git a/Linglib/Dialogue/Gunlogson.lean b/Linglib/Dialogue/Gunlogson.lean index 7074f8284..50f36d0d2 100644 --- a/Linglib/Dialogue/Gunlogson.lean +++ b/Linglib/Dialogue/Gunlogson.lean @@ -37,7 +37,7 @@ Source determines who can challenge: namespace Dialogue.Gunlogson open Discourse.Commitment -open Discourse.CommonGround (ContextSet CG) +open CommonGround (ContextSet) open Discourse (DiscourseRole) open Semantics.Modality.BiasedPQ (ContextualEvidence) @@ -48,7 +48,7 @@ open Semantics.Modality.BiasedPQ (ContextualEvidence) /-- Gunlogson's discourse state: source-tagged commitment slates for speaker and addressee. - Unlike Stalnaker (single CG) or Farkas & Bruce (dcS + dcL + cg), + Unlike Stalnaker (single CommonGround) or Farkas & Bruce (dcS + dcL + cg), Gunlogson tracks the SOURCE of each commitment, not just which participant holds it. -/ structure GunlogsonState (W : Type*) where @@ -338,7 +338,7 @@ theorem confirm_still_unstable {W : Type*} (p : Set W) : -- HasContextSet instance -- ════════════════════════════════════════════════════ -open Discourse.CommonGround in +open CommonGround in /-- Gunlogson states project to a context set via `contextSet` — the intersection of both participants' commitment contexts (regardless of source). -/ diff --git a/Linglib/Dialogue/KOS/Basic.lean b/Linglib/Dialogue/KOS/Basic.lean index 19e515b73..25ad878de 100644 --- a/Linglib/Dialogue/KOS/Basic.lean +++ b/Linglib/Dialogue/KOS/Basic.lean @@ -17,7 +17,7 @@ partition-based answerhood predicate `PropResolvesQUD`. - §1. DGB structural lemmas (initial state) - §2. DGB update operations: pushQud, downdateQud, addFact, recordMove, assertFact - §3. DGB content mapping: mapFacts, mapQud -- §4. HasContextSet bridge to Discourse.CommonGround +- §4. HasContextSet bridge to CommonGround - §5. QUD downdate properties + non-resolve-cond well-formedness - §6. Partition-based answerhood (`PropResolvesQUD`) @@ -147,20 +147,20 @@ theorem DGB.mapFacts_length {Participant Fact Fact' QContent : Type*} {Cont : Ty -- § 4. HasContextSet Bridge -- ════════════════════════════════════════════════════ -open Discourse.CommonGround in +open CommonGround in /-- DGB with `Set W` facts projects to a context set. @cite{ginzburg-2012} Ch. 4: the DGB's FACTS field IS the common ground. -/ instance {W Participant QContent : Type*} {Cont : Type} : HasContextSet (DGB Participant (Set W) QContent Cont) W where toContextSet dgb := λ w => ∀ p ∈ dgb.facts, p w -open Discourse.CommonGround in +open CommonGround in /-- TIS with `Set W` facts inherits the DGB's context set. -/ instance {W Participant QContent : Type*} {Cont : Type} : HasContextSet (TIS Participant (Set W) QContent Cont) W where toContextSet tis := λ w => ∀ p ∈ tis.dgb.facts, p w -open Discourse.CommonGround in +open CommonGround in /-- TIS context set is extracted from the DGB. -/ theorem tis_contextSet_eq_dgb {W Participant QContent : Type*} {Cont : Type} (tis : TIS Participant (Set W) QContent Cont) : diff --git a/Linglib/Dialogue/KOS/Defs.lean b/Linglib/Dialogue/KOS/Defs.lean index 482cc5d84..3d6a2bb11 100644 --- a/Linglib/Dialogue/KOS/Defs.lean +++ b/Linglib/Dialogue/KOS/Defs.lean @@ -273,7 +273,7 @@ public component of a participant's conversational state. The type parameters make content types explicit: - `Participant`: type of participant identifiers (e.g., `String`, `Fin 2`) -- `Fact`: type of accumulated facts (e.g., `Set W` for typed CG access) +- `Fact`: type of accumulated facts (e.g., `Set W` for typed CommonGround access) - `QContent`: type of QUD questions (e.g., partition-based `QUD W`) - `Cont`: type of locutionary content (e.g., `String` for surface form or `BCheckableAustinian S` for TTR-typed propositions) diff --git a/Linglib/Dialogue/ReasonableInference.lean b/Linglib/Dialogue/ReasonableInference.lean index 0476efaca..f6c4e19f1 100644 --- a/Linglib/Dialogue/ReasonableInference.lean +++ b/Linglib/Dialogue/ReasonableInference.lean @@ -16,7 +16,7 @@ The formal apparatus is a triple `(⟦·⟧, A, g)`: * `A(P, k)`: the **appropriateness** relation — whether asserting `P` in context `k` is appropriate; * `g(P, k) = k ∩ ⟦P⟧_k`: the **change function** — the new context after - asserting `P`. This is exactly `Discourse.CommonGround.ContextSet.update`. + asserting `P`. This is exactly `CommonGround.ContextSet.update`. This module defines `Appropriateness`, sequential appropriateness `A*`, sequential update `g*`, and the `reasonableInference` predicate. @@ -29,7 +29,7 @@ exhibits the gap. namespace Dialogue.ReasonableInference -open Discourse.CommonGround +open CommonGround /-- **Appropriateness** of a sentence in a context. Stalnaker leaves this diff --git a/Linglib/Dialogue/Stalnaker.lean b/Linglib/Dialogue/Stalnaker.lean index 6f929935a..651901585 100644 --- a/Linglib/Dialogue/Stalnaker.lean +++ b/Linglib/Dialogue/Stalnaker.lean @@ -12,9 +12,9 @@ and the baseline against which richer theories are compared. - **No commitment/belief separation**: assertion IS adding to shared beliefs. There is no intermediate "commitment" stage. -- **No retraction**: the CG is monotonically updated (worlds are eliminated, +- **No retraction**: the CommonGround is monotonically updated (worlds are eliminated, never restored). -- **No source marking**: all CG updates are symmetric between participants. +- **No source marking**: all CommonGround updates are symmetric between participants. ## Stalnaker's Norm @@ -23,14 +23,14 @@ and the baseline against which richer theories are compared. 2. The speaker believes the proposition (knowledge) 3. The proposition is not already in the common ground (informativity) -This module models the EFFECT of assertion (CG update), not the norms. +This module models the EFFECT of assertion (CommonGround update), not the norms. The norms are relevant to Krifka's separation of commitment from belief. -/ namespace Dialogue.Stalnaker -open Discourse.CommonGround (CG ContextSet) +open CommonGround (ContextSet) -- ════════════════════════════════════════════════════ -- § 1. State = Common Ground @@ -38,17 +38,17 @@ open Discourse.CommonGround (CG ContextSet) /-- Stalnaker's discourse state IS the common ground. No separate commitment layer; assertion directly updates shared beliefs. -/ -abbrev StalnakerState (W : Type*) := CG W +abbrev StalnakerState (W : Type*) := CommonGround W /-- Initial state: empty common ground (all worlds possible). -/ -def initial {W : Type*} : StalnakerState W := CG.empty +def initial {W : Type*} : StalnakerState W := CommonGround.empty /-- Assert p: add it to the common ground. This IS the full effect of assertion — no intermediate step. -/ def assert {W : Type*} (s : StalnakerState W) (p : Set W) : StalnakerState W := s.add p -/-- Context set: directly from CG. -/ +/-- Context set: directly from CommonGround. -/ def contextSet {W : Type*} (s : StalnakerState W) : ContextSet W := s.contextSet @@ -63,14 +63,14 @@ instance {W : Type*} (s : StalnakerState W) : Decidable (isStable s) := -- § 2. Verification -- ════════════════════════════════════════════════════ -/-- Empty CG gives trivial context set. -/ +/-- Empty CommonGround gives trivial context set. -/ theorem initial_trivial {W : Type*} : - contextSet (initial (W := W)) = ContextSet.trivial := CG.empty_contextSet + contextSet (initial (W := W)) = ContextSet.trivial := CommonGround.empty_contextSet /-- Assertion restricts the context set. -/ theorem assert_restricts {W : Type*} (s : StalnakerState W) (p : Set W) : contextSet (assert s p) ⊆ contextSet s := - CG.add_restricts s p + CommonGround.add_restricts s p /-- Stalnaker states are always stable. -/ theorem always_stable {W : Type*} (s : StalnakerState W) : isStable s := trivial @@ -79,14 +79,14 @@ theorem always_stable {W : Type*} (s : StalnakerState W) : isStable s := trivial -- HasContextSet (re-export via abbrev) -- ════════════════════════════════════════════════════ -/-- Theorem (not instance — the `CG W` instance from `Discourse.CommonGround` - already resolves through the `StalnakerState W := CG W` abbrev): the +/-- Theorem (not instance — the `CommonGround W` instance from `CommonGround` + already resolves through the `StalnakerState W := CommonGround W` abbrev): the `HasContextSet` projection on a Stalnaker state agrees with the local `Stalnaker.contextSet` def. Documents the bridge for grep. -/ theorem hasContextSet_eq_contextSet {W : Type*} (s : StalnakerState W) : - Discourse.CommonGround.HasContextSet.toContextSet s = Stalnaker.contextSet s := rfl + CommonGround.HasContextSet.toContextSet s = Stalnaker.contextSet s := rfl -/-- Stalnaker's CG-as-context-set instances `Assertable`: assertion is +/-- Stalnaker's CommonGround-as-context-set instances `Assertable`: assertion is `s.add φ` (set intersection); the two laws are the two halves of intersection membership. -/ instance instAssertable {W : Type*} : diff --git a/Linglib/Discourse/Commitment/Basic.lean b/Linglib/Discourse/Commitment/Basic.lean index a89240f6a..b0cfe324c 100644 --- a/Linglib/Discourse/Commitment/Basic.lean +++ b/Linglib/Discourse/Commitment/Basic.lean @@ -145,7 +145,7 @@ instance : CommitmentGrade Prop where complement := Not -- No `Bool` instance by default — consumers needing decidable grades --- declare locally. Anderson 2021's distributional CG provides +-- declare locally. Anderson 2021's distributional CommonGround provides -- `HasSupport ℝ` at its own site. /-! ### Speaker-Indexed Commitments -/ @@ -246,7 +246,7 @@ end Commitment /-! ### HasContextSet Instance -/ -open Discourse.CommonGround in +open CommonGround in /-- A commitment slate projects to a context set. -/ instance {W : Type*} : HasContextSet (Commitment.CommitmentSlate W) W where toContextSet s := λ w => s.toContextSet w diff --git a/Linglib/Discourse/Commitment/Frame.lean b/Linglib/Discourse/Commitment/Frame.lean index 61c8910b2..c700349ed 100644 --- a/Linglib/Discourse/Commitment/Frame.lean +++ b/Linglib/Discourse/Commitment/Frame.lean @@ -174,7 +174,7 @@ theorem believes_a_implies_believes_b_of_competent fun hbel v hbelB => hbel v (h a b w v hbelB) /-- Composed: Sincerity + Competence ⇒ `a`'s commitment-to-`b` of `π` - entails `b`'s belief in `π`. The mediated CG-update of + entails `b`'s belief in `π`. The mediated CommonGround-update of @cite{bary-2025}, derived not stipulated (@cite{van-der-leer-2026}). -/ theorem committed_implies_addressee_believes_of_sincere_competent {c : CommitmentState W A} (hsin : Sincere c) (hcomp : Competent c) diff --git a/Linglib/Discourse/Commitment/Table.lean b/Linglib/Discourse/Commitment/Table.lean index bf086a311..a94841598 100644 --- a/Linglib/Discourse/Commitment/Table.lean +++ b/Linglib/Discourse/Commitment/Table.lean @@ -19,14 +19,14 @@ commitment slates, and a common ground. ## TODO -* Projected set `ps(CG)`, highlighting (@cite{farkas-roelofsen-2017}), +* Projected set `ps(CommonGround)`, highlighting (@cite{farkas-roelofsen-2017}), item identity (for withdrawal). -/ namespace Discourse.Commitment.Table open Discourse.Commitment (TaggedSlate CommitmentSource CommitmentForce) -open Discourse.CommonGround (CG HasContextSet) +open CommonGround (HasContextSet) open Semantics.Mood (IllocutionaryMood) /-- An at-issue item on the conversational table. -/ @@ -49,14 +49,14 @@ structure DiscourseState (A W I : Type*) where /-- Per-agent discourse commitments. -/ dc : A → TaggedSlate W /-- The common ground. -/ - cg : CG W + cg : CommonGround W namespace DiscourseState variable {A W I : Type*} -/-- Initial state: empty table, empty commitments, trivial CG. -/ +/-- Initial state: empty table, empty commitments, trivial CommonGround. -/ def empty : DiscourseState A W I := - ⟨[], fun _ => TaggedSlate.empty, CG.empty⟩ + ⟨[], fun _ => TaggedSlate.empty, CommonGround.empty⟩ instance : Inhabited (DiscourseState A W I) := ⟨empty⟩ @@ -93,7 +93,7 @@ def addCommit [DecidableEq A] (s : DiscourseState A W I) (a : A) @[simp] theorem empty_table : (empty : DiscourseState A W I).table = [] := rfl @[simp] theorem empty_dc (a : A) : (empty : DiscourseState A W I).dc a = TaggedSlate.empty := rfl -@[simp] theorem empty_cg : (empty : DiscourseState A W I).cg = CG.empty := rfl +@[simp] theorem empty_cg : (empty : DiscourseState A W I).cg = CommonGround.empty := rfl @[simp] theorem empty_isStable : (empty : DiscourseState A W I).IsStable := rfl @[simp] theorem pushItem_table (s : DiscourseState A W I) (i : I) : diff --git a/Linglib/Discourse/CommonGround.lean b/Linglib/Discourse/CommonGround.lean index 268e99bf2..380600539 100644 --- a/Linglib/Discourse/CommonGround.lean +++ b/Linglib/Discourse/CommonGround.lean @@ -4,34 +4,49 @@ import Mathlib.Data.Set.Lattice /-! # Common Ground -@cite{stalnaker-1974} @cite{stalnaker-2002} +Framework-agnostic context management following @cite{stalnaker-1974} and +@cite{stalnaker-2002}: context sets, common ground as proposition lists, and +the `HasContextSet` interface unifying both with the various discourse-state +representations across the discourse layer. -Framework-agnostic context management following @cite{stalnaker-1974}: -context sets (`Set W`), common ground as proposition lists (`CG W`), -and the `HasContextSet` interface unifying both with the various -discourse-state representations across `Theories/`. +## Main definitions -Multi-agent epistemic operators (knowledge, belief, common knowledge) -are in `Semantics/Modality/EpistemicLogic.lean`. +* `ContextSet W` — worlds compatible with the context (a synonym for `Set W`). +* `CommonGround W` — common ground as a list of propositions. +* `CommonGround.HasContextSet` — interface extracting a context set from an + arbitrary discourse state. + +## Implementation notes + +`CommonGround` is the root-level type; its API (and `ContextSet` / +`HasContextSet`) lives in `namespace CommonGround`, mirroring mathlib's +`Finset`. Consumers `open CommonGround` for the API; the type itself is +visible unqualified. + +Multi-agent epistemic operators (knowledge, belief, common knowledge) are in +`Semantics/Modality/EpistemicLogic.lean`. -/ -namespace Discourse.CommonGround +/-- Common ground as a list of mutually believed propositions. -/ +structure CommonGround (W : Type*) where + /-- The propositions in the common ground. -/ + propositions : List (Set W) + +namespace CommonGround + +variable {W : Type*} /-- The set of worlds compatible with the common ground. -/ abbrev ContextSet (W : Type*) := Set W namespace ContextSet -variable {W : Type*} - /-- The trivial context: all worlds possible. Alias for `Set.univ`. -/ abbrev trivial : ContextSet W := Set.univ /-- Entailment: every world in the context satisfies the proposition. -/ abbrev entails (c : ContextSet W) (p : Set W) : Prop := c ⊆ p -@[inherit_doc] notation:50 c " ⊧ " p => entails c p - /-- The context set has at least one world. Alias for `Set.Nonempty`. -/ abbrev nonEmpty (c : ContextSet W) : Prop := c.Nonempty @@ -41,19 +56,17 @@ abbrev compatible (c : ContextSet W) (p : Set W) : Prop := (c ∩ p).Nonempty /-- Update: keep only worlds where the proposition holds. Alias for `(· ∩ ·)`. -/ abbrev update (c : ContextSet W) (p : Set W) : ContextSet W := c ∩ p -@[inherit_doc] scoped notation:60 c " + " p => update c p - /-- Updated context entails the update proposition. -/ -theorem update_entails (c : ContextSet W) (p : Set W) : (c + p) ⊧ p := +theorem update_entails (c : ContextSet W) (p : Set W) : update c p ⊆ p := Set.inter_subset_right /-- Updated context is contained in the original. -/ -theorem update_restricts (c : ContextSet W) (p : Set W) : (c + p) ⊆ c := +theorem update_restricts (c : ContextSet W) (p : Set W) : update c p ⊆ c := Set.inter_subset_left /-- Updating with what's already entailed doesn't change the context. -/ -theorem update_entailed (c : ContextSet W) (p : Set W) (h : c ⊧ p) : - (c + p) = c := +theorem update_eq_self_of_entails (c : ContextSet W) (p : Set W) (h : c ⊆ p) : + update c p = c := Set.inter_eq_left.mpr h /-- Sequential updates are associative. -/ @@ -61,69 +74,46 @@ theorem update_assoc (c p q : Set W) : update (update c p) q = update c (update p q) := Set.inter_assoc c p q -/-- Updating trivial context with `p` gives `p`. -/ -theorem trivial_update (p : Set W) : (trivial + p) = p := +/-- Updating the trivial context with `p` gives `p`. -/ +theorem trivial_update (p : Set W) : update trivial p = p := Set.univ_inter p -/-- Entailment is monotonic: a smaller context entails everything a larger one does. -/ -theorem entails_mono {c₁ c₂ : ContextSet W} {p : Set W} - (h_sub : c₁ ⊆ c₂) (h_ent : c₂ ⊧ p) : c₁ ⊧ p := - h_sub.trans h_ent - -/-- Update is monotonic in the context. -/ -theorem update_mono {c₁ c₂ : ContextSet W} (p : Set W) (h : c₁ ⊆ c₂) : - update c₁ p ⊆ update c₂ p := - Set.inter_subset_inter_left p h - end ContextSet -/-- Common ground as a list of mutually believed propositions. -/ -structure CG (W : Type*) where - /-- The propositions in the common ground -/ - propositions : List (Set W) - -namespace CG - -variable {W : Type*} - /-- The context set determined by a common ground: intersection of its propositions. -/ -def contextSet (cg : CG W) : ContextSet W := +def contextSet (cg : CommonGround W) : ContextSet W := cg.propositions.foldr (· ∩ ·) Set.univ /-- Add a proposition to the common ground. -/ -def add (cg : CG W) (p : Set W) : CG W := +def add (cg : CommonGround W) (p : Set W) : CommonGround W := { propositions := p :: cg.propositions } /-- Empty common ground (no shared beliefs). -/ -def empty : CG W := { propositions := [] } +def empty : CommonGround W := { propositions := [] } -instance : Inhabited (CG W) := ⟨CG.empty⟩ +instance : Inhabited (CommonGround W) := ⟨empty⟩ -/-- Empty CG gives the trivial (universal) context set. -/ -@[simp] theorem empty_contextSet : (empty : CG W).contextSet = ContextSet.trivial := rfl +/-- Empty common ground gives the trivial (universal) context set. -/ +@[simp] theorem empty_contextSet : (empty : CommonGround W).contextSet = Set.univ := rfl /-- Adding a proposition intersects it into the context set. -/ -@[simp] theorem contextSet_add (cg : CG W) (p : Set W) : +@[simp] theorem contextSet_add (cg : CommonGround W) (p : Set W) : (cg.add p).contextSet = p ∩ cg.contextSet := rfl /-- Adding a proposition restricts the context set. -/ -theorem add_restricts (cg : CG W) (p : Set W) : +theorem add_restricts (cg : CommonGround W) (p : Set W) : (cg.add p).contextSet ⊆ cg.contextSet := Set.inter_subset_right -end CG - /-! ### Uniform context-set extraction -/ -/-- A discourse state from which a context set can be extracted. - Instanced by `CG`, `CommitmentSlate`, `CommitmentSpace`, - `DistributionalCG`, `DGB`, `InfoState`, etc. -/ +/-- A discourse state from which a context set can be extracted. -/ class HasContextSet (S : Type*) (W : outParam Type*) where toContextSet : S → ContextSet W namespace HasContextSet -variable {S W : Type*} [HasContextSet S W] +variable {S : Type*} [HasContextSet S W] /-- A discourse state entails a proposition if its context set does. -/ abbrev entails (s : S) (p : Set W) : Prop := toContextSet s ⊆ p @@ -133,21 +123,21 @@ abbrev updateCS (s : S) (p : Set W) : ContextSet W := toContextSet s ∩ p end HasContextSet --- Canonical instances +/-! ### Canonical instances -/ -instance {W : Type*} : HasContextSet (ContextSet W) W where +instance : HasContextSet (ContextSet W) W where toContextSet := id -instance {W : Type*} : HasContextSet (CG W) W where - toContextSet := CG.contextSet +instance : HasContextSet (CommonGround W) W where + toContextSet := contextSet -/-- The CG instance agrees with `CG.contextSet`. -/ -theorem hasContextSet_CG_eq {W : Type*} (cg : CG W) : +/-- The `CommonGround` instance agrees with `CommonGround.contextSet`. -/ +@[simp] theorem hasContextSet_commonGround_eq (cg : CommonGround W) : HasContextSet.toContextSet cg = cg.contextSet := rfl -/-- Adding to CG restricts the HasContextSet extraction. -/ -theorem hasContextSet_add_restricts {W : Type*} (cg : CG W) (p : Set W) : +/-- Adding to the common ground restricts the `HasContextSet` extraction. -/ +theorem hasContextSet_add_restricts (cg : CommonGround W) (p : Set W) : HasContextSet.toContextSet (cg.add p) ⊆ HasContextSet.toContextSet cg := - CG.add_restricts cg p + add_restricts cg p -end Discourse.CommonGround +end CommonGround diff --git a/Linglib/Discourse/Scoreboard.lean b/Linglib/Discourse/Scoreboard.lean index 03bbe33d7..39347cb2f 100644 --- a/Linglib/Discourse/Scoreboard.lean +++ b/Linglib/Discourse/Scoreboard.lean @@ -13,16 +13,16 @@ import Linglib.Semantics.Mood.POSWQ @cite{roberts-2023} @cite{roberts-2012} @cite{lewis-1979} @cite{portner-2004} The scoreboard K for a language game at time t is a tuple -⟨I, M, ≺, CG, QUD, G⟩ (@cite{roberts-2023}), tracking: +⟨I, M, ≺, CommonGround, QUD, G⟩ (@cite{roberts-2023}), tracking: - **I**: the set of interlocutors - **M**: illocutionary moves made so far (with subsets A, Q, D, Acc) - **≺**: temporal order on moves -- **CG**: the common ground (propositions treated as mutually believed) +- **CommonGround**: the common ground (propositions treated as mutually believed) - **QUD**: the ordered set of questions under discussion - **G**: the interlocutors' publicly evident goals, plans, and priorities -The three central elements — CG, QUD, G — are updated by assertion, +The three central elements — CommonGround, QUD, G — are updated by assertion, interrogation, and direction respectively, via the Illocutionary Force Linking Principle (@cite{roberts-2023}). @@ -135,7 +135,7 @@ theorem iflp_roundtrip_imp : /-! ## The Scoreboard -/ -/-- The scoreboard K = ⟨I, M, ≺, CG, QUD, G⟩. The temporal order ≺ +/-- The scoreboard K = ⟨I, M, ≺, CommonGround, QUD, G⟩. The temporal order ≺ is implicit in list position of `moves`. `qud` is specialised to polar-question content (`W → Prop`); the richer `Discourse.QUDStack` over `Semantics.Questions.Basic.Question W` is consumed by other @@ -150,7 +150,7 @@ structure Scoreboard (W : Type*) where namespace Scoreboard -/-- The context set: worlds compatible with all CG propositions. -/ +/-- The context set: worlds compatible with all CommonGround propositions. -/ def contextSet (K : Scoreboard W) : W → Prop := λ w => ∀ p ∈ K.cg, p w @@ -158,7 +158,7 @@ def contextSet (K : Scoreboard W) : W → Prop := def agentGoals (K : Scoreboard W) (i : Nat) : GoalSet W := K.goals.getD i GoalSet.empty -/-- Assertion update: accepted assertion of `p` adds `p` to CG. -/ +/-- Assertion update: accepted assertion of `p` adds `p` to CommonGround. -/ def assertionUpdate (K : Scoreboard W) (p : W → Prop) (agent : Nat) : Scoreboard W := { K with cg := p :: K.cg @@ -196,7 +196,7 @@ def directionUpdate (K : Scoreboard W) (p : W → Prop) goals := addGoalAt K.goals target 0 newGoal moves := ⟨.imperative, p, speaker, True⟩ :: K.moves } -/-- Assertion update adds to CG. -/ +/-- Assertion update adds to CommonGround. -/ @[simp] theorem assertion_adds_to_cg (K : Scoreboard W) (p : W → Prop) (a : Nat) : (K.assertionUpdate p a).cg = p :: K.cg := rfl @@ -212,7 +212,7 @@ def directionUpdate (K : Scoreboard W) (p : W → Prop) @[simp] theorem interrogation_adds_to_qud (K : Scoreboard W) (q : W → Prop) (a : Nat) : (K.interrogationUpdate q a).qud = q :: K.qud := rfl -/-- Interrogation update preserves CG. -/ +/-- Interrogation update preserves CommonGround. -/ @[simp] theorem interrogation_preserves_cg (K : Scoreboard W) (q : W → Prop) (a : Nat) : (K.interrogationUpdate q a).cg = K.cg := rfl @@ -220,7 +220,7 @@ def directionUpdate (K : Scoreboard W) (p : W → Prop) @[simp] theorem interrogation_preserves_goals (K : Scoreboard W) (q : W → Prop) (a : Nat) : (K.interrogationUpdate q a).goals = K.goals := rfl -/-- Direction update preserves CG. -/ +/-- Direction update preserves CommonGround. -/ @[simp] theorem direction_preserves_cg (K : Scoreboard W) (p : W → Prop) (s t pr : Nat) : (K.directionUpdate p s t pr).cg = K.cg := rfl @@ -230,8 +230,8 @@ def directionUpdate (K : Scoreboard W) (p : W → Prop) /-! ### POSW substrate bridge -The scoreboard's CG and G components project jointly into a -`Semantics.Mood.POSW`: CG via `contextSet`, G via the goal-induced +The scoreboard's CommonGround and G components project jointly into a +`Semantics.Mood.POSW`: CommonGround via `contextSet`, G via the goal-induced preference ordering. Assertion ↔ `plus`, direction ↔ `star`. -/ /-- Flat list of goal contents across all agents. -/ @@ -282,7 +282,7 @@ lemma mem_directionUpdate_goalContents (K : Scoreboard W) (p : W → Prop) exact mem_addGoalAt_flatMap K.goals t 0 ⟨p, fun _ => True, pr⟩ (Nat.zero_le _) (by simpa using hin) q -/-- Project the scoreboard into a POSW: `cs` from CG, `le` from +/-- Project the scoreboard into a POSW: `cs` from CommonGround, `le` from goal-induced preference. -/ def toPOSW (K : Scoreboard W) : Semantics.Mood.POSW W where cs := K.contextSet diff --git a/Linglib/Discourse/SpeechAct/Update.lean b/Linglib/Discourse/SpeechAct/Update.lean index 98eedb7ad..d0b33a85d 100644 --- a/Linglib/Discourse/SpeechAct/Update.lean +++ b/Linglib/Discourse/SpeechAct/Update.lean @@ -29,7 +29,7 @@ Instances live with the framework types (e.g. `Dialogue/Stalnaker.lean`, namespace Discourse.SpeechAct -open Discourse.CommonGround (HasContextSet) +open CommonGround (HasContextSet) /-- A dialogue-state type that admits a Stalnakerian one-step assertion: `speakerAssert s φ` is monotone (never adds worlds) diff --git a/Linglib/Features/Topic.lean b/Linglib/Features/Topic.lean index 6030437cd..fa3445fc8 100644 --- a/Linglib/Features/Topic.lean +++ b/Linglib/Features/Topic.lean @@ -15,9 +15,9 @@ follows Krifka in treating topic as a primitive notion, defined per > The topic constituent identifies the entity or set of entities > under which the information expressed in the comment constituent -> should be stored in the CG content. +> should be stored in the CommonGround content. -Following @cite{reinhart-1981}'s file-card metaphor: the CG is +Following @cite{reinhart-1981}'s file-card metaphor: the CommonGround is organized like a subject-oriented library catalogue indexed by topics; each new proposition is filed under the topic it is about. @@ -62,7 +62,7 @@ set_option autoImplicit false namespace Features /-- @cite{reinhart-1981} aboutness topic: whether a constituent is - the entity under which the proposition is filed in the CG. + the entity under which the proposition is filed in the CommonGround. Binary by design — degree-of-topicality theories belong in their own files. -/ inductive TopicMark where diff --git a/Linglib/Fragments/Mandarin/Predicates.lean b/Linglib/Fragments/Mandarin/Predicates.lean index dc28dd0db..8af4de32c 100644 --- a/Linglib/Fragments/Mandarin/Predicates.lean +++ b/Linglib/Fragments/Mandarin/Predicates.lean @@ -69,7 +69,7 @@ formalized as `Semantics.Dynamic.Postsupposition.weakContrafactive`, and exercis /-- 以为 "yǐwéi" — be under the impression that (weak contrafactive). -Has postsupposition ◇¬p (CG compatible with ¬p after utterance). +Has postsupposition ◇¬p (CommonGround compatible with ¬p after utterance). This cannot be derived from veridicality; see @cite{glass-2025} and @cite{glass-2023}. The postsupposition is recorded structurally via `postsupType` and exercised in `Glass2025`. diff --git a/Linglib/Fragments/Marathi/Particles.lean b/Linglib/Fragments/Marathi/Particles.lean index 15d2eaec4..bcafa7e40 100644 --- a/Linglib/Fragments/Marathi/Particles.lean +++ b/Linglib/Fragments/Marathi/Particles.lean @@ -52,7 +52,7 @@ def bara : ParticleEntry where carriesPreferentialCommitment := True /-- *na* — utterance-final particle analyzed in @cite{deo-2023} as - signalling preference for *independent* shared commitment (CG + signalling preference for *independent* shared commitment (CommonGround update; doxastic sourcehood mirror of `bərə`'s dependent-uptake convention). @@ -64,7 +64,7 @@ def bara : ParticleEntry where declarative/interrogative pattern is unverified pending the @cite{deo-2023} formalization. `carriesPreferentialCommitment := false` reflects @cite{deo-2023}'s - framing as a *doxastic* (CG-update) particle, not preferential. -/ + framing as a *doxastic* (CommonGround-update) particle, not preferential. -/ def na : ParticleEntry where form := "na" gloss := "NA" diff --git a/Linglib/Phenomena/Assertion/Compare.lean b/Linglib/Phenomena/Assertion/Compare.lean index abb182751..c8d998e10 100644 --- a/Linglib/Phenomena/Assertion/Compare.lean +++ b/Linglib/Phenomena/Assertion/Compare.lean @@ -113,7 +113,7 @@ missing — without it, the typeclass's cross-framework theorems `speakerAssert_twice_subset_prior`) were dead code. -/ open Discourse.SpeechAct (Assertable) -open Discourse.CommonGround (HasContextSet) +open CommonGround (HasContextSet) /-- **Polymorphic assertion-narrowing**: any `Assertable` framework narrows the context set by the asserted proposition. The diff --git a/Linglib/Phenomena/Dialogue/Basic.lean b/Linglib/Phenomena/Dialogue/Basic.lean index 7e120c04a..fb0be8c09 100644 --- a/Linglib/Phenomena/Dialogue/Basic.lean +++ b/Linglib/Phenomena/Dialogue/Basic.lean @@ -11,7 +11,7 @@ or information-structural. 1. **Common ground development**: shared beliefs become more specific 2. **Belief convergence**: participants learn from each other 3. **Cooperative contributions**: speakers are informative and non-redundant -4. **Contradiction resistance**: CG resists contradictory updates +4. **Contradiction resistance**: CommonGround resists contradictory updates -/ namespace Phenomena.Dialogue diff --git a/Linglib/Phenomena/Verum/Basic.lean b/Linglib/Phenomena/Verum/Basic.lean index f3942e7b6..2bd87c192 100644 --- a/Linglib/Phenomena/Verum/Basic.lean +++ b/Linglib/Phenomena/Verum/Basic.lean @@ -54,7 +54,7 @@ following felicity profile: Saraguro Kichwa — a reportative-evidential antecedent). Theories disagree on the *mechanism* (focus over polarity, VERUM -operator over CG membership, focus + discourse-management); they agree +operator over CommonGround membership, focus + discourse-management); they agree on the *licensing profile*. This file documents the agreement via the shared `VerumOperator` abstraction; the disagreement lives in the `Studies/` files as different `VerumOperator`-instantiating predicates. diff --git a/Linglib/Pragmatics/Expressives/Basic.lean b/Linglib/Pragmatics/Expressives/Basic.lean index f89386b66..dbb3215bc 100644 --- a/Linglib/Pragmatics/Expressives/Basic.lean +++ b/Linglib/Pragmatics/Expressives/Basic.lean @@ -423,11 +423,11 @@ theorem ciStrongerThan_asymm {W : Type*} (φ ψ : TwoDimProp W) presuppositional meaning into two dimensions using @cite{potts-2005}'s CI type system: - **At-issue**: the assertion component (identity function on the propositional content) -- **CI**: the presupposition (projects to root, evaluated against CG) +- **CI**: the presupposition (projects to root, evaluated against CommonGround) This derives de re readings: when a presuppositional expression appears under an attitude verb, the presupposition can be evaluated against the common ground -(CG) rather than the attitude holder's beliefs, because it projects as CI content. +(CommonGround) rather than the attitude holder's beliefs, because it projects as CI content. ### Bridge: PrProp ↔ TwoDimProp @@ -463,8 +463,8 @@ theorem ciLift_ci {W : Type*} (presup assertion : W → Prop) : (ciLift presup assertion).ci = presup := rfl /-- -De re reading: when CG entails the presupposition, the CI dimension is satisfied -at all CG worlds. This means the presupposition is resolved against the CG +De re reading: when CommonGround entails the presupposition, the CI dimension is satisfied +at all CommonGround worlds. This means the presupposition is resolved against the CommonGround regardless of what is embedded under an attitude verb. -/ theorem deRe_from_ciLift {W : Type*} (presup : W → Prop) diff --git a/Linglib/Pragmatics/RSA/Incremental.lean b/Linglib/Pragmatics/RSA/Incremental.lean index e31d5ad16..896cfcdd9 100644 --- a/Linglib/Pragmatics/RSA/Incremental.lean +++ b/Linglib/Pragmatics/RSA/Incremental.lean @@ -15,7 +15,7 @@ extension-based incremental semantics ⟦pfx⟧(r), the chain-rule speaker, the literal-listener categorical L0^UTT, and the full `RSAConfig` — is *derived* rather than re-stipulated per study. -This consolidates what was previously triplicated across CG's Figure 1 +This consolidates what was previously triplicated across CommonGround's Figure 1 scene, the @cite{sedivy-2007} reference-game scene, and the @cite{rubio-fernandez-2016} display: each becomes a single `IncrementalSemantics` value, with `toRSAConfig` producing the model. diff --git a/Linglib/Semantics/Attitudes/Doxastic.lean b/Linglib/Semantics/Attitudes/Doxastic.lean index 818814b89..d4a6be31c 100644 --- a/Linglib/Semantics/Attitudes/Doxastic.lean +++ b/Linglib/Semantics/Attitudes/Doxastic.lean @@ -106,10 +106,10 @@ instance diaAt_decidable {W E : Type*} (R : AccessRel W E) [∀ a w w', Decidabl @cite{glass-2025} proposes a typology of belief verbs based on their presuppositional profile — what they require of the Common Ground: -- **Factive** (know): presupposes p — CG must entail p -- **Nonfactive** (think): no presupposition — no CG requirement +- **Factive** (know): presupposes p — CommonGround must entail p +- **Nonfactive** (think): no presupposition — no CommonGround requirement - **Contrafactive** (hypothetical *contra*): would presuppose ¬p — UNATTESTED -- **Weak contrafactive** (Mandarin yǐwéi): postsupposition ◇¬p — CG compatible with ¬p +- **Weak contrafactive** (Mandarin yǐwéi): postsupposition ◇¬p — CommonGround compatible with ¬p The key insight: this classification is DERIVED from the `PrProp` produced by `DoxasticPredicate.toPrProp`, not stipulated as a separate type. The presup @@ -126,9 +126,9 @@ This emerges from the presup field of the `PrProp` produced by `DoxasticPredicate.toPrProp`. Not a primitive — a derived label. -/ inductive PresupClass where - | factive -- presup = p (know: CG must entail p) - | contrafactive -- presup = ¬p (hypothetical *contra*: CG must entail ¬p — UNATTESTED) - | nonfactive -- presup = true (believe/think: no CG requirement) + | factive -- presup = p (know: CommonGround must entail p) + | contrafactive -- presup = ¬p (hypothetical *contra*: CommonGround must entail ¬p — UNATTESTED) + | nonfactive -- presup = true (believe/think: no CommonGround requirement) | other -- none of the above deriving DecidableEq, Repr @@ -356,10 +356,10 @@ their projective content is fundamentally different: is a postsupposition (about output context) not presupposition (input). Postsuppositions are formalized in `Semantics.Dynamic.Postsupposition`. -2. **Different requirement**: yǐwéi requires CG ◇ ¬p (CG compatible with ¬p), - not CG ⊨ ¬p (CG entails ¬p) +2. **Different requirement**: yǐwéi requires CommonGround ◇ ¬p (CommonGround compatible with ¬p), + not CommonGround ⊨ ¬p (CommonGround entails ¬p) -3. **No causal incoherence**: "p is unsettled in CG" is compatible with +3. **No causal incoherence**: "p is unsettled in CommonGround" is compatible with "there's evidence for p that x acquired" — these are about different epistemic states (communal knowledge vs individual belief) diff --git a/Linglib/Semantics/Attitudes/Parasitic.lean b/Linglib/Semantics/Attitudes/Parasitic.lean index c49500de6..bc44d700b 100644 --- a/Linglib/Semantics/Attitudes/Parasitic.lean +++ b/Linglib/Semantics/Attitudes/Parasitic.lean @@ -291,7 +291,7 @@ theorem parasitic_uses_belief_local_context {W E : Type*} presupAttributedToHolder blc p ↔ ∀ w_star, globalCtx w_star → ∀ w', dox agent w_star w' → p.presup w' := by simp only [toBeliefLocalCtx, presupAttributedToHolder, BeliefLocalCtx.atWorld, - Discourse.CommonGround.ContextSet.entails] + CommonGround.ContextSet.entails] constructor · intro h w_star hw_star w' hdox exact h w_star hw_star (And.intro hw_star hdox) diff --git a/Linglib/Semantics/Comparison/Metalinguistic.lean b/Linglib/Semantics/Comparison/Metalinguistic.lean index b23adac5c..c3a1741e3 100644 --- a/Linglib/Semantics/Comparison/Metalinguistic.lean +++ b/Linglib/Semantics/Comparison/Metalinguistic.lean @@ -493,9 +493,9 @@ def evalMCond {I W Pred Entity : Type} [Fintype I] -- § 6. Connection to Common Ground -- ════════════════════════════════════════════════════════════════ -open Discourse.CommonGround (ContextSet HasContextSet) +open CommonGround (ContextSet HasContextSet) -/-- An ordering-world pair: the enriched index for metalinguistic CG. +/-- An ordering-world pair: the enriched index for metalinguistic CommonGround. The common ground is a set of ordering-world pairs ⟨≤, w⟩ compatible with speakers' factual AND interpretive commitments. -/ @@ -516,7 +516,7 @@ variable {I W : Type} /-- Project to a classical context set by existentially quantifying over semantic orderings. A world w is in the context set iff some -ordering paired with w is in the metalinguistic CG. -/ +ordering paired with w is in the metalinguistic CommonGround. -/ def toContextSet (cg : MetalinguisticCG I W) : ContextSet W := λ w => ∃ ord, cg ⟨ord, w⟩ diff --git a/Linglib/Semantics/Composition/Glue.lean b/Linglib/Semantics/Composition/Glue.lean index 421398eae..3fecb9e82 100644 --- a/Linglib/Semantics/Composition/Glue.lean +++ b/Linglib/Semantics/Composition/Glue.lean @@ -537,7 +537,7 @@ def ResourceCondition.fromNoContraction : List ResourceCondition := 1. **Interpretive** (H&K/QR): Syntax produces LF, which is directly interpreted. Scope ambiguity requires a syntactic operation (QR/covert movement) — two distinct LF trees. - 2. **Parallel** (CG/CCG): Syntax and semantics computed in + 2. **Parallel** (CommonGround/CCG): Syntax and semantics computed in lockstep. Scope ambiguity requires type-shifting operations and corresponding categorial modifications. 3. **Glue** (separable logic): Syntax produces meaning @@ -550,14 +550,14 @@ def ResourceCondition.fromNoContraction : List ResourceCondition := inductive CompositionApproach where | interpretive -- H&K: syntax → LF → interpretation - | parallel -- CG/CCG: syntax ∥ semantics + | parallel -- CommonGround/CCG: syntax ∥ semantics | glueSeparable -- Glue: syntax → premises → proof search deriving DecidableEq, Repr /-- How each approach handles scope ambiguity. -/ inductive ScopeAmbiguityMechanism where | covertMovement -- QR: syntactic operation producing distinct LFs - | typeShifting -- CG/CCG: type-raising / scope-shifting + | typeShifting -- CommonGround/CCG: type-raising / scope-shifting | proofSearch -- Glue: multiple ∀-instantiations → multiple proofs deriving DecidableEq, Repr diff --git a/Linglib/Semantics/Conditionals/Stalnaker.lean b/Linglib/Semantics/Conditionals/Stalnaker.lean index 06ade4ae3..ee0104c21 100644 --- a/Linglib/Semantics/Conditionals/Stalnaker.lean +++ b/Linglib/Semantics/Conditionals/Stalnaker.lean @@ -57,7 +57,7 @@ equivalence within an appropriate context (the namespace Semantics.Conditionals -open Discourse.CommonGround (ContextSet) +open CommonGround (ContextSet) open Semantics.Mood (GramMood) open _root_.Semantics.Conditionals (SelectionFunction selectionPrefers) open Core.Order (SimilarityOrdering) diff --git a/Linglib/Semantics/Dynamic/Effects/Probability.lean b/Linglib/Semantics/Dynamic/Effects/Probability.lean index 1a5607037..1e77ad53f 100644 --- a/Linglib/Semantics/Dynamic/Effects/Probability.lean +++ b/Linglib/Semantics/Dynamic/Effects/Probability.lean @@ -171,7 +171,7 @@ observe : Bool → P Unit observe true continues; observe false blocks ``` -This is the mechanism for assertion: update the CG by observing the asserted +This is the mechanism for assertion: update the CommonGround by observing the asserted proposition is true. -/ diff --git a/Linglib/Semantics/Dynamic/Postsupposition.lean b/Linglib/Semantics/Dynamic/Postsupposition.lean index e4ccd02f3..5c0ff84e8 100644 --- a/Linglib/Semantics/Dynamic/Postsupposition.lean +++ b/Linglib/Semantics/Dynamic/Postsupposition.lean @@ -9,7 +9,7 @@ utterance updates it, as opposed to presuppositions which constrain the *input* context. @cite{glass-2025} argues that Mandarin yǐwéi has a postsupposition -◇¬p — after accepting "x yǐwéi p", the CG must be compatible with ¬p. +◇¬p — after accepting "x yǐwéi p", the CommonGround must be compatible with ¬p. This is distinct from a presupposition (input-context condition) and cannot be derived from veridicality alone. -/ @@ -59,7 +59,7 @@ theorem none_always_satisfied (cs : List W) (p : W → Bool) : none.satisfied cs p = true := rfl /-- Strong contrafactivity entails weak contrafactivity (for nonempty contexts): - if CG ⊨ ¬p (all worlds have ¬p), then CG ◇ ¬p (some world has ¬p). + if CommonGround ⊨ ¬p (all worlds have ¬p), then CommonGround ◇ ¬p (some world has ¬p). This captures @cite{glass-2025}'s key observation that yǐwéi's requirement is strictly weaker than the hypothetical *contra* verb's. -/ theorem strong_entails_weak (cs : List W) (p : W → Bool) (hne : cs ≠ []) : diff --git a/Linglib/Semantics/Lexical/VerbEntry.lean b/Linglib/Semantics/Lexical/VerbEntry.lean index e6ce5c7e1..079593024 100644 --- a/Linglib/Semantics/Lexical/VerbEntry.lean +++ b/Linglib/Semantics/Lexical/VerbEntry.lean @@ -112,7 +112,7 @@ def PresupTriggerType.isSoft : PresupTriggerType → Bool Postsupposition type: output-context constraint distinct from presuppositions. @cite{glass-2025} argues that Mandarin yǐwéi has a postsupposition ◇¬p — -after accepting "x yǐwéi p", the CG must be compatible with ¬p. +after accepting "x yǐwéi p", the CommonGround must be compatible with ¬p. This cannot be derived from veridicality alone. The concrete `Semantics.Dynamic.Postsupposition.Postsupposition W` is parameterized diff --git a/Linglib/Semantics/Modality/BiasedPQ.lean b/Linglib/Semantics/Modality/BiasedPQ.lean index 04a85db45..6c776f416 100644 --- a/Linglib/Semantics/Modality/BiasedPQ.lean +++ b/Linglib/Semantics/Modality/BiasedPQ.lean @@ -37,7 +37,7 @@ for Czech. namespace Semantics.Modality.BiasedPQ open Semantics.Modality.Kratzer -open Discourse.CommonGround +open CommonGround variable {W : Type*} @@ -161,34 +161,34 @@ theorem hiNQ_evidence_neutral_ok : /-- VERUM operator (@cite{romero-han-2004}, line b). -⟦VERUM_x⟧ = λp. λw. ∀w' ∈ Epi_x(w). ∀w'' ∈ Conv_x(w'). [p ∈ CG] +⟦VERUM_x⟧ = λp. λw. ∀w' ∈ Epi_x(w). ∀w'' ∈ Conv_x(w'). [p ∈ CommonGround] "x is sure that p should be added to the Common Ground." We model this as: in all epistemically accessible worlds where the speaker's -conversational goals are fulfilled, p is in the CG. This is a double universal: +conversational goals are fulfilled, p is in the CommonGround. This is a double universal: necessity over epistemic alternatives, then necessity over conversational goals. -/ def verum (epistemic : ModalBase W) (conversational : OrderingSource W) (cg p : Set W) (w : W) : Prop := - -- For all best epistemic worlds w': in the CG induced at w', p holds + -- For all best epistemic worlds w': in the CommonGround induced at w', p holds ∀ w' ∈ bestWorlds epistemic conversational w, cg w' ∧ p w' /-- FALSUM operator (@cite{repp-2013}, @cite{romero-2019}, @cite{romero-2024} def. 33). At-issue content: ¬p -CG-management content: ∀w' ∈ Epi(w). ∀w'' ∈ Conv(w'). [p ∉ CG] +CommonGround-management content: ∀w' ∈ Epi(w). ∀w'' ∈ Conv(w'). [p ∉ CommonGround] "x is sure that p should NOT be added to the Common Ground." -FALSUM is the CG-management negation of VERUM. The at-issue content -is simply ¬p, while the non-at-issue content (CG-management) expresses +FALSUM is the CommonGround-management negation of VERUM. The at-issue content +is simply ¬p, while the non-at-issue content (CommonGround-management) expresses that p is not to become common ground. -/ structure FalsumContent (W : Type*) where /-- At-issue content: ¬p -/ atIssue : Set W - /-- CG-management: p should not be added to CG. + /-- CommonGround-management: p should not be added to CommonGround. Modeled as: the speaker considers it epistemically possible that p, - but p is not CG-entailed. -/ + but p is not CommonGround-entailed. -/ cgManagement : Set W /-- Construct FALSUM content for a proposition p. -/ @@ -198,7 +198,7 @@ def mkFalsum (epistemic : ModalBase W) (conversational : OrderingSource W) cgManagement := fun w => -- Speaker considers p epistemically possible (∃ w' ∈ bestWorlds epistemic conversational w, p w') ∧ - -- But p is not entailed by the CG + -- But p is not entailed by the CommonGround ¬(∀ w', cg w' → p w') /-- FALSUM's at-issue content is propositional negation. -/ @@ -232,7 +232,7 @@ structure FalsumCZ (W : Type*) where This is the definedness condition — the question is defined only if the attitude holder considers the positive prejacent possible. -/ definedness : Set W - /-- CG-management: p is not part of the common ground at w. -/ + /-- CommonGround-management: p is not part of the common ground at w. -/ cgContent : Set W /-- Construct @cite{simik-2024}'s FALSUM^CZ for a proposition p. @@ -375,9 +375,9 @@ theorem inner_entails_medial (f : EvidentialBiasFlavor W) (p : Set W) (w : W) /-! Outer negation (FALSUM) is obligatorily focused (Staňková 2026 §3.2, §4). -FALSUM targets discourse polarity — whether p *is* or *is not* in the CG. +FALSUM targets discourse polarity — whether p *is* or *is not* in the CommonGround. Focus on FALSUM generates Rooth alternatives on polarity. The focus -semantic value of FALSUM is `{λw[p ∉ CG], λw[p ∈ CG]}`, computed by +semantic value of FALSUM is `{λw[p ∉ CommonGround], λw[p ∈ CommonGround]}`, computed by `falsumAlternatives` below. -/ /-- FALSUM generates exactly two alternatives (polarity contrast). -/ diff --git a/Linglib/Semantics/Modality/EpistemicLogic.lean b/Linglib/Semantics/Modality/EpistemicLogic.lean index cb3b46363..d55308aab 100644 --- a/Linglib/Semantics/Modality/EpistemicLogic.lean +++ b/Linglib/Semantics/Modality/EpistemicLogic.lean @@ -11,7 +11,7 @@ Multi-agent epistemic operators from @cite{halpern-2003}: individual knowledge (Kᵢ), everyone knows (E_G), common knowledge (C_G), distributed knowledge (D_G), and their doxastic (KD45 belief) counterparts. -Connects to Stalnaker's common ground via `CG.groundedIn`: a common +Connects to Stalnaker's common ground via `CommonGround.groundedIn`: a common ground is grounded when its context set equals what is commonly known. ## Operators @@ -28,7 +28,7 @@ ground is grounded when its context set equals what is commonly known. This file lives in `Semantics/Modality/` because it makes substantive theoretical commitments (S5 for knowledge, KD45 for belief, fixed-point characterization of common knowledge). The framework-agnostic -context management (`ContextSet`, `CG`) lives in +context management (`ContextSet`, `CommonGround`) lives in `Discourse/CommonGround.lean`. Following mathlib style, all operators are `Prop`-valued; computation @@ -40,7 +40,6 @@ namespace Semantics.Modality.EpistemicLogic open Core.Logic.Intensional (AccessRel AgentAccessRel boxR diamondR IsSerial IsEuclidean IsBeliefRefinementOf boxR_T boxR_D boxR_four boxR_B boxR_five) -open Discourse.CommonGround (CG) /-! ## Individual Knowledge @@ -245,8 +244,8 @@ are common knowledge among the discourse participants. -/ /-- A common ground is grounded in common knowledge when its context set equals the intersection of what is commonly known. -/ -def _root_.Discourse.CommonGround.CG.groundedIn {W E : Type*} - (cg : CG W) (Rs : AgentAccessRel W E) (group : List E) +def _root_.CommonGround.groundedIn {W E : Type*} + (cg : CommonGround W) (Rs : AgentAccessRel W E) (group : List E) (bound : ℕ) : Prop := ∀ w, cg.contextSet w ↔ ∀ p ∈ cg.propositions, commonKnowledge Rs group p bound w diff --git a/Linglib/Semantics/Modality/Kernel.lean b/Linglib/Semantics/Modality/Kernel.lean index 2abcf08f2..6da687403 100644 --- a/Linglib/Semantics/Modality/Kernel.lean +++ b/Linglib/Semantics/Modality/Kernel.lean @@ -923,7 +923,7 @@ The felicity condition has three parts: (i) evidence in K supports the prejacent settled in K. Condition (iii) is the same presupposition as `kernelMust`. -/ /-- Prior information state (beliefs, norms, desires) before encountering -evidence. Distinct from the kernel (direct evidence) and the CG (shared). -/ +evidence. Distinct from the kernel (direct evidence) and the CommonGround (shared). -/ abbrev Background (W : Type*) := List ((W → Prop)) /-- B_U = ⋂U: worlds compatible with the prior information state. -/ diff --git a/Linglib/Semantics/Presupposition/Accommodation.lean b/Linglib/Semantics/Presupposition/Accommodation.lean index 8c0d49f38..d2b1b2321 100644 --- a/Linglib/Semantics/Presupposition/Accommodation.lean +++ b/Linglib/Semantics/Presupposition/Accommodation.lean @@ -39,7 +39,7 @@ namespace Semantics.Presupposition.Accommodation open Classical open Semantics.Presupposition -open Discourse.CommonGround +open CommonGround open Semantics.Presupposition.Context variable {W : Type*} diff --git a/Linglib/Semantics/Presupposition/BeliefEmbedding.lean b/Linglib/Semantics/Presupposition/BeliefEmbedding.lean index 0e86ff6ed..1f8ec1e6f 100644 --- a/Linglib/Semantics/Presupposition/BeliefEmbedding.lean +++ b/Linglib/Semantics/Presupposition/BeliefEmbedding.lean @@ -51,7 +51,7 @@ import Linglib.Semantics.Modality.EpistemicLogic namespace Semantics.Presupposition.BeliefEmbedding open Semantics.Presupposition -open Discourse.CommonGround +open CommonGround open Semantics.Presupposition.Context open Semantics.Presupposition.LocalContext diff --git a/Linglib/Semantics/Presupposition/Context.lean b/Linglib/Semantics/Presupposition/Context.lean index b4a682204..b66866dc1 100644 --- a/Linglib/Semantics/Presupposition/Context.lean +++ b/Linglib/Semantics/Presupposition/Context.lean @@ -36,7 +36,7 @@ world in the context set satisfying it. namespace Semantics.Presupposition.Context open Semantics.Presupposition -open Discourse.CommonGround +open CommonGround variable {W : Type*} @@ -130,7 +130,7 @@ theorem accommodate_eq_defined (c : ContextSet W) (p : PrProp W) (w : W) : -- ════════════════════════════════════════════════════════════════ /-- Presupposition satisfied relative to any discourse state with a - context set. Works with `CG W`, `Commitment.CommitmentSlate W`, + context set. Works with `CommonGround W`, `Commitment.CommitmentSlate W`, `LocalCtx W`, and any other state implementing `HasContextSet`. -/ abbrev presupSatisfiedIn {S : Type*} [HasContextSet S W] (s : S) (p : PrProp W) : Prop := presupSatisfied (HasContextSet.toContextSet s) p diff --git a/Linglib/Semantics/Presupposition/LocalContext.lean b/Linglib/Semantics/Presupposition/LocalContext.lean index beb701b0f..a88d27cdf 100644 --- a/Linglib/Semantics/Presupposition/LocalContext.lean +++ b/Linglib/Semantics/Presupposition/LocalContext.lean @@ -39,7 +39,7 @@ import Linglib.Core.Context.Tower namespace Semantics.Presupposition.LocalContext open Semantics.Presupposition -open Discourse.CommonGround +open CommonGround open Semantics.Presupposition.Context variable {W : Type*} diff --git a/Linglib/Semantics/Presupposition/TonhauserDerivation.lean b/Linglib/Semantics/Presupposition/TonhauserDerivation.lean index f8f556a10..46b99f1d2 100644 --- a/Linglib/Semantics/Presupposition/TonhauserDerivation.lean +++ b/Linglib/Semantics/Presupposition/TonhauserDerivation.lean @@ -88,7 +88,7 @@ import Linglib.Semantics.Presupposition.BeliefEmbedding namespace Semantics.Presupposition.TonhauserDerivation open Semantics.Presupposition -open Discourse.CommonGround +open CommonGround open Semantics.Presupposition.Context open Semantics.Presupposition.LocalContext open Semantics.Presupposition.BeliefEmbedding diff --git a/Linglib/Semantics/Presupposition/TriggerTypology.lean b/Linglib/Semantics/Presupposition/TriggerTypology.lean index 732e7361f..ec30461fc 100644 --- a/Linglib/Semantics/Presupposition/TriggerTypology.lean +++ b/Linglib/Semantics/Presupposition/TriggerTypology.lean @@ -22,7 +22,7 @@ Three patterns of trigger ↔ alternative relationship: The alternative-structure axis predicts obligatoriness: - Deletion / replacement → trigger can be optional or obligatory -- No alternative → trigger is mandatorily omitted under partial CG support +- No alternative → trigger is mandatorily omitted under partial CommonGround support ## Relation to MP infrastructure @@ -138,12 +138,12 @@ Obligatoriness pattern predicted by the alternative-structure typology. @cite{wang-2025} derives three patterns from the interaction of trigger type, alternative structure, and constraint ranking: -1. Obligatory: trigger must be used when CG supports presupposition +1. Obligatory: trigger must be used when CommonGround supports presupposition 2. Optional: trigger may or may not be used 3. Blocked: trigger must NOT be used (mandatorily omitted) -/ inductive Obligatoriness where - /-- Trigger is obligatory when presupposition is fully entailed by CG -/ + /-- Trigger is obligatory when presupposition is fully entailed by CommonGround -/ | obligatory /-- Trigger is optional (either form is acceptable) -/ | optional diff --git a/Linglib/Semantics/TypeTheoretic/Discourse.lean b/Linglib/Semantics/TypeTheoretic/Discourse.lean index 1019cf6fb..b2e18d152 100644 --- a/Linglib/Semantics/TypeTheoretic/Discourse.lean +++ b/Linglib/Semantics/TypeTheoretic/Discourse.lean @@ -17,7 +17,7 @@ declarative/interrogative/imperative slice plus a backchannel constructor; true backchannels live in `Pragmatics/Dialogue/KOS/`). **Information States**: InfoState (gameboard), agenda operations, - bridge to Discourse.CommonGround (§2.6). + bridge to CommonGround (§2.6). **Parametric Content**: Parametric bg/fg, PPpty, PQuant, PQuantDet, PRel2 (§4.2–4.3). Bridge to Semantics.Presupposition.PrProp. @@ -150,17 +150,17 @@ def InfoState.pushAgenda {SignT CommT : Type} InfoState SignT CommT := { s with agenda := signType :: s.agenda } -/-! ## Bridge to Discourse.CommonGround -/ +/-! ## Bridge to CommonGround -/ -/-- Bridge: a `Set W`-based information state's commitments form a CG. -/ +/-- Bridge: a `Set W`-based information state's commitments form a CommonGround. -/ def InfoState.toCG {W SignT : Type} (s : InfoState SignT (List (Set W))) : - Discourse.CommonGround.CG W where + CommonGround W where propositions := s.commitments -/-- InfoState with `Set W` commitments projects to a context set via CG. -/ +/-- InfoState with `Set W` commitments projects to a context set via CommonGround. -/ instance {W SignT : Type} : - Discourse.CommonGround.HasContextSet + CommonGround.HasContextSet (InfoState SignT (List (Set W))) W where toContextSet s := s.toCG.contextSet @@ -168,7 +168,7 @@ instance {W SignT : Type} : theorem infoState_initial_eq_empty_cg (W SignT : Type) : (InfoState.initial (SignT := SignT) ([] : List (Set W))).toCG = - Discourse.CommonGround.CG.empty := rfl + CommonGround.empty := rfl /-- Bridge: integrating a commitment = adding to common ground. -/ theorem integrate_comm_eq_cg_add {W SignT : Type} diff --git a/Linglib/Studies/Anderson2021.lean b/Linglib/Studies/Anderson2021.lean index 40b0ad77d..827b3af57 100644 --- a/Linglib/Studies/Anderson2021.lean +++ b/Linglib/Studies/Anderson2021.lean @@ -13,30 +13,30 @@ import Linglib.Dialogue.DistributionalCG A system for multi-turn conversation update in the Rational Speech Acts framework. The core contributions: -1. **Common ground as distribution**: the CG is a probability distribution +1. **Common ground as distribution**: the CommonGround is a probability distribution over worlds, substituted directly for the RSA world prior -2. **Learning-rate update**: CG evolves via convex combination with +2. **Learning-rate update**: CommonGround evolves via convex combination with Pragmatic Listener posteriors -3. **Shared vs. approximate CG**: two models differing in whether - participants share a single CG representation +3. **Shared vs. approximate CommonGround**: two models differing in whether + participants share a single CommonGround representation 4. **Observation sampling**: weighted, thresholded, and difference-based strategies for cooperative speaker behavior ## Key Connections -The CG update rule `CG'(w) = (1-lr)·CG(w) + lr·post(w)` is algebraically +The CommonGround update rule `CommonGround'(w) = (1-lr)·CommonGround(w) + lr·post(w)` is algebraically identical to @cite{luce-1959}'s linear learning rule with retention rate `1-lr` and reinforcement target `post`. This connects RSA pragmatics to learning theory: multi-turn conversation IS iterated learning over distributions. -The distributional CG refines @cite{stalnaker-2002}'s classical context set: +The distributional CommonGround refines @cite{stalnaker-2002}'s classical context set: worlds with zero weight are excluded from the context, recovering set-intersection update as a special case. ## BToM Connection -Anderson's distributional CG has the type expected by `BToMModel.sharedUpdate` +Anderson's distributional CommonGround has the type expected by `BToMModel.sharedUpdate` (`Shared → Action → World → Shared`). Setting `Shared := DistributionalCG W` instantiates BToM's discourse dynamics for the first time in linglib — the shared state is a distribution that evolves after each utterance via the @@ -51,7 +51,7 @@ utterances describe those features. namespace Anderson2021 -open Discourse.CommonGround (ContextSet) +open CommonGround (ContextSet) -- ════════════════════════════════════════════════════ -- § 1. MutualFriends Domain @@ -132,15 +132,15 @@ theorem studyHumanity_partition : open Dialogue (DistributionalCG) -- ════════════════════════════════════════════════════ --- § 3. CG Update +-- § 3. CommonGround Update -- ════════════════════════════════════════════════════ /-- Convex combination update for distributional common ground: - CG'(w) = (1 - lr) · CG(w) + lr · posterior(w) + CommonGround'(w) = (1 - lr) · CommonGround(w) + lr · posterior(w) The learning rate `lr ∈ [0,1]` controls how much weight is given to new -information vs. the existing CG. -/ +information vs. the existing CommonGround. -/ noncomputable def updateCG {W : Type*} (cg : DistributionalCG W) (posterior : W → ℝ) (post_nonneg : ∀ w, 0 ≤ posterior w) (lr : ℝ) (hlr : 0 ≤ lr) (hlr1 : lr ≤ 1) : @@ -150,19 +150,19 @@ noncomputable def updateCG {W : Type*} (cg : DistributionalCG W) (mul_nonneg (by linarith) (cg.weight_nonneg w)) (mul_nonneg hlr (post_nonneg w)) -/-- The CG update formula is a convex combination — definitionally equal -to `(1 - lr) · CG(w) + lr · posterior(w)`. -/ +/-- The CommonGround update formula is a convex combination — definitionally equal +to `(1 - lr) · CommonGround(w) + lr · posterior(w)`. -/ theorem updateCG_eq {W : Type*} (cg : DistributionalCG W) (posterior : W → ℝ) (hn : ∀ w, 0 ≤ posterior w) (lr : ℝ) (h0 : 0 ≤ lr) (h1 : lr ≤ 1) (w : W) : (updateCG cg posterior hn lr h0 h1).weight w = (1 - lr) * cg.weight w + lr * posterior w := rfl -/-- **Bridge to @cite{luce-1959} linear learning**: the CG update has the same +/-- **Bridge to @cite{luce-1959} linear learning**: the CommonGround update has the same algebraic form as `LinearLearner.update` with retention rate `1 - lr` and reinforcement target `posterior`: - CG'(w) = (1 - lr) · CG(w) + lr · posterior(w) [Anderson] + CommonGround'(w) = (1 - lr) · CommonGround(w) + lr · posterior(w) [Anderson] v'(a) = α · v(a) + (1 - α) · r(a) [Luce §4.C] Setting `α = 1 - lr` and `r = posterior` makes the formulas identical. @@ -175,7 +175,7 @@ theorem updateCG_matches_linear_learning {W : Type*} ((1 - lr) * cg.weight w + (1 - (1 - lr)) * posterior w : ℝ) := by simp only [updateCG_eq]; ring -/-- With learning rate 0, the CG is unchanged (full retention). -/ +/-- With learning rate 0, the CommonGround is unchanged (full retention). -/ theorem updateCG_lr_zero {W : Type*} (cg : DistributionalCG W) (posterior : W → ℝ) (hn : ∀ w, 0 ≤ posterior w) (w : W) : (updateCG cg posterior hn 0 (le_refl 0) zero_le_one).weight w = @@ -183,7 +183,7 @@ theorem updateCG_lr_zero {W : Type*} (cg : DistributionalCG W) show ((1 - (0 : ℝ)) * cg.weight w + (0 : ℝ) * posterior w : ℝ) = cg.weight w ring -/-- With learning rate 1, the CG is replaced by the posterior. -/ +/-- With learning rate 1, the CommonGround is replaced by the posterior. -/ theorem updateCG_lr_one {W : Type*} (cg : DistributionalCG W) (posterior : W → ℝ) (hn : ∀ w, 0 ≤ posterior w) (w : W) : (updateCG cg posterior hn 1 zero_le_one (le_refl 1)).weight w = @@ -198,14 +198,14 @@ theorem updateCG_lr_one {W : Type*} (cg : DistributionalCG W) /-- The state of a two-participant conversation (Figure 2). Tracks the common ground (distributional), each participant's private -beliefs, and the learning rate for updates. In the **shared CG** model +beliefs, and the learning rate for updates. In the **shared CommonGround** model (§5.1, Figure 4), both participants access the same `cg`. In the -**approximate CG** model (§5.2, Figure 6), each maintains a separate +**approximate CommonGround** model (§5.2, Figure 6), each maintains a separate approximation (not yet formalized). -The distributional CG serves as both `RSAConfig.meaning` (L0 prior) and -`RSAConfig.worldPrior` (L1 prior) — the CG enters the RSA model at two -levels (Figure 4). Between turns, the CG evolves via `updateCG`, and the +The distributional CommonGround serves as both `RSAConfig.meaning` (L0 prior) and +`RSAConfig.worldPrior` (L1 prior) — the CommonGround enters the RSA model at two +levels (Figure 4). Between turns, the CommonGround evolves via `updateCG`, and the RSA model is reconstructed via `mfRSAAt`. -/ structure ConversationState (W : Type*) where cg : DistributionalCG W @@ -214,7 +214,7 @@ structure ConversationState (W : Type*) where lr : ℝ speakerIsA : Bool -/-- Initial conversation state: uniform CG, specified beliefs, A speaks first. -/ +/-- Initial conversation state: uniform CommonGround, specified beliefs, A speaks first. -/ noncomputable def ConversationState.initial {W : Type*} (belA belB : DistributionalCG W) (lr : ℝ) : ConversationState W where cg := DistributionalCG.uniform @@ -241,10 +241,10 @@ noncomputable def thresholdedSample {W : Type*} λ w => if bel.weight w ≥ θ then bel.weight w else 0 /-- **Difference-based sampling**: weight worlds by the positive difference -between the speaker's belief and the current CG. Worlds already established -in the CG get downweighted, favoring informative (non-redundant) contributions. +between the speaker's belief and the current CommonGround. Worlds already established +in the CommonGround get downweighted, favoring informative (non-redundant) contributions. - weight(w) = max(0, Bel(w) - CG(w)) + weight(w) = max(0, Bel(w) - CommonGround(w)) This implements a pressure toward Gricean Quantity: don't repeat what's already in the common ground. -/ @@ -261,9 +261,9 @@ theorem differenceSample_nonneg {W : Type*} -- § 6. BToM Shared-State Update -- ════════════════════════════════════════════════════ -/-- Anderson's CG update expressed as a BToM shared-state update. +/-- Anderson's CommonGround update expressed as a BToM shared-state update. -Given a fixed posterior-computation function (from RSA inference), the CG +Given a fixed posterior-computation function (from RSA inference), the CommonGround update has the type required by `BToMModel.sharedUpdate`: Shared → Action → World → Shared @@ -271,7 +271,7 @@ update has the type required by `BToMModel.sharedUpdate`: with `Shared := DistributionalCG W` and `Action := U`. The `World` parameter is unused: the listener doesn't know the true world, -so the CG update depends on the *posterior* (derived from the utterance), +so the CommonGround update depends on the *posterior* (derived from the utterance), not the true world directly. -/ noncomputable def toBToMSharedUpdate {W U : Type*} (posteriorFn : U → W → ℝ) @@ -309,7 +309,7 @@ theorem beliefsB_favors_katie (w : MFWorld) (hw : w ≠ .katie) : cases w <;> simp_all [beliefsB] /-- Under difference-based sampling, A initially prioritizes Nancy -(highest positive difference from uniform CG). -/ +(highest positive difference from uniform CommonGround). -/ noncomputable def aDiffFromUniform : MFWorld → ℝ := differenceSample beliefsA DistributionalCG.uniform @@ -326,16 +326,16 @@ open RSA /-- RSA model for the MutualFriends domain at turn 1. -Anderson's Shared CG model (Figure 4) uses the distributional CG at BOTH +Anderson's Shared CommonGround model (Figure 4) uses the distributional CommonGround at BOTH L0 and L1: - L0(w|u) ∝ ⟦u⟧(w) · CG(w) -- CG enters L0 via `meaning` - S1(u|w) ∝ L0(w|u) -- speaker optimizes CG-weighted informativity - L1(w|u) ∝ S1(u|w) · CG(w) -- CG enters L1 via `worldPrior` + L0(w|u) ∝ ⟦u⟧(w) · CommonGround(w) -- CommonGround enters L0 via `meaning` + S1(u|w) ∝ L0(w|u) -- speaker optimizes CommonGround-weighted informativity + L1(w|u) ∝ S1(u|w) · CommonGround(w) -- CommonGround enters L1 via `worldPrior` -At turn 1, CG is uniform (weight 1 everywhere), so the CG factor drops out +At turn 1, CommonGround is uniform (weight 1 everywhere), so the CommonGround factor drops out of L0 and the meaning reduces to Boolean semantics: `⟦u⟧(w) · 1 = ⟦u⟧(w)`. -The general CG-weighted pattern is visible in `mfRSA_turn2`. -/ +The general CommonGround-weighted pattern is visible in `mfRSA_turn2`. -/ noncomputable def mfRSA : RSAConfig MFUtterance MFWorld where meaning _ _ u w := if mfMeaning u w then 1 else 0 meaning_nonneg _ _ _ _ := by split <;> norm_num @@ -437,18 +437,18 @@ theorem l1_null_uniform (w₁ w₂ : MFWorld) : -- § 11. RSAConfig: Turn 2 (Post-Update Prior) -- ════════════════════════════════════════════════════ -/-- CG weights after hearing "studyHumanity" at turn 1. +/-- CommonGround weights after hearing "studyHumanity" at turn 1. After L1 processes "studyHumanity" with uniform prior, the posterior concentrates on nancy and sally (the German-studying worlds): L1(studyHumanity) = [0, 0, 1/2, 1/2]. Updating the normalized uniform -CG [1/4, 1/4, 1/4, 1/4] via `updateCG` with lr=0.2 (footnote 9) gives: +CommonGround [1/4, 1/4, 1/4, 1/4] via `updateCG` with lr=0.2 (footnote 9) gives: - CG'(w) = 0.8 · 1/4 + 0.2 · L1(w) - CG' = [1/5, 1/5, 3/10, 3/10] + CommonGround'(w) = 0.8 · 1/4 + 0.2 · L1(w) + CommonGround' = [1/5, 1/5, 3/10, 3/10] The weights [2, 2, 3, 3] are proportional to [1/5, 1/5, 3/10, 3/10], -which is the exact post-update CG from the paper's Figure 5, panel 1A. +which is the exact post-update CommonGround from the paper's Figure 5, panel 1A. Since RSA normalizes, proportional weights give identical predictions. -/ def cgTurn2 : MFWorld → ℝ | .ina | .katie => 2 @@ -459,14 +459,14 @@ theorem cgTurn2_nonneg : ∀ w, 0 ≤ cgTurn2 w := by /-- RSA model after hearing "studyHumanity" at turn 1. -The updated CG enters BOTH L0 and L1 (Figure 4), matching Anderson's -Shared CG model: +The updated CommonGround enters BOTH L0 and L1 (Figure 4), matching Anderson's +Shared CommonGround model: - L0(w|u) ∝ ⟦u⟧(w) · CG'(w) -- CG in L0 via `meaning` - L1(w|u) ∝ S1(u|w) · CG'(w) -- CG in L1 via `worldPrior` + L0(w|u) ∝ ⟦u⟧(w) · CommonGround'(w) -- CommonGround in L0 via `meaning` + L1(w|u) ∝ S1(u|w) · CommonGround'(w) -- CommonGround in L1 via `worldPrior` -This means S1 *adapts* to the CG: the speaker reasons about informativity -relative to the current common ground. After "studyHumanity" shifts the CG +This means S1 *adapts* to the CommonGround: the speaker reasons about informativity +relative to the current common ground. After "studyHumanity" shifts the CommonGround toward nancy/sally (weights [2,2,3,3] ∝ [1/5, 1/5, 3/10, 3/10]), utterances that disambiguate *within* that subspace (e.g., "likeOutdoors") become more informative than utterances that merely re-assert the major @@ -489,34 +489,34 @@ noncomputable def mfRSA_turn2 : RSAConfig MFUtterance MFWorld where -- § 12. Turn 2 Predictions -- ════════════════════════════════════════════════════ -/-- After CG update from "studyHumanity", L1("likeOutdoors") now favors +/-- After CommonGround update from "studyHumanity", L1("likeOutdoors") now favors Nancy over Katie. In turn 1, they were symmetric (both like outdoors). -The updated prior (3 vs 1) breaks the tie — Nancy's higher CG weight +The updated prior (3 vs 1) breaks the tie — Nancy's higher CommonGround weight makes her more probable. This is the key multi-turn prediction. -/ theorem l1_turn2_outdoors_favors_nancy : mfRSA_turn2.L1 .likeOutdoors .nancy > mfRSA_turn2.L1 .likeOutdoors .katie := by rsa_predict -/-- After CG update, "likeIndoors" favors Sally over Ina. Both like -indoors, but Sally has higher prior (3 vs 1) from the CG shift. -/ +/-- After CommonGround update, "likeIndoors" favors Sally over Ina. Both like +indoors, but Sally has higher prior (3 vs 1) from the CommonGround shift. -/ theorem l1_turn2_indoors_favors_sally : mfRSA_turn2.L1 .likeIndoors .sally > mfRSA_turn2.L1 .likeIndoors .ina := by rsa_predict -/-- After CG update, "studyScience" still treats Ina and Katie equally: +/-- After CommonGround update, "studyScience" still treats Ina and Katie equally: both study a science and both have equal prior weight (1). -/ theorem l1_turn2_science_ina_eq_katie : mfRSA_turn2.L1 .studyScience .ina = mfRSA_turn2.L1 .studyScience .katie := by rsa_predict -/-- After CG update, "studyHumanity" still treats Nancy and Sally equally: +/-- After CommonGround update, "studyHumanity" still treats Nancy and Sally equally: both study a humanity and both have equal updated prior (3). -/ theorem l1_turn2_humanity_nancy_eq_sally : mfRSA_turn2.L1 .studyHumanity .nancy = mfRSA_turn2.L1 .studyHumanity .sally := by rsa_predict -/-- CG update breaks turn-1 symmetry: in turn 1, L1("likeOutdoors") -assigned equal weight to Nancy and Katie. After the CG shift, Nancy +/-- CommonGround update breaks turn-1 symmetry: in turn 1, L1("likeOutdoors") +assigned equal weight to Nancy and Katie. After the CommonGround shift, Nancy is favored. Multi-turn conversation enriches inference. -/ theorem turn2_breaks_symmetry : mfRSA.L1 .likeOutdoors .nancy = mfRSA.L1 .likeOutdoors .katie ∧ @@ -524,40 +524,40 @@ theorem turn2_breaks_symmetry : exact ⟨by rsa_predict, l1_turn2_outdoors_favors_nancy⟩ -- ════════════════════════════════════════════════════ --- § 12b. Turn 2: S1 CG-Adapted Speaker +-- § 12b. Turn 2: S1 CommonGround-Adapted Speaker -- ════════════════════════════════════════════════════ -/-! With CG entering L0 (Figure 4), the speaker at turn 2 adapts to what's +/-! With CommonGround entering L0 (Figure 4), the speaker at turn 2 adapts to what's already in the common ground. After "studyHumanity" establishes the major -dimension, utterances that disambiguate within the high-CG subspace become -more informative. This section verifies that the CG-weighted S1 captures +dimension, utterances that disambiguate within the high-CommonGround subspace become +more informative. This section verifies that the CommonGround-weighted S1 captures Anderson's cooperative contribution mechanism. -/ -/-- **CG-adapted informativity**: At turn 2, the speaker who knows it's Nancy +/-- **CommonGround-adapted informativity**: At turn 2, the speaker who knows it's Nancy prefers "likeOutdoors" over "studyHumanity". At turn 1, these were equal -(both partition the 4-world space into 2+2). After the CG shifts toward +(both partition the 4-world space into 2+2). After the CommonGround shifts toward nancy/sally (weights [2,2,3,3]), "likeOutdoors" discriminates within the high-weight subspace (L0(nancy|likeOutdoors) = 3/5) while "studyHumanity" merely re-asserts what's already established (L0(nancy|studyHumanity) = 1/2). -This is Anderson's key insight: the CG-weighted L0 makes speakers prefer +This is Anderson's key insight: the CommonGround-weighted L0 makes speakers prefer *new* information over *redundant* information. -/ theorem s1_turn2_nancy_prefers_outdoors : mfRSA_turn2.S1 () .nancy .likeOutdoors > mfRSA_turn2.S1 () .nancy .studyHumanity := by rsa_predict -/-- At turn 1, the same two utterances were equal (pre-CG-adaptation). -/ +/-- At turn 1, the same two utterances were equal (pre-CommonGround-adaptation). -/ theorem s1_turn1_nancy_humanity_eq_outdoors : mfRSA.S1 () .nancy .studyHumanity = mfRSA.S1 () .nancy .likeOutdoors := s1_nancy_humanity_eq_outdoors -/-- CG adaptation works differently for low-CG worlds: at turn 2, +/-- CommonGround adaptation works differently for low-CommonGround worlds: at turn 2, Ina (weight 2) prefers "studyScience" over "likeIndoors" because sally (weight 3) dominates the indoor partition, making -L0(ina|likeIndoors) = 2/5 < L0(ina|studyScience) = 1/2. The CG shift -makes the major dimension MORE informative for low-CG worlds, the opposite -of the high-CG case (nancy, §12b above). -/ +L0(ina|likeIndoors) = 2/5 < L0(ina|studyScience) = 1/2. The CommonGround shift +makes the major dimension MORE informative for low-CommonGround worlds, the opposite +of the high-CommonGround case (nancy, §12b above). -/ theorem s1_turn2_ina_prefers_science : mfRSA_turn2.S1 () .ina .studyScience > mfRSA_turn2.S1 () .ina .likeIndoors := by rsa_predict @@ -583,11 +583,11 @@ theorem s2_nancy_humanity_eq_outdoors : -- § 14. Parametric RSA and Conversation Step -- ════════════════════════════════════════════════════ -/-- RSA model for MutualFriends at an arbitrary CG (Figure 4). +/-- RSA model for MutualFriends at an arbitrary CommonGround (Figure 4). -This is the general form of Anderson's Shared CG model: the CG enters +This is the general form of Anderson's Shared CommonGround model: the CommonGround enters as the L0 meaning weight (via `meaning`) AND as the L1 prior (via -`worldPrior`). One-shot RSA is the special case with uniform CG. +`worldPrior`). One-shot RSA is the special case with uniform CommonGround. Used by `conversationStep` to construct the RSA model at each turn. -/ noncomputable def mfRSAAt (cg : MFWorld → ℝ) (hcg : ∀ w, 0 ≤ cg w) : @@ -602,22 +602,22 @@ noncomputable def mfRSAAt (cg : MFWorld → ℝ) (hcg : ∀ w, 0 ≤ cg w) : worldPrior_nonneg := hcg latentPrior_nonneg _ _ := by norm_num -/-- One step of the Shared CG conversation loop (Figure 2). +/-- One step of the Shared CommonGround conversation loop (Figure 2). -Given the current CG and an utterance: -1. Build the RSA model at the current CG (`mfRSAAt`) +Given the current CommonGround and an utterance: +1. Build the RSA model at the current CommonGround (`mfRSAAt`) 2. Compute L1 posteriors: the pragmatic listener's world beliefs -3. Update the CG via convex combination with the posteriors +3. Update the CommonGround via convex combination with the posteriors -This closes the loop: RSA inference → CG update → new RSA model. -The returned CG serves as the world prior for the next turn's model. +This closes the loop: RSA inference → CommonGround update → new RSA model. +The returned CommonGround serves as the world prior for the next turn's model. **Normalization note**: The L1 posterior is normalized (sums to 1), so -the CG weights should also be normalized for the convex combination -to preserve total weight. With normalized CG, `updateCG` is a true +the CommonGround weights should also be normalized for the convex combination +to preserve total weight. With normalized CommonGround, `updateCG` is a true convex combination and preserves sum-to-1. Starting from `DistributionalCG.uniform` (weight=1 per world) gives correct RSA -predictions but produces CG updates with a different scale than the +predictions but produces CommonGround updates with a different scale than the paper's normalized distributions. -/ noncomputable def conversationStep (cg : DistributionalCG MFWorld) (u : MFUtterance) @@ -629,13 +629,13 @@ noncomputable def conversationStep fun w => rsaModel.L1agent.policy_nonneg u w updateCG cg posterior posterior_nonneg lr hlr hlr1 -/-- The conversation step preserves CG non-negativity. -/ +/-- The conversation step preserves CommonGround non-negativity. -/ theorem conversationStep_nonneg (cg : DistributionalCG MFWorld) (u : MFUtterance) (lr : ℝ) (hlr : 0 ≤ lr) (hlr1 : lr ≤ 1) (w : MFWorld) : 0 ≤ (conversationStep cg u lr hlr hlr1).weight w := (conversationStep cg u lr hlr hlr1).weight_nonneg w -/-- With lr = 0, the conversation step leaves the CG unchanged. -/ +/-- With lr = 0, the conversation step leaves the CommonGround unchanged. -/ theorem conversationStep_lr_zero (cg : DistributionalCG MFWorld) (u : MFUtterance) (w : MFWorld) : (conversationStep cg u 0 (le_refl 0) zero_le_one).weight w = cg.weight w := by simp only [conversationStep] @@ -653,8 +653,8 @@ theorem conversationStep_lr_zero (cg : DistributionalCG MFWorld) (u : MFUtteranc 2. **Uncertainty decreases**: L1 concentrates probability after hearing an informative utterance (this section). -3. **CG-adapted contributions**: At turn 2, S1 adapts to what's already - in the CG, preferring non-redundant information (§12b). -/ +3. **CommonGround-adapted contributions**: At turn 2, S1 adapts to what's already + in the CommonGround, preferring non-redundant information (§12b). -/ /-- L1 concentrates probability after an informative utterance: L1(nancy|studyHumanity) > L1(nancy|null). The null utterance gives @@ -673,16 +673,16 @@ theorem s1_informed_speaker_is_informative : s1_null_suboptimal -- ════════════════════════════════════════════════════ --- § 16. Bridge to Classical CG Update +-- § 16. Bridge to Classical CommonGround Update -- ════════════════════════════════════════════════════ -/-- Anderson's distributional CG update subsumes @cite{stalnaker-2002}'s +/-- Anderson's distributional CommonGround update subsumes @cite{stalnaker-2002}'s set-intersection update as a special case: with learning rate 1 and a posterior that assigns zero weight to worlds where the utterance is false, -the updated CG excludes exactly those worlds — recovering `ContextSet.update`. +the updated CommonGround excludes exactly those worlds — recovering `ContextSet.update`. This bridge connects the probabilistic conversation model to the classical -assertion framework in `Discourse.CommonGround`. -/ +assertion framework in `CommonGround`. -/ theorem lr_one_excludes_false_worlds (cg : DistributionalCG MFWorld) (posterior : MFWorld → ℝ) (hn : ∀ w, 0 ≤ posterior w) (w : MFWorld) (h : posterior w = 0) : @@ -696,7 +696,7 @@ theorem lr_one_excludes_false_worlds (cg : DistributionalCG MFWorld) -- ════════════════════════════════════════════════════ /-! Exact rational values for the turn-1 RSA computations underlying -Figure 5, panel 1A. At turn 1 with uniform CG, the domain's 2×2 +Figure 5, panel 1A. At turn 1 with uniform CommonGround, the domain's 2×2 feature symmetry gives clean fractions: each non-null utterance is true of exactly 2 worlds (L0 = 1/2), null is true of all 4 (L0 = 1/4), and each world makes exactly 2 non-null utterances true, giving @@ -719,7 +719,7 @@ theorem s1_nancy_likeOutdoors_val : theorem s1_nancy_null_val : mfRSA.S1 () .nancy .null = 1/5 := by rsa_predict --- L1(·|studyHumanity): posteriors used in CG update → Figure 5 panel 1A +-- L1(·|studyHumanity): posteriors used in CommonGround update → Figure 5 panel 1A theorem l1_studyHumanity_nancy_val : mfRSA.L1 .studyHumanity .nancy = 1/2 := by rsa_predict @@ -734,28 +734,28 @@ theorem l1_studyHumanity_katie_val : mfRSA.L1 .studyHumanity .katie = 0 := by rsa_predict /-- Null gives uniform L1: every world has the same S1(null|w) by the -domain's symmetry, so L1(w|null) = CG(w)/Σ CG = 1/4. -/ +domain's symmetry, so L1(w|null) = CommonGround(w)/Σ CommonGround = 1/4. -/ theorem l1_null_val (w : MFWorld) : mfRSA.L1 .null w = 1/4 := by cases w <;> rsa_predict -- ════════════════════════════════════════════════════ --- § 18. Approximate CG Model (§5.2, Figure 6) +-- § 18. Approximate CommonGround Model (§5.2, Figure 6) -- ════════════════════════════════════════════════════ -/-! The Approximate Common Ground model relaxes the shared-CG assumption: -each participant maintains their own CG approximation. The speaker uses +/-! The Approximate Common Ground model relaxes the shared-CommonGround assumption: +each participant maintains their own CommonGround approximation. The speaker uses CG_S in production; the listener uses CG_L in comprehension with their private beliefs B_L as the L1 world prior. -Key difference from shared CG (Figure 4): -- Shared: L1(w|u) ∝ S1(u|w) · CG(w) — same CG for everyone +Key difference from shared CommonGround (Figure 4): +- Shared: L1(w|u) ∝ S1(u|w) · CommonGround(w) — same CommonGround for everyone - Approx: L1(w|u) ∝ S1(u|w) · B_L(w) — listener's own beliefs This models realistic divergence: participants with different priors hear the same utterance but reach different posteriors, causing their -CG approximations to drift apart (Figure 7). -/ +CommonGround approximations to drift apart (Figure 7). -/ -/-- State for the Approximate CG model (§5.2, Figure 6). -/ +/-- State for the Approximate CommonGround model (§5.2, Figure 6). -/ structure ApproxCGState (W : Type*) where cgA : DistributionalCG W cgB : DistributionalCG W @@ -789,8 +789,8 @@ noncomputable def approxComprehensionRSA worldPrior_nonneg := hbelL latentPrior_nonneg _ _ := by norm_num -/-- When beliefs equal the CG, the approximate model reduces to the -shared CG model — the split is only meaningful when they diverge. -/ +/-- When beliefs equal the CommonGround, the approximate model reduces to the +shared CommonGround model — the split is only meaningful when they diverge. -/ theorem approx_reduces_to_shared (cg : MFWorld → ℝ) (hcg : ∀ w, 0 ≤ cg w) : approxComprehensionRSA cg hcg cg hcg = mfRSAAt cg hcg := rfl @@ -800,23 +800,23 @@ theorem approx_reduces_to_shared (cg : MFWorld → ℝ) (hcg : ∀ w, 0 ≤ cg w /-! The belief update model extends the conversation system by also updating participants' private beliefs. After comprehension, the -listener updates their beliefs via the same linear rule as CG update: +listener updates their beliefs via the same linear rule as CommonGround update: Bel'(w) = (1 - lr_bel) · Bel(w) + lr_bel · posterior(w) The speaker does not update beliefs (they already knew the info). -Different learning rates for CG vs beliefs allow modeling: -- §6.2: skeptical listeners (low belief lr, high CG lr) +Different learning rates for CommonGround vs beliefs allow modeling: +- §6.2: skeptical listeners (low belief lr, high CommonGround lr) - §6.3: uncertainty-based rates (lr scales with entropy) -/ /-- State for the belief update model (Figure 8). -Extends approximate CG with separate learning rates for CG and beliefs. -/ +Extends approximate CommonGround with separate learning rates for CommonGround and beliefs. -/ structure BeliefUpdateState (W : Type*) where cgA : DistributionalCG W cgB : DistributionalCG W belA : DistributionalCG W belB : DistributionalCG W - /-- Learning rate for CG updates. -/ + /-- Learning rate for CommonGround updates. -/ cgLR : ℝ /-- Learning rate for belief updates (may be lower for skeptical agents). -/ belLR : ℝ @@ -833,7 +833,7 @@ noncomputable def BeliefUpdateState.initial {W : Type*} belLR := belLR speakerIsA := true -/-- Belief update is algebraically identical to CG update — both are +/-- Belief update is algebraically identical to CommonGround update — both are instances of @cite{luce-1959}'s linear learning rule. The only difference is the learning rate parameter and the interpretation (private vs shared). -/ theorem belief_update_is_linear_learning {W : Type*} @@ -850,12 +850,12 @@ theorem belief_update_is_linear_learning {W : Type*} /-! A speaker with uniform beliefs (no private information) assigns equal weight to all worlds under weighted sampling. Since no observation is more probable than any other, the speaker makes random assertions about -worlds they don't know, causing the CG to flip-flop (Figure 12). +worlds they don't know, causing the CommonGround to flip-flop (Figure 12). Solutions: 1. **Threshold sampling** (§7.1.1): filter out low-confidence worlds; a noncommittal speaker passes (null utterance) instead of guessing. -2. **Uncertainty-based lr** (§6.3): scale the CG update rate by the +2. **Uncertainty-based lr** (§6.3): scale the CommonGround update rate by the listener's uncertainty, so confident listeners resist random input. -/ /-- Uniform beliefs assign equal weight to all worlds under weighted @@ -883,23 +883,23 @@ theorem threshold_preserves_confident {W : Type*} -- § 21. Redundancy and Difference Sampling (§7.2) -- ════════════════════════════════════════════════════ -/-! Under weighted sampling, a speaker whose beliefs match the CG keeps +/-! Under weighted sampling, a speaker whose beliefs match the CommonGround keeps repeating already-shared information (Figure 14). Difference-based -sampling fixes this by weighting worlds by `max(0, Bel(w) - CG(w))`: -worlds already established in the CG get zero weight. +sampling fixes this by weighting worlds by `max(0, Bel(w) - CommonGround(w))`: +worlds already established in the CommonGround get zero weight. Combined with thresholding, **thresholded difference-based sampling** gives the best behavior (Figure 15): informed speakers contribute new information, noncommittal speakers pass. -/ -/-- When beliefs match the CG exactly, difference sampling assigns zero +/-- When beliefs match the CommonGround exactly, difference sampling assigns zero weight to all worlds — nothing new to contribute. -/ theorem difference_zero_when_aligned {W : Type*} (cg : DistributionalCG W) (w : W) : differenceSample cg cg w = 0 := by simp only [differenceSample, sub_self, max_self] -/-- Difference sampling assigns positive weight when belief exceeds CG — +/-- Difference sampling assigns positive weight when belief exceeds CommonGround — these worlds carry new information not yet in the common ground. -/ theorem difference_positive_when_exceeds {W : Type*} (bel cg : DistributionalCG W) (w : W) (h : cg.weight w < bel.weight w) : @@ -907,8 +907,8 @@ theorem difference_positive_when_exceeds {W : Type*} simp only [differenceSample] exact lt_of_lt_of_le (by linarith : (0 : ℝ) < bel.weight w - cg.weight w) (le_max_right 0 _) -/-- A's initial difference from uniform CG: Nancy has the highest -positive difference (belief 3 vs CG 1), so A's first contribution +/-- A's initial difference from uniform CommonGround: Nancy has the highest +positive difference (belief 3 vs CommonGround 1), so A's first contribution should describe Nancy — matching the stochastic trace in Figure 5. -/ theorem a_initial_diff_nancy_highest : aDiffFromUniform .nancy > aDiffFromUniform .ina ∧ diff --git a/Linglib/Studies/Beaver2001/Basic.lean b/Linglib/Studies/Beaver2001/Basic.lean index 159a567a5..688ecba70 100644 --- a/Linglib/Studies/Beaver2001/Basic.lean +++ b/Linglib/Studies/Beaver2001/Basic.lean @@ -68,7 +68,7 @@ namespace Beaver2001 open Semantics.Presupposition open Core.Duality -open Discourse.CommonGround +open CommonGround variable {W : Type*} @@ -237,7 +237,7 @@ q's presupposition (from q.presup). @cite{beaver-2001} Ch. 4 discusses @cite{stalnaker-1974}'s common ground and @cite{heim-1983}'s File Change Semantics in detail. The `ContextSet W` -type used here IS the context set from `Discourse.CommonGround`. +type used here IS the context set from `CommonGround`. `ContextSet.update` IS Heim's FCS update: intersect the context set with a proposition, keeping only worlds where the proposition holds. diff --git a/Linglib/Studies/Clark1983.lean b/Linglib/Studies/Clark1983.lean index cc627699a..785489e92 100644 --- a/Linglib/Studies/Clark1983.lean +++ b/Linglib/Studies/Clark1983.lean @@ -67,7 +67,7 @@ level rather than a vacuous law-of-excluded-middle. namespace Clark1983 -open Discourse.CommonGround +open CommonGround open Discourse (PreparatoryCondition) open Morphology.DM (Categorizer Recategorization CategorizedRoot denominal_requires_n recategorization_changes_category) @@ -300,7 +300,7 @@ structure GoalHierarchy (W : Type*) where /-- Subgoal (1): the intended meaning on this occasion. -/ intendedMeaning : W → Prop /-- The common ground used for the inference. -/ - commonGround : CG W + commonGround : CommonGround W /-- Subgoal (2): the meta-recognition that the speaker invokes a convention licensing the direct → intended inference. For conventional uses this is `True` (no specific convention required). @@ -335,7 +335,7 @@ in @cite{clark-1983} p. 321): > and the remaining surface arguments of the denominal verb denote > other roles in the situation. -Conditions (b)–(e) are unified as CG-entailment: the CG uniquely determines +Conditions (b)–(e) are unified as CommonGround-entailment: the CommonGround uniquely determines the situation. Condition (f) requires the parent noun's denotation to hold in every situation-world. -/ @@ -355,10 +355,10 @@ structure DenominalVerbConvention (W : Type*) where /-- The conventional denotation of the parent noun. -/ nounDenotation : W → Prop /-- (e) The common ground of speaker and listener. -/ - commonGround : CG W + commonGround : CommonGround W /-- (b–d) The speaker has good reason to believe the listener can readily compute the situation uniquely from mutual knowledge. - Operationalized as: every CG-compatible world satisfies the + Operationalized as: every CommonGround-compatible world satisfies the situation. -/ cgDeterminesSituation : ∀ w, commonGround.contextSet w → situation w /-- (f, extensional) The noun's denotation is realized in every @@ -387,7 +387,7 @@ def DenominalVerbConvention.toGoalHierarchy {W : Type*} intendedMeaning := conv.situation commonGround := conv.commonGround invokesConvention := - -- (b–d): CG uniquely determines the situation + -- (b–d): CommonGround uniquely determines the situation -- (f, extensional): noun denotation realized in every situation-world -- (f, role-distinctness): parent noun role differs from other surface args' roles (∀ w, conv.commonGround.contextSet w → conv.situation w) ∧ @@ -439,12 +439,12 @@ def teapotSituation (w : TeapotWorld) : Prop := def teapotNoun (w : TeapotWorld) : Prop := w.teapot = true /-- Common ground: shared knowledge about Max's odd habits with teapots. - For the worked example we model the CG as already entailing the - rubbing-with-teapot situation; in a fuller formalization the CG + For the worked example we model the CommonGround as already entailing the + rubbing-with-teapot situation; in a fuller formalization the CommonGround would entail the relevant odd-habit knowledge from which the listener derives the situation. -/ -def teapotCG : CG TeapotWorld := - CG.empty.add { w | w.rubbing = true ∧ w.teapot = true } +def teapotCG : CommonGround TeapotWorld := + CommonGround.empty.add { w | w.rubbing = true ∧ w.teapot = true } /-- The Innovative Denominal Verb Convention (paper p. 321) instantiated for *Max teapotted a policeman* (paper pp. 320–321, 325–326). @@ -590,9 +590,9 @@ def arlenesGoalHierarchy : GoalHierarchy StereosWorld where commonGround := .empty invokesConvention := True -/-- Bombeck's CG: discourse context establishes "owners are common." -/ -def bombecksCG : CG StereosWorld := - CG.empty.add { w | w.ownersCommon = true } +/-- Bombeck's CommonGround: discourse context establishes "owners are common." -/ +def bombecksCG : CommonGround StereosWorld := + CommonGround.empty.add { w | w.ownersCommon = true } /-- Bombeck's goal hierarchy: innovative use. The intended meaning is the nonce reading (owners are common). `invokesConvention` is left at `True` @@ -645,7 +645,7 @@ structure IndirectAct (W : Type*) where condition). -/ prepCondition : Option PreparatoryCondition /-- Common ground licensing the inference. -/ - commonGround : CG W + commonGround : CommonGround W /-- Project an indirect act to a goal hierarchy. @@ -740,7 +740,7 @@ The question reflects subgoal (5); answering with just *yes* satisfies These are NOT preparatory-condition-based indirect acts (Searle 1975 / Clark 1979's mechanism), so `prepCondition := none`. The convention -invoked is goal-hierarchy reconstruction from NP content + CG. -/ +invoked is goal-hierarchy reconstruction from NP content + CommonGround. -/ /-- AmEx case: the question is interpreted as direct only (paper p. 322: 100% gave yes-answers; restaurateurs construed as direct question). @@ -829,41 +829,41 @@ theorem shared_innovativeness_criterion {W : Type*} The deeper formal principle: a contextual expression's meaning is a function from common ground to denotation, not a static denotation. The `GoalHierarchy` -of `§F` is what you get by **evaluating** this function at a specific CG. -/ +of `§F` is what you get by **evaluating** this function at a specific CommonGround. -/ /-- A contextual meaning: meaning is a function from common ground to denotation. `directMeaning` is the conventional denotation; `compute` - maps a CG to the **intended** meaning on a given occasion. -/ + maps a CommonGround to the **intended** meaning on a given occasion. -/ structure ContextualMeaning (W : Type*) where directMeaning : W → Prop - compute : CG W → (W → Prop) + compute : CommonGround W → (W → Prop) -/-- Evaluate a contextual meaning at a specific CG, producing a goal +/-- Evaluate a contextual meaning at a specific CommonGround, producing a goal hierarchy. The convention-recognition is left at `True` here — the - fuller treatment exposes a CG-dependence witness via the source-class + fuller treatment exposes a CommonGround-dependence witness via the source-class projections (`DenominalVerbConvention.toGoalHierarchy` etc.). -/ def ContextualMeaning.evaluate {W : Type*} - (cm : ContextualMeaning W) (cg : CG W) : GoalHierarchy W where + (cm : ContextualMeaning W) (cg : CommonGround W) : GoalHierarchy W where directMeaning := cm.directMeaning intendedMeaning := cm.compute cg commonGround := cg invokesConvention := True -/-- A contextual meaning is **CG-independent** when the CG makes no +/-- A contextual meaning is **CommonGround-independent** when the CommonGround makes no difference. This is sense-selection. -/ def ContextualMeaning.isCGIndependent {W : Type*} (cm : ContextualMeaning W) : Prop := - ∀ cg : CG W, cm.compute cg = cm.directMeaning + ∀ cg : CommonGround W, cm.compute cg = cm.directMeaning -/-- A contextual meaning is **CG-dependent** when there exists a CG that +/-- A contextual meaning is **CommonGround-dependent** when there exists a CommonGround that shifts the intended meaning away from the direct meaning. This is sense-creation. -/ def ContextualMeaning.isCGDependent {W : Type*} (cm : ContextualMeaning W) : Prop := - ∃ cg : CG W, cm.compute cg ≠ cm.directMeaning + ∃ cg : CommonGround W, cm.compute cg ≠ cm.directMeaning theorem cg_independent_conventional {W : Type*} - (cm : ContextualMeaning W) (h : cm.isCGIndependent) (cg : CG W) : + (cm : ContextualMeaning W) (h : cm.isCGIndependent) (cg : CommonGround W) : (cm.evaluate cg).isConventional := h cg theorem cg_dependent_innovative {W : Type*} @@ -875,8 +875,8 @@ open Classical /-- The contextual meaning of *stereos*: the SAME meaning function underlies both Arlene's and Bombeck's uses. The `compute` function - models the inference from CG to intended meaning: - if the CG entails owners-are-common, the intended meaning is + models the inference from CommonGround to intended meaning: + if the CommonGround entails owners-are-common, the intended meaning is `ownersCommon`; otherwise it falls back to the direct meaning. This is a simplified model of the pragmatic computation — the @@ -898,7 +898,7 @@ private theorem bombecksCG_entails_owners : exact h.1 private theorem emptyCG_not_entails_owners : - ¬ ∀ w, (CG.empty : CG StereosWorld).contextSet w → w.ownersCommon = true := by + ¬ ∀ w, (CommonGround.empty : CommonGround StereosWorld).contextSet w → w.ownersCommon = true := by intro h have := h ⟨true, false⟩ (by trivial) exact absurd this (by decide) diff --git a/Linglib/Studies/CohenKrifka2014.lean b/Linglib/Studies/CohenKrifka2014.lean index 10b1ebd6d..092b0ce1c 100644 --- a/Linglib/Studies/CohenKrifka2014.lean +++ b/Linglib/Studies/CohenKrifka2014.lean @@ -22,13 +22,13 @@ The paper's headline claims that our list-shape substrate can support: 1. **GRANT definition** (paper eq. 38, p. 53): `GRANT(φ) := ~ASSERT(¬φ)`. Trivially via the substrate's `denegate` operator. -2. **GRANT structural properties**: preserves CG (substrate's +2. **GRANT structural properties**: preserves CommonGround (substrate's `denegate_preserves_root`), doesn't grow continuations (`denegate_continuation_count_le`), filters precisely the speaker-asserts-¬φ paths (`denegate_surviving_no_match`). 3. **ASSERT entails GRANT** (paper p. 54 prose): ASSERT(φ) and GRANT(φ) - project to context sets in subset relation — asserted CG is a subset - of granted CG. This is the paper's "GRANT is weaker than ASSERT" at + project to context sets in subset relation — asserted CommonGround is a subset + of granted CommonGround. This is the paper's "GRANT is weaker than ASSERT" at the observable resolution. ## What the substrate cannot capture (✗) — explicit deferrals @@ -127,7 +127,7 @@ noncomputable def grant (cs : CommitmentSpace W Prop) (φ : W → Prop) : -- § 2. GRANT structural properties -- ════════════════════════════════════════════════════ -/-- GRANT preserves the root (CG unchanged). Krifka 2015 p. 330: +/-- GRANT preserves the root (CommonGround unchanged). Krifka 2015 p. 330: "denegation does not change the root of the commitment space, but prunes its legal developments". For any cs and φ. -/ theorem grant_preserves_root (cs : CommitmentSpace W Prop) (φ : W → Prop) : @@ -188,7 +188,7 @@ theorem assert_contextSet_subset_grant_contextSet exact h ic (List.mem_cons_of_mem _ hic) /-- The strict-stronger direction: there exist `cs`, `φ`, and `w` such - that `w` is in the granted CG but NOT in the asserted CG. The + that `w` is in the granted CommonGround but NOT in the asserted CommonGround. The asymmetry that makes ASSERT genuinely stronger than GRANT (not just ≤). -/ theorem assert_strictly_stronger_witness : @@ -196,11 +196,11 @@ theorem assert_strictly_stronger_witness : (grant cs φ).toContextSet w ∧ ¬ (cs.assert .speaker φ).toContextSet w := by -- Witness: empty cs, content φ that is False at some world. refine ⟨Bool, CommitmentSpace.empty, fun b => b = true, false, ?_, ?_⟩ - · -- Granted CG: empty root, no constraint, every world survives. + · -- Granted CommonGround: empty root, no constraint, every world survives. intro ic hic rw [grant_preserves_root] at hic exact absurd hic (List.not_mem_nil) - · -- Asserted CG: root contains `commit speaker (· = true)`. The + · -- Asserted CommonGround: root contains `commit speaker (· = true)`. The -- `toCommitment` projection of this commit at world `false` is -- `(fun b => b = true) false = (false = true) = False`. intro h diff --git a/Linglib/Studies/CohnGordonEtAl2019.lean b/Linglib/Studies/CohnGordonEtAl2019.lean index 39d8d1d10..19055b703 100644 --- a/Linglib/Studies/CohnGordonEtAl2019.lean +++ b/Linglib/Studies/CohnGordonEtAl2019.lean @@ -219,7 +219,7 @@ theorem uniform_after_red_for_r2 (w : Word) (hw : w ≠ .red) : for R3 (S1(red|[],R3) = 1), so hearing "red" raises R3's probability. For R1, the speaker could have said "dress" instead, so "red" is less diagnostic. We pick this up below as a structural foreshadowing of - @cite{sedivy-etal-1999}'s contrastive-inference findings; CG themselves + @cite{sedivy-etal-1999}'s contrastive-inference findings; CommonGround themselves cite @cite{sedivy-2007} for the same effect. -/ theorem listener_anticipation : incRSA.L1 .red .redHat > incRSA.L1 .red .redDress := by @@ -392,11 +392,11 @@ need for "tall" to disambiguate from the only other pitcher: there isn't one). The "tall" is therefore diagnostic of the cup with a same-category contrast. -The original empirical effect is from @cite{sedivy-etal-1999}; CG cite +The original empirical effect is from @cite{sedivy-etal-1999}; CommonGround cite the @cite{sedivy-2007} review article that summarizes it. This file formalises both contrast cells. The contrast scene is the -five-word, four-referent `sedivyBundle` from CG's text. The no-contrast +five-word, four-referent `sedivyBundle` from CommonGround's text. The no-contrast scene is a four-word, three-referent companion bundle (`SedivyScene_NoContrast.bundle`) — `.short` is omitted because the shortCup referent it would describe is absent from the display, leaving @@ -454,7 +454,7 @@ from the visual display. The companion bundle drops `.short` from `Word` and the `[short, cup]` utterance from `completeUtterances`. Justification: with no shortCup in the display, a cooperative speaker has no scene-anchored use for -`.short`, and CG's `IncrementalSemantics` is a *scene-specific* +`.short`, and CommonGround's `IncrementalSemantics` is a *scene-specific* production model rather than a lexicon-wide one. (The listener's standing mental lexicon still contains `short`; the bundle here is a model of speaker production for *this scene*, not of mental diff --git a/Linglib/Studies/CondoravdiLauer2012.lean b/Linglib/Studies/CondoravdiLauer2012.lean index 74dd284e4..d5ffa9e41 100644 --- a/Linglib/Studies/CondoravdiLauer2012.lean +++ b/Linglib/Studies/CondoravdiLauer2012.lean @@ -30,7 +30,7 @@ This is the substrate's `CommitmentForce` axis. - §1 — World fixture and propositions - §2 — Declarative-as-doxastic baseline (Krifka 2015 default) - §3 — Imperative-as-preferential (the paper's central claim) -- §4 — Doxastic vs preferential CG divergence (the two projections +- §4 — Doxastic vs preferential CommonGround divergence (the two projections see different things) - §5 — vs Krifka 2015: same substrate, different force; Krifka's framework was purely doxastic @@ -177,8 +177,8 @@ theorem dox_pref_dual (w : AddrPosture) : /-- The conflated `toContextSet` is the conjunction of both projections (substrate-level theorem `toContextSet_eq_doxastic_and_preferential`). - Specialised to `imperativeState`: the conflated CG narrows to - sitting-worlds even though only the preferential-CG component is + Specialised to `imperativeState`: the conflated CommonGround narrows to + sitting-worlds even though only the preferential-CommonGround component is really committed. The conflated view loses information. -/ theorem imperative_conflated_loses_distinction (w : AddrPosture) : imperativeState.space.toContextSet w ↔ isSitting w := by diff --git a/Linglib/Studies/DelPinalBassiSauerland2024.lean b/Linglib/Studies/DelPinalBassiSauerland2024.lean index 2a879906a..dc561e6ec 100644 --- a/Linglib/Studies/DelPinalBassiSauerland2024.lean +++ b/Linglib/Studies/DelPinalBassiSauerland2024.lean @@ -40,7 +40,7 @@ set_option autoImplicit false namespace DelPinalBassiSauerland2024 open Semantics.Presupposition (PrProp) -open Discourse.CommonGround (ContextSet) +open CommonGround (ContextSet) open Exhaustification.Presuppositional open BarLevFox2020 open Exhaustification diff --git a/Linglib/Studies/Enguehard2024.lean b/Linglib/Studies/Enguehard2024.lean index 9b4a37651..5e9b370a6 100644 --- a/Linglib/Studies/Enguehard2024.lean +++ b/Linglib/Studies/Enguehard2024.lean @@ -664,7 +664,7 @@ categorical judgments in examples (5)–(6). world — there is no middle ground. -/ theorem constant_presup_satisfied_iff_satisfiable {W : Type*} (witnessCard : W → Nat) (conceivable : W → Prop) - (c : Discourse.CommonGround.ContextSet W) + (c : CommonGround.ContextSet W) (hne : c.nonEmpty) : Semantics.Presupposition.Context.presupSatisfied c (sgIndefPresup witnessCard conceivable) ↔ diff --git a/Linglib/Studies/Faller2019.lean b/Linglib/Studies/Faller2019.lean index cefb01f05..09bb00315 100644 --- a/Linglib/Studies/Faller2019.lean +++ b/Linglib/Studies/Faller2019.lean @@ -128,7 +128,7 @@ namespace DiscourseState variable {A W : Type*} -/-- The empty discourse state: no commitments, empty Table, trivial CG. -/ +/-- The empty discourse state: no commitments, empty Table, trivial CommonGround. -/ def empty : DiscourseState A W := { Discourse.Commitment.Table.DiscourseState.empty with evidCommit := fun _ _ => CommitmentSlate.empty } diff --git a/Linglib/Studies/FarkasBruce2010.lean b/Linglib/Studies/FarkasBruce2010.lean index 1f856c37f..3addb82ce 100644 --- a/Linglib/Studies/FarkasBruce2010.lean +++ b/Linglib/Studies/FarkasBruce2010.lean @@ -14,7 +14,7 @@ substrate (`Item`, `DiscourseState`, primitive updates) lives in * `assert`, `polarQuestion`, `acceptTop` — F&B moves over `FBState W`. -* `assert_preserves_cg` — F&B's assertion does not touch CG (the +* `assert_preserves_cg` — F&B's assertion does not touch CommonGround (the load-bearing thesis that diverges from @cite{stalnaker-1978}). -/ @@ -44,7 +44,7 @@ def polarQuestion (ds : FBState W) (p : W → Prop) : ds.pushItem ⟨.speaker, .addressee, .interrogative, [p, fun w => ¬ p w]⟩ /-- Addressee accepts the head alternative of the top item: - other-generated doxastic commit, add to CG, pop. -/ + other-generated doxastic commit, add to CommonGround, pop. -/ def acceptTop (ds : FBState W) : FBState W := match ds.table with @@ -99,7 +99,7 @@ theorem accept_after_assert_cg (ds : FBState W) (p : W → Prop) : /-! ### Divergence from Stalnaker -/ /-- F&B's assertion does **not** narrow the common ground, in - contrast to @cite{stalnaker-1978} where assertion is direct CG + contrast to @cite{stalnaker-1978} where assertion is direct CommonGround update. The pre-assertion `cg` is preserved exactly; acceptance is a separate move (`acceptTop`). -/ theorem assert_preserves_cg (ds : FBState W) (p : W → Prop) : diff --git a/Linglib/Studies/Ginzburg2012.lean b/Linglib/Studies/Ginzburg2012.lean index eaf0d31c1..6fc772c91 100644 --- a/Linglib/Studies/Ginzburg2012.lean +++ b/Linglib/Studies/Ginzburg2012.lean @@ -48,7 +48,7 @@ Sluice-split-faithful Table 7.4 taxonomy. @cite{ginzburg-2012} > all references in §12. Cross-framework contrasts with later work (@cite{krifka-2015} commitment-spaces; @cite{anderson-2021} -distributional CG) live inside *those* studies per CLAUDE.md's +distributional CommonGround) live inside *those* studies per CLAUDE.md's "no bridge files" + chronological-dependency rule. ## What this file does NOT cover @@ -560,7 +560,7 @@ end EndToEnd Per the project's chronological-dependency rule, this study engages *pre-2012* siblings here: -- @cite{stalnaker-1978}/@cite{stalnaker-2002} — single shared CG +- @cite{stalnaker-1978}/@cite{stalnaker-2002} — single shared CommonGround - @cite{farkas-bruce-2010} — five-way dcS/dcL/cg/table/ps decomposition - @cite{roberts-1996} — partition-based QUD-stack - @cite{purver-ginzburg-2004} — q-params/dgb-params split @@ -584,19 +584,19 @@ def isRaining : Set RainW := fun w => w = .rainy instance : DecidablePred isRaining := fun w => by unfold isRaining; exact inferInstance -/-! ### vs Stalnaker (single shared CG) +/-! ### vs Stalnaker (single shared CommonGround) @cite{stalnaker-1978}: the common ground is *one shared object*. After -A asserts p, the (single) CG contains p eliminated of ¬p worlds. +A asserts p, the (single) CommonGround contains p eliminated of ¬p worlds. @cite{ginzburg-2012}: each participant has their *own* DGB. After A -asserts p, A's DGB has p in FACTS; B's does not. There is NO shared CG — +asserts p, A's DGB has p in FACTS; B's does not. There is NO shared CommonGround — only coupled DGBs synchronized via Accept. The contrast as a Lean theorem: KOS predicts that two participants' DGBs (after A asserts p, before B accepts) project to *different* context sets — Stalnaker's framework cannot represent this divergence -because it has only one CG. -/ +because it has only one CommonGround. -/ instance : DecidableSupport (Set RainW) String where supports _ _ := False @@ -610,10 +610,10 @@ def kosSpeakerDGB : DGB String (Set RainW) String String := def kosAddresseeDGB : DGB String (Set RainW) String String := DGB.initial -open Discourse.CommonGround in +open CommonGround in /-- KOS-vs-Stalnaker architectural contrast: KOS's two DGBs project to *different* `ContextSet`s after one-sided assertion. Stalnaker's -framework has a single CG that cannot represent this divergence — +framework has a single CommonGround that cannot represent this divergence — the contrast is structural, not a matter of degree. The inequality holds at `RainW.sunny`: the speaker's CS at sunny @@ -640,7 +640,7 @@ theorem kos_vs_stalnaker_per_dgb_divergence : @cite{farkas-bruce-2010}: discourse state has FIVE components (dcS, dcL, cg, table, ps). Assertion adds to *speaker's dcS* (private commitment), pushes an issue on the table; only *acceptance* moves content to the -shared CG. +shared CommonGround. @cite{ginzburg-2012}: per-participant DGBs (no separate dcS/dcL/cg distinction inside one structure). Assertion goes directly to the diff --git a/Linglib/Studies/Glass2025.lean b/Linglib/Studies/Glass2025.lean index 23e6a90a4..3cdbf088b 100644 --- a/Linglib/Studies/Glass2025.lean +++ b/Linglib/Studies/Glass2025.lean @@ -15,20 +15,20 @@ Semantics and Pragmatics 18, Article 8: 1-17. ## Key Claims 1. **Two ways to negate the factive presupposition**: A contrafactive could - *require* ¬p (all CG worlds are ¬p worlds) or require *compatibility* - with ¬p (some CG world is a ¬p world). + *require* ¬p (all CommonGround worlds are ¬p worlds) or require *compatibility* + with ¬p (some CommonGround world is a ¬p world). 2. **Strong contrafactives are unattested**: No verb presupposes ¬p (requiring - CG ⊨ ¬p). This follows from the Predicate Lexicalization Constraint + CommonGround ⊨ ¬p). This follows from the Predicate Lexicalization Constraint (@cite{roberts-ozyildiz-2025}): ¬p cannot causally support B(x)(p). 3. **Weak contrafactives exist**: Mandarin yǐwéi (@cite{glass-2023}) has a - postsupposition ◇¬p — after utterance, the CG must be compatible with ¬p. + postsupposition ◇¬p — after utterance, the CommonGround must be compatible with ¬p. This is a definedness condition on the *output* context, not a presupposition on the input context. -4. **Revised question**: "Why are there belief verbs like *know* (CG ⊨ p) - and yǐwéi (CG ◇ ¬p), but none like *contra* (CG ⊨ ¬p)?" +4. **Revised question**: "Why are there belief verbs like *know* (CommonGround ⊨ p) + and yǐwéi (CommonGround ◇ ¬p), but none like *contra* (CommonGround ⊨ ¬p)?" ## Formalization Strategy @@ -66,13 +66,13 @@ private def prop : MiniWorld → Bool | .w0 => true | .w1 => false -/-- Factive context: all worlds satisfy p (CG ⊨ p). -/ +/-- Factive context: all worlds satisfy p (CommonGround ⊨ p). -/ private def factiveCtx : List MiniWorld := [.w0] -/-- Neutral context: p is open (CG ◇ p ∧ CG ◇ ¬p). -/ +/-- Neutral context: p is open (CommonGround ◇ p ∧ CommonGround ◇ ¬p). -/ private def neutralCtx : List MiniWorld := [.w0, .w1] -/-- Contrafactive context: no world satisfies p (CG ⊨ ¬p). -/ +/-- Contrafactive context: no world satisfies p (CommonGround ⊨ ¬p). -/ private def contrafactiveCtx : List MiniWorld := [.w1] -- ============================================================================ @@ -109,7 +109,7 @@ private def yiweiPresup : PrProp MiniWorld where presup := λ _ => True assertion := λ _ => True -/-- yǐwéi's postsupposition: CG must be compatible with ¬p. -/ +/-- yǐwéi's postsupposition: CommonGround must be compatible with ¬p. -/ private def yiweiPostsup : Postsupposition MiniWorld := Postsupposition.weakContrafactive diff --git a/Linglib/Studies/Heim1992Projection.lean b/Linglib/Studies/Heim1992Projection.lean index 1b508ae22..4dd2ad3a4 100644 --- a/Linglib/Studies/Heim1992Projection.lean +++ b/Linglib/Studies/Heim1992Projection.lean @@ -37,7 +37,7 @@ formalized; the substrate splits along the natural Phenomena boundary namespace Heim1992 open Semantics.Presupposition (PrProp) -open Discourse.CommonGround (ContextSet) +open CommonGround (ContextSet) open Core.Logic.Intensional (IsSerial IsEuclidean IsS5Frame IsKD45Frame IsBeliefRefinementOf) open Semantics.Presupposition.LocalContext (presupFiltered) diff --git a/Linglib/Studies/Hohle1992.lean b/Linglib/Studies/Hohle1992.lean index 2a6503d42..490f90063 100644 --- a/Linglib/Studies/Hohle1992.lean +++ b/Linglib/Studies/Hohle1992.lean @@ -47,7 +47,7 @@ Adjacent studies the substrate is shared with: highlighting + ⟨A, N⟩ machinery applied to Saraguro Kichwa `=mi`. Höhle's German VF and Martínez Vera's `=mi` exemplify the same paper-(60) prediction about the focus-account of verum. -* `Studies/RomeroHan2004.lean` — VERUM as a CG +* `Studies/RomeroHan2004.lean` — VERUM as a CommonGround operator (rather than as focus on the assertion operator). R&H's `forSureCG` is the alternative-line analysis that Höhle's focus-account contrasts with (paper §6's FAT vs. LOT debate). diff --git a/Linglib/Studies/Karttunen1973.lean b/Linglib/Studies/Karttunen1973.lean index 7d8af0b20..111b44e17 100644 --- a/Linglib/Studies/Karttunen1973.lean +++ b/Linglib/Studies/Karttunen1973.lean @@ -32,7 +32,7 @@ namespace Karttunen1973 open Semantics.Presupposition open Semantics.Lexical (ProjectionBehavior VerbCore) -open Discourse.CommonGround (ContextSet) +open CommonGround (ContextSet) open Fragments.English.Predicates.Verbal -- ════════════════════════════════════════════════════════════════ diff --git a/Linglib/Studies/KayFillmore1999.lean b/Linglib/Studies/KayFillmore1999.lean index 53262c614..f621e43cd 100644 --- a/Linglib/Studies/KayFillmore1999.lean +++ b/Linglib/Studies/KayFillmore1999.lean @@ -291,7 +291,7 @@ The two readings are distinguished by the PerspectiveP layer: | 2 | `Expressives/Basic` | Incredulity is CI content (projects through negation) | | 3 | `Semantics.Questions/Hamblin` | Literal = standard `which`; incredulity = degenerate Q | | 4 | `Semantics.ArgumentStructure.Linking/LeftPeriphery` | PerspP disambiguates the two readings | -| 5 | `Core/CommonGround` | Presupposition requires CG entailment | +| 5 | `Core/CommonGround` | Presupposition requires CommonGround entailment | | 6 | `Verb/Aspect` | Progressive requirement (durative ∧ dynamic) | | 7 | `Focus/DomainWidening` | Incongruity = normative expectation violation | | 8 | `Semantics.Questions/Polarity` | Incredulity = rhetorical question | @@ -553,14 +553,14 @@ theorem perspP_disambiguates_wxdy {W : Type*} -- H. Common ground bridge (Core/CommonGround.lean) -- ============================================================================ -open Discourse.CommonGround +open CommonGround /-- The WXDY presupposition must be entailed by the common ground. -For "What's this fly doing in my soup?", the CG must already entail +For "What's this fly doing in my soup?", the CommonGround must already entail that there is a fly in the soup (the speaker sees it). -/ theorem wxdy_presup_requires_cg {W : Type*} (c : ContextSet W) (embeddedProp : W → Prop) - (h : c ⊧ (wxdyPresup embeddedProp).presup) (w : W) (hw : c w) : + (h : ContextSet.entails c (wxdyPresup embeddedProp).presup) (w : W) (hw : c w) : (wxdyPresup embeddedProp).presup w := h hw diff --git a/Linglib/Studies/Krifka2015.lean b/Linglib/Studies/Krifka2015.lean index 48598fd90..2b78113b0 100644 --- a/Linglib/Studies/Krifka2015.lean +++ b/Linglib/Studies/Krifka2015.lean @@ -33,7 +33,7 @@ uses a 2-world Weather model and verifies a specific paper claim. p. 331) cites F&B as the inspiration for his rejection operator ℜ; this section makes the structural relationship Lean-checkable. - §∞ — Deep structure: the Dialogue Completeness observation — - framework-agnostic agreement on observable CG at completed traces. + framework-agnostic agreement on observable CommonGround at completed traces. ## Out of scope (explicit) @@ -115,7 +115,7 @@ theorem assert_by_addressee_root_eq : -- § 3. Monopolar vs Bipolar Questions (paper §3, eqs. 23, 27) -- ════════════════════════════════════════════════════ -/-- Monopolar question preserves the root (CG unchanged) — paper p. 335. -/ +/-- Monopolar question preserves the root (CommonGround unchanged) — paper p. 335. -/ theorem monopolar_root_unchanged : (s₀.monopolarQuestion isRaining).space.root = [] := rfl @@ -397,9 +397,9 @@ Reciprocal entry to `Studies/Ginzburg2012.lean` lines | Question | Krifka 2015 | Ginzburg 2012 (KOS) | |---|---|---| -| Is CG a single object or per-agent? | Single object, but its entries are speaker-indexed (`IndexedCommitment.commit S₁ φ`) | Per-agent (`DGB.facts`) | -| When does an assertion narrow CG? | Immediately (assert puts `commit S₁ φ` in root) | Only after Accept (one-sided FACTS) | -| Are commitments separable from CG? | Yes — root carries indexed commitments + per-agent slates | Only via separate DGBs | +| Is CommonGround a single object or per-agent? | Single object, but its entries are speaker-indexed (`IndexedCommitment.commit S₁ φ`) | Per-agent (`DGB.facts`) | +| When does an assertion narrow CommonGround? | Immediately (assert puts `commit S₁ φ` in root) | Only after Accept (one-sided FACTS) | +| Are commitments separable from CommonGround? | Yes — root carries indexed commitments + per-agent slates | Only via separate DGBs | The architectures cannot be unified by a Galois connection that preserves both Krifka's eager-narrowing root behaviour and KOS's per-DGB asymmetry. @@ -440,7 +440,7 @@ theorem krifka_indexed_root_vs_kos_split_dgbs (p : Weather → Prop) : end vsGinzburg2012 -- ════════════════════════════════════════════════════ --- § N+1. vs Farkas & Bruce 2010 — eager vs lazy CG narrowing +-- § N+1. vs Farkas & Bruce 2010 — eager vs lazy CommonGround narrowing -- ════════════════════════════════════════════════════ /-! ## Krifka commitment-spaces vs Farkas-Bruce discourse-table model @@ -454,14 +454,14 @@ identical event sequences. | Question | Krifka 2015 | Farkas-Bruce 2010 | |---|---|---| -| When does an assertion narrow CG? | Immediately (`commit speaker φ` in root) | Only after addressee accept (one-sided dcS until then) | -| Where does the assertion live pre-acceptance? | Root entry (already in CG, speaker-indexed) | `dcS` slate + `table` issue | +| When does an assertion narrow CommonGround? | Immediately (`commit speaker φ` in root) | Only after addressee accept (one-sided dcS until then) | +| Where does the assertion live pre-acceptance? | Root entry (already in CommonGround, speaker-indexed) | `dcS` slate + `table` issue | | What does acceptance update? | Adds `commit addressee φ` to root | Pops table issue, adds φ to cg + dcL | | What's the "stable" predicate? | `hasNoOpenContinuations` (no pending proposals) | `table.isEmpty` (no items on table) | The eager/lazy distinction is real and non-collapsible at intermediate states. But at the end of a "completed" assertion+acceptance sequence, -both frameworks agree on the observable CG content modulo Krifka's +both frameworks agree on the observable CommonGround content modulo Krifka's speaker indexing — see the Dialogue Completeness observation below. -/ @@ -469,10 +469,10 @@ section vsFarkasBruce2010 open Dialogue.FarkasBruce -/-- Divergence at the assert-only intermediate state: Krifka's CG - narrows immediately (one indexed entry in `root`); F&B's joint CG +/-- Divergence at the assert-only intermediate state: Krifka's CommonGround + narrows immediately (one indexed entry in `root`); F&B's joint CommonGround stays empty because the assertion lives on the table awaiting - acceptance. The two frameworks DISAGREE on what's "in CG" mid-trace. + acceptance. The two frameworks DISAGREE on what's "in CommonGround" mid-trace. @cite{krifka-2015} p. 332 eq. (14) puts `S₁⊢φ` directly in the commitment state; @cite{farkas-bruce-2010}'s `assertDeclarative` @@ -489,7 +489,7 @@ theorem krifka_eager_vs_farkasBruce_lazy_intermediate : refine ⟨rfl, rfl, rfl, rfl⟩ /-- Bridge at the completed-trace state: after the addressee accepts the - assertion, both frameworks have φ in the joint CG (modulo Krifka's + assertion, both frameworks have φ in the joint CommonGround (modulo Krifka's speaker indexing on the root entries; F&B's `cg` is bare `Set W`). Krifka's "addressee accepts" pathway is `assert φ .addressee` @@ -515,7 +515,7 @@ theorem krifka_double_assert_eq_farkasBruce_assert_accept : /-- The headline observation: at a completed assertion+acceptance trace, the two frameworks agree on the **context-set projection** — - Krifka's projected CG content is exactly `isRaining`. + Krifka's projected CommonGround content is exactly `isRaining`. The frameworks disagree on what they STORE at intermediate states (root vs table, indexed vs flat) but agree on the observable @@ -558,7 +558,7 @@ the same world type `W`, equipped with: bipolar question, low/high negated question, accept, reject, …); - A step function `step_i : Sᵢ → DialogueEvent W → Sᵢ`; - A context-set projection `contextSet_i : Sᵢ → Set W` (the observable - CG content); + CommonGround content); - A "completed" predicate `isCompleted_i : Sᵢ → Prop` (no pending proposals, no orphan issues), @@ -574,7 +574,7 @@ the conjecture is: Plain English: **dialogue frameworks differ in the journey through intermediate states; they agree on the observable destination.** -The eager/lazy timing of CG updates, the per-agent commitment slate +The eager/lazy timing of CommonGround updates, the per-agent commitment slate shape, the proposal-tracking apparatus — all of these are framework-internal bookkeeping invisible at completed traces. What's publicly committed (in the projected context-set sense) at the end of diff --git a/Linglib/Studies/MartinezVera2026.lean b/Linglib/Studies/MartinezVera2026.lean index 14e239b4a..735900e9b 100644 --- a/Linglib/Studies/MartinezVera2026.lean +++ b/Linglib/Studies/MartinezVera2026.lean @@ -59,7 +59,7 @@ Three empirical signatures: divergence theorem showing MV's polar partition `{p, pᶜ}` is in general distinct from Romero & Han's verum partition `{forSureCG p, ¬forSureCG p}`. Makes the line-a (focus) vs line-b - (CG-modal verum operator) split visible at the type level. + (CommonGround-modal verum operator) split visible at the type level. ## Substrate consumed @@ -370,7 +370,7 @@ For the polar alternative-set case `{β.atIssue, β.atIssueᶜ}`, MV's `¬β.atIssue` be highlighted in the context. This makes the agreement between the focus-on-polarity (Höhle) and focus-marker (MV) accounts explicit at the type level. The disagreement with @cite{romero-han-2004}'s -CG-modal verum surfaces as the partition divergence in §6 below. +CommonGround-modal verum surfaces as the partition divergence in §6 below. -/ /-- For the polar alternative-set case **with contingent scope**, MV's @@ -434,7 +434,7 @@ theorem mi_eq_hohle_as_verumOperator /-! ### § 6. Cross-framework divergence: MV's partition vs R&H's verum partition -Romero & Han 2004 analyse verum as a CG-modal operator `forSureCG` +Romero & Han 2004 analyse verum as a CommonGround-modal operator `forSureCG` producing an *unbalanced* polar partition `{forSureCG p, ¬forSureCG p}` (line-b account). MV implicitly takes a line-a (focus over polarity) position: the partition over which `=mi` operates is the standard polar diff --git a/Linglib/Studies/MaticNikolaeva2018.lean b/Linglib/Studies/MaticNikolaeva2018.lean index 3f4e2262e..4a5ef9173 100644 --- a/Linglib/Studies/MaticNikolaeva2018.lean +++ b/Linglib/Studies/MaticNikolaeva2018.lean @@ -265,7 +265,7 @@ M&N §2 explicitly target three sibling frameworks beyond the substrate's form-class encoding. Two of them are formalized in linglib: - `Studies/RomeroHan2004.lean` formalizes - @cite{romero-han-2004}'s **FOR-SURE-CG** epistemic-conjunction + @cite{romero-han-2004}'s **FOR-SURE-CommonGround** epistemic-conjunction operator. M&N call this "Lexical Operator Theory" (LOT) and reject it on the same form-meaning grounds (M&N §2 "epistemic account"). @@ -287,14 +287,14 @@ mappings as separate `def`s for now so each framework's coverage profile stays visible at the def-site. -/ /-- Romero & Han's framework offers exactly one analytic option for - salient polarity: the FOR-SURE-CG operator. M&N call this LOT. -/ + salient polarity: the FOR-SURE-CommonGround operator. M&N call this LOT. -/ inductive RHAnalysis where /-- @cite{romero-han-2004}'s `forSureCG` operator analyzes the - structure as expressing speaker certainty about CG-addition. -/ + structure as expressing speaker certainty about CommonGround-addition. -/ | epistemicVerum deriving DecidableEq, Repr -/-- R&H's FOR-SURE-CG analysis is canonically motivated by — and +/-- R&H's FOR-SURE-CommonGround analysis is canonically motivated by — and arguably restricted to — accent on finite verbs / auxiliaries (the prosodic-on-finite-verb subset). For M&N's other 11 structures (periphrastic *tun*, VP fronting, discourse particles, @@ -309,7 +309,7 @@ def romeroHanBestEffort : MNAttestedStructure → Option RHAnalysis | .serbianAccentedAuxiliary => some .epistemicVerum | _ => none -/-- R&H's FOR-SURE-CG analysis cannot encode at least 11 of M&N's 18 +/-- R&H's FOR-SURE-CommonGround analysis cannot encode at least 11 of M&N's 18 attested salient-polarity structures. The framework's analytic scope is the prosodic-on-finite-verb subset; everything else falls outside. -/ @@ -348,7 +348,7 @@ theorem gutzmann_2015_framework_does_not_apply : /-- The M&N argument is universal: at least 10 attested structures fall outside the substrate enum, at least 11 fall outside R&H's - FOR-SURE-CG, and all 18 fall outside Gutzmann 2015's sentence-mood + FOR-SURE-CommonGround, and all 18 fall outside Gutzmann 2015's sentence-mood UCIs. The structures inside the *intersection* of all three frameworks — the canonical prosodic verum focus on finite verbs — are exactly the cases all four traditions agree about; the diff --git a/Linglib/Studies/Ney2026.lean b/Linglib/Studies/Ney2026.lean index c256ebd95..cb653b84b 100644 --- a/Linglib/Studies/Ney2026.lean +++ b/Linglib/Studies/Ney2026.lean @@ -24,7 +24,7 @@ argument), and resolves the challenge by reading the conception of reasonableness as the *intersection* of the interlocutors' individual belief-sets — equivalently, the *union* of the hearer-profiles each agent counts as reasonable (§4 p. 22, revised statement p. 24). The -union is not CG-accessible because membership in it requires private +union is not CommonGround-accessible because membership in it requires private knowledge of either individual conception. ## Encoding choice (relative to @cite{ney-2026} pp. 22, 24) @@ -49,7 +49,7 @@ closures (∧-intro vs universal lift). We pick the hearer-profile encoding because it matches the verbatim revised statement and makes Ney's resolution structurally explicit: the *membership* facts for `RS ⊔ RH` require private knowledge of either RS or RH individually, -hence are not CG-transparent, hence the ``-`` chain breaks. +hence are not CommonGround-transparent, hence the ``-`` chain breaks. ## What this file formalizes vs. what it doesn't @@ -64,14 +64,14 @@ the intent is absent — @cite{ney-2026} §2 (17), the 4chan triple-parentheses case). The §3 prima-facie challenge is formalized abstractly: -`prima_facie_challenge` takes `inCG : Prop → Prop` and a CG-transparency +`prima_facie_challenge` takes `inCG : Prop → Prop` and a CommonGround-transparency hypothesis on the conception. Substantive Ney soundness — that the -resolution holds under a *realistic* CG operator derived from -`commonBelief` (@cite{stalnaker-2002}) — requires a `CG.toAgentAccess : -CG W → AgentAccessRel W E` bridge in `Discourse/CommonGround.lean` +resolution holds under a *realistic* CommonGround operator derived from +`commonBelief` (@cite{stalnaker-2002}) — requires a `CommonGround.toAgentAccess : +CommonGround W → AgentAccessRel W E` bridge in `Discourse/CommonGround.lean` that does not yet exist. Until that bridge lands, the resolution theorems are witnessed by toy operators (a degenerate `inCG := · = True` -that distinguishes intersection-CG-transparency from union-CG-transparency +that distinguishes intersection-CommonGround-transparency from union-CommonGround-transparency on a small carrier). ## Distinguishing the phenomenon (Ney 2026 §2) @@ -103,7 +103,7 @@ language* per @cite{beaver-stanley-2023}. ## Substrate primitives this file leans on (with citations) Imports `Reference.Basic` (@cite{kaplan-1989}'s Character/Content + -@cite{almog-2014}'s ReferentialProfile) and `Discourse.CommonGround` +@cite{almog-2014}'s ReferentialProfile) and `CommonGround` (@cite{stalnaker-2002}'s context set). `SpeakerIntention.intendedRef` parallels @cite{donnellan-1966}'s referential-use intended object; the broader speaker-intent structure connects to @cite{searle-1983} @@ -120,7 +120,7 @@ intentional states (not unified here). `C → E → Prop`. 2. `inCG : Prop → Prop` (here taken as hypothesis) should connect to `commonBelief` in `Semantics/Modality/EpistemicLogic.lean` - once a `CG.toAgentAccess` bridge exists. + once a `CommonGround.toAgentAccess` bridge exists. 3. `SpeakerIntention.intendedRef` parallel-stipulates with `Donnellan.DefiniteDescription.intendedRef`; not unified. @@ -138,7 +138,7 @@ the §5 conclusion proposes the broader "insinuative speech" terminology. namespace Ney2026 -open Semantics.Reference.Basic Discourse.CommonGround +open Semantics.Reference.Basic CommonGround /-! ## §1. Metasemantic apparatus -/ @@ -189,8 +189,8 @@ abbrev ConceptionOfReasonableness (C W E : Type*) := /-- A *metasemantics of demonstratives*: a recipe assigning each speaker intention a success Prop. -`Account` is intentionally CG-free (no `CG W` parameter): in -@cite{ney-2026}'s argument the CG-availability of the success-fact is +`Account` is intentionally CommonGround-free (no `CommonGround W` parameter): in +@cite{ney-2026}'s argument the CommonGround-availability of the success-fact is the load-bearing modal claim, formalized via the abstract `inCG` operator on the `prima_facie_challenge` theorem rather than threaded through every account-application. -/ @@ -314,45 +314,45 @@ paraphrased): > ⟨ONE⟩ A reasonable hearer would recognize the speaker's intention > to make the unavowed referent the semantic value of the > insinuatively-used supplementive (i.e., (B) is satisfied). -> ⟨TWO⟩ It is in CG that the actual hearer is competent, reasonable, +> ⟨TWO⟩ It is in CommonGround that the actual hearer is competent, reasonable, > and attentive (assumption). -> ⟨THREE⟩ It is in CG that the actual hearer recognizes that intention +> ⟨THREE⟩ It is in CommonGround that the actual hearer recognizes that intention > (from ONE + TWO). -> ⟨FOUR⟩ It is in CG that the unavowed referent is the semantic value +> ⟨FOUR⟩ It is in CommonGround that the unavowed referent is the semantic value > (from ONE + THREE). @cite{ney-2026} §3 (p. 17) shows two independent empirical claims that the chain's conclusions contradict: -- **(iia)**: post-utterance, it is NOT in CG that the unavowed referent +- **(iia)**: post-utterance, it is NOT in CommonGround that the unavowed referent IS the semantic value of the insinuatively-used supplementive. Witnessed by paper dialogues (2.2)-(2.5) (pp. 16–17): a hearer's indication of recognizing the semantic value licenses inferences about the hearer that wouldn't be felicitous if the recognition - were already CG. ⟨FOUR⟩ contradicts (iia). + were already CommonGround. ⟨FOUR⟩ contradicts (iia). -- **(iib)**: post-utterance, it is NOT in CG that the speaker had the +- **(iib)**: post-utterance, it is NOT in CommonGround that the speaker had the unavowed referential intention. Witnessed by paper dialogues (2.6)-(2.9): a hearer's indication of recognizing the speaker's intention licenses parallel inferences. ⟨THREE⟩ contradicts (iib). In our encoding, `coordination R s = ∀ h ∈ R, h s` packages "every -reasonable hearer recognizes" (= ⟨THREE⟩ when in CG, contra (iib)) -together with "success" (= ⟨FOUR⟩ when in CG, contra (iia)) — King's +reasonable hearer recognizes" (= ⟨THREE⟩ when in CommonGround, contra (iib)) +together with "success" (= ⟨FOUR⟩ when in CommonGround, contra (iia)) — King's biconditional makes them definitionally the same Prop. The empirical distinction between (iia) and (iib) is therefore documented at this level rather than encoded as separate Lean propositions. The chain only goes through if the universal "every reasonable hearer recognizes" claim — i.e., `coordination R s` for the relevant -conception R — is itself in CG. Under King's "objector" reading +conception R — is itself in CommonGround. Under King's "objector" reading (R = RS ⊓ RH), this is plausible: the intersection of belief-sets is publicly knowable. Under Ney's revision (R = RS ⊔ RH), it is *not*: membership in `RS ∪ RH` requires private knowledge of either individual conception. This is the asymmetry §5 below witnesses. -/ /-- Trivial form: if the universal recognition fact `coordination R s` -is in CG, then it's in CG. The substantive Ney content is in *which +is in CommonGround, then it's in CommonGround. The substantive Ney content is in *which R* makes this premise plausible — see `prima_facie_inter_witness` and `prima_facie_union_failure_witness` in §5. -/ theorem prima_facie_challenge {C W E : Type*} @@ -363,23 +363,23 @@ theorem prima_facie_challenge {C W E : Type*} inCG (coordination R s) := transparent -/-! ## §5. Ney's resolution: intersection is CG-transparent, union is not +/-! ## §5. Ney's resolution: intersection is CommonGround-transparent, union is not @cite{ney-2026}'s §4 resolution (pp. 22–24): the conception of reasonableness as the union of agents' hearer-profile-sets is *not* -CG-accessible — knowing whether a hearer is in `RS ∪ RH` requires +CommonGround-accessible — knowing whether a hearer is in `RS ∪ RH` requires private knowledge of either RS or RH individually. The intersection, by contrast, is the publicly-shared part of the conceptions and is -CG-accessible. +CommonGround-accessible. We exhibit this asymmetry as a single concrete model: a degenerate `inCG := (· = True)` operator (only logically-true propositions count -as "in CG") that returns `True` for the vacuous intersection-success +as "in CommonGround") that returns `True` for the vacuous intersection-success and `False` for the non-vacuous union-failure on a hand-built witness. CAVEAT: This is a toy operator. The substantive Ney claim — that the -asymmetry holds under a *realistic* CG operator derived from -`commonBelief` (@cite{stalnaker-2002}) — requires the `CG.toAgentAccess` +asymmetry holds under a *realistic* CommonGround operator derived from +`commonBelief` (@cite{stalnaker-2002}) — requires the `CommonGround.toAgentAccess` bridge that does not yet exist. -/ /-- A minimal speaker-intention witness over `Bool`: speaker `false`, @@ -395,12 +395,12 @@ private def boolWitness : SpeakerIntention Unit Unit Bool where private def alwaysRejectsProfile : HearerProfile Unit Unit Bool := fun _ => False -/-- The asymmetry @cite{ney-2026} §4 hinges on: there exists a CG +/-- The asymmetry @cite{ney-2026} §4 hinges on: there exists a CommonGround operator and a pair of conceptions where the intersection-success -*is* in CG while the union-success *is not*. Witness: `inCG := id` +*is* in CommonGround while the union-success *is not*. Witness: `inCG := id` (the trivial nonempty operator), `RS = ∅`, `RH = {alwaysRejectsProfile}`. The intersection is empty (success vacuous); the union contains a -hearer that rejects the intention (success false, not in CG). -/ +hearer that rejects the intention (success false, not in CommonGround). -/ theorem coordination_inter_in_cg_but_union_not : ∃ (inCG : Prop → Prop) (RS RH : ConceptionOfReasonableness Unit Unit Bool) @@ -421,7 +421,7 @@ fails (the union contains a non-recognizing hearer). CAVEAT: This extensional gap is incidental to @cite{ney-2026}'s substantive argument — Ney does not appeal to it. Ney's actual -argument is at the CG-availability level (§5 above), not the truth +argument is at the CommonGround-availability level (§5 above), not the truth level. The gap witness is included only to demonstrate that the two account-shapes differ extensionally; it is *not* a model of any @cite{ney-2026} sentence (in his canonical examples both interlocutors @@ -495,7 +495,7 @@ theorem anaphora_discriminator_ney_revision {C W E : Type*} In @cite{ney-2026}'s canonical examples, the speaker uses a demonstrative in a context licensing both an avowable referent and an unavowed referent; both interlocutors in fact recognize the -unavowed intention (the deniability lives at CG-availability, see §5 +unavowed intention (the deniability lives at CommonGround-availability, see §5 above). We model this with a permissive hearer-profile that recognizes the unavowed-or-avowable intention, attributed to both RS and RH. -/ @@ -636,7 +636,7 @@ theorem all_four_examples_have_insinuative_structure : /-- All four canonical sentences are jointly successful under both King's objector reconstruction (intersection) and Ney's revision (union) — the hearer in fact recognizes the unavowed intention; both -conceptions cover. The discriminator is at the CG-availability level +conceptions cover. The discriminator is at the CommonGround-availability level — see §4–§5 above. -/ theorem all_four_examples_are_jointly_successful : (coordination (Sentence1.scenario.RS ⊓ Sentence1.scenario.RH) @@ -750,7 +750,7 @@ disambiguation) but does NOT admit felicitous deniability. The first-pass response cannot distinguish them, hence over-generates. Ney's positive proposal (§5 above) localizes the asymmetry differently: the *conception* of reasonableness — specifically `RS ⊔ RH` — is not -CG-accessible. +CommonGround-accessible. The current encoding cannot fully express the empirical asymmetry ("Lennon has the structure but lacks deniability") because the diff --git a/Linglib/Studies/PullumGazdar1982.lean b/Linglib/Studies/PullumGazdar1982.lean index d3ff527a9..ac89f4b8e 100644 --- a/Linglib/Studies/PullumGazdar1982.lean +++ b/Linglib/Studies/PullumGazdar1982.lean @@ -200,7 +200,7 @@ open Symbol in Syntactic rules (29a): - A → BCD | CE - - C → BCF | CG | BH | I + - C → BCF | CommonGround | BH | I The grammar ensures each transitive verb has an NP argument and each intransitive verb does not, producing cross-serial NP-verb dependencies @@ -217,7 +217,7 @@ def dutchGrammar : ContextFreeGrammar DutchT where rules := { ⟨.A, [terminal .np, nonterminal .C, terminal .transInf]⟩, -- A → BCD ⟨.A, [nonterminal .C, terminal .intrans]⟩, -- A → CE ⟨.C, [terminal .np, nonterminal .C, terminal .trVPInf]⟩, -- C → BCF - ⟨.C, [nonterminal .C, terminal .inVPInf]⟩, -- C → CG + ⟨.C, [nonterminal .C, terminal .inVPInf]⟩, -- C → CommonGround ⟨.C, [terminal .np, terminal .trVPFin]⟩, -- C → BH ⟨.C, [terminal .inVPFin]⟩ } -- C → I diff --git a/Linglib/Studies/QingGoodmanLassiter2016.lean b/Linglib/Studies/QingGoodmanLassiter2016.lean index e788df954..90780de7b 100644 --- a/Linglib/Studies/QingGoodmanLassiter2016.lean +++ b/Linglib/Studies/QingGoodmanLassiter2016.lean @@ -161,10 +161,10 @@ theorem always_matches_continuation (w : WorldState) : (eq. 8). The paper's full model uses 15 non-empty subsets with 5% noise; the omitted 6 (e.g., `change = {(T,F),(F,T)}`) have negligible prior. -/ inductive ContextSet where - | pastTrue -- +past: CG entails John smoked - | pastFalse -- -past: CG entails John didn't smoke - | nowTrue -- +now: CG entails John smokes - | nowFalse -- -now: CG entails John doesn't smoke + | pastTrue -- +past: CommonGround entails John smoked + | pastFalse -- -past: CommonGround entails John didn't smoke + | nowTrue -- +now: CommonGround entails John smokes + | nowFalse -- -now: CommonGround entails John doesn't smoke | pastTrueNowTrue -- +past+now | pastTrueNowFalse -- +past-now | pastFalseNowTrue -- -past+now @@ -236,9 +236,9 @@ def utterancePrior : Utterance → ℚ theorem utterancePrior_nonneg (u : Utterance) : 0 ≤ utterancePrior u := by cases u <;> simp [utterancePrior] -/-- Context set prior (eq. 8): Pr(C) ∝ Σ_{CG⊆Obs} P(CG) · δ_{C=∩CG}. - Each observation enters CG independently with probability 0.4. - P(CG) = 0.4^|CG| × 0.6^(4-|CG|). +/-- Context set prior (eq. 8): Pr(C) ∝ Σ_{CommonGround⊆Obs} P(CommonGround) · δ_{C=∩CommonGround}. + Each observation enters CommonGround independently with probability 0.4. + P(CommonGround) = 0.4^|CommonGround| × 0.6^(4-|CommonGround|). - 0 observations (universe): 0.6^4 ∝ 9 - 1 observation (single): 0.4 × 0.6^3 ∝ 6 - 2 observations (pair): 0.4^2 × 0.6^2 ∝ 4 -/ @@ -256,7 +256,7 @@ theorem contextPrior_pos (cs : ContextSet) : 0 < contextPrior cs := by -- ============================================================================ /-- RSA model parameterized by QUD. The paper's final model uses QUD_now with - CG prior. + CommonGround prior. - L0: meaning = compatibility ∧ literal truth (eq. 5) - S1: utterancePrior × rpow(qudAggregate(L0), α) (eq. 6) @@ -278,13 +278,13 @@ noncomputable def cfg (qud : QUD) : RSA.RSAConfig Utterance WorldState where latentPrior _ cs := (contextPrior cs : ℝ) latentPrior_nonneg _ cs := Rat.cast_nonneg.mpr (le_of_lt (contextPrior_pos cs)) -/-- Final model: CG prior + QUD_now (paper's main prediction). -/ +/-- Final model: CommonGround prior + QUD_now (paper's main prediction). -/ noncomputable abbrev cfgNow := cfg .now -/-- Comparison model: CG prior + QUD_max. -/ +/-- Comparison model: CommonGround prior + QUD_max. -/ noncomputable abbrev cfgMax := cfg .max -/-- Comparison model: CG prior + QUD_past. -/ +/-- Comparison model: CommonGround prior + QUD_past. -/ noncomputable abbrev cfgPast := cfg .past -- ============================================================================ @@ -381,7 +381,7 @@ the speaker is much more likely to use "didn't stop" when the +past context holds, and L1 infers this. Figure 3 shows that (T,T) with context set +past is the unique maximum of the -joint distribution under CG prior + QUD_now. -/ +joint distribution under CommonGround prior + QUD_now. -/ set_option maxHeartbeats 3200000 in /-- **Context set projection**: L1 infers +past context over -past context. -/ diff --git a/Linglib/Studies/RitchieSchiller2024.lean b/Linglib/Studies/RitchieSchiller2024.lean index 45245427c..7746aa0f3 100644 --- a/Linglib/Studies/RitchieSchiller2024.lean +++ b/Linglib/Studies/RitchieSchiller2024.lean @@ -419,7 +419,7 @@ speaker and hearer derive the same DDRP. Different perceptual access yields different DDRPs, motivating R&S's requirement of perceptual co-presence. -/ open Core -open Discourse.CommonGround +open CommonGround /-- The RSA-BToM bridge applies to the domain restriction RSA config. -/ theorem rsa_btom_bridge (u : Utterance) (w : World) : diff --git a/Linglib/Studies/Roberts2023.lean b/Linglib/Studies/Roberts2023.lean index 3727beff4..ea188db70 100644 --- a/Linglib/Studies/Roberts2023.lean +++ b/Linglib/Studies/Roberts2023.lean @@ -138,7 +138,7 @@ restipulated) here. -/ @cite{portner-2018}'s `HasPOSWTarget IllocutionaryMood` instance: the imperative targets the preferential POSW component (= the addressee's preference structure), not the - informational component (= CG). + informational component (= CommonGround). This is the type-level shadow of "deontic force is pragmatic, not LF": deontic-style content lives where the preference @@ -157,7 +157,7 @@ theorem imperative_targets_preferential : (`¬ (· ).toPOSW.le w v`). The dual negative claim — that the **informational** component - (CG) is untouched — is `Scoreboard.direction_preserves_cg` (a + (CommonGround) is untouched — is `Scoreboard.direction_preserves_cg` (a `@[simp]` lemma). The two together discharge Roberts's claim that deontic content arises pragmatically via the preference structure rather than via assertion to common ground. diff --git a/Linglib/Studies/RomeroHan2004.lean b/Linglib/Studies/RomeroHan2004.lean index 40b9b2e10..e436981fb 100644 --- a/Linglib/Studies/RomeroHan2004.lean +++ b/Linglib/Studies/RomeroHan2004.lean @@ -8,7 +8,7 @@ import Linglib.Core.Word ## Core Contribution Preposed negation in yes/no questions forces an epistemic implicature via -the VERUM operator (FOR-SURE-CG). Ladd's PI/NI ambiguity is scope ambiguity: +the VERUM operator (FOR-SURE-CommonGround). Ladd's PI/NI ambiguity is scope ambiguity: - PI: [Q [not [VERUM [p]]]] → speaker believes p, double-checking - NI: [Q [VERUM [not [p]]]] → speaker believes ¬p, double-checking @@ -19,16 +19,16 @@ The VERUM operator is the conversational-epistemic mechanism: "For all worlds compatible with x's knowledge, for all worlds compatible with x's conversational goals, p is in the Common Ground." Short form: -"It is for sure that we should add p to the CG." +"It is for sure that we should add p to the CommonGround." ## Results -1. VERUM creates unbalanced partitions: {FOR-SURE-CG(p), ¬FOR-SURE-CG(p)} +1. VERUM creates unbalanced partitions: {FOR-SURE-CommonGround(p), ¬FOR-SURE-CommonGround(p)} rather than {p, ¬p}. 2. Ladd's PI/NI ambiguity is scope ambiguity over VERUM and negation. 3. Epistemic implicature follows from intent/pronunciation: - - Asserting ¬FOR-SURE-CG(p) (PI) implicates belief in p - - Asserting FOR-SURE-CG(¬p) (NI) implicates belief in ¬p + - Asserting ¬FOR-SURE-CommonGround(p) (PI) implicates belief in p + - Asserting FOR-SURE-CommonGround(¬p) (NI) implicates belief in ¬p ## Related Work @@ -76,19 +76,19 @@ structure VerumFrame (W : Type*) where epiAccessible : EpistemicAccessibility W /-- Conversational accessibility (Conv_x) -/ convAccessible : ConversationalAccessibility W - /-- Common Ground function: for each world, what's in the CG -/ + /-- Common Ground function: for each world, what's in the CommonGround -/ commonGround : W → List (W → Bool) -- Part 1.2: The VERUM Operator -/-- FOR-SURE-CG: The VERUM operator. +/-- FOR-SURE-CommonGround: The VERUM operator. ∀w' ∈ Epi_x(w)[∀w'' ∈ Conv_x(w')[p ∈ CG_w'']] For all epistemic alternatives w', for all conversational alternatives w'', p is in the Common Ground at w''. -This captures: "It is for sure that we should add p to the CG." +This captures: "It is for sure that we should add p to the CommonGround." -/ def forSureCG {W : Type*} (frame : VerumFrame W) (w : W) (p : W → Bool) : Bool := @@ -97,13 +97,13 @@ def forSureCG {W : Type*} (frame : VerumFrame W) frame.worlds.all λ w'' => if frame.convAccessible w' w'' then (frame.commonGround w'').any λ q => - frame.worlds.all λ v => p v == q v -- p ∈ CG means p equals some CG proposition + frame.worlds.all λ v => p v == q v -- p ∈ CommonGround means p equals some CommonGround proposition else true else true /-- Simplified VERUM for finite models -/ def verum {W : Type*} [DecidableEq W] - (cgMembership : W → (W → Bool) → Bool) -- Is p in CG at w? + (cgMembership : W → (W → Bool) → Bool) -- Is p in CommonGround at w? (epiWorlds : W → List W) -- Epi_x(w) (convWorlds : W → List W) -- Conv_x(w') (w : W) (p : W → Bool) : Bool := @@ -128,10 +128,10 @@ def balancedQuestion {W : Type*} (p : W → Bool) : QuestionPartition W := { pronounced := p } -/-- Unbalanced VERUM question: {FOR-SURE-CG(p), ¬FOR-SURE-CG(p)} +/-- Unbalanced VERUM question: {FOR-SURE-CommonGround(p), ¬FOR-SURE-CommonGround(p)} When VERUM is present, the partition is about epistemic commitment -to CG membership, not about p's truth directly. +to CommonGround membership, not about p's truth directly. -/ def verumQuestion {W : Type*} [DecidableEq W] (cgMembership : W → (W → Bool) → Bool) @@ -143,8 +143,8 @@ def verumQuestion {W : Type*} [DecidableEq W] cell1 := λ w => verum cgMembership epiWorlds convWorlds w p cell2 := λ w => !verum cgMembership epiWorlds convWorlds w p pronounced := if pronounceNeg - then λ w => !verum cgMembership epiWorlds convWorlds w p -- PI: ¬FOR-SURE-CG(p) - else λ w => verum cgMembership epiWorlds convWorlds w p -- NI: FOR-SURE-CG(p) + then λ w => !verum cgMembership epiWorlds convWorlds w p -- PI: ¬FOR-SURE-CommonGround(p) + else λ w => verum cgMembership epiWorlds convWorlds w p -- NI: FOR-SURE-CommonGround(p) } -- Part 1.4: Ladd's Ambiguity (PI vs NI) @@ -174,8 +174,8 @@ def NegQuestionLF.reading {W : Type*} : NegQuestionLF W → NegQuestionReading /-- Interpret a negative question LF as a partition -- PI: {¬FOR-SURE-CG(p), FOR-SURE-CG(p)} -- NI: {FOR-SURE-CG(¬p), ¬FOR-SURE-CG(¬p)} +- PI: {¬FOR-SURE-CommonGround(p), FOR-SURE-CommonGround(p)} +- NI: {FOR-SURE-CommonGround(¬p), ¬FOR-SURE-CommonGround(¬p)} -/ def interpretNegQuestion {W : Type*} [DecidableEq W] (cgMembership : W → (W → Bool) → Bool) @@ -184,10 +184,10 @@ def interpretNegQuestion {W : Type*} [DecidableEq W] (lf : NegQuestionLF W) : QuestionPartition W := match lf with | .piLF p => - -- PI: asking about ¬FOR-SURE-CG(p) + -- PI: asking about ¬FOR-SURE-CommonGround(p) verumQuestion cgMembership epiWorlds convWorlds p true | .niLF p => - -- NI: VERUM scopes over negation, asking about FOR-SURE-CG(¬p) + -- NI: VERUM scopes over negation, asking about FOR-SURE-CommonGround(¬p) let notP : W → Bool := λ w => !p w verumQuestion cgMembership epiWorlds convWorlds notP false @@ -204,8 +204,8 @@ structure SpeakerEpistemicState (W : Type*) where The pronounced cell of a VERUM question implicates the speaker's prior belief: -- PI pronounces ¬FOR-SURE-CG(p) → implicates belief in p -- NI pronounces FOR-SURE-CG(¬p) → implicates belief in ¬p +- PI pronounces ¬FOR-SURE-CommonGround(p) → implicates belief in p +- NI pronounces FOR-SURE-CommonGround(¬p) → implicates belief in ¬p -/ def epistemicImplicature {W : Type*} (reading : NegQuestionReading) @@ -230,7 +230,7 @@ inductive PolarityItem where /-- Check if polarity item is licensed under a reading -- PPIs licensed under PI reading (in scope of ¬FOR-SURE-CG) +- PPIs licensed under PI reading (in scope of ¬FOR-SURE-CommonGround) - NPIs licensed under NI reading (in scope of VERUM over negation) -/ def isLicensed (item : PolarityItem) (reading : NegQuestionReading) : Bool := @@ -475,8 +475,8 @@ def generalization2 : String := /-- Example: "Doesn't John drink?" (PI reading) LF: [Q [not [VERUM [John drinks]]]] -Partition: {¬FOR-SURE-CG(drinks(j)), FOR-SURE-CG(drinks(j))} -Pronounced: ¬FOR-SURE-CG(drinks(j)) +Partition: {¬FOR-SURE-CommonGround(drinks(j)), FOR-SURE-CommonGround(drinks(j))} +Pronounced: ¬FOR-SURE-CommonGround(drinks(j)) Implicature: Speaker believes John drinks -/ def examplePI : NegQuestionLF Unit := .piLF (λ () => true) @@ -484,8 +484,8 @@ def examplePI : NegQuestionLF Unit := .piLF (λ () => true) /-- Example: "Doesn't John drink?" (NI reading, with "either") LF: [Q [VERUM [not [John drinks]]]] -Partition: {FOR-SURE-CG(¬drinks(j)), ¬FOR-SURE-CG(¬drinks(j))} -Pronounced: FOR-SURE-CG(¬drinks(j)) +Partition: {FOR-SURE-CommonGround(¬drinks(j)), ¬FOR-SURE-CommonGround(¬drinks(j))} +Pronounced: FOR-SURE-CommonGround(¬drinks(j)) Implicature: Speaker believes John doesn't drink -/ def exampleNI : NegQuestionLF Unit := .niLF (λ () => true) diff --git a/Linglib/Studies/RonderosEtAl2024.lean b/Linglib/Studies/RonderosEtAl2024.lean index 991496dc7..0e350f0ec 100644 --- a/Linglib/Studies/RonderosEtAl2024.lean +++ b/Linglib/Studies/RonderosEtAl2024.lean @@ -146,7 +146,7 @@ is observable independent of any contrast manipulation. `LookProportion` satisfies the pattern — this would derive the Ronderos effects from the noise-discrimination ordering rather than observing structural alignment between two independently stipulated - orderings. The CG-style vanilla `IncrementalSemantics` (no noise + orderings. The CommonGround-style vanilla `IncrementalSemantics` (no noise channel) cannot satisfy `SatisfiesRonderosPattern` because it would predict equal contrast effects for all adjective types — a useful negative result that could itself be a theorem. diff --git a/Linglib/Studies/Rudin2025.lean b/Linglib/Studies/Rudin2025.lean index 55d0cb197..12e964bd7 100644 --- a/Linglib/Studies/Rudin2025.lean +++ b/Linglib/Studies/Rudin2025.lean @@ -30,7 +30,7 @@ predicates carry `[DecidablePred p]` constraints. namespace Rudin2025 -open Discourse.CommonGround +open CommonGround abbrev World := Fin 4 diff --git a/Linglib/Studies/Schlenker2009.lean b/Linglib/Studies/Schlenker2009.lean index 7a9fd0783..6a979b559 100644 --- a/Linglib/Studies/Schlenker2009.lean +++ b/Linglib/Studies/Schlenker2009.lean @@ -77,7 +77,7 @@ example : ProjectiveTrigger.appositive.toClass.ole = .notObligatory := rfl from the SCF x OLE feature space. -/ open Semantics.Presupposition -open Discourse.CommonGround +open CommonGround open Semantics.Presupposition.LocalContext open Semantics.Presupposition.TonhauserDerivation diff --git a/Linglib/Studies/SeeligerRepp2018.lean b/Linglib/Studies/SeeligerRepp2018.lean index e8e61573b..e5d0867d6 100644 --- a/Linglib/Studies/SeeligerRepp2018.lean +++ b/Linglib/Studies/SeeligerRepp2018.lean @@ -206,9 +206,9 @@ def DeclQuestionType.declPolarity : DeclQuestionType → Features.Polarity [ForceP FALSUM/VERUM [Force' REJECTQ [TP ...]]] FALSUM signals zero commitment to the proposition (the speaker is - essentially not committed to adding q to the CG). Used in NRQs. + essentially not committed to adding q to the CommonGround). Used in NRQs. VERUM signals full commitment (the speaker is sure q should be in - the CG). Used in PRQs. In PRQs, Swedish *visst*/*nog* or an + the CommonGround). Used in PRQs. In PRQs, Swedish *visst*/*nog* or an evidential version of VERUM may appear. These correspond to the operators defined in @@ -217,8 +217,8 @@ inductive IllocutionaryModifier where /-- FALSUM: zero commitment to q (non-propositional negation). @cite{repp-2013}: speaker is not committed to q at issue. -/ | falsum - /-- VERUM: full commitment to q (q should be in the CG). - @cite{romero-han-2004}: for-sure-CG that q should be added. -/ + /-- VERUM: full commitment to q (q should be in the CommonGround). + @cite{romero-han-2004}: for-sure-CommonGround that q should be added. -/ | verum deriving DecidableEq, Repr @@ -270,7 +270,7 @@ def IllocutionaryModifier.evidentialBias : IllocutionaryModifier → BiasValue /-- Derive the epistemic bias from the IM choice in REJECTQ. The epistemic presupposition is [IM(q)]^epist: - - IM = VERUM: speaker is epistemically sure q should be in CG + - IM = VERUM: speaker is epistemically sure q should be in CommonGround → epistemic [+positive] (speaker assumed q) - IM = FALSUM: speaker has zero epistemic commitment to q → epistemic [+negative] (by pragmatic strengthening in the diff --git a/Linglib/Studies/SolstadBott2024.lean b/Linglib/Studies/SolstadBott2024.lean index 7361f4f79..d90e10be0 100644 --- a/Linglib/Studies/SolstadBott2024.lean +++ b/Linglib/Studies/SolstadBott2024.lean @@ -62,7 +62,7 @@ open Phenomena.Presupposition.ProjectiveContent open SolstadBott2022 open Fragments.German.Predicates open Semantics.Presupposition -open Discourse.CommonGround +open CommonGround open Discourse.AtIssueness -- ════════════════════════════════════════════════════ diff --git a/Linglib/Studies/Stakov2026Typology.lean b/Linglib/Studies/Stakov2026Typology.lean index a5082a428..fb480f804 100644 --- a/Linglib/Studies/Stakov2026Typology.lean +++ b/Linglib/Studies/Stakov2026Typology.lean @@ -48,7 +48,7 @@ def NegPosition.biasStrength : NegPosition → EvidentialBiasStrength /-- Whether the negation position requires obligatory focus. Only outer negation (FALSUM) is obligatorily focused — it targets discourse -polarity and generates alternatives on whether p is or isn't in the CG +polarity and generates alternatives on whether p is or isn't in the CommonGround (Staňková §3.2, §4). -/ def NegPosition.requiresFocus : NegPosition → Bool | .outer => true diff --git a/Linglib/Studies/Stalnaker1975.lean b/Linglib/Studies/Stalnaker1975.lean index 3bc35be44..ff4c763f0 100644 --- a/Linglib/Studies/Stalnaker1975.lean +++ b/Linglib/Studies/Stalnaker1975.lean @@ -73,7 +73,7 @@ The two universal pragmatic postulates from the Appendix namespace Stalnaker1975 open Semantics.Mood (GramMood) -open Discourse.CommonGround (ContextSet) +open CommonGround (ContextSet) open _root_.Semantics.Conditionals (SelectionFunction) open Semantics.Conditionals open Dialogue.ReasonableInference @@ -254,7 +254,7 @@ substrate-level proof (the typeclass's narrowing law is sufficient). -/ open Discourse.SpeechAct (Assertable) -open Discourse.CommonGround (HasContextSet) +open CommonGround (HasContextSet) /-- **Bridge theorem**: Stalnaker's `changeFn` operator equals the `HasContextSet`-projection of `Assertable.speakerAssert` at the diff --git a/Linglib/Studies/VanDerLeer2026.lean b/Linglib/Studies/VanDerLeer2026.lean index 4b22d546e..b357b6c34 100644 --- a/Linglib/Studies/VanDerLeer2026.lean +++ b/Linglib/Studies/VanDerLeer2026.lean @@ -121,7 +121,7 @@ theorem assert_creates_commitment exact hcom.2 ⟨rfl, rfl⟩ /-- **T26** — under Sincerity + Competence, commitment transfers to - the addressee's belief. The mediated CG-update of @cite{bary-2025}. -/ + the addressee's belief. The mediated CommonGround-update of @cite{bary-2025}. -/ theorem committed_implies_belief_under_sincerity_competence {c : CommitmentState W A} (hsin : Sincere c) (hcomp : Competent c) (a b : A) (π : Set W) (w : W) : @@ -196,7 +196,7 @@ theorem assert_adds_to_DC assert_creates_commitment a b π C w /-- Under sincerity+competence, the addressee believes the asserted - `π` — the F&B "ASSERT enters CG" effect, mediated. -/ + `π` — the F&B "ASSERT enters CommonGround" effect, mediated. -/ theorem assert_enters_CG_under_sincerity_competence (a b : A) (π : Set W) (C : CommitmentSpace W A) (w : W) (hsin : Sincere (apply (SpeechAct.assert a b π) C).root) diff --git a/Linglib/Studies/Wang2025.lean b/Linglib/Studies/Wang2025.lean index a0c63cc4a..6836b844b 100644 --- a/Linglib/Studies/Wang2025.lean +++ b/Linglib/Studies/Wang2025.lean @@ -21,9 +21,9 @@ that derives Wang's three-way obligatoriness pattern. ### Experiment 1: Naturalness Judgments (9 triggers × 3 contexts) 9 Mandarin presupposition triggers tested in 3 context conditions: -- **Full**: CG fully entails the presupposition -- **Partial**: CG partially entails the presupposition -- **None**: CG does not support the presupposition +- **Full**: CommonGround fully entails the presupposition +- **Partial**: CommonGround partially entails the presupposition +- **None**: CommonGround does not support the presupposition ### Experiment 2: Polarity-Reversed Alternatives (4 triggers × 3 contexts) 4 triggers with polarity-reversed non-presuppositional alternatives: @@ -31,7 +31,7 @@ tests whether alternative structure affects felicity. ### Experiment 3: De Re Judgments Presuppositional triggers under attitude verbs: tests whether presuppositions -can be resolved de re (against CG) vs. de dicto (against attitude holder's +can be resolved de re (against CommonGround) vs. de dicto (against attitude holder's beliefs). ## Constraint-based Formalization @@ -42,19 +42,19 @@ Presuppositional sentences `S_p` compete with non-presuppositional alternatives 1. **IC** (Internal Coherence): `S_p`'s presupposition is consistent with its assertion. *Non-violable* — IC violation always blocks the presuppositional form. -2. **FP** (Felicity Presupposition): CG entails `S_p`'s presupposition. - *Violable* — partial CG support may be tolerated. -3. **MP** (Maximize Presupposition): prefer `S_p` over `S` when CG supports the +2. **FP** (Felicity Presupposition): CommonGround entails `S_p`'s presupposition. + *Violable* — partial CommonGround support may be tolerated. +3. **MP** (Maximize Presupposition): prefer `S_p` over `S` when CommonGround supports the presupposition and `S_p` is more informative. *Violable* — overridable by IC or FP violations. The ranking IC ≫ FP ≫ MP, together with the trigger's alternative structure (Wang's Table 4.1), derives three obligatoriness patterns: - **Obligatory** triggers (ye, you, reng): deletion alternatives — MP forces - use of the trigger when CG fully supports presupposition. + use of the trigger when CommonGround fully supports presupposition. - **Optional** triggers (buzai, kaishi): replacement alternatives — competitor is informative enough that MP doesn't strongly prefer the trigger. -- **Blocked** triggers (jiu, zhidao under partial CG): no alternative or +- **Blocked** triggers (jiu, zhidao under partial CommonGround): no alternative or replacement with stronger assertion — FP violation blocks the trigger. ## K Operator Interaction @@ -72,9 +72,9 @@ open Fragments.Mandarin.Particles (MandarinTrigger) /-- Context condition for presupposition support. -/ inductive ContextCondition where - | full -- CG fully entails the presupposition - | partialSupport -- CG partially entails the presupposition - | noSupport -- CG does not support the presupposition + | full -- CommonGround fully entails the presupposition + | partialSupport -- CommonGround partially entails the presupposition + | noSupport -- CommonGround does not support the presupposition deriving DecidableEq, Repr /-- A single naturalness judgment datum (Experiment 1). -/ @@ -89,7 +89,7 @@ structure Exp1Datum where felicity : Acceptability deriving Repr -/-- Experiment 1 key finding: ye/also is felicitous under full and partial CG. -/ +/-- Experiment 1 key finding: ye/also is felicitous under full and partial CommonGround. -/ def ye_full : Exp1Datum := { trigger := .ye, context := .full, meanRating := 62/10, felicity := .ok } @@ -99,7 +99,7 @@ def ye_partial : Exp1Datum := def ye_none : Exp1Datum := { trigger := .ye, context := .noSupport, meanRating := 28/10, felicity := .anomalous } -/-- Experiment 1 key finding: you/again is felicitous under full and partial CG. -/ +/-- Experiment 1 key finding: you/again is felicitous under full and partial CommonGround. -/ def you_full : Exp1Datum := { trigger := .you, context := .full, meanRating := 6, felicity := .ok } @@ -109,7 +109,7 @@ def you_partial : Exp1Datum := def you_none : Exp1Datum := { trigger := .you, context := .noSupport, meanRating := 25/10, felicity := .anomalous } -/-- Experiment 1 key finding: jiu/only is blocked under partial CG. -/ +/-- Experiment 1 key finding: jiu/only is blocked under partial CommonGround. -/ def jiu_full : Exp1Datum := { trigger := .jiu, context := .full, meanRating := 58/10, felicity := .ok } @@ -119,7 +119,7 @@ def jiu_partial : Exp1Datum := def jiu_none : Exp1Datum := { trigger := .jiu, context := .noSupport, meanRating := 22/10, felicity := .anomalous } -/-- Experiment 1 key finding: zhidao/know is blocked under partial CG. -/ +/-- Experiment 1 key finding: zhidao/know is blocked under partial CommonGround. -/ def zhidao_full : Exp1Datum := { trigger := .zhidao, context := .full, meanRating := 59/10, felicity := .ok } @@ -129,18 +129,18 @@ def zhidao_partial : Exp1Datum := def zhidao_none : Exp1Datum := { trigger := .zhidao, context := .noSupport, meanRating := 2, felicity := .anomalous } -/-- Key contrast: ye and jiu diverge under partial CG support. -/ +/-- Key contrast: ye and jiu diverge under partial CommonGround support. -/ theorem ye_jiu_partial_diverge : ye_partial.felicity ≠ jiu_partial.felicity := by decide -/-- Obligatory triggers are felicitous under both full and partial CG. -/ +/-- Obligatory triggers are felicitous under both full and partial CommonGround. -/ theorem obligatory_trigger_pattern : ye_full.felicity = .ok ∧ ye_partial.felicity = .ok ∧ ye_none.felicity = .anomalous := by exact ⟨rfl, rfl, rfl⟩ -/-- Blocked triggers are only felicitous under full CG. -/ +/-- Blocked triggers are only felicitous under full CommonGround. -/ theorem blocked_trigger_pattern : jiu_full.felicity = .ok ∧ jiu_partial.felicity = .anomalous ∧ @@ -154,7 +154,7 @@ theorem blocked_trigger_pattern : /-- Resolution locus for presupposition under attitude verbs. -/ inductive Resolution where - /-- Presupposition resolved against CG (de re) -/ + /-- Presupposition resolved against CommonGround (de re) -/ | deRe /-- Presupposition resolved against attitude holder's beliefs (de dicto) -/ | deDicto @@ -185,7 +185,7 @@ theorem additive_deRe_available : ye_deRe.accepted = true := rfl -- ============================================================================ open Semantics.Presupposition (PrProp) -open Discourse.CommonGround (ContextSet) +open CommonGround (ContextSet) /-- Local Bool-valued accessibility used by Wang2025 for `List.all` evaluation of the speaker-K operator. The Prop-valued canonical version lives in @@ -200,7 +200,7 @@ open Pragmatics.Expressives (ciLift) - IC (Internal Coherence): S_p's presupposition is consistent with its assertion. Non-violable. -- FP (Felicity Presupposition): S_p's presupposition is entailed by the CG. +- FP (Felicity Presupposition): S_p's presupposition is entailed by the CommonGround. Violable but ranked above MP. - MP (Maximize Presupposition): Prefer the presuppositional S_p over its non-presuppositional alternative S when context supports it. Violable. @@ -208,7 +208,7 @@ open Pragmatics.Expressives (ciLift) inductive PragConstraint where /-- Internal Coherence: presupposition consistent with assertion (non-violable) -/ | IC - /-- Felicity Presupposition: CG entails presupposition (violable) -/ + /-- Felicity Presupposition: CommonGround entails presupposition (violable) -/ | FP /-- Maximize Presupposition: prefer presuppositional form (violable) -/ | MP @@ -245,14 +245,14 @@ def satisfiesIC (p : PrProp W) : Prop := /-- FP (Felicity Presupposition): the common ground entails the presupposition. -Standard Stalnakerian presupposition satisfaction. When the CG only partially +Standard Stalnakerian presupposition satisfaction. When the CommonGround only partially entails the presupposition, FP is violated but may be tolerated. -/ def satisfiesFP (cg : ContextSet W) (p : PrProp W) : Prop := ∀ w, cg w → PrProp.defined w p /-- -Partial FP satisfaction: the presupposition is compatible with the CG +Partial FP satisfaction: the presupposition is compatible with the CommonGround but not fully entailed. @cite{wang-2025} Ch. 2-3: some triggers tolerate partial satisfaction (ye, you, reng) @@ -263,10 +263,10 @@ def partialFP (cg : ContextSet W) (p : PrProp W) : Prop := /-- MP (Maximize Presupposition): prefer S_p over S when the presuppositional -form is more informative and the CG supports its presupposition. +form is more informative and the CommonGround supports its presupposition. MP is violated when the non-presuppositional alternative S is used despite -the CG supporting S_p's presupposition. +the CommonGround supporting S_p's presupposition. -/ def mpPrefers (cg : ContextSet W) (sp : PrProp W) : Prop := satisfiesFP cg sp ∧ satisfiesIC sp @@ -284,48 +284,48 @@ Predict obligatoriness from alternative structure and context. def predictObligatoriness (altStr : AltStructure) (cgEntailsPresup : Bool) (cgPartialPresup : Bool) : Obligatoriness := match altStr, cgEntailsPresup, cgPartialPresup with - -- Full CG support: MP forces presuppositional form (obligatory) + -- Full CommonGround support: MP forces presuppositional form (obligatory) | .deletion, true, _ => .obligatory | .replacement, true, _ => .obligatory | .none, true, _ => .obligatory - -- Partial CG support with deletion alternative: still OK (obligatory/optional) + -- Partial CommonGround support with deletion alternative: still OK (obligatory/optional) | .deletion, false, true => .optional - -- Partial CG support with replacement: depends on alternative strength + -- Partial CommonGround support with replacement: depends on alternative strength | .replacement, false, true => .optional - -- Partial CG support with no alternative: blocked + -- Partial CommonGround support with no alternative: blocked | .none, false, true => .blocked - -- No CG support: blocked for all + -- No CommonGround support: blocked for all | _, false, false => .blocked /-- -Triggers with deletion alternatives remain felicitous under partial CG. +Triggers with deletion alternatives remain felicitous under partial CommonGround. @cite{wang-2025} Ch. 4: ye/also, you/again, reng/still have deletion alternatives, -so even when the CG only partially entails the presupposition, the +so even when the CommonGround only partially entails the presupposition, the presuppositional form is not blocked. -/ theorem deletion_alt_partial_resolution : predictObligatoriness .deletion false true = .optional := rfl /-- -Triggers with no structural alternative are blocked under partial CG. +Triggers with no structural alternative are blocked under partial CommonGround. @cite{wang-2025} Ch. 4: jiu/only has no non-presuppositional alternative, so -when the CG doesn't fully support the presupposition, the presuppositional +when the CommonGround doesn't fully support the presupposition, the presuppositional form cannot be used. -/ theorem no_alt_blocked_partial : predictObligatoriness .none false true = .blocked := rfl /-- -Full CG support always yields obligatoriness (for any alternative structure). +Full CommonGround support always yields obligatoriness (for any alternative structure). -/ theorem full_cg_obligatory (alt : AltStructure) (b : Bool) : predictObligatoriness alt true b = .obligatory := by cases alt <;> rfl /-- -No CG support always blocks (for any alternative structure). +No CommonGround support always blocks (for any alternative structure). -/ theorem no_cg_blocks (alt : AltStructure) : predictObligatoriness alt false false = .blocked := by @@ -374,9 +374,9 @@ structure WangInput (W : Type*) where sentence : PrProp W /-- The trigger's alternative structure -/ altStructure : AltStructure - /-- Whether CG fully entails the presupposition -/ + /-- Whether CommonGround fully entails the presupposition -/ cgFull : Bool - /-- Whether CG partially entails the presupposition -/ + /-- Whether CommonGround partially entails the presupposition -/ cgPartial : Bool /-- Whether the sentence is internally coherent -/ ic : Bool @@ -385,7 +385,7 @@ structure WangInput (W : Type*) where @cite{wang-2025} felicity check: evaluates constraint satisfaction. IC violation → odd (non-violable). Otherwise, obligatoriness prediction -from alternative structure and CG support determines the status. +from alternative structure and CommonGround support determines the status. -/ def wangCheck (input : WangInput W) : Acceptability := if !input.ic then @@ -397,11 +397,11 @@ def wangCheck (input : WangInput W) : Acceptability := | .blocked => .anomalous /-- -IC violation always yields oddness, regardless of CG support and alternative structure. +IC violation always yields oddness, regardless of CommonGround support and alternative structure. @cite{wang-2025}: IC is the only non-violable constraint. A sentence whose presupposition contradicts its assertion is always infelicitous, no matter -what the CG says or what alternatives exist. +what the CommonGround says or what alternatives exist. -/ theorem IC_violation_always_blocks (input : WangInput W) (hIC : input.ic = false) : wangCheck input = .anomalous := by @@ -413,9 +413,9 @@ theorem IC_violation_always_blocks (input : WangInput W) (hIC : input.ic = false -- ============================================================================ /-- -When CG entails the presupposition, the CI-lifted form yields a +When CommonGround entails the presupposition, the CI-lifted form yields a felicitous two-dimensional meaning where the CI content (presupposition) -is satisfied at all CG worlds. +is satisfied at all CommonGround worlds. This connects the constraint-based analysis to the CI bifurcation approach for de re presupposition. diff --git a/Linglib/Syntax/ConstructionGrammar/Studies/GoldbergShirtz2025.lean b/Linglib/Syntax/ConstructionGrammar/Studies/GoldbergShirtz2025.lean index 0f62472c6..93ac4928d 100644 --- a/Linglib/Syntax/ConstructionGrammar/Studies/GoldbergShirtz2025.lean +++ b/Linglib/Syntax/ConstructionGrammar/Studies/GoldbergShirtz2025.lean @@ -28,7 +28,7 @@ namespace ConstructionGrammar.Studies.GoldbergShirtz2025 open ConstructionGrammar open Semantics.Presupposition -open Discourse.CommonGround +open CommonGround open Pragmatics.Expressives /-! ## Section 1: PAL Construction definitions -/ @@ -154,7 +154,7 @@ def palConstructicon : Constructicon := /-! ## Section 2: Presupposition bridge Connect PAL's familiarity presupposition to Semantics.Presupposition and -Discourse.CommonGround infrastructure. -/ +CommonGround infrastructure. -/ /-- PAL presupposes the situation type is in the common ground. @@ -180,7 +180,7 @@ def palTwoDim (W : Type*) (atIssue : W → Prop) (familiar : W → Prop) : is satisfied. -/ theorem pal_presup_satisfied_by_cg (W : Type*) (situationType : W → Prop) (c : ContextSet W) - (h : c ⊧ situationType) : + (h : ContextSet.entails c situationType) : ∀ w, c w → (palPresupposition W situationType).presup w := h diff --git a/Linglib/Typology/PolarityMarking.lean b/Linglib/Typology/PolarityMarking.lean index 0c987aeaa..65497917f 100644 --- a/Linglib/Typology/PolarityMarking.lean +++ b/Linglib/Typology/PolarityMarking.lean @@ -53,7 +53,7 @@ keeps the form-class enum because (a) it has 8 cross-language consumers via TBD2014, (b) M&N's framework is one alternative among several — alongside @cite{hohle-1992}'s verum-as-illocutionary-operator (`Studies/Hohle1992.lean`), -@cite{romero-han-2004}'s epistemic-CONJ FOR-SURE-CG +@cite{romero-han-2004}'s epistemic-CONJ FOR-SURE-CommonGround (`Studies/RomeroHan2004.lean`), and @cite{gutzmann-2015}'s use-conditional sentence-mood operators (`Semantics/Mood/Gutzmann.lean` +