Partee (1973): Some Structural Analogies between Tenses and Pronouns in English

Partee argues that tenses have the uses of pronouns, deictic, anaphoric and bound, and so refer to times as pronouns refer to individuals, where the tense operators of Prior quantify over them. Uttered halfway down the turnpike, I didn't turn off the stove is about a definite interval that the context makes salient, and says that the speaker did not turn off the stove then. An existential past gives the sentence two readings, by the scope of the negation, and it has neither: that the speaker never turned off the stove is too strong, and that there is a past time at which the speaker did not is too weak. In Sheila had a party last Friday and Sam got drunk the second tense picks up the time of the first, as an anaphoric pronoun picks up its antecedent, which two existential pasts do not require.

Main statements

• never_entails_deictic, deictic_entails_sometime_not: the deictic reading of the stove sentence follows from the reading on which the speaker never turned off the stove and entails the one on which the speaker at some past time did not.
• never_too_strong, sometime_not_too_weak: neither converse holds.
• anaphoric_iff, existential_pasts_not_anaphoric: two past tenses with one index locate their clauses at one time, and two existential pasts need not.
• exists_past_iff_sometime: with its index bound by an existential quantifier, the past tense is Prior's past.

Implementation notes

• A time is an interval of a linear order, mathlib's NonemptyInterval, and a tense is an index of an assignment of times, read as a pronoun by HeimKratzer.interpPronoun.
• A clause in the past tense says that the time of its index precedes the speech time and that the clause holds at that time, as a conjunction.

References

• [Par73]
• [Pri67]

def Partee1973.Past {T : Type u_1} [LinearOrder T] (n : ℕ) (P : NonemptyInterval T → Prop) (σ : NonemptyInterval T) : Assignment (NonemptyInterval T) → Prop

A clause in the past tense with index n says that the time of n precedes the speech time σ and that the clause holds at it.

Equations

• Partee1973.Past n P σ g = (Tense.Perspective.Presup (Semantics.Denotes.denote Tense.past) σ (HeimKratzer.interpPronoun n g) ∧ P (HeimKratzer.interpPronoun n g))

theorem Partee1973.past_iff {T : Type u_1} [LinearOrder T] {P : NonemptyInterval T → Prop} {σ : NonemptyInterval T} {g : Assignment (NonemptyInterval T)} {n : ℕ} : Past n P σ g ↔ (g n).Precedes σ ∧ P (g n)

theorem Partee1973.dependsOn_past {T : Type u_1} [LinearOrder T] {P : NonemptyInterval T → Prop} {σ : NonemptyInterval T} {n : ℕ} : DependsOn (Past n P σ) {n}

A past tense is free in its clause, which depends on the context only for the time of the tense's index.

theorem Partee1973.Past.sometime {T : Type u_1} [LinearOrder T] {P : NonemptyInterval T → Prop} {σ : NonemptyInterval T} {g : Assignment (NonemptyInterval T)} {n : ℕ} (h : Past n P σ g) : ModalLogic.Diamond (Tense.Perspective.toSetRel (Semantics.Denotes.denote Tense.past)) P σ

What held at the time of a past tense held at some past time.

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

With its index bound by an existential quantifier, the past tense is Prior's past.

The stove

I didn't turn off the stove, with P the times at which the speaker turns off the stove.

theorem Partee1973.never_entails_deictic {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 σ) : Past n (fun (t : NonemptyInterval T) => ¬P t) σ g

A speaker who never turned off the stove did not turn it off at the salient time.

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

A speaker who did not turn off the stove at the salient time did not turn it off at some past time.

theorem Partee1973.never_too_strong : ∃ (σ : NonemptyInterval ℤ) (g : Assignment (NonemptyInterval ℤ)) (P : NonemptyInterval ℤ → Prop), Past 0 (fun (t : NonemptyInterval ℤ) => ¬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 on an earlier occasion and not at the salient time, so the reading on which the speaker never turned it off is too strong.

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

The sentence is false of a speaker who turned off the stove at the salient time, although there are past times at which the speaker did not, so that reading is too weak.

Anaphora

Sheila had a party last Friday and Sam got drunk, with P the times of the party and Q those of Sam's getting drunk.

theorem Partee1973.anaphoric_iff {T : Type u_1} [LinearOrder T] {P Q : NonemptyInterval T → Prop} {σ : NonemptyInterval T} {g : Assignment (NonemptyInterval T)} {n : ℕ} : Past n P σ g ∧ Past n Q σ g ↔ Past n (fun (t : NonemptyInterval T) => P t ∧ Q t) σ g

Two past tenses with one index locate their clauses at one time, as an anaphoric pronoun and its antecedent pick out one individual.

theorem Partee1973.existential_pasts_not_anaphoric : ∃ (σ : NonemptyInterval ℤ) (P : NonemptyInterval ℤ → Prop) (Q : NonemptyInterval ℤ → Prop), ModalLogic.Diamond (Tense.Perspective.toSetRel (Semantics.Denotes.denote Tense.past)) P σ ∧ ModalLogic.Diamond (Tense.Perspective.toSetRel (Semantics.Denotes.denote Tense.past)) Q σ ∧ ∀ (t : NonemptyInterval ℤ), ¬(P t ∧ Q t)

Two existential pasts may be true of different times and of no common one.