Perspectival tense

This file evaluates the comparison cells of Semantics/Tense/Defs.lean on time intervals, the perspectival presuppositions of Tsilia and Zhao. Tenses and temporal deictic adverbs are temporal pronouns: each denotes a time, an interval of a linear order, and presupposes that it stands to a temporal perspective π, itself an interval, in one of the positions its cell admits. An interval precedes, overlaps or follows another (NonemptyInterval.position), so PRES, which presupposes overlap with π, is the cell present; PAST, which presupposes precedence, is past; and the adverb ⌈then⌉, which presupposes disjointness, is presentᶜ. On point intervals the presupposition is the comparison of the points, which the pronominal tense of Semantics/Tense/Pronoun.lean presupposes (presup_pure).

The perspective is an interpretation parameter that an operator rebinds for a whole clause, so a clausemate tense and adverb read the same π, and the adverb restricts the tense: the reference of the tense lies within that of the adverb. Overlap passes to a containing interval, so an adverb can restrict a present tense exactly when its cell admits overlap (exists_presup_present_iff). The adverbs whose cell excludes it are the distal ones, and their clash with the present is the ⌈then⌉-present puzzle.

Main definitions

• Tense.DeicticAdverb: the lexical entry of a temporal deictic adverb, a surface form with the cell of positions its reference may occupy relative to its anchor.
• Tense.DeicticAdverb.IsDistal: the cell excludes overlap, as for English then.
• Tense.Perspective.Presup: the presupposition of a temporal pronoun with a given cell, relative to a perspective.
• Tense.Perspective.toSetRel: a cell as a relation between intervals.

Main results

• Tense.Perspective.not_presup_of_presup_present: a reference overlapping the perspective cannot be restricted by a distal adverb.
• Tense.Perspective.exists_presup_present_iff: the distal cells are exactly those that cannot restrict a present.
• Tense.Perspective.Presup.mono: a stronger cell satisfies a weaker one's presupposition, so a reference that precedes the perspective is disjoint from it.

References

• [TZ26]
• [Zha25]

structure Tense.DeicticAdverb : Type

A temporal deictic adverb is a pro-form for a time located relative to an anchor, such as English then and now, Greek tóte, and Russian togda and sejčas. The entry records the positions the adverb's reference may occupy relative to the anchor as a comparison cell; what the anchor is, the utterance time or a shiftable perspective, is a matter of analysis and is left to studies.

• form : String

  The surface form.

• cell : Finset Ordering

  The positions relative to the anchor that the adverb's reference may occupy.

@[instance_reducible]

instance Tense.instDecidableEqDeicticAdverb : DecidableEq DeicticAdverb

Equations

• Tense.instDecidableEqDeicticAdverb = Tense.instDecidableEqDeicticAdverb.decEq

def Tense.instDecidableEqDeicticAdverb.decEq (x✝ x✝¹ : DeicticAdverb) : Decidable (x✝ = x✝¹)

Equations

