Centered-World Temporal De Re

@cite{lewis-1979-attitudes} (centered-worlds + de se reduction); @cite{cresswell-vonstechow-1982} (de re belief generalized); @cite{abusch-1997} (the temporal application).

Abusch 1997's temporal de re analysis: a tense morpheme can take wide scope over an attitude operator by occupying the res position. The res contributes a time-concept (Intension (KContext) T) plus a base-world condition (in w₀, the actual time-denotation is picked out by an acquaintance relation relative to the holder's centered context — Abusch §3 p. 9).

Abusch §3 develops the centered-proposition framework using the individual Ortcutt case: equation (12) defines an acquaintance relation R₁ : eeiwt to individuals, and (13) shows the centered-proposition assembly that combines R₁ with the complement-property P. The substrate's TimeConcept is the temporal specialization of this framework (cf. Abusch's own generalization in §12), where the res is a time rather than an individual.

This file is anchored on the centered-world de re framework, not on Abusch 1997 alone — Lewis 1979 + Cresswell & von Stechow 1982 are the foundational layer Abusch builds on. Paper-anchored derivation theorems live in Phenomena/TenseAspect/Studies/Abusch1997.lean.

Reuse

• Core.Intension W τ (Core/Logic/Intensional/Rigidity.lean) — substrate for time-concepts. IsRigid captures the "same time across alternatives" property that distinguishes de re from de dicto temporal anaphora. IsRigidOn (set-relativized) is the workhorse for modal-alternative rigidity.
• Core.Context.KContext W E P T (Core/Context/Basic.lean) — the centered Kaplanian context ⟨agent, addressee, world, time, position⟩. Abusch's ⟨x_self, t_now, w⟩ is a 3-field projection; KContext is the richer object the rest of linglib already commits to. KContext.shiftWorldTime provides the alternative-shift operation.
• Semantics.Reference.Acquaintance — polymorphic Cover, nameCover, isAcquaintedWith. The temporal-de-re reading is the Idx := KContext, Res := T instance of the same acquaintance machinery PLA uses for individual de re (Theories/Semantics/Dynamic/PLA/Belief.lean).
• Semantics.Tense.TensePronoun.fullPresupposition — the value-level shadow this file connects to (the deleted TemporalDeRe triple was a shadow of this shadow; see the isFelicitousWith_iff_… theorem below for the bridge).
• Core.Modality.HistoricalAlternatives.actualHistoryBase — Klecha 2016 DOX substrate, available as the metaphysical instantiation via metaphysicalAlternatives.

Two felicity predicates (value-level vs Abusch-faithful)

• isFelicitousWith — local constraint check at the holder's now (= holderContext.time). The value-level shadow of Abusch's reading. Equivalent to TensePronoun.fullPresupposition (see shadow lemma).
• isAbuschFelicitous — adds Abusch §3 modal rigidity: the time-concept identifies the same time across an alternative-set parameter. The substrate is agnostic about whether the alternatives are doxastic (Hintikka belief alternatives, the Abusch-canonical case) or metaphysical (Lewis-Cariani-Santorio shared-past, Klecha 2016 DOX). The user supplies whichever set the consumer's framework demands; convenience constructors metaphysicalAlternatives (legacy) and doxasticAlternatives make the parallel explicit. Concept-rigidity (Core.Intension.IsRigid) is sufficient to discharge modal-rigidity for any alternative-set — a constant-intension concept is automatically rigid.

Design choices

• The holderContext field represents the attitude holder's centered context, NOT the outer speaker's context. Per @cite{abusch-1997} §7 ULC (p. 24-25), the relevant evaluation time for embedded tenses is the holder's now (= holderContext.time), not the outer speech time.
• IsRigidAcrossAlternatives is parameterized on Set (WorldTimeIndex W T) rather than committing to a particular modal base. Doxastic (the @cite{abusch-1997}-canonical Hintikka setup) and metaphysical (Klecha 2016 DOX, Lewis-Cariani-Santorio shared past) become explicit instantiation choices via convenience constructors doxasticAlternatives and metaphysicalAlternatives.

What's deferred

