Heim (1994): Comments on Abusch's Theory of Tense

This file formalizes the implementation that [Hei94a] gives [Abu97]'s sequence-of-tense analysis: tenses are time variables whose distinctive content is a presupposition, attitude verbs quantify over the world–time pairs compatible with the holder's beliefs, and the Upper Limit Constraint is the presupposition (16) that no tense denotes a time after the local evaluation time, the distinguished variable 0 rebound by the abstractor in Comp. LF is the fragment of the paper's logical forms and Def its presuppositions under the tense entries (4) of Sections 1 and 2, so that the calculations of Section 2 are theorems: the presuppositions of the de dicto past under a past (20), of the simultaneous (29) and free (30) construals of John believed that Bill was asleep, and the four presuppositions of the double-access (38) through res-movement and time-concepts (33), with the consequence that the res concept must overlap the utterance time and so cannot be backshifting. Section 3's zero affixes < and ¬< carry the ordering presuppositions instead, Def', and the Tense Licensing Condition TLC with the definition (67) of "in the domain of" licenses (50), (51), (56), (63) and (65) and excludes (57), (62) and (66).

Implementation notes

• Times are nonempty intervals, so that < is NonemptyInterval.Precedes, o is NonemptyInterval.Overlaps and "does not follow" is NotAfter, the library's Tense.upperLimitConstraint as a perspectival presupposition on intervals.
• Predicates carry their subjects, de dicto descriptions are atomic and always defined, and the presuppositions of the nuclear scopes of woll and of res-moved believe project universally, the law the paper invokes for some and believe. The time-concept is supplied by the context, as in footnote 26.
• Relative clauses and the extensional NP argument of (59)–(60) are outside the fragment, so (52) is taken without its relative clause and the contrast between the definitions (53) and (61) of "in the domain of" is carried by the res-moved (62)–(66).

References

• [Hei94a]
• [Abu97]

Times

def Heim1994a.NotAfter {T : Type u_1} [LinearOrder T] (t t₀ : NonemptyInterval T) : Prop

t does not follow t₀, the relation ¬> of (16).

Equations

• Heim1994a.NotAfter t t₀ = ¬t₀.Precedes t

theorem Heim1994a.notAfter_iff_presup {T : Type u_1} [LinearOrder T] (t t₀ : NonemptyInterval T) : NotAfter t t₀ ↔ Tense.Perspective.Presup Tense.upperLimitConstraint t₀ t

Not following is the library's Upper Limit Constraint as a perspectival presupposition: the interval a tense denotes stands to the local evaluation time in the constraint's cell.

theorem Heim1994a.notAfter_self {T : Type u_1} [LinearOrder T] (t : NonemptyInterval T) : NotAfter t t

theorem Heim1994a.notAfter_of_precedes {T : Type u_1} [LinearOrder T] {t t₀ : NonemptyInterval T} (h : t.Precedes t₀) : NotAfter t t₀

theorem Heim1994a.notAfter_of_overlaps {T : Type u_1} [LinearOrder T] {t t₀ : NonemptyInterval T} (h : t.Overlaps t₀) : NotAfter t t₀

Logical forms

@[reducible, inline]

abbrev Heim1994a.Var : Type

Time variables; 0 is the distinguished evaluation-time variable of Section 1.

Equations

• Heim1994a.Var = ℕ

@[reducible, inline]

abbrev Heim1994a.Assignment (T : Type u_2) [LinearOrder T] : Type u_2

Assignments of times to variables.

Equations

• Heim1994a.Assignment T = (Heim1994a.Var → NonemptyInterval T)

inductive Heim1994a.TenseNode : Type

What occupies a tense position: a tense morpheme (1), the infinitival marker bound from Comp (12), (25), or the trace of a res-moved tense (32).

• PAST (i : Var) : TenseNode
• PRES (i : Var) : TenseNode
• INF (i : Var) : TenseNode
• trace (i : Var) : TenseNode

def Heim1994a.instDecidableEqTenseNode.decEq (x✝ x✝¹ : TenseNode) : Decidable (x✝ = x✝¹)

Equations

