Abusch (1997): Sequence of Tense and Temporal De Re

Abusch starts from a theory that evaluates every tense relative to the utterance time, treats tenses as anaphoric pronouns, and interprets a tense anaphoric across an attitude de re, through an acquaintance relation to the res time. The simultaneous reading of Mary believed it was raining is then de re with identity as the acquaintance relation. That theory explains neither the missing forward-shifted readings nor past morphology on a tense that precedes nothing. For the first, the now of an epistemic alternative is an upper limit for the denotation of tenses, since from an alternative the past is determinate and the future branches. For the second, every temporal argument carries a relation variable relating its time to its local evaluation time, an intensional operator transmits its relation to its complement, and a tense constrains the relations it has access to: a past requires one of them to be precedence, a present requires each to exclude it. A present under a past then has no consistent reading in place, so it scopes out de re, and the counterpart correspondence between the base world and the belief world leaves only the double access reading.

Main statements

• histories_subset_of_upperLimit, not_histories_subset_of_branching: a time the upper limit constraint admits lies on every history through the now, and a time after a branching does not.
• PastConstraint.nonLocallyLicensed_of_coindexed: a past coindexed with its local evaluation time is licensed by a transmitted relation.
• expects_no_simultaneous: under a present matrix an embedded past has no simultaneous reading.
• doubleAccess_of_counterpart: a present under a past has only the double access reading.

Implementation notes

• Relation variables are numbered by the paper's superscripts and times by its indices, 0 being the utterance time and 2 the local evaluation time of an attitude complement.
• The feature passing that transmits relations is not modelled: each tense is given the set of relation variables it has access to.
• The examples are the rows of Data.Examples.Abusch1997.

References

• [Abu97]
• [Hei94a]
• [Lew79a]
• [CvS82]
• [Par73]
• [Ogi89]

De re interpretation across attitude contexts

theorem Abusch1997.simultaneous_deRe {E : Type u_1} {W : Type u_2} {T : Type u_3} (rain : T → W → Prop) : (Acquaintance.deRe Acquaintance.identity fun (t x : T) (w : W) => rain t w) = fun (x : E) (t : T) (w : W) => rain t w

On the simultaneous reading of Mary believed it was raining (Examples.ex2) the embedded past is anaphoric to the matrix past, hence de re, with identity to the now as acquaintance relation, and the believed centered proposition is rain at the believer's now. This is also what the reading licensed by the matrix past ascribes, so the sentence has two equivalent logical forms.

The upper limit constraint

The now of an epistemic alternative is an upper limit for the denotation of tenses (Tense.upperLimitConstraint). Epistemic alternatives are moments of a branching frame, where the past of a moment is determinate and its future is not.

theorem Abusch1997.histories_subset_of_upperLimit {M : Type u_4} [PartialOrder M] [IsLeftLinear M] {now t : M} (h : (now, t) ∈ Tense.toSetRel Tense.upperLimitConstraint) : BranchingTime.histories now ⊆ BranchingTime.histories t

From an epistemic alternative the past is determinate, in that a time the upper limit constraint admits lies on every history through the now.

theorem Abusch1997.not_histories_subset_of_branching {M : Type u_4} [PartialOrder M] [IsLeftLinear M] {now t t' : M} (ht' : now ≤ t') (h : ¬t ≤ t') (h' : ¬t' ≤ t) : ¬BranchingTime.histories now ⊆ BranchingTime.histories t

The future is not determinate, in that where two later times lie on different branches, neither lies on every history through the now.

theorem Abusch1997.forwardShifted_not_upperLimit {T : Type u_3} [LinearOrder T] {thinking opening : T} (h : thinking < opening) : compare opening thinking ∉ Tense.upperLimitConstraint

On the forward-shifted reading of he thought that a burglar attacked him (Examples.ex3_ULC), an embedded past anaphoric to the later opening of the door violates the upper limit constraint at the thinking time.

Transmitted temporal relations

structure Abusch1997.TemporalArgument : Type

A temporal argument, a tense or the covert time of a noun such as desire, has a relation variable, the index of its time, and the index of its local evaluation time.

• rel : ℕ

  The relation variable.

• index : ℕ

  The index of the argument's time.