• LF res-movement as a Tree C W rewrite operator. This file exposes the output of res-movement (a coherent ⟨concept, holder⟩ bundle), not the syntactic operation that produces it.
• PLA-side individual unification. The EntityConcept analog at Idx := Assignment E × WitnessSeq E is what PLA's Concept E is (definitionally); the formal unification theorem is in Phenomena/TenseAspect/Studies/Abusch1997.lean.

@[reducible, inline]

abbrev Semantics.Tense.DeRe.TimeConcept (W : Type u_1) (E : Type u_2) (P : Type u_3) (T : Type u_4) : Type (max (max (max (max u_4 u_3) u_2) u_1) u_4)

A time-concept: an intension from a centered Kaplanian context to a time. The temporal specialization of @cite{abusch-1997}'s centered-proposition framework (§3 develops it for individuals via the acquaintance relation R₁ : eeiwt at eq. 12; §12 generalizes to times). The Lewis-style "way of identifying a time" Abusch's R₁ : eeiwt builds on.

Equations

• Semantics.Tense.DeRe.TimeConcept W E P T = Core.Intension (Core.Context.KContext W E P T) T

@[reducible, inline]

abbrev Semantics.Tense.DeRe.EntityConcept (W : Type u_1) (E : Type u_2) (P : Type u_3) (T : Type u_4) : Type (max (max (max (max u_4 u_3) u_2) u_1) u_2)

An entity-concept (@cite{lewis-1979-attitudes} centered-world de re, @cite{cresswell-vonstechow-1982}): an intension from a centered Kaplanian context to an entity. The dual of TimeConcept — instantiating Abusch 1997's individual ↔ temporal de re parallel on the entity side at the same evaluation index.

Equations

• Semantics.Tense.DeRe.EntityConcept W E P T = Core.Intension (Core.Context.KContext W E P T) E

