Centered-world temporal de re

[Abu97]'s temporal de re: a tense morpheme can take wide scope over an attitude operator by occupying the res position. The res contributes a time-concept (TimeConcept) plus a base-world condition — in the base world, the res denotation is picked out by an acquaintance relation relative to the holder's centered context ([Abu97] §3 p. 9). The centered-world framework is [Lew79a]'s de se reduction as generalized by [CvS82]; Abusch develops it for individuals in §3 (the acquaintance relation R₁ : eeiwt, eq. 12, and the centered-proposition assembly, eq. 13) and applies it to times in §4 (temporal acquaintance relations) and §11. Paper-anchored derivation theorems live in Studies/Abusch1997.lean.

Implementation notes

Time-concepts are Intensional.Intensions from the centered Kaplanian context Semantics.Context.KContext (Semantics/Reference/Context/Basic.lean) — Abusch's ⟨x_self, t_now, w⟩ is a three-field projection of the richer context the rest of linglib commits to. Rigidity across alternatives is Intension.IsRigidOn after KContext.shiftWorldTime; the alternative set is a bare Set (Index W T), so doxastic (Hintikka belief alternatives, the Abusch-canonical case) and metaphysical ([Kle16] DOX via HistoricalAlternatives.actualHistoryBase) modal bases are call-site instantiations (doxasticAlternatives, metaphysicalAlternatives).

Time-concepts

@[reducible, inline]

abbrev 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 — a way of identifying a time across centered-world alternatives. The temporal instance of [Abu97]'s centered-proposition framework (§3 develops it for individuals via the acquaintance relation R₁ : eeiwt, eq. 12; §4 applies it to times).

Equations

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

Temporal de re reading

structure 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 ([Abu97] §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), so the base-world condition (§3 p. 9) holds by construction.

• concept : TimeConcept W E P T

  The time-concept: the way of identifying the res time across centered-world alternatives.

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

  The attitude holder's centered Kaplanian context. Per [Abu97] §7 ULC, holderContext.time is the holder's now — the perspective time for embedded tense evaluation, not the outer speaker's speech time.

theorem 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

theorem 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

def 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: the concept evaluated at the holder's centered context.

Equations

• dr.actualRes = dr.concept dr.holderContext

Felicity

def 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 : Finset Ordering) : Prop

Value-level 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 ([Abu97] §7 ULC, p. 24–25) — a past-marked tense res-moved from under believe must denote a time before the believer's now, not before the outer speech time.

Equations

• dr.IsFelicitousWith constraint = Core.Order.holds constraint dr.actualRes dr.holderContext.time

def 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 (Intensional.Index W T)) : Prop

Modal rigidity: the time-concept evaluates to the same time at every world-time pair in the alternative set — what distinguishes a wide-scope res-time from a de dicto descriptive concept. This lifts [Abu97]'s base-world condition (§3 p. 9) to a quantification over the holder's alternatives; Abusch herself states the analysis through acquaintance relations, not rigidity. The alternative set is modal-base-agnostic: doxastic ([Abu97]'s Hintikka setup) or metaphysical ([Kle16] DOX) — see the constructors below.

Equations

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

def Tense.DeRe.TemporalDeReReading.IsFelicitous {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 (Intensional.Index W T)) (constraint : Finset Ordering) : Prop

Felicity of a temporal de re reading ([Abu97] §3): the value-level constraint check at the holder's now (IsFelicitousWith) together with modal rigidity across the supplied alternative set (IsRigidAcrossAlternatives).

Equations

• dr.IsFelicitous alternatives constraint = (dr.IsFelicitousWith constraint ∧ dr.IsRigidAcrossAlternatives alternatives)

theorem Tense.DeRe.TemporalDeReReading.isRigidAcrossAlternatives_of_isRigid {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (dr : TemporalDeReReading W E P T) (h : Intensional.Intension.IsRigid dr.concept) (alternatives : Set (Intensional.Index W T)) : dr.IsRigidAcrossAlternatives alternatives

A rigid time-concept (Intensional.Intension.IsRigid) is rigid across any alternative set: pre-composition with shiftWorldTime preserves rigidity (IsRigid.precomp), and full rigidity restricts to any set (IsRigid.isRigidOn).

Alternative-set constructors (modal-base instantiations)

def Tense.DeRe.TemporalDeReReading.metaphysicalAlternatives {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [LE T] (history : HistoricalAlternatives W T) (dr : TemporalDeReReading W E P T) : Set (Intensional.Index W T)

Metaphysical alternative set ([Kle16] DOX): the worlds sharing the holder's actual history up to her now, paired with times at-or-before her now.

Equations

• Tense.DeRe.TemporalDeReReading.metaphysicalAlternatives history dr = history.actualHistoryBase dr.holderContext.toIndex

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

Doxastic alternative set ([Abu97] §3, Hintikka belief alternatives): the world-time pairs the holder considers possible, for a doxastic accessibility relation dox over centered alternatives.

Equations

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