diff --git a/Linglib/Semantics/Modality/Exclusion.lean b/Linglib/Semantics/Modality/Exclusion.lean index 256160741..941106e72 100644 --- a/Linglib/Semantics/Modality/Exclusion.lean +++ b/Linglib/Semantics/Modality/Exclusion.lean @@ -59,7 +59,7 @@ namespace Semantics.Modality.Exclusion open Core.Context (KContext ContextTower ContextShift RichContext hpShift xMarkingShift DomainExpanding temporalShift) -open Semantics.Modality.HistoricalAlternatives (WorldHistory historicalBase) +open HistoricalAlternatives (historicalBase) open Semantics.Mood (subjShift) open Semantics.Reference.Kaplan (opActually_access opActually_shift_invariant) open Semantics.Tense (upperLimitConstraint) @@ -394,12 +394,12 @@ theorem domain_expansion_avoids_triviality backward time shift → the HP-shifted domain contains the original. Connects three layers: -1. `BranchingTime.WorldHistory.backwardsClosed` (semantic property) +1. `BranchingTime.HistoricalAlternatives.backwardsClosed` (semantic property) 2. `ConditionalShift.history_monotone_set` (set-level monotonicity) 3. `hpShift` installs the expanded domain -/ theorem oMarking_hpShift_expanding {W : Type*} {T : Type*} [Preorder T] - (history : WorldHistory W T) (h_bc : history.backwardsClosed) + (history : HistoricalAlternatives W T) (h_bc : history.backwardsClosed) (w₀ : W) (t₀ t' : T) (h_earlier : t' ≤ t₀) (D : Set W) (h_domain : D ⊆ history ⟨w₀, t₀⟩) : D ⊆ history ⟨w₀, t'⟩ := diff --git a/Linglib/Semantics/Modality/HistoricalAlternatives.lean b/Linglib/Semantics/Modality/HistoricalAlternatives.lean index 795264db5..39107f4aa 100644 --- a/Linglib/Semantics/Modality/HistoricalAlternatives.lean +++ b/Linglib/Semantics/Modality/HistoricalAlternatives.lean @@ -4,235 +4,169 @@ import Linglib.Core.WorldTimeIndex /-! # Historical Alternatives -@cite{condoravdi-2002} @cite{thomason-1984} @cite{cariani-santorio-2018} -@cite{klecha-2016} @cite{abusch-1997} - -Framework-agnostic relational structure on worlds: the **historical -alternatives** of a world at a time are the worlds that perfectly match -it in matters of particular fact up to that time -(@cite{lewis-1979}, @cite{cariani-santorio-2018}). This is the substrate -of the historical modal base used by metaphysical and future-oriented -modality. - -## Key Concepts - -1. **Partial history time predicates** — `isActualHistory`, - `isFutureHistory`, etc. The framework-neutral interval predicates - over `LE Time` / `LT Time` that index the situation-base slices. - Named for @cite{klecha-2016} Definition 3. -2. **World history function** — the relation between a ⟨world, time⟩ - point and the worlds that share its history up to that time. -3. **Historical/actual/future bases** — the three temporal slices of - the historical modal base, defined as situations whose time - component satisfies one of the partial-history predicates. -4. **Klecha 2016 ULC derivation** — the Upper Limit Constraint - (@cite{abusch-1997}) is *derived* from `actualHistoryBase` membership - by `.2` projection, rather than stipulated. -5. **Historical equivalence** — the equivalence relation `≃_t` of - @cite{condoravdi-2002} §4.1. -6. **Metaphysical modal base** — the equivalence class of the - evaluation world under `≃_t`. - -## What's not here - -This file is foundational: it commits to no specific modal theory -(Kratzer, Stalnaker selection, etc.). It defines the relational -substrate that any modal theory referring to "historical -alternatives" can use. The selectional semantics for *will* -(@cite{cariani-santorio-2018}) lives in -`Semantics/Modality/Selectional.lean`. + +The **historical alternatives** of a world at a time are the worlds that +perfectly match it in matters of particular fact up to that time +(@cite{lewis-1979}, @cite{cariani-santorio-2018}). + +## Main definitions + +* `HistoricalAlternatives` : the relation between a ⟨world, time⟩ index and the + worlds that share its history up to that time; +* `isActualHistory`, `isFutureHistory`, `isPastHistory`, `isProspectiveHistory`, + `isMaximalHistory` : interval predicates indexing the situation-base slices; +* `historicalBase`, `actualHistoryBase`, `futureHistoryBase` : the temporal + slices of the historical modal base; +* `histEquiv` : historical equivalence `≃_t` of @cite{condoravdi-2002}; +* `metaphysicalBase` : the equivalence class of the evaluation world under `≃_t`. + +## Main results + +* `upperLimitConstraintModal_implies_value` : the Upper Limit Constraint + (@cite{abusch-1997}) is derived from `actualHistoryBase` membership; +* `alternatives_antitone`, `metaphysicalBase_antitone` : the metaphysical base + shrinks as time advances; +* `settled_not_diverse` : settled properties block metaphysical readings. -/ open Core (WorldTimeIndex) -namespace Semantics.Modality.HistoricalAlternatives +/-- Historical-alternatives relation: given a ⟨world, time⟩ index, returns the + worlds that agree with that world up to that time. This is the basis for the + "historical" or "open future" modal base used in future-oriented modality. -/ +def HistoricalAlternatives (W Time : Type*) := WorldTimeIndex W Time → Set W + +namespace HistoricalAlternatives + +variable {W Time : Type*} /-! ## Partial History Taxonomy -@cite{klecha-2016} Definition 3 defines five kinds of partial history, -distinguished by the temporal component of the world-time pair relative -to a reference time `t`. We formalize all five as predicates on time -pairs. Only actual and future are used in the core DOX/CIR mechanism, -but the full taxonomy is needed for extensions (e.g., prospective is -the temporal component of `historicalBase` below). +@cite{klecha-2016} distinguishes five kinds of partial history by the temporal +component of the world-time pair relative to a reference time `t`. We formalize +all five as predicates on time pairs. Only actual and future drive the core +DOX/CIR mechanism, but the full taxonomy is needed for extensions (prospective +is the temporal component of `historicalBase` below). -These are framework-neutral interval predicates over `LE Time` / `LT Time`; -the @cite{klecha-2016} citation is for the terminology, not the -mathematical content (which is just `≤`, `<`, `>`, `≥`). -/ +These are framework-neutral interval predicates over `LE Time` / `LT Time`; the +@cite{klecha-2016} citation is for the terminology, not the mathematical content +(which is just `≤`, `<`, `>`, `≥`). -/ -/-- Maximal history: unrestricted temporal extent. - @cite{klecha-2016} Definition 3(v): Ω_t = all histories. -/ -def isMaximalHistory {Time : Type*} (_evalTime _historyTime : Time) : Prop := +/-- Maximal history: unrestricted temporal extent (Ω_t = all histories). -/ +def isMaximalHistory (_evalTime _historyTime : Time) : Prop := True -/-- Actual history: temporal component ends at or before `t`. - @cite{klecha-2016} Definition 3(vi): 𝒜_t = {i : τ(i) = (-∞, t]}. -/ -def isActualHistory {Time : Type*} [LE Time] - (evalTime historyTime : Time) : Prop := +/-- Actual history: temporal component ends at or before `t` (𝒜_t). -/ +def isActualHistory [LE Time] (evalTime historyTime : Time) : Prop := historyTime ≤ evalTime -/-- Past history: temporal component ends strictly before `t`. - @cite{klecha-2016} Definition 3(viii): 𝒫_t = {i : τ(i) = (-∞, t)}. +/-- Past history: temporal component ends strictly before `t` (𝒫_t). Distinct from actual: past excludes `t` itself. -/ -def isPastHistory {Time : Type*} [LT Time] - (evalTime historyTime : Time) : Prop := +def isPastHistory [LT Time] (evalTime historyTime : Time) : Prop := historyTime < evalTime -/-- Future history: temporal component starts strictly after `t`. - @cite{klecha-2016} Definition 3(vii): ℱ_t = {j : τ(j) = (t, ∞)}. -/ -def isFutureHistory {Time : Type*} [LT Time] - (evalTime historyTime : Time) : Prop := +/-- Future history: temporal component starts strictly after `t` (ℱ_t). -/ +def isFutureHistory [LT Time] (evalTime historyTime : Time) : Prop := historyTime > evalTime -/-- Prospective history: temporal component starts at or after `t`. - @cite{klecha-2016} Definition 3(ix): ℙ_t = {j : τ(j) = [t, ∞)}. - This is exactly the temporal component of `historicalBase` below: - `s'.time ≥ s.time`. -/ -def isProspectiveHistory {Time : Type*} [LE Time] - (evalTime historyTime : Time) : Prop := +/-- Prospective history: temporal component starts at or after `t` (ℙ_t). + This is exactly the temporal component of `historicalBase`. -/ +def isProspectiveHistory [LE Time] (evalTime historyTime : Time) : Prop := historyTime ≥ evalTime /-- Actual and future histories are complementary: every time is either ≤ t (actual) or > t (future). -/ -theorem actual_future_complementary {Time : Type*} [LinearOrder Time] +theorem actual_future_complementary [LinearOrder Time] (evalTime historyTime : Time) : isActualHistory evalTime historyTime ∨ isFutureHistory evalTime historyTime := (lt_or_ge evalTime historyTime).elim Or.inr Or.inl /-- Past and prospective histories are complementary: every time is either < t (past) or ≥ t (prospective). -/ -theorem past_prospective_complementary {Time : Type*} [LinearOrder Time] +theorem past_prospective_complementary [LinearOrder Time] (evalTime historyTime : Time) : isPastHistory evalTime historyTime ∨ isProspectiveHistory evalTime historyTime := (lt_or_ge historyTime evalTime).elim Or.inl Or.inr /-- Past ⊂ actual: strict past implies actual. -/ -theorem past_implies_actual {Time : Type*} [Preorder Time] +theorem past_implies_actual [Preorder Time] (evalTime historyTime : Time) (h : isPastHistory evalTime historyTime) : isActualHistory evalTime historyTime := le_of_lt h /-- Future ⊂ prospective: strict future implies prospective. -/ -theorem future_implies_prospective {Time : Type*} [Preorder Time] +theorem future_implies_prospective [Preorder Time] (evalTime historyTime : Time) (h : isFutureHistory evalTime historyTime) : isProspectiveHistory evalTime historyTime := le_of_lt h /-- Actual ∩ prospective = simultaneous: a time that is both actual and prospective is exactly the evaluation time. -/ -theorem actual_and_prospective_iff_simultaneous {Time : Type*} [PartialOrder Time] +theorem actual_and_prospective_iff_simultaneous [PartialOrder Time] (evalTime historyTime : Time) : isActualHistory evalTime historyTime ∧ isProspectiveHistory evalTime historyTime ↔ historyTime = evalTime := ⟨λ ⟨hle, hge⟩ => le_antisymm hle hge, λ h => ⟨le_of_eq h, ge_of_eq h⟩⟩ /-- Past and future are disjoint: no time is both < t and > t. -/ -theorem past_future_disjoint {Time : Type*} [Preorder Time] +theorem past_future_disjoint [Preorder Time] (evalTime historyTime : Time) : ¬(isPastHistory evalTime historyTime ∧ isFutureHistory evalTime historyTime) := by intro ⟨h1, h2⟩ exact lt_asymm h1 h2 +/-! ## Situation Bases -/ -/-! ## World History Functions and Situation Bases -/ - -/-- -World history function: given a world and time, returns worlds that -agree with that world up to that time. - -This is the basis for the "historical" or "open future" modal base -used in future-oriented modality. - -Intuition: At time t in world w, multiple futures are possible. -The historical alternatives are all worlds that share the same -past with w up to t. --/ -def WorldHistory (W Time : Type*) := WorldTimeIndex W Time → Set W - -/-- -Historical modal base: situations whose worlds agree with s up to τ(s), -and whose times are at or after τ(s). - -Following @cite{thomason-1984} and @cite{condoravdi-2002}: -- Past is fixed (determined) -- Future branches (open) - -hist(s) = {s' : w_{s'} ∈ H(wₛ, τ(s)) ∧ τ(s') ≥ τ(s)} --/ -def historicalBase {W Time : Type*} [LE Time] - (history : WorldHistory W Time) +/-- Historical modal base: situations whose worlds agree with `s` up to τ(s), + and whose times are at or after τ(s). Past is fixed, the future branches + (@cite{thomason-1984}, @cite{condoravdi-2002}). -/ +def historicalBase [LE Time] + (history : HistoricalAlternatives W Time) (s : WorldTimeIndex W Time) : Set (WorldTimeIndex W Time) := { s' | s'.world ∈ history s ∧ isProspectiveHistory s.time s'.time } -/-- -Actual history base (@cite{klecha-2016} DOX): situations whose worlds -agree with `s` and whose times are at or before τ(s). - -This is the temporal mirror of `historicalBase` (which uses ≥). -DOX returns actual histories — world-time pairs where the temporal -component ends at the evaluation time: 𝒜_t = {i : τ(i) = (-∞, t]}. --/ -def actualHistoryBase {W Time : Type*} [LE Time] - (history : WorldHistory W Time) +/-- Actual history base (@cite{klecha-2016} DOX): situations whose worlds agree + with `s` and whose times are at or before τ(s) — the temporal mirror of + `historicalBase`. -/ +def actualHistoryBase [LE Time] + (history : HistoricalAlternatives W Time) (s : WorldTimeIndex W Time) : Set (WorldTimeIndex W Time) := { s' | s'.world ∈ history s ∧ isActualHistory s.time s'.time } -/-- -Future history base (@cite{klecha-2016} CIR): situations whose worlds -agree with `s` and whose times are strictly after τ(s). - -CIR returns future histories — world-time pairs where the temporal -component departs from the evaluation time: ℱ_t = {j : τ(j) = (t, ∞)}. --/ -def futureHistoryBase {W Time : Type*} [LT Time] - (history : WorldHistory W Time) +/-- Future history base (@cite{klecha-2016} CIR): situations whose worlds agree + with `s` and whose times are strictly after τ(s). -/ +def futureHistoryBase [LT Time] + (history : HistoricalAlternatives W Time) (s : WorldTimeIndex W Time) : Set (WorldTimeIndex W Time) := { s' | s'.world ∈ history s ∧ isFutureHistory s.time s'.time } -/-- -A world history is reflexive if every world agrees with itself. --/ -def WorldHistory.reflexive {W Time : Type*} (h : WorldHistory W Time) : Prop := +/-- A historical-alternatives relation is reflexive if every world agrees with + itself. -/ +def reflexive (h : HistoricalAlternatives W Time) : Prop := ∀ s : WorldTimeIndex W Time, s.world ∈ h s -/-- -A world history is symmetric: if w' agrees with w up to t, -then w agrees with w' up to t. - -@cite{condoravdi-2002} §4.1, condition (i): ≃_t is an equivalence -relation for all t. Symmetry ensures historical equivalence is -bidirectional — "sharing a history" is a mutual relationship. --/ -def WorldHistory.symmetric {W Time : Type*} - (h : WorldHistory W Time) : Prop := +/-- A historical-alternatives relation is symmetric: if `w'` agrees with `w` up + to `t`, then `w` agrees with `w'` up to `t`. Part of `≃_t` being an + equivalence relation (@cite{condoravdi-2002}). -/ +def symmetric (h : HistoricalAlternatives W Time) : Prop := ∀ (w w' : W) (t : Time), w' ∈ h ⟨w, t⟩ → w ∈ h ⟨w', t⟩ -/-- -A world history is transitive: if w' agrees with w up to t -and w'' agrees with w' up to t, then w'' agrees with w up to t. --/ -def WorldHistory.transitive {W Time : Type*} - (h : WorldHistory W Time) : Prop := +/-- A historical-alternatives relation is transitive: if `w'` agrees with `w` up + to `t` and `w''` agrees with `w'` up to `t`, then `w''` agrees with `w` up + to `t`. -/ +def transitive (h : HistoricalAlternatives W Time) : Prop := ∀ (w w' w'' : W) (t : Time), w' ∈ h ⟨w, t⟩ → w'' ∈ h ⟨w', t⟩ → w'' ∈ h ⟨w, t⟩ -/-- -A world history is backwards-closed: if w' agrees with w up to t, -and t' ≤ t, then w' agrees with w up to t'. - -"If two worlds agree up to time t, they also agree up to any earlier time." -@cite{condoravdi-2002} §4.1, condition (ii). --/ -def WorldHistory.backwardsClosed {W Time : Type*} [LE Time] - (h : WorldHistory W Time) : Prop := +/-- A historical-alternatives relation is backwards-closed: if `w'` agrees with + `w` up to `t` and `t' ≤ t`, then `w'` agrees with `w` up to `t'` + (@cite{condoravdi-2002}). -/ +def backwardsClosed [LE Time] (h : HistoricalAlternatives W Time) : Prop := ∀ (w w' : W) (t t' : Time), t' ≤ t → w' ∈ h ⟨w, t⟩ → w' ∈ h ⟨w, t'⟩ -/-- -Standard historical modal base properties. -@cite{condoravdi-2002} §4.1: ≃_t is an equivalence relation (i) that -is monotone in time (ii). --/ -structure HistoricalProperties {W Time : Type*} [LE Time] - (h : WorldHistory W Time) : Prop where +/-- Standard historical modal base properties: `≃_t` is an equivalence relation + that is monotone in time (@cite{condoravdi-2002}). -/ +structure HistoricalProperties [LE Time] + (h : HistoricalAlternatives W Time) : Prop where /-- Every world agrees with itself -/ refl : h.reflexive /-- Historical agreement is symmetric -/ @@ -242,146 +176,110 @@ structure HistoricalProperties {W Time : Type*} [LE Time] /-- Agreement is preserved for earlier times -/ backwards : h.backwardsClosed - -/-- -A temporal proposition: true or false at each situation. - -This is the situation-semantic analog of Prop' W. --/ +/-- A temporal proposition: true or false at each situation. The + situation-semantic analog of `Prop' W`. -/ abbrev TProp (W Time : Type*) := WorldTimeIndex W Time → Prop -/-- -Lift a world proposition to a temporal proposition. - -The lifted proposition is true at situation s iff the original -proposition is true at s.world. --/ -def liftProp {W Time : Type*} (p : W → Prop) : TProp W Time := +/-- Lift a world proposition to a temporal proposition, true at situation `s` + iff the original holds at `s.world`. -/ +def liftProp (p : W → Prop) : TProp W Time := λ s => p s.world -/-- -A proposition holds at time t in world w. --/ -def holdsAt {W Time : Type*} (p : TProp W Time) (w : W) (t : Time) : Prop := +/-- A proposition holds at time `t` in world `w`. -/ +def holdsAt (p : TProp W Time) (w : W) (t : Time) : Prop := p ⟨w, t⟩ - /-! ## Klecha 2016: ULC derived from history structure -The Upper Limit Constraint — embedded RT under a doxastic attitude -must be ≤ matrix EvalT — was stated by @cite{abusch-1997} §7 ("the -now of an epistemic alternative is an upper limit for the denotation -of tenses"), with the presuppositional construal due to -@cite{heim-1994-comments} and endorsed by Abusch 1997 fn 20. -@cite{klecha-2016} §4.2 *derives* the same constraint from the -temporal character of the doxastic modal base: DOX returns actual -histories 𝒜_t (Klecha eq 35a); membership in 𝒜_t entails RT ≤ t by -`.2` projection through the situation-base definition. Symmetrically, -CIR returns ℱ_t and membership entails RT > t. The theorems below -make the projection kernel-checked. +The Upper Limit Constraint — embedded RT under a doxastic attitude must be +≤ matrix EvalT — was stated by @cite{abusch-1997} ("the now of an epistemic +alternative is an upper limit for the denotation of tenses"), with the +presuppositional construal due to @cite{heim-1994-comments}. +@cite{klecha-2016} *derives* the same constraint from the temporal character of +the doxastic modal base: DOX returns actual histories 𝒜_t, and membership +entails RT ≤ t by `.2` projection through the situation-base definition. +Symmetrically, CIR returns ℱ_t and membership entails RT > t. The theorems +below make the projection kernel-checked. This is what distinguishes @cite{klecha-2016}'s account from -@cite{abusch-1997}'s ("identical in spirit, if not in implementation" -per Klecha §4.2): both rely on the branching-futures motivation, but -Klecha derives ULC from history structure while Abusch -states it as a constraint on tense-node denotation. The -Klecha-namespace dispatch on `ModalBaseKind` lives in -`Semantics/Modality/TemporalConstraint.lean`. - -**Note:** the modal-alternative quantification in Abusch's formulation -("the now of an *epistemic alternative*") is captured here at the -substrate level by `WorldHistory` membership; the value-level -projection `s'.time ≤ s.time` recovers Abusch's bare-`≤` form. -/ - -/-- A situation in `historicalBase` has prospective time: - `s' ∈ historicalBase h s → isProspectiveHistory s.time s'.time`. -/ -theorem historicalBase_time_prospective {W Time : Type*} [LE Time] - (history : WorldHistory W Time) (s s' : WorldTimeIndex W Time) +@cite{abusch-1997}'s: both rely on the branching-futures motivation, but Klecha +derives ULC from history structure while Abusch states it as a constraint on +tense-node denotation. The Klecha-namespace dispatch on `ModalBaseKind` lives in +`Semantics/Modality/TemporalConstraint.lean`. The modal-alternative +quantification in Abusch's formulation is captured here at the substrate level +by `HistoricalAlternatives` membership; the value-level projection +`s'.time ≤ s.time` recovers Abusch's bare-`≤` form. -/ + +/-- A situation in `historicalBase` has prospective time. -/ +theorem historicalBase_time_prospective [LE Time] + (history : HistoricalAlternatives W Time) (s s' : WorldTimeIndex W Time) (h : s' ∈ historicalBase history s) : isProspectiveHistory s.time s'.time := h.2 -/-- A situation in `actualHistoryBase` has actual time: - `s' ∈ actualHistoryBase h s → isActualHistory s.time s'.time`. -/ -theorem actualHistoryBase_time_actual {W Time : Type*} [LE Time] - (history : WorldHistory W Time) (s s' : WorldTimeIndex W Time) +/-- A situation in `actualHistoryBase` has actual time. -/ +theorem actualHistoryBase_time_actual [LE Time] + (history : HistoricalAlternatives W Time) (s s' : WorldTimeIndex W Time) (h : s' ∈ actualHistoryBase history s) : isActualHistory s.time s'.time := h.2 -/-- Modal-layer Upper Limit Constraint (@cite{abusch-1997}'s - formulation that quantifies over doxastic alternatives, NOT just - times). An embedded situation `s'` satisfies the modal-layer ULC - relative to a matrix situation `s` and a doxastic accessibility - `history` iff `s'` is a member of `s`'s actual-history base - (i.e., `s'` agrees with `s` on world history up to `s.time`, and - `s'.time ≤ s.time`). - - The value-level `Semantics/Tense/Basic.lean.upperLimitConstraint` - is the `.2`-projection of this modal-layer formulation; the - `world` component of the conjunction is what carries the - doxastic-alternative quantification Abusch's original prose - statement requires. -/ -def upperLimitConstraintModal {W Time : Type*} [LE Time] - (history : WorldHistory W Time) +/-- Modal-layer Upper Limit Constraint: an embedded situation `s'` satisfies it + relative to a matrix situation `s` and doxastic accessibility `history` iff + `s'` lies in `s`'s actual-history base. See the section note for how this + recovers @cite{abusch-1997}'s alternative-quantifying formulation. -/ +def upperLimitConstraintModal [LE Time] + (history : HistoricalAlternatives W Time) (matrixSituation embeddedSituation : WorldTimeIndex W Time) : Prop := embeddedSituation ∈ actualHistoryBase history matrixSituation -/-- The modal-layer Upper Limit Constraint implies the value-level - one (`embeddedSituation.time ≤ matrixSituation.time`). The proof - is `.2` projection through the `actualHistoryBase` definition. - This is the structural soundness lemma justifying the value-level - `Semantics/Tense/Basic.lean.upperLimitConstraint` as a - faithful reduction of @cite{abusch-1997}'s modal formulation. -/ -theorem upperLimitConstraintModal_implies_value {W Time : Type*} [LE Time] - (history : WorldHistory W Time) +/-- The modal-layer Upper Limit Constraint implies the value-level one + (`embeddedSituation.time ≤ matrixSituation.time`), by `.2` projection + through `actualHistoryBase`. -/ +theorem upperLimitConstraintModal_implies_value [LE Time] + (history : HistoricalAlternatives W Time) (s s' : WorldTimeIndex W Time) (h : upperLimitConstraintModal history s s') : s'.time ≤ s.time := h.2 -/-- A situation in `futureHistoryBase` has future time: - `s' ∈ futureHistoryBase h s → isFutureHistory s.time s'.time`. -/ -theorem futureHistoryBase_time_future {W Time : Type*} [LT Time] - (history : WorldHistory W Time) (s s' : WorldTimeIndex W Time) +/-- A situation in `futureHistoryBase` has future time. -/ +theorem futureHistoryBase_time_future [LT Time] + (history : HistoricalAlternatives W Time) (s s' : WorldTimeIndex W Time) (h : s' ∈ futureHistoryBase history s) : isFutureHistory s.time s'.time := h.2 /-- `futureHistoryBase ⊆ historicalBase`: future situations are prospective. - This is the situation-semantic instantiation of `future_implies_prospective`. -/ -theorem futureHistoryBase_subset_historicalBase {W Time : Type*} [Preorder Time] - (history : WorldHistory W Time) (s : WorldTimeIndex W Time) : + The situation-semantic instantiation of `future_implies_prospective`. -/ +theorem futureHistoryBase_subset_historicalBase [Preorder Time] + (history : HistoricalAlternatives W Time) (s : WorldTimeIndex W Time) : futureHistoryBase history s ⊆ historicalBase history s := λ _ ⟨hw, ht⟩ => ⟨hw, le_of_lt ht⟩ -/-- `actualHistoryBase ∩ historicalBase` contains only simultaneous situations: - if `s'.time ≤ s.time` and `s'.time ≥ s.time`, then `s'.time = s.time`. - This is the situation-semantic instantiation of +/-- `actualHistoryBase ∩ historicalBase` contains only simultaneous situations. + The situation-semantic instantiation of `actual_and_prospective_iff_simultaneous`. -/ -theorem actualBase_inter_historicalBase_simultaneous {W Time : Type*} [PartialOrder Time] - (history : WorldHistory W Time) (s s' : WorldTimeIndex W Time) +theorem actualBase_inter_historicalBase_simultaneous [PartialOrder Time] + (history : HistoricalAlternatives W Time) (s s' : WorldTimeIndex W Time) (hActual : s' ∈ actualHistoryBase history s) (hHist : s' ∈ historicalBase history s) : s'.time = s.time := le_antisymm hActual.2 hHist.2 -/-- Actual and future history bases are disjoint on the time component: - no situation can have time both ≤ t and > t. - This is the situation-semantic instantiation of `past_future_disjoint` - (actual ∩ future = ∅ since actual ⊃ past). -/ -theorem actualBase_futureBase_disjoint {W Time : Type*} [Preorder Time] - (history : WorldHistory W Time) (s s' : WorldTimeIndex W Time) : +/-- Actual and future history bases are disjoint on the time component. + The situation-semantic instantiation of `past_future_disjoint`. -/ +theorem actualBase_futureBase_disjoint [Preorder Time] + (history : HistoricalAlternatives W Time) (s s' : WorldTimeIndex W Time) : ¬(s' ∈ actualHistoryBase history s ∧ s' ∈ futureHistoryBase history s) := by intro ⟨⟨_, hle⟩, ⟨_, hgt⟩⟩ exact lt_irrefl _ (lt_of_lt_of_le hgt hle) -/-- Every situation is in `actualHistoryBase ∪ futureHistoryBase` (on the time - component): for any `s'`, either `s'.time ≤ s.time` or `s'.time > s.time`. - This is the situation-semantic instantiation of +/-- Every situation is in `actualHistoryBase ∪ futureHistoryBase` on the time + component. The situation-semantic instantiation of `actual_future_complementary`. -/ -theorem actualBase_futureBase_complementary {W Time : Type*} [LinearOrder Time] - (history : WorldHistory W Time) (s s' : WorldTimeIndex W Time) +theorem actualBase_futureBase_complementary [LinearOrder Time] + (history : HistoricalAlternatives W Time) (s s' : WorldTimeIndex W Time) (hw : s'.world ∈ history s) : s' ∈ actualHistoryBase history s ∨ s' ∈ futureHistoryBase history s := (le_or_gt s'.time s.time).elim @@ -389,10 +287,9 @@ theorem actualBase_futureBase_complementary {W Time : Type*} [LinearOrder Time] (λ h => Or.inr ⟨hw, h⟩) /-- Converse: prospective time + world agreement → membership in - `historicalBase`. The time predicate fully characterizes the temporal - component of the base. -/ -theorem prospective_time_mem_historicalBase {W Time : Type*} [LE Time] - (history : WorldHistory W Time) (s s' : WorldTimeIndex W Time) + `historicalBase`. -/ +theorem prospective_time_mem_historicalBase [LE Time] + (history : HistoricalAlternatives W Time) (s s' : WorldTimeIndex W Time) (hw : s'.world ∈ history s) (ht : isProspectiveHistory s.time s'.time) : s' ∈ historicalBase history s := @@ -400,8 +297,8 @@ theorem prospective_time_mem_historicalBase {W Time : Type*} [LE Time] /-- Converse: actual time + world agreement → membership in `actualHistoryBase`. -/ -theorem actual_time_mem_actualHistoryBase {W Time : Type*} [LE Time] - (history : WorldHistory W Time) (s s' : WorldTimeIndex W Time) +theorem actual_time_mem_actualHistoryBase [LE Time] + (history : HistoricalAlternatives W Time) (s s' : WorldTimeIndex W Time) (hw : s'.world ∈ history s) (ht : isActualHistory s.time s'.time) : s' ∈ actualHistoryBase history s := @@ -409,8 +306,8 @@ theorem actual_time_mem_actualHistoryBase {W Time : Type*} [LE Time] /-- Converse: future time + world agreement → membership in `futureHistoryBase`. -/ -theorem future_time_mem_futureHistoryBase {W Time : Type*} [LT Time] - (history : WorldHistory W Time) (s s' : WorldTimeIndex W Time) +theorem future_time_mem_futureHistoryBase [LT Time] + (history : HistoricalAlternatives W Time) (s s' : WorldTimeIndex W Time) (hw : s'.world ∈ history s) (ht : isFutureHistory s.time s'.time) : s' ∈ futureHistoryBase history s := @@ -418,23 +315,19 @@ theorem future_time_mem_futureHistoryBase {W Time : Type*} [LT Time] /-! ## Historical Equivalence -@cite{condoravdi-2002} §4.1: historical equivalence ≃_t groups worlds -that share the same history up to time t. The equivalence classes are -the "ways things might have gone" — worlds that agree on the past but -may diverge in the future. -/ - -variable {W Time : Type*} +@cite{condoravdi-2002}: historical equivalence `≃_t` groups worlds that share +the same history up to time `t`. The equivalence classes are the "ways things +might have gone" — worlds that agree on the past but may diverge in the future. -/ /-- Historical equivalence: `w'` agrees with `w` up to time `t`. `w ≃_t w'` iff `w' ∈ history(w, t)`. -/ -def histEquiv (history : WorldHistory W Time) (t : Time) +def histEquiv (history : HistoricalAlternatives W Time) (t : Time) (w w' : W) : Prop := w' ∈ history ⟨w, t⟩ -/-- `histEquiv history t` is an equivalence relation when `history` - satisfies the standard properties. This is the content of - @cite{condoravdi-2002} §4.1, condition (i). -/ -def histEquiv_equivalence {history : WorldHistory W Time} +/-- `histEquiv history t` is an equivalence relation when `history` satisfies the + standard properties (@cite{condoravdi-2002}). -/ +def histEquiv_equivalence {history : HistoricalAlternatives W Time} (hRefl : history.reflexive) (hSymm : history.symmetric) (hTrans : history.transitive) (t : Time) : Equivalence (histEquiv history t) where @@ -443,38 +336,38 @@ def histEquiv_equivalence {history : WorldHistory W Time} trans h₁ h₂ := hTrans _ _ _ t h₁ h₂ /-- The `Setoid` induced by historical equivalence at time `t`. -/ -def histSetoid {history : WorldHistory W Time} +def histSetoid {history : HistoricalAlternatives W Time} (hRefl : history.reflexive) (hSymm : history.symmetric) (hTrans : history.transitive) (t : Time) : Setoid W where r := histEquiv history t iseqv := histEquiv_equivalence hRefl hSymm hTrans t /-- `histEquiv_equivalence` from bundled `HistoricalProperties`. -/ -def histEquiv_equivalence' {history : WorldHistory W Time} [LE Time] +def histEquiv_equivalence' {history : HistoricalAlternatives W Time} [LE Time] (hp : HistoricalProperties history) (t : Time) : Equivalence (histEquiv history t) := histEquiv_equivalence hp.refl hp.symm hp.trans t /-- `histSetoid` from bundled `HistoricalProperties`. -/ -def histSetoid' {history : WorldHistory W Time} [LE Time] +def histSetoid' {history : HistoricalAlternatives W Time} [LE Time] (hp : HistoricalProperties history) (t : Time) : Setoid W := histSetoid hp.refl hp.symm hp.trans t -/-- Historical equivalence is reflexive (from `WorldHistory.reflexive`). -/ -theorem histEquiv_refl {history : WorldHistory W Time} +/-- Historical equivalence is reflexive (from `reflexive`). -/ +theorem histEquiv_refl {history : HistoricalAlternatives W Time} (hRefl : history.reflexive) (t : Time) (w : W) : histEquiv history t w w := hRefl ⟨w, t⟩ -/-- Historical equivalence is symmetric (from `WorldHistory.symmetric`). -/ -theorem histEquiv_symm {history : WorldHistory W Time} +/-- Historical equivalence is symmetric (from `symmetric`). -/ +theorem histEquiv_symm {history : HistoricalAlternatives W Time} (hSymm : history.symmetric) (t : Time) {w w' : W} (h : histEquiv history t w w') : histEquiv history t w' w := hSymm w w' t h -/-- Historical equivalence is transitive (from `WorldHistory.transitive`). -/ -theorem histEquiv_trans {history : WorldHistory W Time} +/-- Historical equivalence is transitive (from `transitive`). -/ +theorem histEquiv_trans {history : HistoricalAlternatives W Time} (hTrans : history.transitive) (t : Time) {w w' w'' : W} (h₁ : histEquiv history t w w') (h₂ : histEquiv history t w' w'') : @@ -482,22 +375,18 @@ theorem histEquiv_trans {history : WorldHistory W Time} hTrans w w' w'' t h₁ h₂ variable [LE Time] in -/-- Historical equivalence is monotone in time: agreement up to a later - time implies agreement up to an earlier time - (from `WorldHistory.backwardsClosed`). -/ -theorem histEquiv_mono {history : WorldHistory W Time} +/-- Historical equivalence is monotone in time: agreement up to a later time + implies agreement up to an earlier time (from `backwardsClosed`). -/ +theorem histEquiv_mono {history : HistoricalAlternatives W Time} (hBC : history.backwardsClosed) {t t' : Time} (w w' : W) (hle : t' ≤ t) (h : histEquiv history t w w') : histEquiv history t' w w' := hBC w w' t t' hle h variable [LE Time] in -/-- @cite{condoravdi-2002} §4.1: "as time advances the set of - metaphysical alternatives to any given world decreases." - - The function `t ↦ { w' | w ≃_t w' }` is antitone: later times - yield smaller (or equal) equivalence classes. -/ -theorem alternatives_antitone {history : WorldHistory W Time} +/-- The set of metaphysical alternatives shrinks as time advances + (@cite{condoravdi-2002}): `t ↦ { w' | w ≃_t w' }` is antitone. -/ +theorem alternatives_antitone {history : HistoricalAlternatives W Time} (hBC : history.backwardsClosed) (w : W) {t t' : Time} (hle : t ≤ t') : { w' | histEquiv history t' w w' } ⊆ @@ -506,20 +395,20 @@ theorem alternatives_antitone {history : WorldHistory W Time} /-! ## Metaphysical Modal Base -@cite{condoravdi-2002} §4.1: for modals expressing metaphysical modality, -the modal base consists of historical alternatives: `MB(w,t) = {w' | w ≃_t w'}`. -This is the maximal modal base compatible with the world's history up to `t`. -/ +@cite{condoravdi-2002}: for modals expressing metaphysical modality, the modal +base consists of historical alternatives `MB(w,t) = {w' | w ≃_t w'}` — the +maximal modal base compatible with the world's history up to `t`. -/ -/-- The metaphysical modal base: at world `w` and time `t`, the set of - all worlds sharing `w`'s history up to `t`. -/ -def metaphysicalBase (history : WorldHistory W Time) : +/-- The metaphysical modal base: at world `w` and time `t`, the set of all worlds + sharing `w`'s history up to `t`. -/ +def metaphysicalBase (history : HistoricalAlternatives W Time) : W → Time → Set W := λ w t => { w' | histEquiv history t w w' } variable [LE Time] in -/-- The metaphysical modal base is antitone in time: later times yield - smaller accessible sets. -/ -theorem metaphysicalBase_antitone {history : WorldHistory W Time} +/-- The metaphysical modal base is antitone in time: later times yield smaller + accessible sets. -/ +theorem metaphysicalBase_antitone {history : HistoricalAlternatives W Time} (hBC : history.backwardsClosed) (w : W) {t t' : Time} (hle : t ≤ t') : metaphysicalBase history w t' ⊆ metaphysicalBase history w t := @@ -527,42 +416,31 @@ theorem metaphysicalBase_antitone {history : WorldHistory W Time} /-! ## Settledness and Diversity -@cite{condoravdi-2002} §4.1: an issue is **settled** at time t₀ when - all historically equivalent worlds agree on its resolution. - Past and present issues are always settled; future issues may not be. - - The **diversity condition** [45] is the felicity condition for - associating a metaphysical modal base with a possibility modal: - the modal base must contain worlds that disagree on the property. -/ - -/-- Settledness [44]: within each equivalence class of the common ground, - the property `P` is resolved uniformly — all historically equivalent - worlds agree on whether `P` holds. +@cite{condoravdi-2002}: an issue is **settled** at time `t₀` when all historically +equivalent worlds agree on its resolution; past and present issues are always +settled, future issues may not be. The **diversity condition** is the felicity +condition for associating a metaphysical modal base with a possibility modal: the +base must contain worlds that disagree on the property. -/ - @cite{condoravdi-2002}: "the past and the present are settled." -/ -def settled (history : WorldHistory W Time) (cg : Set W) +/-- Settledness: within each common-ground equivalence class, the property `P` is + resolved uniformly — all historically equivalent worlds agree on `P`. -/ +def settled (history : HistoricalAlternatives W Time) (cg : Set W) (t₀ : Time) (P : W → Prop) : Prop := ∀ w ∈ cg, ∀ w', histEquiv history t₀ w w' → (P w ↔ P w') -/-- Diversity Condition [45]: there exists a world in the common ground - whose modal base contains worlds that disagree on `P`. - - This is the felicity condition for associating a metaphysical modal - base with a possibility modal applying to property `P`. Without - diversity, the modal assertion would be equivalent to a non-modal - assertion, violating the distinctness requirement. -/ +/-- Diversity condition: there is a common-ground world whose modal base contains + worlds disagreeing on `P`. The felicity condition for pairing a metaphysical + modal base with a possibility modal (@cite{condoravdi-2002}). -/ def diverse (MB : W → Time → Set W) (cg : Set W) (t : Time) (P : W → Prop) : Prop := ∃ w ∈ cg, ∃ w' ∈ MB w t, ∃ w'' ∈ MB w t, P w' ∧ ¬ P w'' -/-- When `MB(w,t) ⊆ {w' | w ≃_t w'}` (the metaphysical case) and `P` is - settled, diversity fails: all worlds in the modal base agree on `P`, - so no pair can witness disagreement. - - This is the key theorem blocking metaphysical readings for settled - properties. -/ +/-- When `MB(w,t) ⊆ {w' | w ≃_t w'}` (the metaphysical case) and `P` is settled, + diversity fails: all worlds in the modal base agree on `P`, so no pair can + witness disagreement. The key theorem blocking metaphysical readings for + settled properties. -/ theorem settled_not_diverse - (history : WorldHistory W Time) (MB : W → Time → Set W) + (history : HistoricalAlternatives W Time) (MB : W → Time → Set W) (cg : Set W) (t : Time) (P : W → Prop) (hMB : ∀ w ∈ cg, ∀ w' ∈ MB w t, histEquiv history t w w') (hSettled : settled history cg t P) : @@ -572,9 +450,9 @@ theorem settled_not_diverse have heq'' := hSettled w hwcg w'' (hMB w hwcg w'' hw''MB) exact hnPw'' (heq''.mp (heq'.mpr hPw')) -/-- Diversity is witnessed by the common ground: if `P` holds for some - world in `cg` and fails for another, and both are accessible from - some `w` via `MB`, then diversity holds. -/ +/-- Diversity is witnessed by the common ground: if `P` holds for some world in + `cg` and fails for another, both accessible from some `w` via `MB`, then + diversity holds. -/ theorem diverse_of_witnesses (MB : W → Time → Set W) (cg : Set W) (t : Time) (P : W → Prop) (w : W) (hwcg : w ∈ cg) @@ -583,4 +461,4 @@ theorem diverse_of_witnesses diverse MB cg t P := ⟨w, hwcg, w', hw', w'', hw'', hP, hnP⟩ -end Semantics.Modality.HistoricalAlternatives +end HistoricalAlternatives diff --git a/Linglib/Semantics/Modality/Selectional.lean b/Linglib/Semantics/Modality/Selectional.lean index 9e3598654..96d580555 100644 --- a/Linglib/Semantics/Modality/Selectional.lean +++ b/Linglib/Semantics/Modality/Selectional.lean @@ -64,7 +64,7 @@ set_option autoImplicit false namespace Semantics.Modality.Selectional open _root_.Semantics.Conditionals (SelectionFunction) -open _root_.Semantics.Modality.HistoricalAlternatives +open HistoricalAlternatives open scoped ENNReal variable {W : Type*} @@ -286,7 +286,7 @@ Selectional `will` parameterized by the metaphysical modal base of the prejacent at the world selected from the metaphysical modal base at ⟨w, t⟩. -/ def willHistorical {Time : Type*} (s : SelectionFunction W) - (history : WorldHistory W Time) (A : W → Prop) + (history : HistoricalAlternatives W Time) (A : W → Prop) (w : W) (t : Time) : Prop := willSem s A (metaphysicalBase history w t) w @@ -294,7 +294,7 @@ def willHistorical {Time : Type*} (s : SelectionFunction W) @cite{condoravdi-2002} §4.1 condition (i)), `willHistorical` collapses to its prejacent: `will_t A` at `w` reduces to `A w`. -/ theorem willHistorical_reflexive_collapse {Time : Type*} - (s : SelectionFunction W) {history : WorldHistory W Time} + (s : SelectionFunction W) {history : HistoricalAlternatives W Time} (hRefl : history.reflexive) (A : W → Prop) (w : W) (t : Time) : willHistorical s history A w t ↔ A w := by unfold willHistorical diff --git a/Linglib/Semantics/Modality/TemporalConstraint.lean b/Linglib/Semantics/Modality/TemporalConstraint.lean index c923571ff..8485012b9 100644 --- a/Linglib/Semantics/Modality/TemporalConstraint.lean +++ b/Linglib/Semantics/Modality/TemporalConstraint.lean @@ -17,7 +17,7 @@ bridges from `Attitude` / `ModalFlavor` to `ModalBaseKind`. The framework-neutral interval predicates (`isActualHistory`, `isFutureHistory`, etc.) and the situation-base derivation theorems live -in `Semantics.Modality.HistoricalAlternatives`. This file's role is the +in `HistoricalAlternatives`. This file's role is the Klecha-specific projection: dispatch on `ModalBaseKind` to select between the actual-history (RT ≤ EvalT) and future-history (RT > EvalT) constraints. @@ -33,7 +33,7 @@ in the modal base pronoun: The ULC is **derived** by `.2` projection from `actualHistoryBase` membership (see `actualHistoryBase_derives_ulc` in -`Semantics.Modality.HistoricalAlternatives`); the dispatch theorem +`HistoricalAlternatives`); the dispatch theorem `attitudeTemporalConstraint_derived_doxastic` below makes the Klecha-namespace face of that derivation kernel-checked. -/ @@ -41,10 +41,9 @@ Klecha-namespace face of that derivation kernel-checked. namespace Semantics.Modality.TemporalConstraint open Semantics.Modality (ModalBaseKind) -open Semantics.Modality.HistoricalAlternatives +open HistoricalAlternatives (isActualHistory isFutureHistory actualHistoryBase futureHistoryBase - actualHistoryBase_time_actual futureHistoryBase_time_future - WorldHistory) + actualHistoryBase_time_actual futureHistoryBase_time_future) /-! ## Temporal Constraints on Embedded RT -/ @@ -127,7 +126,7 @@ DOX, `futureHistoryBase` for CIR), not stipulated. This is the formal contrast with @cite{abusch-1997}'s ULC, which is stipulated as a presupposition on T-nodes; here, ULC follows by `.2` projection through the situation-base definition. The substrate -derivation lives in `Semantics.Modality.HistoricalAlternatives` as +derivation lives in `HistoricalAlternatives` as `actualHistoryBase_time_actual` / `futureHistoryBase_time_future`; these theorems re-express it in the Klecha-namespace `attitudeTemporalConstraint` form. -/ @@ -137,7 +136,7 @@ these theorems re-express it in the Klecha-namespace constraint (Upper Limit Constraint) by `.2` projection. -/ theorem attitudeTemporalConstraint_derived_doxastic {W Time : Type*} [LinearOrder Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (s s' : Core.WorldTimeIndex W Time) (h : s' ∈ actualHistoryBase history s) : attitudeTemporalConstraint .doxastic s.time s'.time := @@ -148,7 +147,7 @@ theorem attitudeTemporalConstraint_derived_doxastic temporal constraint (future orientation) by `.2` projection. -/ theorem attitudeTemporalConstraint_derived_circumstantial {W Time : Type*} [LinearOrder Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (s s' : Core.WorldTimeIndex W Time) (h : s' ∈ futureHistoryBase history s) : attitudeTemporalConstraint .circumstantial s.time s'.time := diff --git a/Linglib/Semantics/Mood/Basic.lean b/Linglib/Semantics/Mood/Basic.lean index ebcccf89b..af12c3e3b 100644 --- a/Linglib/Semantics/Mood/Basic.lean +++ b/Linglib/Semantics/Mood/Basic.lean @@ -45,7 +45,7 @@ namespace Semantics.Mood open Core (WorldTimeIndex) open Core.Time -open Semantics.Modality.HistoricalAlternatives +open HistoricalAlternatives /-- @@ -86,7 +86,7 @@ The subjunctive: Analogous to an indefinite for situations. -/ def SUBJ {W Time : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (P : SitPred W Time) (s₀ : WorldTimeIndex W Time) : Prop := ∃ s₁ : WorldTimeIndex W Time, @@ -220,7 +220,7 @@ This explains why SF enables future reference: the subjunctive introduces a future situation that the main clause can refer back to. -/ def conditionalSF {W Time : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (antecedent : WorldTimeIndex W Time → Prop) -- "Maria is home" (consequent : WorldTimeIndex W Time → WorldTimeIndex W Time → Prop) -- "she answers" (s₀ : WorldTimeIndex W Time) : Prop := @@ -245,7 +245,7 @@ def conditionalIND {W Time : Type*} SUBJ is existential: it introduces a situation. -/ theorem subj_is_existential {W Time : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (P : SitPred W Time) (s₀ : WorldTimeIndex W Time) : SUBJ history P s₀ → ∃ s₁, P s₁ s₀ := by @@ -257,7 +257,7 @@ SUBJ constrains to historical base: the introduced situation is in the historical alternatives. -/ theorem subj_in_hist {W Time : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (P : SitPred W Time) (s₀ : WorldTimeIndex W Time) : SUBJ history P s₀ → ∃ s₁, s₁ ∈ historicalBase history s₀ ∧ P s₁ s₀ := by @@ -279,7 +279,7 @@ SUBJ with reflexive history: if the history is reflexive, the current situation is always an option. -/ theorem subj_current_option {W Time : Type*} [Preorder Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (h_refl : history.reflexive) (P : SitPred W Time) (s₀ : WorldTimeIndex W Time) @@ -313,7 +313,7 @@ This follows from the existential nature of SUBJ: it quantifies over situations in the historical base, which includes non-actual futures. -/ theorem subj_nonveridical {W Time : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) -- Need: history has an option distinct from the evaluation point (h_branching : ∃ s₀ s₁ : WorldTimeIndex W Time, s₁ ∈ historicalBase history s₀ ∧ s₀ ≠ s₁) : @@ -359,7 +359,7 @@ section AttitudeTemporalAnchor perspective time shifts to the matrix event time. Both mechanisms create a new temporal reference point for embedded evaluation. -/ theorem subj_temporal_anchor {W Time : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (P : SitPred W Time) (s₀ : WorldTimeIndex W Time) (h : SUBJ history P s₀) : @@ -428,7 +428,7 @@ theorem subjShift_preserves_agent {E P : Type*} This is the bridge between the existential `SUBJ` and the tower `push`. -/ theorem subj_as_tower_push [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (Q : SitPred W Time) (s₀ : WorldTimeIndex W Time) : SUBJ history Q s₀ ↔ diff --git a/Linglib/Semantics/Mood/Dynamic.lean b/Linglib/Semantics/Mood/Dynamic.lean index 95e6bcf14..d4607a2ee 100644 --- a/Linglib/Semantics/Mood/Dynamic.lean +++ b/Linglib/Semantics/Mood/Dynamic.lean @@ -75,7 +75,7 @@ operator and the modal donkey anaphora chain that consumes namespace Semantics.Mood open _root_.Core (Assignment WorldTimeIndex) -open Semantics.Modality.HistoricalAlternatives +open HistoricalAlternatives open Semantics.Dynamic.Core @@ -102,7 +102,7 @@ every `s₁ ∈ historicalBase history s₀`. The current situation is updated to the freshly drawn `s₁`, and `v` is bound to it. -/ def dynSUBJ {W Time : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (v : SVar) : SitContext W Time → SitContext W Time := dynIntroduce (historicalBase history) v @@ -117,7 +117,7 @@ theorem dynIND_eq_dynRelationOn_sameWorld {W Time : Type*} dynRelationOn (fun gs => gs.2) (fun gs => gs.1 v) sameWorld c := rfl theorem dynSUBJ_eq_dynIntroduce_historicalBase {W Time : Type*} [LE Time] - (history : WorldHistory W Time) (v : SVar) (c : SitContext W Time) : + (history : HistoricalAlternatives W Time) (v : SVar) (c : SitContext W Time) : dynSUBJ history v c = dynIntroduce (historicalBase history) v c := rfl @@ -153,7 +153,7 @@ theorem dynIND_idempotent {W Time : Type*} /-- SUBJ is existential over the historical base. Inherited from `dynIntroduce_current_in_gen`. -/ theorem dynSUBJ_existential {W Time : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (v : SVar) (c : SitContext W Time) (gs : Assignment (WorldTimeIndex W Time) × WorldTimeIndex W Time) @@ -164,7 +164,7 @@ theorem dynSUBJ_existential {W Time : Type*} [LE Time] /-- After `dynSUBJ`, looking up `v` always returns the current situation. Inherited from `dynIntroduce_binds_current`. -/ theorem dynSUBJ_binds_current {W Time : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (v : SVar) (c : SitContext W Time) (gs : Assignment (WorldTimeIndex W Time) × WorldTimeIndex W Time) @@ -212,7 +212,7 @@ set rather than just an existential iff. The output of `dynSUBJ` on `s₁ ∈ historicalBase history s₀`. -/ theorem dynSUBJ_singleton_eq {W Time : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (v : SVar) (g : Assignment (WorldTimeIndex W Time)) (s₀ : WorldTimeIndex W Time) : @@ -236,7 +236,7 @@ For a singleton context `{(g, s₀)}`, the set of situations reachable via `SUBJ` existentially quantifies over. -/ theorem dynSUBJ_realizes_SUBJ {W Time : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (v : SVar) (g : Assignment (WorldTimeIndex W Time)) (s₀ : WorldTimeIndex W Time) @@ -265,7 +265,7 @@ on `v` is trivially satisfied — `gs.2 = s₁ = gs.1 v` by shared variables preserves the full SUBJ output. -/ theorem dynIND_after_dynSUBJ_same_var {W Time : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (v : SVar) (c : SitContext W Time) : dynIND v (dynSUBJ history v c) = dynSUBJ history v c := by diff --git a/Linglib/Semantics/Tense/Basic.lean b/Linglib/Semantics/Tense/Basic.lean index 8393f4423..32dd645f0 100644 --- a/Linglib/Semantics/Tense/Basic.lean +++ b/Linglib/Semantics/Tense/Basic.lean @@ -392,7 +392,7 @@ ULC: embedded R' ≤ matrix E (= embedded P). **Note on faithfulness:** the value-level reduction `embeddedR ≤ matrixE` strips the modal-alternative quantification Abusch's formulation carries (the "now of an epistemic alternative" quantifies over -doxastic alternatives). A modal-layer formulation (over `WorldHistory +doxastic alternatives). A modal-layer formulation (over `HistoricalAlternatives W Time`, à la @cite{klecha-2016}'s `actualHistoryBase`) would be more faithful to the original; deferred future work. -/ diff --git a/Linglib/Semantics/Tense/ConditionalShift.lean b/Linglib/Semantics/Tense/ConditionalShift.lean index 15828f17c..dc647313a 100644 --- a/Linglib/Semantics/Tense/ConditionalShift.lean +++ b/Linglib/Semantics/Tense/ConditionalShift.lean @@ -37,7 +37,7 @@ open Core (WorldTimeIndex) open Core.Time open Core.Context (RichContext KContext ContextTower ContextShift hpShift DomainExpanding) -open Semantics.Modality.HistoricalAlternatives +open HistoricalAlternatives open Semantics.Mood -- ════════════════════════════════════════════════════════════════ @@ -95,7 +95,7 @@ variable {W : Type*} {T : Type*} [Preorder T] O-marking (Non-Past / HP) in Japanese Anderson conditionals expands the domain without X-marking. -/ theorem hp_achieves_expansion - (history : WorldHistory W T) + (history : HistoricalAlternatives W T) (h_bc : history.backwardsClosed) (s₀ : WorldTimeIndex W T) (t' : T) (h_earlier : t' ≤ s₀.time) (w : W) (hw : w ∈ history s₀) : @@ -111,7 +111,7 @@ theorem hp_achieves_expansion evaluation time backward, and backward time yields more historical alternatives, i.e., domain expansion. -/ theorem history_monotone_set - (history : WorldHistory W T) + (history : HistoricalAlternatives W T) (h_bc : history.backwardsClosed) (s₀ : WorldTimeIndex W T) (t' : T) (h_earlier : t' ≤ s₀.time) : (history s₀ : Set W) ⊆ (history ⟨s₀.world, t'⟩ : Set W) := @@ -121,7 +121,7 @@ theorem history_monotone_set situations with the same worlds as the later base, plus potentially more. This is the situation-level version of domain expansion. -/ theorem historicalBase_monotone - (history : WorldHistory W T) + (history : HistoricalAlternatives W T) (h_bc : history.backwardsClosed) (s₀ : WorldTimeIndex W T) (t' : T) (h_earlier : t' ≤ s₀.time) (s₁ : WorldTimeIndex W T) (h_s₁ : s₁ ∈ historicalBase history s₀) @@ -252,7 +252,7 @@ variable {W : Type*} {T : Type*} [Preorder T] When the history is backwards-closed, SUBJ at an earlier time introduces a situation whose world is in the expanded historical alternatives. -/ theorem subj_subsumes_hp_expansion - (history : WorldHistory W T) + (history : HistoricalAlternatives W T) (P : WorldTimeIndex W T → WorldTimeIndex W T → Prop) (s : WorldTimeIndex W T) (h : SUBJ history P s) : diff --git a/Linglib/Semantics/Tense/DeRe.lean b/Linglib/Semantics/Tense/DeRe.lean index e67fa3449..a5ccfe8c8 100644 --- a/Linglib/Semantics/Tense/DeRe.lean +++ b/Linglib/Semantics/Tense/DeRe.lean @@ -50,7 +50,7 @@ live in `Studies/Abusch1997.lean`. shadow this file connects to (the deleted `TemporalDeRe` triple was a shadow of *this* shadow; see the `isFelicitousWith_iff_…` theorem below for the bridge). -- `Semantics.Modality.HistoricalAlternatives.actualHistoryBase` — +- `HistoricalAlternatives.actualHistoryBase` — Klecha 2016 DOX substrate, available as the metaphysical instantiation via `metaphysicalAlternatives`. @@ -101,7 +101,7 @@ namespace Semantics.Tense.DeRe open Core (Intension WorldTimeIndex) open Core.Context (KContext) -open Semantics.Modality.HistoricalAlternatives (WorldHistory actualHistoryBase) +open HistoricalAlternatives (actualHistoryBase) open Core.Time.Tense (TensePronoun GramTense TemporalAssignment) @@ -282,9 +282,9 @@ theorem isFelicitousWith_of_isAbuschFelicitous [LinearOrder T] /-- **Metaphysical** alternative-set instantiation (@cite{klecha-2016} DOX): the worlds sharing the holder's actual world's history up to her now, paired with times at-or-before her now. Recovers the - legacy `WorldHistory`-based behavior as a special case. -/ + legacy `HistoricalAlternatives`-based behavior as a special case. -/ def metaphysicalAlternatives [LE T] - (history : WorldHistory W T) (dr : TemporalDeReReading W E P T) : + (history : HistoricalAlternatives W T) (dr : TemporalDeReReading W E P T) : Set (WorldTimeIndex W T) := actualHistoryBase history dr.holderContext.toSituation diff --git a/Linglib/Studies/Abusch1997.lean b/Linglib/Studies/Abusch1997.lean index 7aebd86fa..34aa0ea44 100644 --- a/Linglib/Studies/Abusch1997.lean +++ b/Linglib/Studies/Abusch1997.lean @@ -50,7 +50,7 @@ constructors). See `Tense/DeRe.lean` docstring for what's deferred formalized at the value level as `embeddedR ≤ matrixE`. **Note:** this value-level reduction strips the modal-alternative quantification the original formulation carries; making the modal - layer explicit (over `WorldHistory W Time` à la @cite{klecha-2016}) + layer explicit (over `HistoricalAlternatives W Time` à la @cite{klecha-2016}) is deferred. 3. **Temporal de re**: tense variable in the res position of an attitude. The value-level shadow uses `TensePronoun.fullPresupposition`: @@ -296,14 +296,14 @@ theorem abusch_derives_temporal_de_re_full /-- **Metaphysical-instantiation specialization** of `abusch_derives_temporal_de_re_full`. Recovers the legacy - `WorldHistory`-based formulation as a corollary at the + `HistoricalAlternatives`-based formulation as a corollary at the `metaphysicalAlternatives` instance, demonstrating backward compatibility with Klecha 2016 DOX-shaped reasoning. -/ theorem abusch_derives_temporal_de_re_full_metaphysical {W E P Time : Type*} [LinearOrder Time] (dr : Semantics.Tense.DeRe.TemporalDeReReading W E P Time) (hRigid : Core.Intension.IsRigid dr.concept) - (history : Semantics.Modality.HistoricalAlternatives.WorldHistory W Time) + (history : HistoricalAlternatives W Time) (hBefore : dr.actualRes < dr.holderContext.time) : dr.isAbuschFelicitous (dr.metaphysicalAlternatives history) .past := abusch_derives_temporal_de_re_full dr hRigid _ hBefore diff --git a/Linglib/Studies/BeaverCondoravdi2003.lean b/Linglib/Studies/BeaverCondoravdi2003.lean index 15d1d056f..65ed75d0f 100644 --- a/Linglib/Studies/BeaverCondoravdi2003.lean +++ b/Linglib/Studies/BeaverCondoravdi2003.lean @@ -81,44 +81,44 @@ def altMonotone (alt : HistAlt W T) : Prop := ∀ w t t', t ≤ t' → alt w t' ⊆ alt w t -- ============================================================================ --- § 1b: Bridge to BranchingTime.WorldHistory +-- § 1b: Bridge to BranchingTime.HistoricalAlternatives -- ============================================================================ -/-- Convert a `WorldHistory` (situation-indexed) to curried `HistAlt` form. -/ -def histAltOfWorldHistory (h : Semantics.Modality.HistoricalAlternatives.WorldHistory W T) : +/-- Convert a `HistoricalAlternatives` (situation-indexed) to curried `HistAlt` form. -/ +def histAltOfWorldHistory (h : HistoricalAlternatives W T) : HistAlt W T := fun w t => h ⟨w, t⟩ -/-- Convert curried `HistAlt` to `WorldHistory` (situation-indexed) form. -/ +/-- Convert curried `HistAlt` to `HistoricalAlternatives` (situation-indexed) form. -/ def worldHistoryOfHistAlt (a : HistAlt W T) : - Semantics.Modality.HistoricalAlternatives.WorldHistory W T := + HistoricalAlternatives W T := fun s => a s.world s.time omit [LinearOrder T] in -/-- Round-trip: `WorldHistory → HistAlt → WorldHistory` is identity. -/ +/-- Round-trip: `HistoricalAlternatives → HistAlt → HistoricalAlternatives` is identity. -/ theorem histAlt_worldHistory_roundtrip - (h : Semantics.Modality.HistoricalAlternatives.WorldHistory W T) : + (h : HistoricalAlternatives W T) : worldHistoryOfHistAlt (histAltOfWorldHistory h) = h := rfl omit [LinearOrder T] in -/-- Round-trip: `HistAlt → WorldHistory → HistAlt` is identity. -/ +/-- Round-trip: `HistAlt → HistoricalAlternatives → HistAlt` is identity. -/ theorem worldHistory_histAlt_roundtrip (a : HistAlt W T) : histAltOfWorldHistory (worldHistoryOfHistAlt a) = a := rfl omit [LinearOrder T] in -/-- `altReflexive` is equivalent to `WorldHistory.reflexive`. -/ +/-- `altReflexive` is equivalent to `HistoricalAlternatives.reflexive`. -/ theorem altReflexive_iff_reflexive (a : HistAlt W T) : altReflexive a ↔ (worldHistoryOfHistAlt a).reflexive := by - unfold altReflexive Semantics.Modality.HistoricalAlternatives.WorldHistory.reflexive + unfold altReflexive HistoricalAlternatives.reflexive worldHistoryOfHistAlt constructor · intro h s; exact h s.world s.time · intro h w t; exact h ⟨w, t⟩ -/-- `altMonotone` is equivalent to `WorldHistory.backwardsClosed`. -/ +/-- `altMonotone` is equivalent to `HistoricalAlternatives.backwardsClosed`. -/ theorem altMonotone_iff_backwardsClosed (a : HistAlt W T) : altMonotone a ↔ (worldHistoryOfHistAlt a).backwardsClosed := by - unfold altMonotone Semantics.Modality.HistoricalAlternatives.WorldHistory.backwardsClosed + unfold altMonotone HistoricalAlternatives.backwardsClosed worldHistoryOfHistAlt constructor · intro h w w' t t' hle hw' @@ -127,31 +127,31 @@ theorem altMonotone_iff_backwardsClosed (a : HistAlt W T) : exact h w w' t' t hle hw' omit [LinearOrder T] in -/-- `HistAlt` symmetry is equivalent to `WorldHistory.symmetric`: +/-- `HistAlt` symmetry is equivalent to `HistoricalAlternatives.symmetric`: if w' ∈ alt(w,t) then w ∈ alt(w',t). -/ theorem altSymmetric_iff_symmetric (a : HistAlt W T) : (∀ w t, ∀ w' ∈ a w t, w ∈ a w' t) ↔ (worldHistoryOfHistAlt a).symmetric := by - unfold Semantics.Modality.HistoricalAlternatives.WorldHistory.symmetric worldHistoryOfHistAlt + unfold HistoricalAlternatives.symmetric worldHistoryOfHistAlt constructor · intro h w w' t hw'; exact h w t w' hw' · intro h w t w' hw'; exact h w w' t hw' omit [LinearOrder T] in -/-- `HistAlt` transitivity is equivalent to `WorldHistory.transitive`: +/-- `HistAlt` transitivity is equivalent to `HistoricalAlternatives.transitive`: if w' ∈ alt(w,t) and w'' ∈ alt(w',t) then w'' ∈ alt(w,t). -/ theorem altTransitive_iff_transitive (a : HistAlt W T) : (∀ w t, ∀ w' ∈ a w t, ∀ w'' ∈ a w' t, w'' ∈ a w t) ↔ (worldHistoryOfHistAlt a).transitive := by - unfold Semantics.Modality.HistoricalAlternatives.WorldHistory.transitive worldHistoryOfHistAlt + unfold HistoricalAlternatives.transitive worldHistoryOfHistAlt constructor · intro h w w' w'' t h₁ h₂; exact h w t w' h₁ w'' h₂ · intro h w t w' h₁ w'' h₂; exact h w w' w'' t h₁ h₂ /-- B&C's `alt(w,t)` is exactly the `histEquiv` equivalence class: `w' ∈ alt(w,t)` iff `histEquiv history t w w'`. -/ -theorem histAlt_eq_histEquiv (h : Semantics.Modality.HistoricalAlternatives.WorldHistory W T) (w : W) (t : T) : - histAltOfWorldHistory h w t = { w' | Semantics.Modality.HistoricalAlternatives.histEquiv h t w w' } := rfl +theorem histAlt_eq_histEquiv (h : HistoricalAlternatives W T) (w : W) (t : T) : + histAltOfWorldHistory h w t = { w' | HistoricalAlternatives.histEquiv h t w w' } := rfl -- ============================================================================ -- § 2: Earliest Across Alternatives diff --git a/Linglib/Studies/Condoravdi2002.lean b/Linglib/Studies/Condoravdi2002.lean index e8c00695e..82153e5c0 100644 --- a/Linglib/Studies/Condoravdi2002.lean +++ b/Linglib/Studies/Condoravdi2002.lean @@ -45,7 +45,7 @@ open Core.Time open Features (Dynamicity) open Semantics.Events open Semantics.Aspect -open Semantics.Modality.HistoricalAlternatives +open HistoricalAlternatives open Semantics.Modality (TemporalPerspective TemporalOrientation) /-! ## The AT relation @@ -323,7 +323,7 @@ variable {W Time : Type*} [LinearOrder Time] past properties are), then a metaphysical modal base cannot satisfy diversity — restricting MODAL > PERF to epistemic modality. -/ theorem modal_over_perf_blocks_metaphysical - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (MB : W → Time → Set W) (cg : Set W) (now : Time) (P : EventPred W Time) @@ -338,7 +338,7 @@ theorem modal_over_perf_blocks_metaphysical base wider. This is the structural source of the counterfactual reading's "could have been otherwise" force. -/ theorem counterfactual_widens_domain - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (hBC : history.backwardsClosed) (w : W) {t' now : Time} (hle : t' ≤ now) : metaphysicalBase history w now ⊆ metaphysicalBase history w t' := diff --git a/Linglib/Studies/Klecha2016.lean b/Linglib/Studies/Klecha2016.lean index 7a92b1ab3..06dd4d05c 100644 --- a/Linglib/Studies/Klecha2016.lean +++ b/Linglib/Studies/Klecha2016.lean @@ -56,8 +56,8 @@ namespace Klecha2016 open Features (Attitude Preferential Veridicality) open Semantics.Modality (ModalBaseKind) -open Semantics.Modality.HistoricalAlternatives - (WorldHistory actualHistoryBase futureHistoryBase +open HistoricalAlternatives + (actualHistoryBase futureHistoryBase upperLimitConstraintModal upperLimitConstraintModal_implies_value) open Semantics.Modality.TemporalConstraint (attitudeTemporalConstraint doxConstrainsRT cirConstrainsRT Attitude.toModalBaseKind @@ -306,7 +306,7 @@ This is what differentiates Klecha's ULC from @cite{abusch-1997}'s stipulated one — the upper limit is a kernel-checked consequence of DOX-pronoun's lexical entry, not a separately-asserted presupposition on T-nodes. The substrate derivation lives in -`Semantics.Modality.HistoricalAlternatives` (`actualHistoryBase_time_actual`, +`HistoricalAlternatives` (`actualHistoryBase_time_actual`, `futureHistoryBase_time_future`); the `attitudeTemporalConstraint` projection in `Semantics/Modality/TemporalConstraint.lean` delegates to it. -/ @@ -316,7 +316,7 @@ delegates to it. -/ doxastic temporal constraint. The proof is Klecha's eq 35a derivation specialized to ℤ. -/ theorem ulc_via_history_base {W : Type*} - (history : WorldHistory W ℤ) + (history : HistoricalAlternatives W ℤ) (matrix embedded : Core.WorldTimeIndex W ℤ) (h : embedded ∈ actualHistoryBase history matrix) : attitudeTemporalConstraint .doxastic matrix.time embedded.time := @@ -327,7 +327,7 @@ theorem ulc_via_history_base {W : Type*} base satisfies the circumstantial temporal constraint. Klecha eq 35b specialized to ℤ. -/ theorem future_via_history_base {W : Type*} - (history : WorldHistory W ℤ) + (history : HistoricalAlternatives W ℤ) (matrix embedded : Core.WorldTimeIndex W ℤ) (h : embedded ∈ futureHistoryBase history matrix) : attitudeTemporalConstraint .circumstantial matrix.time embedded.time := @@ -355,7 +355,7 @@ proposition: via `actualHistoryBase_time_actual : s' ∈ actualHistoryBase history s → s'.time ≤ s.time`, a `.2`-projection through the situation-base definition. The doxastic-alternative quantification is carried by - `WorldHistory W Time` membership. + `HistoricalAlternatives W Time` membership. - **Abusch route** (in `Semantics/Tense/Basic.lean`): the predicate is stated directly as `abbrev upperLimitConstraint @@ -367,8 +367,8 @@ proposition: So the equivalence is strict at the value level. **It is *not* strict at the modal-layer level**: Klecha's substrate carries doxastic -alternatives via `WorldHistory`; Abusch's bare-`≤` form has dropped -them. A modal-layer `upperLimitConstraint` over `WorldHistory W Time` +alternatives via `HistoricalAlternatives`; Abusch's bare-`≤` form has dropped +them. A modal-layer `upperLimitConstraint` over `HistoricalAlternatives W Time` matching Abusch's original "now of an epistemic alternative" is deferred. -/ @@ -654,11 +654,11 @@ makes the world-component subset relation kernel-checked. -/ situation-base + structural unfolding of `metaphysicalBase` / `histEquiv`. -/ theorem klecha_cir_world_in_condoravdi_metaphysical - {W : Type*} (history : WorldHistory W ℤ) + {W : Type*} (history : HistoricalAlternatives W ℤ) (s s' : Core.WorldTimeIndex W ℤ) (h : s' ∈ futureHistoryBase history s) : s'.world ∈ - Semantics.Modality.HistoricalAlternatives.metaphysicalBase history s.world s.time := + HistoricalAlternatives.metaphysicalBase history s.world s.time := h.1 /-- Phase F bridge — Klecha-Condoravdi: the world-component of any @@ -666,11 +666,11 @@ theorem klecha_cir_world_in_condoravdi_metaphysical in @cite{condoravdi-2002}'s metaphysical modal base. The proof is `.1` projection (same as the CIR case). -/ theorem klecha_dox_world_in_condoravdi_metaphysical - {W : Type*} (history : WorldHistory W ℤ) + {W : Type*} (history : HistoricalAlternatives W ℤ) (s s' : Core.WorldTimeIndex W ℤ) (h : s' ∈ actualHistoryBase history s) : s'.world ∈ - Semantics.Modality.HistoricalAlternatives.metaphysicalBase history s.world s.time := + HistoricalAlternatives.metaphysicalBase history s.world s.time := h.1 @@ -707,7 +707,7 @@ sides* now carry the modal-alternative quantification (via layer, in contrast to §5c's value-level `klecha_dox_iff_abusch_ulc` which strips it. -/ theorem klecha_dox_iff_abusch_ulc_modal {W : Type*} - (history : WorldHistory W ℤ) + (history : HistoricalAlternatives W ℤ) (matrix embedded : Core.WorldTimeIndex W ℤ) : embedded ∈ actualHistoryBase history matrix ↔ upperLimitConstraintModal history matrix embedded := @@ -720,7 +720,7 @@ theorem klecha_dox_iff_abusch_ulc_modal {W : Type*} components. Composes `upperLimitConstraintModal_implies_value` with the substrate's `attitudeTemporalConstraint_derived_doxastic`. -/ theorem abusch_modal_ulc_implies_klecha_dox {W : Type*} - (history : WorldHistory W ℤ) + (history : HistoricalAlternatives W ℤ) (matrix embedded : Core.WorldTimeIndex W ℤ) (h : upperLimitConstraintModal history matrix embedded) : attitudeTemporalConstraint .doxastic matrix.time embedded.time := @@ -803,7 +803,7 @@ theorem klecha_covers_hope_future_oriented_reading Klecha's DOX behavior; this theorem makes the equivalence kernel-checked (provable by `rfl`). -/ theorem klecha_actualHistoryBase_eq_substrate_metaphysicalAlternatives - {W : Type*} (history : WorldHistory W ℤ) + {W : Type*} (history : HistoricalAlternatives W ℤ) (concept : Semantics.Tense.DeRe.TimeConcept W Unit Unit ℤ) (matrix : Core.Context.KContext W Unit Unit ℤ) : let dr : Semantics.Tense.DeRe.TemporalDeReReading W Unit Unit ℤ := diff --git a/Linglib/Studies/Mendes2025.lean b/Linglib/Studies/Mendes2025.lean index ca14bf3a9..0d4f7a014 100644 --- a/Linglib/Studies/Mendes2025.lean +++ b/Linglib/Studies/Mendes2025.lean @@ -39,7 +39,7 @@ namespace Mendes2025 open Core (Assignment WorldTimeIndex) open Core.Time -open Semantics.Modality.HistoricalAlternatives +open HistoricalAlternatives open Semantics.Dynamic.Core open Semantics.Tense open Semantics.Mood @@ -66,7 +66,7 @@ This is the compositional derivation: ⟦SF⟧ = ⟦SUBJ⟧ ∘ ⟦FUT⟧ -/ def subordinateFuture {W Time : Type*} [LE Time] [LT Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (newSitVar : SVar) -- Fresh variable for introduced situation (refSitVar : SVar) -- Variable for reference situation (c : SitContext W Time) : SitContext W Time := @@ -85,7 +85,7 @@ Conditional with SF antecedent (dynamic version). 3. Consequent: temporally anchored to s₁ (future relative to s₀) -/ def conditionalWithSF {W Time : Type*} [LE Time] [LT Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (antecedentVar : SVar) -- Situation introduced by SF (speechVar : SVar) -- Speech time situation (antecedent : SitContext W Time → SitContext W Time) -- "Maria is home" @@ -110,7 +110,7 @@ Structure: 3. Nuclear scope (get cookie) evaluated with temporal anchor from s₁ -/ def relativeClauseSF {W Time : Type*} [LE Time] [LT Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (rcVar : SVar) -- Situation variable for relative clause (speechVar : SVar) -- Speech time situation (c : SitContext W Time) : SitContext W Time := @@ -128,7 +128,7 @@ The SF in the restrictor: 3. Nuclear scope inherits temporal anchor from s₁ -/ def everyWithSFRestrictor {W Time : Type*} [LE Time] [LT Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (rcVar speechVar : SVar) (restrictor : SitContext W Time → SitContext W Time) -- "book that M reads" (nuclear : SitContext W Time → SitContext W Time) -- "is interesting" @@ -151,7 +151,7 @@ SF introduces a future situation. The subordinate future always introduces a situation with time ≥ current. -/ theorem sf_introduces_future {W Time : Type*} [Preorder Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (newVar refVar : SVar) (c : SitContext W Time) (gs : Assignment (WorldTimeIndex W Time) × WorldTimeIndex W Time) @@ -180,7 +180,7 @@ Modal donkey anaphora explains why subjunctive mood enables future reference in subordinate clauses. -/ theorem temporal_shift_parasitic_on_modal {W Time : Type*} [Preorder Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (sfVar speechVar : SVar) (c : SitContext W Time) -- For any situation in the output of SF application... @@ -230,7 +230,7 @@ Restrictor and nuclear must be context filters (`IsContextFilter`). Linguistically, predicates filter contexts without modifying assignments. -/ theorem sf_restrictor_future_reference {W Time : Type*} [Preorder Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (rcVar speechVar : SVar) (restrictor nuclear : SitContext W Time → SitContext W Time) (c : SitContext W Time) @@ -253,7 +253,7 @@ theorem sf_restrictor_future_reference {W Time : Type*} [Preorder Time] -- ════════════════════════════════════════════════════════════════ variable {W Time E : Type*} [LE Time] [LT Time] -variable (history : WorldHistory W Time) +variable (history : HistoricalAlternatives W Time) /-- Maria — proper name. @@ -461,7 +461,7 @@ def deriveCounterfactual SF constrains to future; counterfactual allows past/present. -/ theorem sf_vs_counterfactual_temporal {W Time : Type*} [Preorder Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) {E : Type*} (maria : E) (atHomeRel answerRel : E → WorldTimeIndex W Time → Prop) @@ -509,7 +509,7 @@ SF restrictor: quantifies over historical alternatives. "Every book that Maria reads.SF..." → no categorical existence presupposition. -/ def sfRestrictor {W Time E : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (restrictor : E → WorldTimeIndex W Time → Prop) (s₀ : WorldTimeIndex W Time) : E → Prop := λ x => ∃ s₁ ∈ historicalBase history s₀, restrictor x s₁ @@ -529,7 +529,7 @@ SF weakens existential presupposition: even without actual existence at s₀, the SF restrictor can be satisfied in alternative situations. -/ theorem sf_weakens_presup {W Time E : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (restrictor : E → WorldTimeIndex W Time → Prop) (s₀ : WorldTimeIndex W Time) (h_no_actual : ¬∃ x, restrictor x s₀) @@ -544,7 +544,7 @@ theorem sf_weakens_presup {W Time E : Type*} [LE Time] SF makes strong quantifiers felicitous under uncertainty. -/ theorem sf_felicitous_under_uncertainty {W Time E : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (restrictor : E → WorldTimeIndex W Time → Prop) (s₀ : WorldTimeIndex W Time) (h_uncertainty : (∃ s₁ ∈ historicalBase history s₀, ∃ x, restrictor x s₁) ∧ @@ -564,14 +564,14 @@ Relative clause with SF weakens strong quantifier presupposition. This is the formal version of the indicative-vs-SF contrast in restrictors. -/ def relClauseSF {W Time E : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (noun : E → WorldTimeIndex W Time → Prop) (relClause : E → WorldTimeIndex W Time → Prop) (s₀ : WorldTimeIndex W Time) : E → Prop := λ x => ∃ s₁ ∈ historicalBase history s₀, noun x s₁ ∧ relClause x s₁ theorem relClause_sf_weakens_quantifier {W Time E : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (noun relClause : E → WorldTimeIndex W Time → Prop) (s₀ : WorldTimeIndex W Time) (h_none_actual : ¬∃ x, noun x s₀ ∧ relClause x s₀) @@ -587,7 +587,7 @@ Modal displacement: SF introduces quantification over situations, "displacing" the existential presupposition to be local within each situation. -/ def modalDisplacement {W Time E : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (restrictor nuclear : E → WorldTimeIndex W Time → Prop) (s₀ : WorldTimeIndex W Time) : Prop := ∀ s₁ ∈ historicalBase history s₀, @@ -598,7 +598,7 @@ def modalDisplacement {W Time E : Type*} [LE Time] SF semantics is equivalent to modal displacement. -/ theorem sf_is_modal_displacement {W Time E : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (restrictor nuclear : E → WorldTimeIndex W Time → Prop) (s₀ : WorldTimeIndex W Time) : modalDisplacement history restrictor nuclear s₀ ↔ @@ -617,7 +617,7 @@ theorem sf_is_modal_displacement {W Time E : Type*} [LE Time] Modal displacement is weaker than global accommodation. -/ theorem modal_displacement_weaker_than_accommodation {W Time E : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (restrictor : E → WorldTimeIndex W Time → Prop) (s₀ : WorldTimeIndex W Time) (h_global : ∀ s₁ ∈ historicalBase history s₀, ∃ x, restrictor x s₁) @@ -661,7 +661,7 @@ Example: ↑ SUBJ introduces s₁ ↑ IND retrieves s₁ -/ def crossClausalBinding {W Time : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (antecedentVar _consequentVar : SVar) (c : SitContext W Time) : SitContext W Time := dynIND antecedentVar (dynSUBJ history antecedentVar c) @@ -672,7 +672,7 @@ introduced in the antecedent and retrieved in the consequent, the two clauses are evaluated at the same world. -/ theorem cross_clausal_same_world {W Time : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (v : SVar) (c : SitContext W Time) (gs : Assignment (WorldTimeIndex W Time) × WorldTimeIndex W Time) @@ -688,7 +688,7 @@ predicate filters at `s₁`, IND retrieves `s₁` (same-world check), and the consequent inherits the temporal anchor from `s₁`. -/ def subjIndChain {W Time : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (v : SVar) (antecedentPred : SitContext W Time → SitContext W Time) (consequentPred : SitContext W Time → SitContext W Time) @@ -703,7 +703,7 @@ is evaluated at a world that agrees with the bound situation's world. modifying assignments. -/ theorem subj_ind_chain_modal_donkey {W Time : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (v : SVar) (P Q : SitContext W Time → SitContext W Time) (c : SitContext W Time) @@ -723,7 +723,7 @@ universally over situations satisfying the antecedent — the modal analog of donkey universals. -/ theorem unselective_universal_force {W Time : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (v : SVar) (antecedent consequent : WorldTimeIndex W Time → Prop) (c : SitContext W Time) : @@ -754,7 +754,7 @@ characterizes the static existential conjunction `∃ s₁ ∈ historicalBase(s₀), P(s₁) ∧ Q(s₁)`. -/ theorem subjIndChain_singleton {W Time : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (v : SVar) (g : Assignment (WorldTimeIndex W Time)) (s₀ : WorldTimeIndex W Time) @@ -779,7 +779,7 @@ Conjunction is stronger than implication: if the dynamic pipeline finds an `s₁` satisfying both `P` and `Q`, then `P(s₁) → Q(s₁)` holds trivially. -/ theorem subjIndChain_entails_conditionalSF {W Time : Type*} [LE Time] - (history : WorldHistory W Time) + (history : HistoricalAlternatives W Time) (v : SVar) (g : Assignment (WorldTimeIndex W Time)) (s₀ : WorldTimeIndex W Time) diff --git a/Linglib/Studies/Roberts2023.lean b/Linglib/Studies/Roberts2023.lean index ea188db70..7ce6f233f 100644 --- a/Linglib/Studies/Roberts2023.lean +++ b/Linglib/Studies/Roberts2023.lean @@ -38,7 +38,7 @@ This file is a **configuration of existing infrastructure**, not a standalone formalization of an imperative mood ontology: - The futurate modal base reuses - `Semantics.Modality.HistoricalAlternatives.futureHistoryBase`. + `HistoricalAlternatives.futureHistoryBase`. - The goal-based ordering and circumstantial modal base are `Kratzer.OrderingSource` / `ModalBase`, packaged as `TeleologicalFlavor` (no parallel types). @@ -68,7 +68,7 @@ namespace Roberts2023 open Core (WorldTimeIndex) open Discourse (forceLinkingPrinciple defaultSemanticType sincerityCondition Scoreboard) open Semantics.Mood (POSW POSWQ POSWTarget IllocutionaryMood HasPOSWTarget) -open Semantics.Modality.HistoricalAlternatives +open HistoricalAlternatives open Semantics.Modality.Kratzer abbrev World := Fin 4 @@ -77,12 +77,12 @@ abbrev World := Fin 4 Roberts's "circumstance" ⟨w, t⟩ (eq. 45), SameHistory (47), and FUT (48) all instantiate the canonical world-time substrate in -`Core.WorldTimeIndex` and `Semantics.Modality.HistoricalAlternatives`: +`Core.WorldTimeIndex` and `HistoricalAlternatives`: Roberts Linglib substrate ──────────────────────────── ──────────────────────────── ⟨w, t⟩ circumstance `WorldTimeIndex W T` - SameHistory(w', w, t) `WorldHistory W T` predicate + SameHistory(w', w, t) `HistoricalAlternatives W T` predicate FUT(⟨w, t⟩) `futureHistoryBase history s` No new types are introduced for these. -/ @@ -179,7 +179,7 @@ theorem pragmatic_deontic_routing /-! ## §1 Desideratum (h): Futurate Flavor Restated against `futureHistoryBase` (the canonical Condoravdi/CIR -substrate in `Semantics.Modality.HistoricalAlternatives`) rather than a +substrate in `HistoricalAlternatives`) rather than a local `FUT` enumeration. -/ /-- **(h) Futurate flavor** (@cite{roberts-2023} Table 1, §1, exx. @@ -187,7 +187,7 @@ local `FUT` enumeration. -/ ⟨w, t⟩ has a strictly later time than t. Direct consequence of `futureHistoryBase`'s definition. -/ theorem futurate {W T : Type*} [LT T] - (history : WorldHistory W T) + (history : HistoricalAlternatives W T) (s s' : WorldTimeIndex W T) (h : s' ∈ futureHistoryBase history s) : s.time < s'.time := h.2