structure Semantics.Tense.DeRe.TemporalDeReReading (W : Type u_1) (E : Type u_2) (P : Type u_3) (T : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

A temporal de re reading (@cite{abusch-1997} §3): a time-concept paired with the attitude holder's centered context. The actual res-denotation is the concept evaluated at the holder's context (actualRes); the base-world condition (Abusch p. 9) is satisfied by construction.

The holderContext field carries the attitude bearer's centered Kaplanian context — agent = the believer, world = her actual world, time = her now (the perspective time at which embedded tenses are evaluated, per @cite{abusch-1997} §7 ULC). It is not the outer speaker's speech context; for unembedded uses the speaker is treated as her own attitude holder.

• concept : TimeConcept W E P T

  The time-concept (Abusch's R₁): the way of identifying the res time across centered-world alternatives.

• holderContext : Core.Context.KContext W E P T

  The attitude holder's centered Kaplanian context. Per @cite{abusch-1997} §7 ULC, holderContext.time is the relevant perspective time for embedded tense evaluation — not the outer speaker's speech time.

theorem Semantics.Tense.DeRe.TemporalDeReReading.ext_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {x y : TemporalDeReReading W E P T} : x = y ↔ x.concept = y.concept ∧ x.holderContext = y.holderContext

theorem Semantics.Tense.DeRe.TemporalDeReReading.ext {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {x y : TemporalDeReReading W E P T} (concept : x.concept = y.concept) (holderContext : x.holderContext = y.holderContext) : x = y

def Semantics.Tense.DeRe.TemporalDeReReading.actualRes {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (dr : TemporalDeReReading W E P T) : T

The actual time-denotation of the res, derived from the concept and the holder's centered context.

Equations

• dr.actualRes = dr.concept dr.holderContext

theorem Semantics.Tense.DeRe.TemporalDeReReading.baseCoherent {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (dr : TemporalDeReReading W E P T) : dr.concept dr.holderContext = dr.actualRes

Base-world coherence (@cite{abusch-1997} §3 p. 9): the actual res-time equals the concept's value at the holder's centered context. True by construction in this substrate.

def Semantics.Tense.DeRe.TemporalDeReReading.isFelicitousWith {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [LinearOrder T] (dr : TemporalDeReReading W E P T) (constraint : Core.Time.Tense.GramTense) : Prop

Felicity of a temporal de re reading under a tense constraint: the actual res-time stands in the constraint's relation to the holder's now (= holderContext.time). Per @cite{abusch-1997} §7 ULC (p. 24-25), the holder's now is the relevant evaluation time for embedded tenses — a past-marked tense res-moved from under believe is constrained to denote a time before the believer's now, NOT before the outer speaker's speech time.

Equations

• dr.isFelicitousWith constraint = constraint.constrains dr.actualRes dr.holderContext.time

theorem Semantics.Tense.DeRe.TemporalDeReReading.isFelicitousWith_iff_tensePronoun_fullPresupposition {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [LinearOrder T] (dr : TemporalDeReReading W E P T) (tp : Core.Time.Tense.TensePronoun) (g : Core.Time.Tense.TemporalAssignment T) (hRes : tp.resolve g = dr.actualRes) (hEval : tp.evalTime g = dr.holderContext.time) : dr.isFelicitousWith tp.constraint ↔ tp.fullPresupposition g

Value-level shadow lemma: a temporal de re reading is felicitous with tp.constraint iff the corresponding TensePronoun.fullPresupposition holds at any temporal assignment that resolves the variable to the de re reading's actualRes and the eval-time to the holder's now.

This makes precise the sense in which the deleted bare-triple substrate (referent, evalTime, constraint : GramTense) was a value-level shadow of the centered-world account: pick referent := dr.actualRes, evalTime := dr.holderContext.time.

def Semantics.Tense.DeRe.TemporalDeReReading.IsRigidAcrossAlternatives {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (dr : TemporalDeReReading W E P T) (alternatives : Set (Core.WorldTimeIndex W T)) : Prop

Modal rigidity: the time-concept evaluates to the same time at every world-time pair in a supplied alternative set, when that alternative is plugged into the holder's centered context. This is the de re property — what distinguishes a wide-scope res-time from a de dicto descriptive concept.

Substrate-level lift of @cite{abusch-1997}'s base-world condition (§3 p. 9: "in the base world, the [res] is picked out by the acquaintance relation relative to the believer and the believing time") to a quantification over the believer's alternative set. Abusch herself does not state "modal rigidity" in those terms; the framing is the substrate's reformulation of her acquaintance-based de re analysis.

The alternatives parameter is agnostic about modal base: the substrate accepts any Set (WorldTimeIndex W T). Abusch's canonical setup uses doxastic alternatives (the believer's Hintikka belief set); Klecha 2016 DOX uses metaphysical alternatives (worlds sharing the holder's actual past, via actualHistoryBase). The consumer chooses at the call site. Convenience constructors metaphysicalAlternatives and doxasticAlternatives provide the two standard instantiations.

Equations

• dr.IsRigidAcrossAlternatives alternatives = Core.Intension.IsRigidOn (fun (s : Core.WorldTimeIndex W T) => dr.concept (dr.holderContext.shiftWorldTime s)) alternatives

def Semantics.Tense.DeRe.TemporalDeReReading.isAbuschFelicitous {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [LinearOrder T] (dr : TemporalDeReReading W E P T) (alternatives : Set (Core.WorldTimeIndex W T)) (constraint : Core.Time.Tense.GramTense) : Prop

Full Abusch felicity (@cite{abusch-1997} §3): value-level constraint check (actual res-time stands in the constraint's relation to the holder's now) AND modal rigidity across a supplied alternative-set. The value-level shadow isFelicitousWith captures only the first conjunct; this predicate is what an Abusch-faithful study should use.

Equations

• dr.isAbuschFelicitous alternatives constraint = (dr.isFelicitousWith constraint ∧ dr.IsRigidAcrossAlternatives alternatives)

theorem Semantics.Tense.DeRe.TemporalDeReReading.IsRigidAcrossAlternatives_of_concept_isRigid {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (dr : TemporalDeReReading W E P T) (h : Core.Intension.IsRigid dr.concept) (alternatives : Set (Core.WorldTimeIndex W T)) : dr.IsRigidAcrossAlternatives alternatives

A rigid time-concept (constant intension, Core.Intension.IsRigid) is automatically rigid across any alternative-set. The rigid-concept derivations in Studies/Abusch1997.lean discharge IsRigidAcrossAlternatives "for free" via this lemma.

Composes two general substrate lemmas: Intension.IsRigid.precomp (pre-composition with the shiftWorldTime map preserves rigidity) and Intension.IsRigid.isRigidOn (full rigidity implies rigidity-on-any-set). The chain makes the substrate's design visible: temporal de re ≡ rigidity preserved under the centered coordinate-shift, restricted to whichever alternative set the consumer supplies.

theorem Semantics.Tense.DeRe.TemporalDeReReading.isFelicitousWith_of_isAbuschFelicitous {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [LinearOrder T] (dr : TemporalDeReReading W E P T) (alternatives : Set (Core.WorldTimeIndex W T)) (constraint : Core.Time.Tense.GramTense) (h : dr.isAbuschFelicitous alternatives constraint) : dr.isFelicitousWith constraint

Abusch felicity ⇒ value-level felicity: the modal-quantified predicate strictly refines the value-level shadow. Old code that only checks isFelicitousWith is conservative — anything proved via isAbuschFelicitous projects through.

def Semantics.Tense.DeRe.TemporalDeReReading.metaphysicalAlternatives {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [LE T] (history : Core.Modality.HistoricalAlternatives.WorldHistory W T) (dr : TemporalDeReReading W E P T) : Set (Core.WorldTimeIndex W 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.

Equations

• Semantics.Tense.DeRe.TemporalDeReReading.metaphysicalAlternatives history dr = Core.Modality.HistoricalAlternatives.actualHistoryBase history dr.holderContext.toSituation

def Semantics.Tense.DeRe.TemporalDeReReading.doxasticAlternatives {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (dox : E → W → Core.WorldTimeIndex W T → Prop) (dr : TemporalDeReReading W E P T) : Set (Core.WorldTimeIndex W T)

Doxastic alternative-set instantiation (@cite{abusch-1997} §3, Hintikka belief alternatives): the world-time pairs the holder considers epistemically possible. Parameterized on a generic dox : E → W → WorldTimeIndex W T → Prop representing the holder's doxastic accessibility relation over centered alternatives. This is the modal-base @cite{abusch-1997} canonically uses, distinct from the metaphysical version above.

Equations

• Semantics.Tense.DeRe.TemporalDeReReading.doxasticAlternatives dox dr = {s' : Core.WorldTimeIndex W T | dox dr.holderContext.agent dr.holderContext.world s'}

@[reducible, inline]

abbrev Semantics.Tense.DeRe.TemporalDeReReading.TimeCover (W : Type u_5) (E : Type u_6) (P : Type u_7) (T : Type u_8) : Type (max u_8 (max (max u_8 u_7) u_6) u_5)

The Aloni cover for time-concepts: a set of TimeConcepts representing the believer's available "ways of identifying" a time. Instantiates Acquaintance.Cover at the centered-context index.

Equations

• Semantics.Tense.DeRe.TemporalDeReReading.TimeCover W E P T = Semantics.Reference.Acquaintance.Cover (Core.Context.KContext W E P T) T

@[reducible, inline]

abbrev Semantics.Tense.DeRe.TemporalDeReReading.isTemporallyAcquaintedWith {W : Type u_5} {E : Type u_6} {P : Type u_7} {T : Type u_8} (t : T) (C : TimeCover W E P T) (c : Core.Context.KContext W E P T) : Prop

A time t is temporally-acquainted at the holder's context c (with respect to a time-cover C) when some concept in C picks out t at c. The temporal analog of @cite{lewis-1979-attitudes}'s acquaintance — instantiating polymorphic isAcquaintedWith at Idx := KContext, Res := T.

Equations

• Semantics.Tense.DeRe.TemporalDeReReading.isTemporallyAcquaintedWith t C c = Semantics.Reference.Acquaintance.isAcquaintedWith t C c

theorem Semantics.Tense.DeRe.TemporalDeReReading.actualRes_isTemporallyAcquaintedWith {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (dr : TemporalDeReReading W E P T) : isTemporallyAcquaintedWith dr.actualRes {dr.concept} dr.holderContext

The holder-anchored res-time of a de re reading is acquainted-with via the singleton time-cover {dr.concept}. The concept itself witnesses the acquaintance.