Schlenker (2004a): Context of Thought and Context of Utterance

This file formalizes the two-context logic of [Sch04b]. A sentence is evaluated against a Context of Utterance, the point at which a thought is expressed, and a Context of Thought, the point at which it originates. Tenses and pronouns are sorted variables: the assignment gives their value, and the Context of Utterance fixes the domain that value must lie in, on pain of referential failure (Term.sorted, Term.Defined). Every other indexical is a function of the Context of Thought (Term.indexical, Term.value). The Context of Utterance therefore enters the definedness conditions and never the truth conditions, which is the paper's Elimination of the Context of Utterance: Formula.Realize takes the Context of Thought alone, and replacing the sorted variables by simple ones (Formula.strip) preserves truth (realize_strip) and removes every source of failure (defined_strip).

Free Indirect Discourse and the Historical Present are the two ways in which exactly one of the two contexts is the actual one. In Tomorrow was Monday (1), a past tense under an adverbial of the Context of Thought is defined only when the thought precedes the utterance (defined_lamPast_iff), so against a single context the sentence is contradictory (not_defined_lamPast_self) and the two contexts must differ (ne_of_defined_lamPast). In Fifty eight years ago ... the Germans attack Vercors (2), a present tense under the adverbial is defined only when the Context of Utterance lies fifty-eight years before the Context of Thought (defined_lamPres_iff), and a first person pronoun in the same passage makes that past context improper (not_proper_of_defined_lamPres).

Implementation notes

• The appendix's sole world term actually, the world of the Context of Thought, is built into the atomic clauses; the paper's two predicate arities are Formula.atom₀ and Formula.atom₁, with the predicates given as Lean propositions.
• Truth is the paper's pair of predicates: Formula.Defined is the negation of weird and Formula.Realize is true, read with the junk-value convention where the paper leaves truth undefined. A λ-abstraction whose argument fails is weird, which the appendix leaves implicit.
• The rows of Data/Examples/Schlenker2004a.json are the paper's (1) and (2); the schemas Formula.lamPast and Formula.lamPres are their logical forms with the predicate left open. Banfield's Priority of SPEAKER and the interpretation of gender features are discussed in the paper without a formal proposal and are not formalized.

References

• [Sch04b]
• [Ban82]
• [Kap89]

Terms

inductive Schlenker2004a.Term (C : Type u_1) (α : Type u_2) : Type (max u_1 u_2)

A term of the two-context logic over contexts C, valued in α. A simple variable and a multiply sorted variable both take their value from the assignment; the sorted variable is in addition restricted to a domain fixed by the Context of Utterance, outside which it fails to refer. An indexical is a function of the Context of Thought.

• var {C : Type u_1} {α : Type u_2} (k : ℕ) : Term C α
• sorted {C : Type u_1} {α : Type u_2} (k : ℕ) (domain : C → α → Prop) : Term C α
• indexical {C : Type u_1} {α : Type u_2} (f : C → α) : Term C α

def Schlenker2004a.Term.value {C : Type u_1} {α : Type u_2} : Term C α → Assignment α → C → α

The value of a term: the assignment's value at a variable, the Context of Thought's at an indexical. The Context of Utterance plays no role.

Equations

• (Schlenker2004a.Term.var k).value x✝¹ x✝ = x✝¹ k
• (Schlenker2004a.Term.sorted k domain).value x✝¹ x✝ = x✝¹ k
• (Schlenker2004a.Term.indexical f).value x✝¹ x✝ = f x✝

def Schlenker2004a.Term.Defined {C : Type u_1} {α : Type u_2} : Term C α → Assignment α → C → Prop

A term is defined unless it is a sorted variable whose value lies outside its domain at the Context of Utterance. The Context of Thought plays no role.

Equations

• (Schlenker2004a.Term.sorted k D).Defined x✝¹ x✝ = D x✝ (x✝¹ k)
• x✝².Defined x✝¹ x✝ = True

def Schlenker2004a.Term.strip {C : Type u_1} {α : Type u_2} : Term C α → Term C α

Replace a sorted variable by the simple variable of the same index.