• evalIndex : ℕ

  The index of the local evaluation time.

def Abusch1997.TemporalArgument.Con {T : Type u_3} (a : TemporalArgument) (ρ : ℕ → T → T → Prop) (g : ℕ → T) : Prop

The argument's relation holds between its time and its local evaluation time.

Equations

• a.Con ρ g = ρ a.rel (g a.index) (g a.evalIndex)

def Abusch1997.TemporalArgument.LocallyLicensed {T : Type u_3} [LT T] (a : TemporalArgument) (ρ : ℕ → T → T → Prop) : Prop

A temporal argument is locally licensed when its own relation is temporal precedence.

Equations

• a.LocallyLicensed ρ = (ρ a.rel = fun (x1 x2 : T) => x1 < x2)

def Abusch1997.TemporalArgument.NonLocallyLicensed {T : Type u_3} [LT T] (a : TemporalArgument) (ρ : ℕ → T → T → Prop) (acc : Finset ℕ) : Prop

A temporal argument is non-locally licensed when a transmitted relation, not its own, is temporal precedence.

Equations

• a.NonLocallyLicensed ρ acc = ∃ r ∈ acc, r ≠ a.rel ∧ ρ r = fun (x1 x2 : T) => x1 < x2

def Abusch1997.PastConstraint {T : Type u_3} [LT T] (ρ : ℕ → T → T → Prop) (acc : Finset ℕ) : Prop

The past tense requires one of the relations it has access to to be temporal precedence.

Equations

• Abusch1997.PastConstraint ρ acc = ∃ r ∈ acc, ρ r = fun (x1 x2 : T) => x1 < x2

def Abusch1997.PresentConstraint {T : Type u_3} [LT T] (ρ : ℕ → T → T → Prop) (acc : Finset ℕ) : Prop

The present tense requires each of the relations it has access to to exclude temporal precedence.

Equations

