Ogihara (1989): Temporal Reference in English and Japanese

The first chapter of the dissertation weighs the quantificational analysis of tense against the referential analysis of Partee and keeps a part of each: a tense is an existential quantifier over times, and what depends on context is a restriction of the quantifier to an interval that the context makes salient. In answer to Did you see Mary?, Yes, I saw her says that the speaker saw Mary at some time within the day, which the speaker need not be able to name, so the tense is not a free variable. I didn't turn off the stove says that the salient interval is past and that the speaker turned off the stove at none of its subintervals. The referential reading is weaker, since turning off a stove takes less time than the salient interval and so does not hold at the interval as a whole, and the reading on which the speaker never turned off the stove is stronger.

Main statements

• restricted_iff_exists_past: the past restricted to a salient interval is Partee's past tense with its index bound by an existential quantifier over the subintervals of that interval.
• no_subinterval_iff_not_restricted: the stove sentence says that the salient interval is past and denies the past restricted to it.
• no_subinterval_entails_deictic, deictic_too_weak: this reading entails the referential one, which is also true when the stove was turned off within the salient interval.
• never_entails_no_subinterval, never_too_strong: it follows from the reading on which the speaker never turned off the stove and does not entail it.

Implementation notes

• A clause holds at an interval when the interval is among its times, and the subinterval relation is the order ≤ of NonemptyInterval.
• The examples are the rows of Data.Examples.Ogihara1989.

TODO

• The theory of sequence of tense of the second chapter and the fragments of English and Japanese of the third are not formalized.

References

• [Ogi89]
• [Par73]
• [Pri67]

theorem Ogihara1989.restricted_iff_exists_past {T : Type u_1} [LinearOrder T] {P : NonemptyInterval T → Prop} {K σ : NonemptyInterval T} {g : Assignment (NonemptyInterval T)} {n : ℕ} : ModalLogic.Diamond (Tense.Perspective.toSetRel (Semantics.Denotes.denote Tense.past)) (fun (t : NonemptyInterval T) => t ≤ K ∧ P t) σ ↔ ∃ t ≤ K, HeimKratzer.lambdaAbsG n (Partee1973.Past n P σ) g t

The past restricted to the salient interval K holds when the clause held at a past subinterval of K, as Yes, I saw her (Examples.ex_57) says of the day. It is Partee's past tense with its index bound by an existential quantifier over the subintervals of K.

The stove

I didn't turn off the stove (Examples.ex_46a), with P the times at which the speaker turns off the stove and the time of the tense's index the salient interval. The sentence says that this interval is past and has no subinterval at which the speaker turned off the stove.

theorem Ogihara1989.no_subinterval_iff_not_restricted {T : Type u_1} [LinearOrder T] {P : NonemptyInterval T → Prop} {σ : NonemptyInterval T} {g : Assignment (NonemptyInterval T)} {n : ℕ} : Partee1973.Past n (fun (t : NonemptyInterval T) => ¬∃ t' ≤ t, P t') σ g ↔ Tense.Perspective.Presup (Semantics.Denotes.denote Tense.past) σ (g n) ∧ ¬ModalLogic.Diamond (Tense.Perspective.toSetRel (Semantics.Denotes.denote Tense.past)) (fun (t : NonemptyInterval T) => t ≤ g n ∧ P t) σ

The stove sentence says that the salient interval is past and denies the past restricted to it.

theorem Ogihara1989.no_subinterval_entails_deictic {T : Type u_1} [LinearOrder T] {P : NonemptyInterval T → Prop} {σ : NonemptyInterval T} {g : Assignment (NonemptyInterval T)} {n : ℕ} (h : Partee1973.Past n (fun (t : NonemptyInterval T) => ¬∃ t' ≤ t, P t') σ g) : Partee1973.Past n (fun (t : NonemptyInterval T) => ¬P t) σ g

A speaker who turned off the stove at no subinterval of the salient interval did not turn it off at that interval.

theorem Ogihara1989.deictic_too_weak : ∃ (σ : NonemptyInterval ℤ) (g : Assignment (NonemptyInterval ℤ)) (P : NonemptyInterval ℤ → Prop), Partee1973.Past 0 (fun (t : NonemptyInterval ℤ) => ¬P t) σ g ∧ ¬Partee1973.Past 0 (fun (t : NonemptyInterval ℤ) => ¬∃ t' ≤ t, P t') σ g

Turning off the stove takes a moment, so a speaker who did so within the salient interval did not do so at that interval, and the referential reading is true where the sentence is false.

theorem Ogihara1989.never_entails_no_subinterval {T : Type u_1} [LinearOrder T] {P : NonemptyInterval T → Prop} {σ : NonemptyInterval T} {g : Assignment (NonemptyInterval T)} {n : ℕ} (hn : Tense.Perspective.Presup (Semantics.Denotes.denote Tense.past) σ (g n)) (h : ¬ModalLogic.Diamond (Tense.Perspective.toSetRel (Semantics.Denotes.denote Tense.past)) P σ) : Partee1973.Past n (fun (t : NonemptyInterval T) => ¬∃ t' ≤ t, P t') σ g

A speaker who never turned off the stove turned it off at no subinterval of the salient interval.

theorem Ogihara1989.never_too_strong : ∃ (σ : NonemptyInterval ℤ) (g : Assignment (NonemptyInterval ℤ)) (P : NonemptyInterval ℤ → Prop), Partee1973.Past 0 (fun (t : NonemptyInterval ℤ) => ¬∃ t' ≤ t, P t') σ g ∧ ModalLogic.Diamond (Tense.Perspective.toSetRel (Semantics.Denotes.denote Tense.past)) P σ

The sentence is true of a speaker who turned off the stove before the salient interval.