Equations

• (Schlenker2004a.Term.sorted k domain).strip = Schlenker2004a.Term.var k
• x✝.strip = x✝

def Schlenker2004a.Term.name {C : Type u_1} {α : Type u_2} (a : α) : Term C α

A name: the indexical constant at a.

Equations

• Schlenker2004a.Term.name a = Schlenker2004a.Term.indexical fun (x : C) => a

@[simp]

theorem Schlenker2004a.Term.value_var {C : Type u_1} {α : Type u_2} {s : Assignment α} {ct : C} {k : ℕ} : (var k).value s ct = s k

@[simp]

theorem Schlenker2004a.Term.value_sorted {C : Type u_1} {α : Type u_2} {s : Assignment α} {ct : C} {k : ℕ} {D : C → α → Prop} : (sorted k D).value s ct = s k

@[simp]

theorem Schlenker2004a.Term.value_indexical {C : Type u_1} {α : Type u_2} {s : Assignment α} {ct : C} {f : C → α} : (indexical f).value s ct = f ct

@[simp]

theorem Schlenker2004a.Term.value_name {C : Type u_1} {α : Type u_2} {s : Assignment α} {ct : C} (a : α) : (name a).value s ct = a

@[simp]

theorem Schlenker2004a.Term.defined_var {C : Type u_1} {α : Type u_2} {s : Assignment α} {cu : C} {k : ℕ} : (var k).Defined s cu

@[simp]

theorem Schlenker2004a.Term.defined_sorted {C : Type u_1} {α : Type u_2} {s : Assignment α} {cu : C} {k : ℕ} {D : C → α → Prop} : (sorted k D).Defined s cu ↔ D cu (s k)

@[simp]

theorem Schlenker2004a.Term.defined_indexical {C : Type u_1} {α : Type u_2} {s : Assignment α} {cu : C} {f : C → α} : (indexical f).Defined s cu

@[simp]

theorem Schlenker2004a.Term.defined_name {C : Type u_1} {α : Type u_2} {s : Assignment α} {cu : C} (a : α) : (name a).Defined s cu

@[simp]

theorem Schlenker2004a.Term.value_strip {C : Type u_1} {α : Type u_2} {s : Assignment α} {ct : C} (t : Term C α) : t.strip.value s ct = t.value s ct

@[simp]

theorem Schlenker2004a.Term.defined_strip {C : Type u_1} {α : Type u_2} {s : Assignment α} {cu : C} (t : Term C α) : t.strip.Defined s cu

The lexicon of (20) and (21)

Pronouns and tenses are sorted variables whose domains are read off the Context of Utterance; the remaining indexicals are functions of the Context of Thought.