• Heim1994a.instDecidableEqTenseNode.decEq (Heim1994a.TenseNode.PAST a) (Heim1994a.TenseNode.PAST b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Heim1994a.instDecidableEqTenseNode.decEq (Heim1994a.TenseNode.PAST i) (Heim1994a.TenseNode.PRES i_1) = isFalse ⋯
• Heim1994a.instDecidableEqTenseNode.decEq (Heim1994a.TenseNode.PAST i) (Heim1994a.TenseNode.INF i_1) = isFalse ⋯
• Heim1994a.instDecidableEqTenseNode.decEq (Heim1994a.TenseNode.PAST i) (Heim1994a.TenseNode.trace i_1) = isFalse ⋯
• Heim1994a.instDecidableEqTenseNode.decEq (Heim1994a.TenseNode.PRES i) (Heim1994a.TenseNode.PAST i_1) = isFalse ⋯
• Heim1994a.instDecidableEqTenseNode.decEq (Heim1994a.TenseNode.PRES a) (Heim1994a.TenseNode.PRES b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Heim1994a.instDecidableEqTenseNode.decEq (Heim1994a.TenseNode.PRES i) (Heim1994a.TenseNode.INF i_1) = isFalse ⋯
• Heim1994a.instDecidableEqTenseNode.decEq (Heim1994a.TenseNode.PRES i) (Heim1994a.TenseNode.trace i_1) = isFalse ⋯
• Heim1994a.instDecidableEqTenseNode.decEq (Heim1994a.TenseNode.INF i) (Heim1994a.TenseNode.PAST i_1) = isFalse ⋯
• Heim1994a.instDecidableEqTenseNode.decEq (Heim1994a.TenseNode.INF i) (Heim1994a.TenseNode.PRES i_1) = isFalse ⋯
• Heim1994a.instDecidableEqTenseNode.decEq (Heim1994a.TenseNode.INF a) (Heim1994a.TenseNode.INF b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Heim1994a.instDecidableEqTenseNode.decEq (Heim1994a.TenseNode.INF i) (Heim1994a.TenseNode.trace i_1) = isFalse ⋯
• Heim1994a.instDecidableEqTenseNode.decEq (Heim1994a.TenseNode.trace i) (Heim1994a.TenseNode.PAST i_1) = isFalse ⋯
• Heim1994a.instDecidableEqTenseNode.decEq (Heim1994a.TenseNode.trace i) (Heim1994a.TenseNode.PRES i_1) = isFalse ⋯
• Heim1994a.instDecidableEqTenseNode.decEq (Heim1994a.TenseNode.trace i) (Heim1994a.TenseNode.INF i_1) = isFalse ⋯
• Heim1994a.instDecidableEqTenseNode.decEq (Heim1994a.TenseNode.trace a) (Heim1994a.TenseNode.trace b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Heim1994a.instDecidableEqTenseNode : DecidableEq TenseNode

Equations

• Heim1994a.instDecidableEqTenseNode = Heim1994a.instDecidableEqTenseNode.decEq

def Heim1994a.TenseNode.var : TenseNode → Var

The variable a tense position denotes (1).

Equations

• (Heim1994a.TenseNode.PAST i).var = i
• (Heim1994a.TenseNode.PRES i).var = i
• (Heim1994a.TenseNode.INF i).var = i
• (Heim1994a.TenseNode.trace i).var = i

inductive Heim1994a.Affix : Type

The zero affixes of Section 3, < (past) and ¬< (non-past).

• past : Affix
• nonpast : Affix

@[instance_reducible]

instance Heim1994a.instDecidableEqAffix : DecidableEq Affix

Equations

• Heim1994a.instDecidableEqAffix x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Heim1994a.LF (V : Type u_2) (D : Type u_3) (A : Type u_4) : Type (max (max u_2 u_3) u_4)

Logical forms: a predicate with its event-time argument and affix; a de dicto description binding a variable, as his 40th birthday λ2 in (20); x believe [λ0 φ] (10); x believe t_res [λj λ0 φ] with a res-moved tense (32); and woll [λ0 φ] (25).

• pred {V : Type u_2} {D : Type u_3} {A : Type u_4} (v : V) (τ : TenseNode) (a : Affix) : LF V D A
• bind {V : Type u_2} {D : Type u_3} {A : Type u_4} (d : D) (j : Var) (φ : LF V D A) : LF V D A
• believe {V : Type u_2} {D : Type u_3} {A : Type u_4} (x : A) (τ : TenseNode) (a : Affix) (φ : LF V D A) : LF V D A
• believeRes {V : Type u_2} {D : Type u_3} {A : Type u_4} (x : A) (τ : TenseNode) (a : Affix) (res : TenseNode) (j : Var) (φ : LF V D A) : LF V D A
• woll {V : Type u_2} {D : Type u_3} {A : Type u_4} (τ : TenseNode) (a : Affix) (φ : LF V D A) : LF V D A

structure Heim1994a.Model (V : Type u_2) (D : Type u_3) (A : Type u_4) (W : Type u_5) (T : Type u_6) [LinearOrder T] : Type (max (max (max (max u_2 u_3) u_4) u_5) u_6)

A model: the extensions of the predicates (3), the values of the de dicto descriptions, and the world–time pairs compatible with a holder's beliefs at a world and time (9).

• ext : V → NonemptyInterval T → W → Prop
• desc : D → W → NonemptyInterval T
• dox : A → W → NonemptyInterval T → Set (Reference.Index W (NonemptyInterval T))

structure Heim1994a.Context (W : Type u_2) (T : Type u_3) [LinearOrder T] : Type (max u_2 u_3)

A context: its world and utterance time and the suitable time-concept it supplies (33), a function from world–time pairs to times.

• world : W
• time : NonemptyInterval T
• concept : Reference.Index W (NonemptyInterval T) → NonemptyInterval T

Sections 1 and 2: the tense entries (4) and the Upper Limit Constraint

def Heim1994a.TenseNode.Def {T : Type u_1} [LinearOrder T] {W : Type u_5} (c : Context W T) (g : Assignment T) : TenseNode → Prop

The lexical presuppositions (4) of the tense morphemes, precedence of and overlap with the utterance time, together with the Upper Limit Constraint (18) on every tense position.

Equations

• Heim1994a.TenseNode.Def c g (Heim1994a.TenseNode.PAST i) = ((g i).Precedes c.time ∧ Heim1994a.NotAfter (g i) (g 0))
• Heim1994a.TenseNode.Def c g (Heim1994a.TenseNode.PRES i) = ((g i).Overlaps c.time ∧ Heim1994a.NotAfter (g i) (g 0))
• Heim1994a.TenseNode.Def c g (Heim1994a.TenseNode.INF i) = Heim1994a.NotAfter (g i) (g 0)
• Heim1994a.TenseNode.Def c g (Heim1994a.TenseNode.trace i) = Heim1994a.NotAfter (g i) (g 0)

def Heim1994a.Def {T : Type u_1} [LinearOrder T] {V : Type u_2} {D : Type u_3} {A : Type u_4} {W : Type u_5} (M : Model V D A W T) (c : Context W T) : LF V D A → Assignment T → W → Prop

Definedness: the presuppositions of a logical form at an assignment and world. Attitude verbs project the presuppositions of their complement to every doxastic alternative (21), a res-moved tense is the context's concept at the holder's world and time (33), and woll projects to every later time.

Equations

• One or more equations did not get rendered due to their size.
• Heim1994a.Def M c (Heim1994a.LF.pred v τ a) x✝¹ x✝ = Heim1994a.TenseNode.Def c x✝¹ τ
• Heim1994a.Def M c (Heim1994a.LF.bind d j φ) x✝¹ x✝ = Heim1994a.Def M c φ (Function.update x✝¹ j (M.desc d x✝)) x✝
• Heim1994a.Def M c (Heim1994a.LF.believe x_3 τ a φ) x✝¹ x✝ = (Heim1994a.TenseNode.Def c x✝¹ τ ∧ ∀ s ∈ M.dox x_3 x✝ (x✝¹ τ.var), Heim1994a.Def M c φ (Function.update x✝¹ 0 s.time) s.world)
• Heim1994a.Def M c (Heim1994a.LF.woll τ a φ) x✝¹ x✝ = (Heim1994a.TenseNode.Def c x✝¹ τ ∧ ∀ (t : NonemptyInterval T), (x✝¹ τ.var).Precedes t → Heim1994a.Def M c φ (Function.update x✝¹ 0 t) x✝)

def Heim1994a.Sat {T : Type u_1} [LinearOrder T] {V : Type u_2} {D : Type u_3} {A : Type u_4} {W : Type u_5} (M : Model V D A W T) (c : Context W T) : LF V D A → Assignment T → W → Prop

Truth: (3), (9), (26) and (33).

Equations

• Heim1994a.Sat M c (Heim1994a.LF.pred v τ a) x✝¹ x✝ = M.ext v (x✝¹ τ.var) x✝
• Heim1994a.Sat M c (Heim1994a.LF.bind d j φ) x✝¹ x✝ = Heim1994a.Sat M c φ (Function.update x✝¹ j (M.desc d x✝)) x✝
• Heim1994a.Sat M c (Heim1994a.LF.believe x_3 τ a φ) x✝¹ x✝ = ∀ s ∈ M.dox x_3 x✝ (x✝¹ τ.var), Heim1994a.Sat M c φ (Function.update x✝¹ 0 s.time) s.world
• Heim1994a.Sat M c (Heim1994a.LF.believeRes x_3 τ a res j φ) x✝¹ x✝ = ∀ s ∈ M.dox x_3 x✝ (x✝¹ τ.var), Heim1994a.Sat M c φ (Function.update (Function.update x✝¹ 0 s.time) j (c.concept s)) s.world
• Heim1994a.Sat M c (Heim1994a.LF.woll τ a φ) x✝¹ x✝ = ∃ (t : NonemptyInterval T), (x✝¹ τ.var).Precedes t ∧ Heim1994a.Sat M c φ (Function.update x✝¹ 0 t) x✝

theorem Heim1994a.def_bind_past {T : Type u_1} [LinearOrder T] {V : Type u_2} {D : Type u_3} {A : Type u_4} {W : Type u_5} (M : Model V D A W T) (c : Context W T) (x : A) (v : V) (d : D) (g : Assignment T) (w : W) : Def M c (LF.believe x (TenseNode.PAST 1) Affix.past (LF.bind d 2 (LF.pred v (TenseNode.PAST 2) Affix.nonpast))) g w ↔ TenseNode.Def c g (TenseNode.PAST 1) ∧ ∀ s ∈ M.dox x w (g 1), (M.desc d s.world).Precedes c.time ∧ NotAfter (M.desc d s.world) s.time

(20): the de dicto past under a past presupposes, at every doxastic alternative of the holder, that the described time precedes the utterance time, (i), and does not follow the alternative's time, (ii).

theorem Heim1994a.def_simultaneous {T : Type u_1} [LinearOrder T] {V : Type u_2} {D : Type u_3} {A : Type u_4} {W : Type u_5} (M : Model V D A W T) (c : Context W T) (x : A) (v : V) (g : Assignment T) (w : W) : Def M c (LF.believe x (TenseNode.PAST 1) Affix.past (LF.pred v (TenseNode.PAST 0) Affix.nonpast)) g w ↔ TenseNode.Def c g (TenseNode.PAST 1) ∧ ∀ s ∈ M.dox x w (g 1), s.time.Precedes c.time

(29): with the lower past bound from Comp, the Upper Limit Constraint is innocuous and only the lexical presupposition of PAST remains, that every doxastic alternative time precedes the utterance time, footnote 23.

theorem Heim1994a.def_free_coindexed {T : Type u_1} [LinearOrder T] {V : Type u_2} {D : Type u_3} {A : Type u_4} {W : Type u_5} (M : Model V D A W T) (c : Context W T) (x : A) (v : V) (g : Assignment T) (w : W) : Def M c (LF.believe x (TenseNode.PAST 1) Affix.past (LF.pred v (TenseNode.PAST 1) Affix.nonpast)) g w ↔ TenseNode.Def c g (TenseNode.PAST 1) ∧ ∀ s ∈ M.dox x w (g 1), (g 1).Precedes c.time ∧ NotAfter (g 1) s.time

(30): with the lower past free and coindexed with the matrix tense, the Upper Limit Constraint projects the presupposition that the holder located himself at or after the matrix time.

theorem Heim1994a.def_res {T : Type u_1} [LinearOrder T] {V : Type u_2} {D : Type u_3} {A : Type u_4} {W : Type u_5} (M : Model V D A W T) (c : Context W T) (x : A) (v : V) (g : Assignment T) (w : W) : Def M c (LF.believeRes x (TenseNode.PAST 1) Affix.past (TenseNode.PAST 2) 3 (LF.pred v (TenseNode.trace 3) Affix.nonpast)) g w ↔ TenseNode.Def c g (TenseNode.PAST 1) ∧ TenseNode.Def c g (TenseNode.PAST 2) ∧ c.concept (w, g 1) = g 2 ∧ ∀ s ∈ M.dox x w (g 1), NotAfter (c.concept s) s.time

(32): res-movement of the lower past. The context's concept yields the res at the holder's world and time, and the Upper Limit Constraint on the trace requires the concept to imply simultaneity or anteriority across the holder's alternatives.

theorem Heim1994a.not_def_res_of_precedes {T : Type u_1} [LinearOrder T] {V : Type u_2} {D : Type u_3} {A : Type u_4} {W : Type u_5} (M : Model V D A W T) (c : Context W T) (x : A) (v : V) (g : Assignment T) (w : W) {s : Reference.Index W (NonemptyInterval T)} (hs : s ∈ M.dox x w (g 1)) (h : s.time.Precedes (c.concept s)) : ¬Def M c (LF.believeRes x (TenseNode.PAST 1) Affix.past (TenseNode.PAST 2) 3 (LF.pred v (TenseNode.trace 3) Affix.nonpast)) g w

A concept that locates a later time at some alternative, as "the next time the lights go out" does, fails the presupposition of (32).

def Heim1994a.doubleAccess {V : Type u_2} {D : Type u_3} {A : Type u_4} (x : A) (v : V) : LF V D A

The double-access LF (38): a present under a past through res-movement.

Equations

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

theorem Heim1994a.def_doubleAccess {T : Type u_1} [LinearOrder T] {V : Type u_2} {D : Type u_3} {A : Type u_4} {W : Type u_5} (M : Model V D A W T) (c : Context W T) (x : A) (v : V) (g : Assignment T) (w : W) (h0 : g 0 = c.time) : Def M c (doubleAccess x v) g w ↔ (g 1).Precedes c.time ∧ (g 2).Overlaps c.time ∧ (∀ s ∈ M.dox x w (g 1), NotAfter (c.concept s) s.time) ∧ c.concept (w, g 1) = g 2

The four presuppositions of (38): (i) the believing time precedes the utterance time, (ii) the res overlaps it, (iii) the concept does not follow the alternative's time at any doxastic alternative, and (iv) the concept yields the res at the holder's world and time.

theorem Heim1994a.overlaps_of_def_doubleAccess {T : Type u_1} [LinearOrder T] {V : Type u_2} {D : Type u_3} {A : Type u_4} {W : Type u_5} (M : Model V D A W T) (c : Context W T) (x : A) (v : V) (g : Assignment T) (w : W) (h0 : g 0 = c.time) (h : Def M c (doubleAccess x v) g w) : (c.concept (w, g 1)).Overlaps c.time

(ii) and (iv) together: the concept, at the holder's actual world and time, overlaps the utterance time, so that "she is pregnant today" is reportable by (38) on the same day only.

theorem Heim1994a.snd_lt_of_def_doubleAccess {T : Type u_1} [LinearOrder T] {V : Type u_2} {D : Type u_3} {A : Type u_4} {W : Type u_5} (M : Model V D A W T) (c : Context W T) (x : A) (v : V) (g : Assignment T) (w : W) (h0 : g 0 = c.time) (h : Def M c (doubleAccess x v) g w) : (g 1).toProd.2 < (c.concept (w, g 1)).toProd.2

With (i), the res must outlast the believing time: its end lies strictly after the end of the believing time, as the day of a "today" or the duration of a pregnancy does.

theorem Heim1994a.not_def_doubleAccess_of_backshifting {T : Type u_1} [LinearOrder T] {V : Type u_2} {D : Type u_3} {A : Type u_4} {W : Type u_5} (M : Model V D A W T) (c : Context W T) (x : A) (v : V) (g : Assignment T) (w : W) (h0 : g 0 = c.time) (hf : ∀ (s : Reference.Index W (NonemptyInterval T)), (c.concept s).Precedes s.time) : ¬Def M c (doubleAccess x v) g w

A backshifting concept, one whose value precedes its argument as "a year ago" does, cannot satisfy (i), (ii) and (iv): (38) can never report such a belief.

Section 3: the affixes and the Tense Licensing Condition

def Heim1994a.Affix.Def {T : Type u_1} [LinearOrder T] (g : Assignment T) (t : NonemptyInterval T) : Affix → Prop

The presuppositions of the affixed predicates (46)–(48): the event time precedes, or does not precede, the evaluation time.

Equations

• Heim1994a.Affix.Def g t Heim1994a.Affix.past = t.Precedes (g 0)
• Heim1994a.Affix.Def g t Heim1994a.Affix.nonpast = ¬t.Precedes (g 0)

def Heim1994a.TenseNode.Def' {T : Type u_1} [LinearOrder T] (g : Assignment T) : TenseNode → Prop

The tense entries of Section 3: PAST a bare variable (1a), PRES with the presupposition (64) of overlapping the evaluation time, and the Upper Limit Constraint on every position.

Equations

• Heim1994a.TenseNode.Def' g (Heim1994a.TenseNode.PAST i) = Heim1994a.NotAfter (g i) (g 0)
• Heim1994a.TenseNode.Def' g (Heim1994a.TenseNode.PRES i) = ((g i).Overlaps (g 0) ∧ Heim1994a.NotAfter (g i) (g 0))
• Heim1994a.TenseNode.Def' g (Heim1994a.TenseNode.INF i) = Heim1994a.NotAfter (g i) (g 0)
• Heim1994a.TenseNode.Def' g (Heim1994a.TenseNode.trace i) = Heim1994a.NotAfter (g i) (g 0)

def Heim1994a.Def' {T : Type u_1} [LinearOrder T] {V : Type u_2} {D : Type u_3} {A : Type u_4} {W : Type u_5} (M : Model V D A W T) (c : Context W T) : LF V D A → Assignment T → W → Prop

Definedness under the entries of Section 3, every predicate affixed.

Equations

• One or more equations did not get rendered due to their size.
• Heim1994a.Def' M c (Heim1994a.LF.pred v τ a) x✝¹ x✝ = (Heim1994a.TenseNode.Def' x✝¹ τ ∧ Heim1994a.Affix.Def x✝¹ (x✝¹ τ.var) a)
• Heim1994a.Def' M c (Heim1994a.LF.bind d j φ) x✝¹ x✝ = Heim1994a.Def' M c φ (Function.update x✝¹ j (M.desc d x✝)) x✝

def Heim1994a.TenseNode.Licensed (host : Affix) (above : Bool) : TenseNode → Prop

Whether a tense is licensed at a position, (49) with (67): a PAST must have its host predicate <-affixed or sit inside an intensional argument of a <-affixed predicate (above), a PRES must have neither.

Equations

• Heim1994a.TenseNode.Licensed host above (Heim1994a.TenseNode.PAST i) = (host = Heim1994a.Affix.past ∨ above = true)
• Heim1994a.TenseNode.Licensed host above (Heim1994a.TenseNode.PRES i) = (host = Heim1994a.Affix.nonpast ∧ above = false)
• Heim1994a.TenseNode.Licensed host above (Heim1994a.TenseNode.INF i) = True
• Heim1994a.TenseNode.Licensed host above (Heim1994a.TenseNode.trace i) = True

def Heim1994a.traceHost {V : Type u_2} {D : Type u_3} {A : Type u_4} (j : Var) : LF V D A → Option Affix

The affix of the predicate whose event-time argument is the trace of variable j, the host of a res-moved tense under (67).

Equations

• Heim1994a.traceHost j (Heim1994a.LF.pred v (Heim1994a.TenseNode.trace i) a) = if i = j then some a else none
• Heim1994a.traceHost j (Heim1994a.LF.pred v τ a) = none
• Heim1994a.traceHost j (Heim1994a.LF.bind d j_1 φ) = Heim1994a.traceHost j φ
• Heim1994a.traceHost j (Heim1994a.LF.believe x_1 (Heim1994a.TenseNode.trace i) a φ) = if i = j then some a else Heim1994a.traceHost j φ
• Heim1994a.traceHost j (Heim1994a.LF.believe x_1 τ a φ) = Heim1994a.traceHost j φ
• Heim1994a.traceHost j (Heim1994a.LF.believeRes x_1 (Heim1994a.TenseNode.trace i) a res j_1 φ) = if i = j then some a else Heim1994a.traceHost j φ
• Heim1994a.traceHost j (Heim1994a.LF.believeRes x_1 τ a res j_1 φ) = Heim1994a.traceHost j φ
• Heim1994a.traceHost j (Heim1994a.LF.woll (Heim1994a.TenseNode.trace i) a φ) = if i = j then some a else Heim1994a.traceHost j φ
• Heim1994a.traceHost j (Heim1994a.LF.woll τ a φ) = Heim1994a.traceHost j φ

def Heim1994a.TLC {V : Type u_2} {D : Type u_3} {A : Type u_4} : Bool → LF V D A → Prop

The Tense Licensing Condition (49) under the definition (67) of "in the domain of": above records whether the position is contained in an intensional argument, the complement of an attitude verb or of woll, of a <-affixed predicate; a res-moved tense is licensed through the host of its trace, its own position being an extensional argument.

Equations

• One or more equations did not get rendered due to their size.
• Heim1994a.TLC x✝ (Heim1994a.LF.pred v τ a) = Heim1994a.TenseNode.Licensed a x✝ τ
• Heim1994a.TLC x✝ (Heim1994a.LF.bind d j φ) = Heim1994a.TLC x✝ φ
• Heim1994a.TLC x✝ (Heim1994a.LF.believe x_2 τ a φ) = (Heim1994a.TenseNode.Licensed a x✝ τ ∧ Heim1994a.TLC (x✝ || decide (a = Heim1994a.Affix.past)) φ)
• Heim1994a.TLC x✝ (Heim1994a.LF.woll τ a φ) = (Heim1994a.TenseNode.Licensed a x✝ τ ∧ Heim1994a.TLC (x✝ || decide (a = Heim1994a.Affix.past)) φ)

theorem Heim1994a.precedes_of_tlc {T : Type u_1} [LinearOrder T] {V : Type u_2} {D : Type u_3} {A : Type u_4} {W : Type u_5} (M : Model V D A W T) (c : Context W T) (v : V) (g : Assignment T) (w : W) {i : Var} {a : Affix} (h : TLC false (LF.pred v (TenseNode.PAST i) a)) (hd : Def' M c (LF.pred v (TenseNode.PAST i) a) g w) : (g i).Precedes (g 0)

An unembedded PAST conveys anteriority: the condition forces the <-affix, whose presupposition is that the event time precedes the utterance time.

theorem Heim1994a.tlc_cry {V : Type u_2} {D : Type u_3} {A : Type u_4} (v : V) : TLC false (LF.pred v (TenseNode.PAST 1) Affix.past)

(50): John PAST₁ <-cry is licensed.

theorem Heim1994a.tlc_decide {V : Type u_2} {D : Type u_3} {A : Type u_4} (x y : A) (having : V) : TLC false (LF.believe x (TenseNode.PAST 1) Affix.past (LF.believe y (TenseNode.INF 0) Affix.nonpast (LF.pred having (TenseNode.PAST 0) Affix.nonpast)))

(51): he PAST₁ <-decide [λ0 PRO to₀ ¬<-tell [λ0 they PAST₀ ¬<-be having ...]], the lower PAST licensed non-locally by <-decide.

theorem Heim1994a.tlc_say {V : Type u_2} {D : Type u_3} {A : Type u_4} (x : A) (buy : V) : TLC false (LF.believe x (TenseNode.PAST 1) Affix.past (LF.woll (TenseNode.PAST 0) Affix.nonpast (LF.pred buy (TenseNode.INF 0) Affix.nonpast)))

(52) without its relative clause: he PAST₁ <-say [λ0 PAST₀ ¬<-woll [λ0 he INF₀ ¬<-buy]], the PAST of woll licensed by <-say across the non-past future.

theorem Heim1994a.tlc_simultaneous {V : Type u_2} {D : Type u_3} {A : Type u_4} (x : A) (v : V) : TLC false (LF.believe x (TenseNode.PAST 1) Affix.past (LF.pred v (TenseNode.PAST 0) Affix.nonpast))

(56): the simultaneous LF of (28) with its affixes, John PAST₁ <-believe [λ0 Bill PAST₀ ¬<-be asleep], is licensed.

theorem Heim1994a.def'_simultaneous {T : Type u_1} [LinearOrder T] {V : Type u_2} {D : Type u_3} {A : Type u_4} {W : Type u_5} (M : Model V D A W T) (c : Context W T) (x : A) (v : V) (g : Assignment T) (w : W) (h0 : g 0 = c.time) : Def' M c (LF.believe x (TenseNode.PAST 1) Affix.past (LF.pred v (TenseNode.PAST 0) Affix.nonpast)) g w ↔ (g 1).Precedes c.time

Under the entries of Section 3, (56) presupposes only that the believing time precedes the utterance time: the presupposition of footnote 23 is gone.

theorem Heim1994a.not_tlc_present_under_past {V : Type u_2} {D : Type u_3} {A : Type u_4} (x : A) (v : V) : ¬TLC false (LF.believe x (TenseNode.PAST 1) Affix.past (LF.pred v (TenseNode.PRES 0) Affix.nonpast))

(57): a present bound from Comp under a <-affixed attitude verb violates clause (ii).

def Heim1994a.resMoved {V : Type u_2} {D : Type u_3} {A : Type u_4} (x : A) (v : V) (res : TenseNode) (a : Affix) : LF V D A

The res-moved LFs of (36) and (28) with their affixes, (62), (63), (65), (66): the res tense res and the affix a of the embedded predicate hosting its trace.

Equations

• Heim1994a.resMoved x v res a = Heim1994a.LF.believeRes x (Heim1994a.TenseNode.PAST 1) Heim1994a.Affix.past res 3 (Heim1994a.LF.pred v (Heim1994a.TenseNode.trace 3) a)

theorem Heim1994a.tlc_63 {V : Type u_2} {D : Type u_3} {A : Type u_4} (x : A) (v : V) : TLC false (resMoved x v (TenseNode.PRES 2) Affix.nonpast)

(63) is licensed: the res-moved PRES is in the domain of ¬<-be pregnant alone.

theorem Heim1994a.not_tlc_62 {V : Type u_2} {D : Type u_3} {A : Type u_4} (x : A) (v : V) : ¬TLC false (resMoved x v (TenseNode.PRES 2) Affix.past)

(62) is excluded: the res-moved PRES is in the domain of <-be pregnant.

theorem Heim1994a.tlc_65 {V : Type u_2} {D : Type u_3} {A : Type u_4} (x : A) (v : V) : TLC false (resMoved x v (TenseNode.PAST 2) Affix.past)

(65) is licensed: the back-shifted reading, the res-moved PAST hosted by <-be asleep.

theorem Heim1994a.not_tlc_66 {V : Type u_2} {D : Type u_3} {A : Type u_4} (x : A) (v : V) : ¬TLC false (resMoved x v (TenseNode.PAST 2) Affix.nonpast)

(66) is excluded: the res-moved PAST is in the domain of no <-affixed predicate.

theorem Heim1994a.def'_63 {T : Type u_1} [LinearOrder T] {V : Type u_2} {D : Type u_3} {A : Type u_4} {W : Type u_5} (M : Model V D A W T) (c : Context W T) (x : A) (v : V) (g : Assignment T) (w : W) (h0 : g 0 = c.time) : Def' M c (resMoved x v (TenseNode.PRES 2) Affix.nonpast) g w ↔ (g 1).Precedes c.time ∧ (g 2).Overlaps c.time ∧ c.concept (w, g 1) = g 2 ∧ ∀ s ∈ M.dox x w (g 1), NotAfter (c.concept s) s.time ∧ ¬(c.concept s).Precedes s.time

The presuppositions of (63): (i) from the < on the matrix verb, (ii) from (64), (iv) from (33), and at every doxastic alternative (iii) from the Upper Limit Constraint on the trace and (vi) from the ¬< on the embedded predicate, that the concept neither follows nor precedes the alternative's time.