Schlenker (2004b): Sequence Phenomena and Double Access Readings Generalized

This file formalizes the chapter's two remarks. The first is that sequence of tense is one instance of an agreement mechanism shared by person, tense and mood. An attitude verb quantifies over the contexts compatible with the attitude, an embedded argument read de se is a coordinate of the bound context variable, and the features it is pronounced with are copied from the arguments of the embedding verb by the formation rule (22) (Features.ofArgs) without being interpreted. The fragment of Appendix A is given as terms carrying features (Term, TimeTerm), formulas with the attitude construction (Formula), and their value and definedness at an assignment and an utterance context. A de se report then has the truth conditions of (13b) and inherits no presupposition from its embedded features, whereas interpreting a person, tense or mood feature on a coordinate makes its presupposition project universally over the attitude's contexts, which the examples (16), (19) and (21) refute (past_coord_weird, ind_coord_not_weird_iff). Features are transmitted unchanged down a chain of attitudes, also through a future auxiliary, which (22) keeps out of agreement (Features.ofArgs_coord_fut), as the example (24) of [KR83] requires.

The second remark generalizes the upper limit constraint of [Abu97] from tense to mood. After the de re transformation a tense or mood denotes a description of times or worlds relative to the local context, and the coordinate of that context is an upper limit for it: a time description may not lie entirely after the context's time, and a world description must contain its world, one constraint for both (ULC). Double access for tense follows as in Abusch, and the same argument yields its modal counterpart, the reading on which the agent's thought is about the actual world as well as the world of the thought act (doubleAccess_of_ulc, worldDoubleAccess_of_ulc): in both the description contains the coordinate of the thought and the actual one.

Implementation notes

• Failure of denotation is a definedness predicate beside a total value rather than a partial denotation, and the diacritic of a context variable is read off the enclosing attitude's arguments by (22) rather than stored on its coordinates, so the feature a term is pronounced with is the feature appearing in it. Disjunction is omitted. Vividness of descriptions is left to the hypotheses of the double access theorems.
• The chapter states the upper limit constraint for present and past time terms and indicative world terms only; the constraint here is on descriptions, and which terms it applies to is left to its application.

References

• [Sch04c]
• [Abu97]
• [Hei94b]
• [KR83]

The fragment (Appendix A)

inductive Schlenker2004b.PersonFeature : Type

The person features.

• he : PersonFeature
• she : PersonFeature

@[instance_reducible]

instance Schlenker2004b.instDecidableEqPersonFeature : DecidableEq PersonFeature

Equations

• Schlenker2004b.instDecidableEqPersonFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Schlenker2004b.TenseFeature : Type

The tense features.

• pres : TenseFeature
• past : TenseFeature

@[instance_reducible]

instance Schlenker2004b.instDecidableEqTenseFeature : DecidableEq TenseFeature

Equations

• Schlenker2004b.instDecidableEqTenseFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Schlenker2004b.MoodFeature : Type

The mood features.

• ind : MoodFeature
• subj : MoodFeature

@[instance_reducible]

instance Schlenker2004b.instDecidableEqMoodFeature : DecidableEq MoodFeature

Equations

• Schlenker2004b.instDecidableEqMoodFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Schlenker2004b.Features : Type

The feature triple a complementizer carries, each coordinate possibly absent.

• person : Option PersonFeature
• tense : Option TenseFeature
• mood : Option MoodFeature

@[instance_reducible]

instance Schlenker2004b.instDecidableEqFeatures : DecidableEq Features

Equations

• Schlenker2004b.instDecidableEqFeatures = Schlenker2004b.instDecidableEqFeatures.decEq

def Schlenker2004b.instDecidableEqFeatures.decEq (x✝ x✝¹ : Features) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

inductive Schlenker2004b.Term (φ : Type) : Type

A term of one of the fragment's sorts: a bare variable, the corresponding coordinate of the context variable c_i, or a term carrying a feature.

• var {φ : Type} (k : ℕ) : Term φ
• coord {φ : Type} (i : ℕ) : Term φ
• feat {φ : Type} (f : φ) (t : Term φ) : Term φ