def Schlenker2004a.Term.I {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (k : ℕ) : Term (Reference.Context W E P T) E

First person: an individual variable restricted to the speaker of the Context of Utterance.

Equations

• Schlenker2004a.Term.I k = Schlenker2004a.Term.sorted k fun (cu : Reference.Context W E P T) (e : E) => e = cu.agent

def Schlenker2004a.Term.you {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (k : ℕ) : Term (Reference.Context W E P T) E

Second person: an individual variable restricted to the addressee of the Context of Utterance.

Equations

• Schlenker2004a.Term.you k = Schlenker2004a.Term.sorted k fun (cu : Reference.Context W E P T) (e : E) => e = cu.addressee

def Schlenker2004a.Term.third {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (gender : E → T → W → Prop) (k : ℕ) : Term (Reference.Context W E P T) E

Third person of a gender: an individual variable restricted to the individuals of that gender, at the time and in the world of the Context of Utterance, who are neither its speaker nor its addressee.

Equations

• Schlenker2004a.Term.third gender k = Schlenker2004a.Term.sorted k fun (cu : Reference.Context W E P T) (e : E) => gender e cu.time cu.world ∧ e ≠ cu.agent ∧ e ≠ cu.addressee

def Schlenker2004a.Term.pres {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (k : ℕ) : Term (Reference.Context W E P T) T

Present tense: a time variable restricted to the time of the Context of Utterance.

Equations

• Schlenker2004a.Term.pres k = Schlenker2004a.Term.sorted k fun (cu : Reference.Context W E P T) (t : T) => t = cu.time

def Schlenker2004a.Term.past {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [LT T] (k : ℕ) : Term (Reference.Context W E P T) T

Past tense: a time variable restricted to the times before the Context of Utterance.

Equations

• Schlenker2004a.Term.past k = Schlenker2004a.Term.sorted k fun (cu : Reference.Context W E P T) (t : T) => t < cu.time

def Schlenker2004a.Term.timeIndexical {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (f : T → T) : Term (Reference.Context W E P T) T

A time indexical: f applied to the time of the Context of Thought. Now is the identity, tomorrow the day successor, fifty eight years ago the subtraction of fifty-eight years.

Equations

• Schlenker2004a.Term.timeIndexical f = Schlenker2004a.Term.indexical fun (ct : Reference.Context W E P T) => f ct.time

@[simp]

theorem Schlenker2004a.Term.defined_I {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sE : Assignment E} {c : Reference.Context W E P T} {k : ℕ} : (I k).Defined sE c ↔ sE k = c.agent

@[simp]

theorem Schlenker2004a.Term.defined_you {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sE : Assignment E} {c : Reference.Context W E P T} {k : ℕ} : (you k).Defined sE c ↔ sE k = c.addressee

@[simp]

theorem Schlenker2004a.Term.defined_third {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sE : Assignment E} {c : Reference.Context W E P T} {k : ℕ} (gender : E → T → W → Prop) : (third gender k).Defined sE c ↔ gender (sE k) c.time c.world ∧ sE k ≠ c.agent ∧ sE k ≠ c.addressee

@[simp]

theorem Schlenker2004a.Term.defined_pres {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sT : Assignment T} {c : Reference.Context W E P T} {k : ℕ} : (pres k).Defined sT c ↔ sT k = c.time

@[simp]

theorem Schlenker2004a.Term.defined_past {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sT : Assignment T} {c : Reference.Context W E P T} {k : ℕ} [LT T] : (past k).Defined sT c ↔ sT k < c.time

@[simp]

theorem Schlenker2004a.Term.defined_timeIndexical {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sT : Assignment T} {c : Reference.Context W E P T} (f : T → T) : (timeIndexical f).Defined sT c

@[simp]

theorem Schlenker2004a.Term.value_I {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sE : Assignment E} {c : Reference.Context W E P T} {k : ℕ} : (I k).value sE c = sE k

@[simp]

theorem Schlenker2004a.Term.value_you {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sE : Assignment E} {c : Reference.Context W E P T} {k : ℕ} : (you k).value sE c = sE k

@[simp]

theorem Schlenker2004a.Term.value_third {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sE : Assignment E} {c : Reference.Context W E P T} {k : ℕ} (gender : E → T → W → Prop) : (third gender k).value sE c = sE k

@[simp]

theorem Schlenker2004a.Term.value_pres {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sT : Assignment T} {c : Reference.Context W E P T} {k : ℕ} : (pres k).value sT c = sT k

@[simp]

theorem Schlenker2004a.Term.value_past {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sT : Assignment T} {c : Reference.Context W E P T} {k : ℕ} [LT T] : (past k).value sT c = sT k

@[simp]

theorem Schlenker2004a.Term.value_timeIndexical {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sT : Assignment T} {c : Reference.Context W E P T} (f : T → T) : (timeIndexical f).value sT c = f c.time

Formulas

inductive Schlenker2004a.Formula (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 formula of the two-context logic: atomic predications of the paper's two arities, whose world argument is actually; λ-abstraction over an individual or a time variable applied to a term; and the Boolean connectives.

• atom₀ {W : Type u_5} {E : Type u_6} {P : Type u_7} {T : Type u_8} (R : T → W → Prop) (t : Term (Reference.Context W E P T) T) : Formula W E P T
• atom₁ {W : Type u_5} {E : Type u_6} {P : Type u_7} {T : Type u_8} (Q : E → T → W → Prop) (i : Term (Reference.Context W E P T) E) (t : Term (Reference.Context W E P T) T) : Formula W E P T
• lamE {W : Type u_5} {E : Type u_6} {P : Type u_7} {T : Type u_8} (i : Term (Reference.Context W E P T) E) (k : ℕ) (φ : Formula W E P T) : Formula W E P T
• lamT {W : Type u_5} {E : Type u_6} {P : Type u_7} {T : Type u_8} (t : Term (Reference.Context W E P T) T) (k : ℕ) (φ : Formula W E P T) : Formula W E P T
• not {W : Type u_5} {E : Type u_6} {P : Type u_7} {T : Type u_8} (φ : Formula W E P T) : Formula W E P T
• and {W : Type u_5} {E : Type u_6} {P : Type u_7} {T : Type u_8} (φ ψ : Formula W E P T) : Formula W E P T
• or {W : Type u_5} {E : Type u_6} {P : Type u_7} {T : Type u_8} (φ ψ : Formula W E P T) : Formula W E P T

def Schlenker2004a.Formula.Realize {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} : Formula W E P T → Assignment E → Assignment T → Reference.Context W E P T → Prop

Truth at an assignment and a Context of Thought. The Context of Utterance plays no role: this signature is the paper's Elimination of the Context of Utterance.

Equations

• (Schlenker2004a.Formula.atom₀ R t).Realize x✝² x✝¹ x✝ = R (t.value x✝¹ x✝) x✝.world
• (Schlenker2004a.Formula.atom₁ Q i t).Realize x✝² x✝¹ x✝ = Q (i.value x✝² x✝) (t.value x✝¹ x✝) x✝.world
• (Schlenker2004a.Formula.lamE i k φ).Realize x✝² x✝¹ x✝ = φ.Realize (Function.update x✝² k (i.value x✝² x✝)) x✝¹ x✝
• (Schlenker2004a.Formula.lamT t k φ).Realize x✝² x✝¹ x✝ = φ.Realize x✝² (Function.update x✝¹ k (t.value x✝¹ x✝)) x✝
• φ.not.Realize x✝² x✝¹ x✝ = ¬φ.Realize x✝² x✝¹ x✝
• (φ.and ψ).Realize x✝² x✝¹ x✝ = (φ.Realize x✝² x✝¹ x✝ ∧ ψ.Realize x✝² x✝¹ x✝)
• (φ.or ψ).Realize x✝² x✝¹ x✝ = (φ.Realize x✝² x✝¹ x✝ ∨ ψ.Realize x✝² x✝¹ x✝)

def Schlenker2004a.Formula.Defined {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} : Formula W E P T → Assignment E → Assignment T → Reference.Context W E P T → Reference.Context W E P T → Prop

Definedness, the negation of the paper's weird, at an assignment, a Context of Utterance and a Context of Thought: every sorted variable, under the values the abstractions bind, lies in its domain at the Context of Utterance.

Equations

• (Schlenker2004a.Formula.atom₀ R t).Defined x✝³ x✝² x✝¹ x✝ = t.Defined x✝² x✝¹
• (Schlenker2004a.Formula.atom₁ Q i t).Defined x✝³ x✝² x✝¹ x✝ = (i.Defined x✝³ x✝¹ ∧ t.Defined x✝² x✝¹)
• (Schlenker2004a.Formula.lamE i k φ).Defined x✝³ x✝² x✝¹ x✝ = (i.Defined x✝³ x✝¹ ∧ φ.Defined (Function.update x✝³ k (i.value x✝³ x✝)) x✝² x✝¹ x✝)
• (Schlenker2004a.Formula.lamT t k φ).Defined x✝³ x✝² x✝¹ x✝ = (t.Defined x✝² x✝¹ ∧ φ.Defined x✝³ (Function.update x✝² k (t.value x✝² x✝)) x✝¹ x✝)
• φ.not.Defined x✝³ x✝² x✝¹ x✝ = φ.Defined x✝³ x✝² x✝¹ x✝
• (φ.and ψ).Defined x✝³ x✝² x✝¹ x✝ = (φ.Defined x✝³ x✝² x✝¹ x✝ ∧ ψ.Defined x✝³ x✝² x✝¹ x✝)
• (φ.or ψ).Defined x✝³ x✝² x✝¹ x✝ = (φ.Defined x✝³ x✝² x✝¹ x✝ ∧ ψ.Defined x✝³ x✝² x✝¹ x✝)

def Schlenker2004a.Formula.strip {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} : Formula W E P T → Formula W E P T

The stripped formula φ* of (23): every sorted variable replaced by the simple variable of its index.

Equations

• (Schlenker2004a.Formula.atom₀ R t).strip = Schlenker2004a.Formula.atom₀ R t.strip
• (Schlenker2004a.Formula.atom₁ Q i t).strip = Schlenker2004a.Formula.atom₁ Q i.strip t.strip
• (Schlenker2004a.Formula.lamE i k φ).strip = Schlenker2004a.Formula.lamE i.strip k φ.strip
• (Schlenker2004a.Formula.lamT t k φ).strip = Schlenker2004a.Formula.lamT t.strip k φ.strip
• φ.not.strip = φ.strip.not
• (φ.and ψ).strip = φ.strip.and ψ.strip
• (φ.or ψ).strip = φ.strip.or ψ.strip

theorem Schlenker2004a.Formula.defined_strip {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {cu ct : Reference.Context W E P T} (φ : Formula W E P T) (sE : Assignment E) (sT : Assignment T) : φ.strip.Defined sE sT cu ct

A stripped formula never fails to refer.

theorem Schlenker2004a.Formula.realize_strip {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {ct : Reference.Context W E P T} (φ : Formula W E P T) (sE : Assignment E) (sT : Assignment T) : φ.strip.Realize sE sT ct ↔ φ.Realize sE sT ct

Elimination of the Context of Utterance, (23): stripping preserves truth. The paper restricts the claim to formulas that are not weird because its truth predicate is undefined elsewhere; here it holds outright.

theorem Schlenker2004a.Formula.not_defined_lamT_and_past_pres {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sE : Assignment E} {sT : Assignment T} {cu ct : Reference.Context W E P T} {k : ℕ} [Preorder T] (t : Term (Reference.Context W E P T) T) (R R' : T → W → Prop) : ¬(lamT t k ((atom₀ R (Term.past k)).and (atom₀ R' (Term.pres k)))).Defined sE sT cu ct

(28c): a past and a present tense under one time abstraction cannot both be defined, so the choice of tense in a passage must be consistent.

Free Indirect Discourse: a past tense under an adverbial of the Context of Thought

def Schlenker2004a.Formula.lamPast {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [LT T] (f : T → T) (R : T → W → Prop) (k : ℕ) : Formula W E P T

The logical form of (1), Tomorrow was Monday (Examples.ex1), and of the appendix's Now it was raining: a time indexical f of the Context of Thought abstracted over the time argument of a past-tense predication.

Equations

• Schlenker2004a.Formula.lamPast f R k = Schlenker2004a.Formula.lamT (Schlenker2004a.Term.timeIndexical f) k (Schlenker2004a.Formula.atom₀ R (Schlenker2004a.Term.past k))

@[simp]

theorem Schlenker2004a.Formula.defined_lamPast_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sE : Assignment E} {sT : Assignment T} {cu ct : Reference.Context W E P T} {k : ℕ} {f : T → T} {R : T → W → Prop} [LT T] : (lamPast f R k).Defined sE sT cu ct ↔ f ct.time < cu.time

(1) is defined exactly when the adverbial's time precedes the Context of Utterance.

@[simp]

theorem Schlenker2004a.Formula.realize_lamPast_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sE : Assignment E} {sT : Assignment T} {ct : Reference.Context W E P T} {k : ℕ} {f : T → T} {R : T → W → Prop} [LT T] : (lamPast f R k).Realize sE sT ct ↔ R (f ct.time) ct.world

(1) is true exactly when the predicate holds at the adverbial's time in the world of the Context of Thought; the Context of Utterance has been eliminated.

theorem Schlenker2004a.Formula.not_defined_lamPast_self {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sE : Assignment E} {sT : Assignment T} {c : Reference.Context W E P T} {k : ℕ} {f : T → T} {R : T → W → Prop} [Preorder T] (hf : ∀ (t : T), t ≤ f t) : ¬(lamPast f R k).Defined sE sT c c

(9b): against a single context, a past tense under now or tomorrow is contradictory.

theorem Schlenker2004a.Formula.ne_of_defined_lamPast {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sE : Assignment E} {sT : Assignment T} {cu ct : Reference.Context W E P T} {k : ℕ} {f : T → T} {R : T → W → Prop} [Preorder T] (hf : ∀ (t : T), t ≤ f t) (hd : (lamPast f R k).Defined sE sT cu ct) : cu ≠ ct

A felicitous (1) is evaluated against two distinct contexts, the paper's decisive argument for the Context of Thought: in Free Indirect Discourse the Context of Utterance is the actual one and the character's thought lies in its past, in the Historical Present the Context of Thought is the actual one and the utterance is set in the past.

The Historical Present: a present tense under an adverbial of the Context of Thought

def Schlenker2004a.Formula.lamPres {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (f : T → T) (Q : E → T → W → Prop) (i : Term (Reference.Context W E P T) E) (k : ℕ) : Formula W E P T

The logical form of (2), Fifty eight years ago ... the Germans attack Vercors (Examples.ex2): a time indexical f of the Context of Thought abstracted over the time argument of a present-tense predication of the individual term i.

Equations

• Schlenker2004a.Formula.lamPres f Q i k = Schlenker2004a.Formula.lamT (Schlenker2004a.Term.timeIndexical f) k (Schlenker2004a.Formula.atom₁ Q i (Schlenker2004a.Term.pres k))

@[simp]

theorem Schlenker2004a.Formula.defined_lamPres_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sE : Assignment E} {sT : Assignment T} {cu ct : Reference.Context W E P T} {k : ℕ} {f : T → T} {Q : E → T → W → Prop} {i : Term (Reference.Context W E P T) E} : (lamPres f Q i k).Defined sE sT cu ct ↔ i.Defined sE cu ∧ f ct.time = cu.time

(29c): (2) is defined exactly when the individual term is and the Context of Utterance is at the adverbial's time.

@[simp]

theorem Schlenker2004a.Formula.realize_lamPres_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sE : Assignment E} {sT : Assignment T} {ct : Reference.Context W E P T} {k : ℕ} {f : T → T} {Q : E → T → W → Prop} {i : Term (Reference.Context W E P T) E} : (lamPres f Q i k).Realize sE sT ct ↔ Q (i.value sE ct) (f ct.time) ct.world

(29c): (2) is true exactly when the predicate holds of the individual at the adverbial's time in the world of the Context of Thought.

theorem Schlenker2004a.Formula.not_defined_lamPres_name_self {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sE : Assignment E} {sT : Assignment T} {c : Reference.Context W E P T} {k : ℕ} {f : T → T} {Q : E → T → W → Prop} (hf : ∀ (t : T), f t ≠ t) (a : E) : ¬(lamPres f Q (Term.name a) k).Defined sE sT c c

Against a single context, a present tense under an adverbial that moves the time is contradictory.

theorem Schlenker2004a.Formula.not_proper_of_defined_lamPres {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {sE : Assignment E} {sT : Assignment T} {cu ct : Reference.Context W E P T} {k : ℕ} {f : T → T} {Q : E → T → W → Prop} (alive : E → T → W → Prop) {j : ℕ} (hd : (lamPres f Q (Term.I j) k).Defined sE sT cu ct) (h : ¬alive (sE j) cu.time cu.world) : ¬cu.Proper fun (x1 : E) (x2 : W) => alive x1 cu.time x2

The necessity of improper contexts (31): a first person pronoun in the Historical Present denotes the speaker of the Context of Utterance, so when that speaker is not alive at its time in its world the context is improper in the sense of [Kap89].