• Abusch1997.PresentConstraint ρ acc = ∀ r ∈ acc, ∀ (t t' : T), ρ r t t' → ¬t < t'

theorem Abusch1997.pastConstraint_singleton {T : Type u_3} {ρ : ℕ → T → T → Prop} {r : ℕ} [LT T] : PastConstraint ρ {r} ↔ ρ r = fun (x1 x2 : T) => x1 < x2

theorem Abusch1997.PresentConstraint.ne_lt {T : Type u_3} {ρ : ℕ → T → T → Prop} {acc : Finset ℕ} {r : ℕ} [LT T] (hq : PresentConstraint ρ acc) (hr : r ∈ acc) {t t' : T} (h : ρ r t t') : ρ r ≠ fun (x1 x2 : T) => x1 < x2

A relation under a present constraint that holds somewhere is not temporal precedence.

theorem Abusch1997.TemporalArgument.not_locallyLicensed_of_coindexed {T : Type u_3} {ρ : ℕ → T → T → Prop} {g : ℕ → T} {a : TemporalArgument} [Preorder T] (hcon : a.Con ρ g) (h : a.index = a.evalIndex) : ¬a.LocallyLicensed ρ

A temporal argument coindexed with its local evaluation time is not locally licensed.

theorem Abusch1997.PastConstraint.nonLocallyLicensed_of_coindexed {T : Type u_3} {ρ : ℕ → T → T → Prop} {g : ℕ → T} {acc : Finset ℕ} {a : TemporalArgument} [Preorder T] (hp : PastConstraint ρ acc) (hcon : a.Con ρ g) (h : a.index = a.evalIndex) : a.NonLocallyLicensed ρ acc

A past coindexed with its local evaluation time is licensed by a transmitted relation.

Non-local and local licensing

def Abusch1997.matrix : TemporalArgument

The matrix tense of Mary believed, John promised and Sue expects, with the relation R¹(t₁, t₀).

Equations

• Abusch1997.matrix = { rel := 1, index := 1, evalIndex := 0 }

def Abusch1997.embeddedPast : TemporalArgument

The embedded past of it was raining coindexed with the complement's evaluation time, with the relation R²(t₂, t₂).

Equations

• Abusch1997.embeddedPast = { rel := 2, index := 2, evalIndex := 2 }

theorem Abusch1997.simultaneous_nonLocal {T : Type u_3} {ρ : ℕ → T → T → Prop} {g : ℕ → T} [Preorder T] (h₁ : matrix.Con ρ g) (h₂ : embeddedPast.Con ρ g) (hp₁ : PastConstraint ρ {1}) (hp₂ : PastConstraint ρ {1, 2}) : g 1 < g 0 ∧ embeddedPast.NonLocallyLicensed ρ {1, 2}

The simultaneous reading of Mary believed it was raining is licensed non-locally, since the embedded relation holds of the now and itself, so the matrix relation is the one that is precedence, and the believing precedes the utterance time.

theorem Abusch1997.narrowScope_forward (k : ℕ) (hk : k ≠ 1) : ∃ (ρ : ℕ → ℤ → ℤ → Prop) (g : ℕ → ℤ), matrix.Con ρ g ∧ { rel := k, index := 2, evalIndex := 2 }.Con ρ g ∧ PastConstraint ρ {1} ∧ PastConstraint ρ {1, k} ∧ compare (g 2) (g 2) ∈ Tense.upperLimitConstraint ∧ g 0 < g 2

On the narrow-scope reading of John promised to talk about the topic that the participants were interested in (Examples.ex53), the past of the relative clause, coindexed with the talking time, is licensed by the matrix relation, so the interest may lie after the utterance time, within the upper limit constraint.

theorem Abusch1997.wideScope_precedes {T : Type u_3} {ρ : ℕ → T → T → Prop} {g : ℕ → T} [Preorder T] {k i : ℕ} (hcon : { rel := k, index := i, evalIndex := 0 }.Con ρ g) (hp : PastConstraint ρ {k}) : g i < g 0

On the wide-scope reading the relative clause is outside the attitude, so its past has access only to its own relation, evaluated at the utterance time, and the interest precedes the utterance.

theorem Abusch1997.expects_local {T : Type u_3} {ρ : ℕ → T → T → Prop} {g : ℕ → T} [Preorder T] (h₁ : matrix.Con ρ g) (hq : PresentConstraint ρ {1}) (hp : PastConstraint ρ {1, 3}) (h₃ : { rel := 3, index := 3, evalIndex := 2 }.Con ρ g) : g 3 < g 2

A present matrix forces local licensing, so the past of a man she met recently (Examples.ex60) must itself be precedence, and the meeting precedes the marrying.

theorem Abusch1997.expects_no_simultaneous {T : Type u_3} {ρ : ℕ → T → T → Prop} {g : ℕ → T} [Preorder T] (h₁ : matrix.Con ρ g) (hq : PresentConstraint ρ {1}) (hp : PastConstraint ρ {1, 3}) (h₃ : { rel := 3, index := 2, evalIndex := 2 }.Con ρ g) : False

Sue expects to marry a man she loved (Examples.ex63) has no simultaneous reading, since coindexing the embedded past with the marrying time leaves no relation to license it.

Present under past

theorem Abusch1997.presentUnderPast_false {T : Type u_3} {ρ : ℕ → T → T → Prop} {g : ℕ → T} [Preorder T] (h₁ : matrix.Con ρ g) (hp : PastConstraint ρ {1}) (hq : PresentConstraint ρ {1, 3}) : False

John believed that Mary is pregnant (Examples.ex8_doubleAccess) has no reading with the present in place, since the matrix past makes R¹ precedence, and the embedded present, which has access to R¹, requires it to exclude precedence.

theorem Abusch1997.doubleAccess_of_counterpart {T : Type u_3} [LinearOrder T] {I J : Set T} (hI : I.OrdConnected) {believing utterance now : T} (hlt : believing < utterance) (hU : utterance ∈ I) (hulc : ∃ s ∈ J, s ≤ now) (hafter : (∀ s ∈ I, believing < s) ↔ ∀ s ∈ J, now < s) (hoverlap : believing ∈ I ↔ now ∈ J) : {believing, utterance} ⊆ I ∧ now ∈ J

On the double access reading the scoped present denotes an interval I overlapping the utterance time, and its trace denotes J in the belief world, bounded by the upper limit constraint at the believer's now. The counterpart correspondence, on which I follows the believing time iff J follows the now and I overlaps it iff J overlaps the now, leaves only the reading where I overlaps the believing time as well.