Musan (1995): On the Temporal Interpretation of Noun Phrases

Musan's dissertation accounts pragmatically for life-time effects in its second chapter. Out of the blue, Gregory was from America suggests that Gregory is dead while Gregory was silent does not. Tenses quantify existentially over times, every predicate carries a life-time presupposition that its argument exists at the predication time (holdsAt), and an individual-level predicate holds of an individual at every time of its life if at any (IndividualLevel). The present-tense sentence is then more informative than the past-tense one, entailing it without being entailed by it (present_entails_past, past_not_entails_present), so a speaker choosing the past tense implicates that the property is over, and for an individual-level predicate that is to implicate that the individual no longer exists (lifetime_effect); a stage-level predicate supports the first implicature but not the second (no_lifetime_effect_of_stage_level).

Implementation notes

Times are the points of a linear order, the past tense is the quantificational past of Semantics/Tense/Quantificational.lean, and the present tense is evaluation at the utterance time, where the dissertation quantifies over intervals surrounding it. The neutralization of life-time effects in temporally specific contexts, the existence-independent predicates, and the third chapter's account of the predication times of noun phrases are not represented.

References

• [Mus95a]

def Musan1995.holdsAt {T : Type u_1} (alive P : T → Prop) (t : T) : Prop

holdsAt alive P is the predicate P with its life-time presupposition, holding at a time only of an individual alive at that time.

Equations

• Musan1995.holdsAt alive P t = (alive t ∧ P t)

def Musan1995.IndividualLevel {T : Type u_1} (alive P : T → Prop) : Prop

An individual-level predicate holds throughout the individual's life if it holds at all.

Equations

• Musan1995.IndividualLevel alive P = ((∃ (t : T), Musan1995.holdsAt alive P t) → ∀ (t : T), alive t → P t)

theorem Musan1995.present_entails_past {T : Type u_1} [LinearOrder T] {alive P : T → Prop} {now : T} (hP : IndividualLevel alive P) (hborn : ∃ t < now, alive t) (h : holdsAt alive P now) : ModalLogic.Diamond (Tense.toSetRel (Semantics.Denotes.denote Tense.past)) (holdsAt alive P) now

For an individual-level predicate of an individual alive before now, the present-tense sentence entails the past-tense one.

theorem Musan1995.past_not_entails_present : ∃ (alive : ℕ → Prop) (P : ℕ → Prop), IndividualLevel alive P ∧ ModalLogic.Diamond (Tense.toSetRel (Semantics.Denotes.denote Tense.past)) (holdsAt alive P) 1 ∧ ¬holdsAt alive P 1

The past-tense sentence does not entail the present-tense one, since the individual may have died.

theorem Musan1995.lifetime_effect {T : Type u_1} [LinearOrder T] {alive P : T → Prop} {now : T} (hP : IndividualLevel alive P) (h : ModalLogic.Diamond (Tense.toSetRel (Semantics.Denotes.denote Tense.past)) (holdsAt alive P) now) (hover : ¬P now) : ¬alive now

In the life-time effect, the past-tense sentence together with the implicature that the property is over yields, for an individual-level predicate, that the individual no longer exists.

theorem Musan1995.no_lifetime_effect_of_stage_level : ∃ (alive : ℕ → Prop) (P : ℕ → Prop), ModalLogic.Diamond (Tense.toSetRel (Semantics.Denotes.denote Tense.past)) (holdsAt alive P) 1 ∧ ¬P 1 ∧ alive 1

Without the individual-level property the same implicature leaves existence open, as for an individual who was silent, is silent no longer, and is still alive.