inductive Schlenker2004b.TimeTerm : Type

A time term: a term, or a future built on a time term with a variable of its own.

• base (t : Term TenseFeature) : TimeTerm
• fut (k : ℕ) (t : TimeTerm) : TimeTerm

def Schlenker2004b.Term.feature {φ : Type} (proj : Features → Option φ) (env : ℕ → Features) : Term φ → Option φ

The feature appearing in a term, which is also the feature it is pronounced with; the diacritic of a context variable is supplied by the environment env (Appendix A, Note A).

Equations

• Schlenker2004b.Term.feature proj env (Schlenker2004b.Term.var k) = none
• Schlenker2004b.Term.feature proj env (Schlenker2004b.Term.coord i) = proj (env i)
• Schlenker2004b.Term.feature proj env (Schlenker2004b.Term.feat f t) = some f

def Schlenker2004b.TimeTerm.feature (env : ℕ → Features) : TimeTerm → Option TenseFeature

The tense feature appearing in a time term; a future auxiliary contributes none.

Equations

• Schlenker2004b.TimeTerm.feature env (Schlenker2004b.TimeTerm.base t) = Schlenker2004b.Term.feature Schlenker2004b.Features.tense env t
• Schlenker2004b.TimeTerm.feature env (Schlenker2004b.TimeTerm.fut k t) = Schlenker2004b.TimeTerm.feature env t

def Schlenker2004b.Features.ofArgs (env : ℕ → Features) (i : Term PersonFeature) (t : TimeTerm) (w : Term MoodFeature) : Features

(22): the diacritic of the complementizer of an attitude verb with arguments i, t and w, the person, tense and mood features appearing in them.

Equations

• One or more equations did not get rendered due to their size.

theorem Schlenker2004b.Features.ofArgs_coord (env : ℕ → Features) (k : ℕ) : ofArgs env (Term.coord k) (TimeTerm.base (Term.coord k)) (Term.coord k) = env k

An attitude verb whose arguments are the coordinates of the context variable c_k passes that variable's diacritic on unchanged.

theorem Schlenker2004b.Features.ofArgs_coord_fut (env : ℕ → Features) (k j : ℕ) : ofArgs env (Term.coord k) (TimeTerm.fut j (TimeTerm.base (Term.coord k))) (Term.coord k) = env k

(24): the diacritic passes through a future auxiliary on the time argument, so would, the future of a past coordinate, transmits past.

structure Schlenker2004b.Model (W : Type u_5) (E : Type u_6) (P : Type u_7) (T : Type u_8) : Type (max (max (max u_5 u_6) u_7) u_8)

A model of the fragment: the genders behind he and she, the simple predicates, and the contexts compatible with each attitude verb at an individual, time and world, when there is such an attitude.

• male : E → T → W → Prop

  Being male at a time in a world.

• female : E → T → W → Prop

  Being female at a time in a world.

• pred : ℕ → E → T → W → Prop

  The simple predicates, indexed.

• att : ℕ → E → T → W → Option (Set (Reference.Context W E P T))

  The contexts compatible with attitude verb V held by an individual at a time in a world, if there is such an attitude.

structure Schlenker2004b.Assignment (W : Type u_5) (E : Type u_6) (P : Type u_7) (T : Type u_8) : Type (max (max (max u_5 u_6) u_7) u_8)

An assignment of values to the individual, time, world and context variables.

• ind : ℕ → E

  Values of the individual variables.

• time : ℕ → T

  Values of the time variables.

• world : ℕ → W

  Values of the world variables.

• ctx : ℕ → Reference.Context W E P T

  Values of the context variables.