• Tense.instDecidableEqDeicticAdverb.decEq { form := a, cell := a_1 } { form := b, cell := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Tense.DeicticAdverb.IsDistal (a : DeicticAdverb) : Prop

A distal adverb refers to a time away from its anchor, so its cell excludes overlap.

Equations

• a.IsDistal = (Ordering.eq ∉ a.cell)

@[instance_reducible]

instance Tense.instDecidablePredDeicticAdverbIsDistal : DecidablePred DeicticAdverb.IsDistal

Equations

• Tense.instDecidablePredDeicticAdverbIsDistal a = { decide := !decide (Ordering.eq ∈ a.cell), reflects_decide := ⋯ }

def Tense.Perspective.Presup {T : Type u_1} [LinearOrder T] (C : Finset Ordering) (π ref : NonemptyInterval T) : Prop

The perspectival presupposition of a temporal pronoun with cell C is that its reference stands to the perspective π in one of the positions of C.

Equations

• Tense.Perspective.Presup C π ref = (ref.position π ∈ C)

@[instance_reducible]

instance Tense.Perspective.instDecidablePresup {T : Type u_1} [LinearOrder T] {C : Finset Ordering} {π r : NonemptyInterval T} : Decidable (Presup C π r)

Equations

• Tense.Perspective.instDecidablePresup = Tense.Perspective.instDecidablePresup._aux_1

@[simp]

theorem Tense.Perspective.presup_present {T : Type u_1} [LinearOrder T] {π r : NonemptyInterval T} : Presup (Semantics.Denotes.denote present) π r ↔ r.Overlaps π

PRES presupposes that its reference overlaps the perspective.

@[simp]

theorem Tense.Perspective.presup_past {T : Type u_1} [LinearOrder T] {π r : NonemptyInterval T} : Presup (Semantics.Denotes.denote past) π r ↔ r.Precedes π

PAST presupposes that its reference precedes the perspective.

@[simp]

theorem Tense.Perspective.presup_future {T : Type u_1} [LinearOrder T] {π r : NonemptyInterval T} : Presup (Semantics.Denotes.denote future) π r ↔ π.Precedes r

@[simp]

theorem Tense.Perspective.presup_compl_present {T : Type u_1} [LinearOrder T] {π r : NonemptyInterval T} : Presup (Semantics.Denotes.denote present)ᶜ π r ↔ ¬r.Overlaps π

⌈then⌉ presupposes that its reference is disjoint from the perspective.

@[simp]

theorem Tense.Perspective.presup_top {T : Type u_1} [LinearOrder T] {π r : NonemptyInterval T} : Presup ⊤ π r

A pronoun with the full cell, such as a deleted tense, presupposes nothing.

@[simp]

theorem Tense.Perspective.presup_pure {T : Type u_1} [LinearOrder T] {C : Finset Ordering} {p t : T} : Presup C (NonemptyInterval.pure p) (NonemptyInterval.pure t) ↔ compare t p ∈ C

On point intervals the presupposition is the comparison of the points.

theorem Tense.Perspective.Presup.mono {T : Type u_1} [LinearOrder T] {C D : Finset Ordering} {π r : NonemptyInterval T} (h : Presup C π r) (hCD : C ⊆ D) : Presup D π r

def Tense.Perspective.toSetRel {T : Type u_1} [LinearOrder T] (C : Finset Ordering) : SetRel (NonemptyInterval T) (NonemptyInterval T)

The relation of a cell on intervals relates a perspective to the intervals that stand to it in one of the cell's positions.

Equations

• Tense.Perspective.toSetRel C = {x : NonemptyInterval T × NonemptyInterval T | Tense.Perspective.Presup C x.1 x.2}

@[simp]

theorem Tense.Perspective.mem_toSetRel {T : Type u_1} [LinearOrder T] {C : Finset Ordering} {π r : NonemptyInterval T} : (π, r) ∈ toSetRel C ↔ Presup C π r

@[instance_reducible]

instance Tense.Perspective.instDecidableMemProdNonemptyIntervalSetRelToSetRelMk {T : Type u_1} [LinearOrder T] {C : Finset Ordering} {π r : NonemptyInterval T} : Decidable ((π, r) ∈ toSetRel C)

Equations

• Tense.Perspective.instDecidableMemProdNonemptyIntervalSetRelToSetRelMk = Tense.Perspective.instDecidableMemProdNonemptyIntervalSetRelToSetRelMk._aux_1

theorem Tense.Perspective.pure_mem_toSetRel {T : Type u_1} [LinearOrder T] {C : Finset Ordering} {p t : T} : (NonemptyInterval.pure p, NonemptyInterval.pure t) ∈ toSetRel C ↔ (p, t) ∈ Tense.toSetRel C

On point intervals the relation of a cell is its relation on points.

theorem Tense.Perspective.toSetRel_past_comp_self {T : Type u_1} [LinearOrder T] [DenselyOrdered T] : (toSetRel (Semantics.Denotes.denote past)).comp (toSetRel (Semantics.Denotes.denote past)) = toSetRel (Semantics.Denotes.denote past)

On dense time the past relation on intervals composed with itself is the past relation.

Restriction by an adverb

theorem Tense.Perspective.eq_mem_of_presup_present {T : Type u_1} [LinearOrder T] {C : Finset Ordering} {π r th : NonemptyInterval T} (hr : Presup (Semantics.Denotes.denote present) π r) (hle : r ≤ th) (hth : Presup C π th) : Ordering.eq ∈ C

An adverb restricts the reference of the tense it modifies, so if the tense is a present its cell must admit overlap with their common perspective.

theorem Tense.Perspective.not_presup_of_presup_present {T : Type u_1} [LinearOrder T] {C : Finset Ordering} {π r th : NonemptyInterval T} (hC : Ordering.eq ∉ C) (hr : Presup (Semantics.Denotes.denote present) π r) (hle : r ≤ th) : ¬Presup C π th

A reference overlapping the perspective cannot be restricted by an adverb whose cell excludes overlap with it, the ⌈then⌉-present clash.

theorem Tense.Perspective.exists_presup_present_iff {T : Type u_1} [LinearOrder T] {C : Finset Ordering} [Nonempty T] : (∃ (π : NonemptyInterval T) (r : NonemptyInterval T) (th : NonemptyInterval T), Presup (Semantics.Denotes.denote present) π r ∧ r ≤ th ∧ Presup C π th) ↔ Ordering.eq ∈ C

The cells that can restrict a present tense are exactly those that admit overlap.