Embedded tense: the Upper Limit Constraint and past under past #

A tense embedded under an attitude verb is evaluated from the attitude holder's now. Abusch makes that local evaluation time an upper limit for the denotation of tenses, and accepts Heim's construal of the constraint as a presupposition of every tense node. As a constraint on how the reference time of a tense stands to its local evaluation time, the Upper Limit Constraint is the cell of the past and the present positions (upperLimitConstraint).

A past under a past attitude places its reference time before the attitude's now. In a language with the Sequence of Tense rule the embedded past may instead be deleted and read as a zero tense bound to the now, so it coincides with it. The positions an embedded past may take are therefore the past cell, joined with the present cell where the rule applies (pastUnderPast). Every such position obeys the Upper Limit Constraint, and the positions exhaust it exactly where the rule applies.

Main definitions #

Tense.upperLimitConstraint: the Upper Limit Constraint, the cell of the past and the present.
Tense.pastUnderPast: the positions of an embedded past against the attitude's now.

Main results #

Tense.pastUnderPast_le_upperLimitConstraint, Tense.pastUnderPast_eq_upperLimitConstraint_iff: every reading of a past under a past obeys the constraint, and the readings exhaust it exactly where the Sequence of Tense rule applies.
Tense.eq_mem_pastUnderPast_iff: the simultaneous reading is available exactly where the rule applies.

Implementation notes #

Abusch motivates the constraint by the branching of the future across epistemic alternatives, which Studies/Abusch1997.lean states on branching frames; the derivation of the cell from a doxastic modal base is Klecha's (Studies/Klecha2016.lean).

References #

source

def Tense.upperLimitConstraint :

Finset Ordering

The Upper Limit Constraint is the cell of the positions a tense's reference time may take against its local evaluation time, before it or at it and never after it.

Equations

Tense.upperLimitConstraint = (Semantics.Denotes.denote Tense.future)ᶜ

Instances For

source

theorem Tense.upperLimitConstraint_eq_past_sup_present :

upperLimitConstraint = Semantics.Denotes.denote past ⊔ Semantics.Denotes.denote present

The Upper Limit Constraint admits the past and the present positions.

source

theorem Tense.mem_upperLimitConstraint {o : Ordering} :

o ∈ upperLimitConstraint ↔ o ≠ Ordering.gt

source

@[simp]

theorem Tense.compare_mem_upperLimitConstraint {T : Type u_1} [LinearOrder T] (r p : T) :

compare r p ∈ upperLimitConstraint ↔ r ≤ p

source

@[simp]

theorem Tense.mem_toSetRel_upperLimitConstraint {T : Type u_1} [PartialOrder T] {p r : T} :

(p, r) ∈ toSetRel upperLimitConstraint ↔ r ≤ p

On any partial order of times, branching ones among them, the upper limit constraint relates a time to the times at or before it.

source

def Tense.pastUnderPast (sot : Prop) [Decidable sot] :

Finset Ordering

pastUnderPast sot is the cell of the positions an embedded past's reference time may take against the attitude's now, where sot says whether the Sequence of Tense rule can delete it. A genuine past precedes the now, and a deleted past is a zero tense bound to it.

Equations