def Schlenker2004b.Assignment.updateCtx {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (s : Assignment W E P T) (k : ℕ) (c : Reference.Context W E P T) : Assignment W E P T

The assignment with the context variable k set to c.

Equations

• s.updateCtx k c = { ind := s.ind, time := s.time, world := s.world, ctx := Function.update s.ctx k c }

def Schlenker2004b.PersonFeature.Presup {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (M : Model W E P T) (c₀ : Reference.Context W E P T) : PersonFeature → E → Prop

The presupposition of a person feature at the utterance context c₀.

Equations

• Schlenker2004b.PersonFeature.Presup M c₀ Schlenker2004b.PersonFeature.he x✝ = M.male x✝ c₀.time c₀.world
• Schlenker2004b.PersonFeature.Presup M c₀ Schlenker2004b.PersonFeature.she x✝ = M.female x✝ c₀.time c₀.world

def Schlenker2004b.TenseFeature.Presup {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c₀ : Reference.Context W E P T) [Preorder T] : TenseFeature → T → Prop

The presupposition of a tense feature at the utterance context c₀.

Equations

• Schlenker2004b.TenseFeature.Presup c₀ Schlenker2004b.TenseFeature.pres x✝ = (x✝ = c₀.time)
• Schlenker2004b.TenseFeature.Presup c₀ Schlenker2004b.TenseFeature.past x✝ = (x✝ < c₀.time)

def Schlenker2004b.MoodFeature.Presup {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c₀ : Reference.Context W E P T) : MoodFeature → W → Prop

The presupposition of a mood feature at the utterance context c₀; the subjunctive carries none.

Equations

• Schlenker2004b.MoodFeature.Presup c₀ Schlenker2004b.MoodFeature.ind x✝ = (x✝ = c₀.world)
• Schlenker2004b.MoodFeature.Presup c₀ Schlenker2004b.MoodFeature.subj x✝ = True

def Schlenker2004b.Term.value {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (s : Assignment W E P T) {φ : Type} {α : Type u_5} (val : ℕ → α) (coordOf : Reference.Context W E P T → α) : Term φ → α

The value of a term: a variable's value, the coordinate of the context variable's value, or the value of the term a feature is attached to.

Equations

• Schlenker2004b.Term.value s val coordOf (Schlenker2004b.Term.var k) = val k
• Schlenker2004b.Term.value s val coordOf (Schlenker2004b.Term.coord i) = coordOf (s.ctx i)
• Schlenker2004b.Term.value s val coordOf (Schlenker2004b.Term.feat f t) = Schlenker2004b.Term.value s val coordOf t

def Schlenker2004b.Term.Weird {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (s : Assignment W E P T) {φ : Type} {α : Type u_5} (val : ℕ → α) (coordOf : Reference.Context W E P T → α) (presup : φ → α → Prop) : Term φ → Prop

A term is weird when a feature on it has its presupposition violated by the value of the term it is attached to.

Equations

• Schlenker2004b.Term.Weird s val coordOf presup (Schlenker2004b.Term.var k) = False
• Schlenker2004b.Term.Weird s val coordOf presup (Schlenker2004b.Term.coord i) = False
• Schlenker2004b.Term.Weird s val coordOf presup (Schlenker2004b.Term.feat f t) = (Schlenker2004b.Term.Weird s val coordOf presup t ∨ ¬presup f (Schlenker2004b.Term.value s val coordOf t))

def Schlenker2004b.TimeTerm.value {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (s : Assignment W E P T) : TimeTerm → T

The value of a time term; a future denotes its own variable.

Equations

• Schlenker2004b.TimeTerm.value s (Schlenker2004b.TimeTerm.base t) = Schlenker2004b.Term.value s s.time Reference.Context.time t
• Schlenker2004b.TimeTerm.value s (Schlenker2004b.TimeTerm.fut k t) = s.time k

def Schlenker2004b.TimeTerm.Weird {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c₀ : Reference.Context W E P T) (s : Assignment W E P T) [Preorder T] : TimeTerm → Prop

A future is weird unless its variable is after the term it is built on.

Equations

• Schlenker2004b.TimeTerm.Weird c₀ s (Schlenker2004b.TimeTerm.base t) = Schlenker2004b.Term.Weird s s.time Reference.Context.time (Schlenker2004b.TenseFeature.Presup c₀) t
• Schlenker2004b.TimeTerm.Weird c₀ s (Schlenker2004b.TimeTerm.fut k t) = (Schlenker2004b.TimeTerm.Weird c₀ s t ∨ ¬Schlenker2004b.TimeTerm.value s t < s.time k)

def Schlenker2004b.ArgsWeird {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (M : Model W E P T) (c₀ : Reference.Context W E P T) (s : Assignment W E P T) [Preorder T] (i : Term PersonFeature) (t : TimeTerm) (w : Term MoodFeature) : Prop

Weirdness of the three arguments of a predicate or attitude verb.

Equations

• One or more equations did not get rendered due to their size.

inductive Schlenker2004b.Formula : Type

The formulas: atomic predications, negation, conjunction, and the attitude construction i V-t-w that_{c_k} φ, whose complementizer binds the context variable k.

• atom (P : ℕ) (i : Term PersonFeature) (t : TimeTerm) (w : Term MoodFeature) : Formula
• neg (φ : Formula) : Formula
• conj (φ ψ : Formula) : Formula
• att (V : ℕ) (i : Term PersonFeature) (t : TimeTerm) (w : Term MoodFeature) (k : ℕ) (φ : Formula) : Formula

def Schlenker2004b.args {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (s : Assignment W E P T) (i : Term PersonFeature) (t : TimeTerm) (w : Term MoodFeature) : E × T × W

The individual, time and world arguments of a predicate or attitude verb.

Equations

• Schlenker2004b.args s i t w = (Schlenker2004b.Term.value s s.ind Reference.Context.agent i, Schlenker2004b.TimeTerm.value s t, Schlenker2004b.Term.value s s.world Reference.Context.world w)

def Schlenker2004b.attAt {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (M : Model W E P T) (s : Assignment W E P T) (V : ℕ) (i : Term PersonFeature) (t : TimeTerm) (w : Term MoodFeature) : Option (Set (Reference.Context W E P T))

The contexts compatible with the attitude V at the arguments, if there is one.

Equations

• One or more equations did not get rendered due to their size.

def Schlenker2004b.Formula.Weird {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (M : Model W E P T) (c₀ : Reference.Context W E P T) [Preorder T] : Assignment W E P T → Formula → Prop

Presupposition failure of a formula: an argument is weird, or some context compatible with the attitude makes the complement weird.

Equations

• One or more equations did not get rendered due to their size.
• Schlenker2004b.Formula.Weird M c₀ x✝ (Schlenker2004b.Formula.atom P_1 i t w) = Schlenker2004b.ArgsWeird M c₀ x✝ i t w
• Schlenker2004b.Formula.Weird M c₀ x✝ φ.neg = Schlenker2004b.Formula.Weird M c₀ x✝ φ
• Schlenker2004b.Formula.Weird M c₀ x✝ (φ.conj ψ) = (Schlenker2004b.Formula.Weird M c₀ x✝ φ ∨ Schlenker2004b.Formula.Weird M c₀ x✝ ψ)

def Schlenker2004b.Formula.Holds {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (M : Model W E P T) : Assignment W E P T → Formula → Prop

Truth of a formula: an attitude report holds when there is such an attitude and its complement holds at every compatible context.

Equations

• One or more equations did not get rendered due to their size.
• Schlenker2004b.Formula.Holds M x✝ φ.neg = ¬Schlenker2004b.Formula.Holds M x✝ φ
• Schlenker2004b.Formula.Holds M x✝ (φ.conj ψ) = (Schlenker2004b.Formula.Holds M x✝ φ ∧ Schlenker2004b.Formula.Holds M x✝ ψ)
• Schlenker2004b.Formula.Holds M x✝ (Schlenker2004b.Formula.att V i t w k φ) = ∃ A ∈ Schlenker2004b.attAt M x✝ V i t w, ∀ c ∈ A, Schlenker2004b.Formula.Holds M (x✝.updateCtx k c) φ

De se readings and agreement (§1)

def Schlenker2004b.deSe (V Pr : ℕ) (i : Term PersonFeature) (t : TimeTerm) (w : Term MoodFeature) (k : ℕ) : Formula

(13b), (23b): the report whose embedded arguments are all read de se, the coordinates of the bound context variable, pronounced with the features of the diacritic.

Equations

• One or more equations did not get rendered due to their size.

theorem Schlenker2004b.deSe_holds_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (M : Model W E P T) (s : Assignment W E P T) (V Pr : ℕ) (i : Term PersonFeature) (t : TimeTerm) (w : Term MoodFeature) (k : ℕ) : Formula.Holds M s (deSe V Pr i t w k) ↔ ∃ A ∈ attAt M s V i t w, ∀ c ∈ A, M.pred Pr c.agent c.time c.world

(13b): a de se report holds iff there is such an attitude and at every compatible context its agent satisfies the predicate at its time in its world.

theorem Schlenker2004b.deSe_weird_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (M : Model W E P T) (c₀ : Reference.Context W E P T) (s : Assignment W E P T) (V Pr : ℕ) (i : Term PersonFeature) (t : TimeTerm) (w : Term MoodFeature) (k : ℕ) [Preorder T] : Formula.Weird M c₀ s (deSe V Pr i t w k) ↔ ArgsWeird M c₀ s i t w

The embedded features of a de se report, being uninterpreted, add no presupposition: the report is weird only through its matrix arguments.

theorem Schlenker2004b.past_coord_weird_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (M : Model W E P T) (c₀ : Reference.Context W E P T) (s : Assignment W E P T) (V Pr : ℕ) (i : Term PersonFeature) (t : TimeTerm) (w : Term MoodFeature) (k : ℕ) [Preorder T] : Formula.Weird M c₀ s (Formula.att V i t w k (Formula.atom Pr (Term.coord k) (TimeTerm.base (Term.feat TenseFeature.past (Term.coord k))) (Term.coord k))) ↔ ArgsWeird M c₀ s i t w ∨ ∃ A ∈ attAt M s V i t w, ∃ c ∈ A, ¬c.time < c₀.time

(17b), (18): interpreting the past feature on the de se time coordinate presupposes, at every context compatible with the attitude, that its time precedes the utterance time.

theorem Schlenker2004b.past_coord_weird {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (M : Model W E P T) (c₀ : Reference.Context W E P T) (s : Assignment W E P T) (V Pr : ℕ) (i : Term PersonFeature) (t : TimeTerm) (w : Term MoodFeature) (k : ℕ) [Preorder T] (h : ∃ A ∈ attAt M s V i t w, A.Nonempty ∧ ∀ c ∈ A, c₀.time < c.time) : Formula.Weird M c₀ s (Formula.att V i t w k (Formula.atom Pr (Term.coord k) (TimeTerm.base (Term.feat TenseFeature.past (Term.coord k))) (Term.coord k)))

(19): when the attitude holder takes the time of her thought to be after the utterance time, an interpreted embedded past is weird, although the sentence is fine.

theorem Schlenker2004b.he_coord_weird {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (M : Model W E P T) (c₀ : Reference.Context W E P T) (s : Assignment W E P T) (V Pr : ℕ) (i : Term PersonFeature) (t : TimeTerm) (w : Term MoodFeature) (k : ℕ) [Preorder T] (hex : ∀ (x : E), M.female x c₀.time c₀.world → ¬M.male x c₀.time c₀.world) (h : ∃ A ∈ attAt M s V i t w, A.Nonempty ∧ ∀ c ∈ A, M.female c.agent c₀.time c₀.world) : Formula.Weird M c₀ s (Formula.att V i t w k (Formula.atom Pr (Term.feat PersonFeature.he (Term.coord k)) (TimeTerm.base (Term.coord k)) (Term.coord k)))

(16): interpreting a masculine feature on the de se subject presupposes that the agent of every compatible context is male, which the report of a hope to become a woman refutes.

theorem Schlenker2004b.ind_coord_not_weird_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (M : Model W E P T) (c₀ : Reference.Context W E P T) (s : Assignment W E P T) (V Pr : ℕ) (i : Term PersonFeature) (t : TimeTerm) (w : Term MoodFeature) (k : ℕ) [Preorder T] (hargs : ¬ArgsWeird M c₀ s i t w) : ¬Formula.Weird M c₀ s (Formula.att V i t w k (Formula.atom Pr (Term.coord k) (TimeTerm.base (Term.coord k)) (Term.feat MoodFeature.ind (Term.coord k)))) ↔ ∀ A ∈ attAt M s V i t w, ∀ c ∈ A, c.world = c₀.world

(21): interpreting the indicative on the de se world coordinate presupposes that the world of every compatible context is the actual world, that is, that the agent is omniscient.

The generalized upper limit constraint (§2)

def Schlenker2004b.ULC {C : Type u_5} {α : Type u_6} (beyond : α → α → Prop) (κ : C → α) (d : C → Set α) (c : C) : Prop

(38), (40): the coordinate κ c of the local context c is an upper limit for the description d in its scope, which may not lie entirely beyond it. For times, beyond is strictly after; for worlds, distinct.

Equations

• Schlenker2004b.ULC beyond κ d c = ¬∀ x ∈ d c, beyond (κ c) x

theorem Schlenker2004b.ulc_time_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [LinearOrder T] (d : Reference.Context W E P T → Set T) (c : Reference.Context W E P T) : ULC (fun (x1 x2 : T) => x1 < x2) Reference.Context.time d c ↔ ∃ t ∈ d c, t ≤ c.time

(38): a time description satisfies the constraint iff it reaches the local time.

theorem Schlenker2004b.ulc_world_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (e : Reference.Context W E P T → Set W) (c : Reference.Context W E P T) : ULC (fun (x1 x2 : W) => x1 ≠ x2) Reference.Context.world e c ↔ c.world ∈ e c

(40): a world description satisfies the constraint iff it contains the local world.

theorem Schlenker2004b.ulc_singleton_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [LinearOrder T] (r : T) (c : Reference.Context W E P T) : ULC (fun (x1 x2 : T) => x1 < x2) Reference.Context.time (fun (x : Reference.Context W E P T) => {r}) c ↔ compare r c.time ∈ Tense.upperLimitConstraint

On a description denoting a single time the constraint is the upper limit constraint on reference times of Semantics/Tense/Embedding.

theorem Schlenker2004b.doubleAccess_of_ulc {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c₀ : Reference.Context W E P T) [LinearOrder T] {A : Set (Reference.Context W E P T)} {c : Reference.Context W E P T} (hc : c ∈ A) (d : Reference.Context W E P T → Set T) (hd : (d c).OrdConnected) (hle : c.time ≤ c₀.time) (hii : c₀.time ∈ d c) (hiii : ∀ c' ∈ A, ULC (fun (x1 x2 : T) => x1 < x2) Reference.Context.time d c') : {c.time, c₀.time} ⊆ d c

(39): a present tense under a past attitude denotes the utterance time (i'), the description contains it at the actual context of the thought (ii'), and the constraint holds at every compatible context (iii'); when the agent is not mistaken about the time, so that the actual context is compatible with the thought, the description is about both the time of the thought and the utterance time.

theorem Schlenker2004b.worldDoubleAccess_of_ulc {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c₀ : Reference.Context W E P T) {A : Set (Reference.Context W E P T)} {c : Reference.Context W E P T} (hc : c ∈ A) (e : Reference.Context W E P T → Set W) (hii : c₀.world ∈ e c) (hiii : ∀ c' ∈ A, ULC (fun (x1 x2 : W) => x1 ≠ x2) Reference.Context.world e c') : {c.world, c₀.world} ⊆ e c

(41): the modal counterpart. An indicative under a subjunctive attitude denotes the actual world (i'), the description contains it at the actual context of the thought (ii'), and the constraint holds at every compatible context (iii'); when the actual context is compatible with the thought, the description is about both the world of the thought and the actual world.