Embedded tense: frames under attitude verbs

[Abu97] [Hei94a] [Ogi89]

The frame of a clause embedded under an attitude verb: embeddedFrame re-anchors the embedded perspective time to the matrix event time (P′ = E_matrix), so embedded tense locates R′ against the attitude holder's now rather than speech time. simultaneousFrame pins R′ to the matrix event time (the SOT-deletion reading); the shifted reading is embeddedFrame with R′ < E_matrix as a hypothesis at use sites. EmbeddedTenseReading and availableReadings parameterize the shifted/simultaneous split by a language's SOTParameter, and upperLimitConstraint is [Abu97]'s ULC in [Hei94a]'s presuppositional construal.

Embedded frames

def Tense.embeddedFrame {Time : Type u_1} (matrixFrame : _root_.Time.ReichenbachFrame Time) (embeddedR embeddedE : Time) : _root_.Time.ReichenbachFrame Time

The Reichenbach frame of a clause embedded under an attitude verb: embedded perspective time P′ = matrix event time E, so the embedded tense locates its R′ relative to the attitude holder's now, not speech time. embeddedR and embeddedE are the embedded clause's reference and event times, determined by its tense and aspect.

Equations

• Tense.embeddedFrame matrixFrame embeddedR embeddedE = { speechTime := matrixFrame.speechTime, perspectiveTime := matrixFrame.eventTime, referenceTime := embeddedR, eventTime := embeddedE }

def Tense.simultaneousFrame {Time : Type u_1} (matrixFrame : _root_.Time.ReichenbachFrame Time) (embeddedE : Time) : _root_.Time.ReichenbachFrame Time

The simultaneous reading's frame: embedded R′ = matrix E ("John said Mary was sick" — sick at the saying time), so embedded tense is PRESENT relative to the embedded perspective (simultaneousFrame_isPresent).

Equations

• Tense.simultaneousFrame matrixFrame embeddedE = Tense.embeddedFrame matrixFrame matrixFrame.eventTime embeddedE

theorem Tense.simultaneousFrame_isPresent {Time : Type u_1} (matrixFrame : _root_.Time.ReichenbachFrame Time) (embeddedE : Time) : (simultaneousFrame matrixFrame embeddedE).isPresent

The simultaneous frame satisfies PRESENT (R = P) relative to the embedded perspective.

Embedded tense readings

inductive Tense.SOTParameter : Type

Sequence-of-tense parameter: whether embedded tense is interpreted relative to the matrix (SOT languages, English) or absolutely, against utterance time (non-SOT languages, Japanese).

• relative : SOTParameter

  Embedded tense relative to matrix (English).

• absolute : SOTParameter

  Embedded tense absolute, against utterance time (Japanese).

@[instance_reducible]

instance Tense.instDecidableEqSOTParameter : DecidableEq SOTParameter

Equations

• Tense.instDecidableEqSOTParameter x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Tense.instReprSOTParameter : Repr SOTParameter

Equations

• Tense.instReprSOTParameter = { reprPrec := Tense.instReprSOTParameter.repr }

def Tense.instReprSOTParameter.repr : SOTParameter → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

inductive Tense.EmbeddedTenseReading : Type

The two readings of past under a past attitude verb: shifted (embedded event before the matrix event, R′ < P′) or simultaneous (embedded event at the matrix event time, R′ = P′, via SOT deletion — [Ogi89] §11.2 (83)).

• shifted : EmbeddedTenseReading

  Embedded event before the matrix event (back-shifted).

• simultaneous : EmbeddedTenseReading

  Embedded event at the matrix event time (SOT deletion).

@[instance_reducible]

instance Tense.instDecidableEqEmbeddedTenseReading : DecidableEq EmbeddedTenseReading

Equations

• Tense.instDecidableEqEmbeddedTenseReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Tense.instReprEmbeddedTenseReading.repr : EmbeddedTenseReading → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Tense.instReprEmbeddedTenseReading : Repr EmbeddedTenseReading

Equations

• Tense.instReprEmbeddedTenseReading = { reprPrec := Tense.instReprEmbeddedTenseReading.repr }

@[instance_reducible]

instance Tense.instInhabitedEmbeddedTenseReading : Inhabited EmbeddedTenseReading

Equations

• Tense.instInhabitedEmbeddedTenseReading = { default := Tense.instInhabitedEmbeddedTenseReading.default }

def Tense.availableReadings : SOTParameter → List EmbeddedTenseReading

The readings a language's SOTParameter licenses for past-under-past: SOT (relative, English) languages have both; non-SOT (absolute, Japanese) languages only the shifted reading.

Equations

• Tense.availableReadings Tense.SOTParameter.relative = [Tense.EmbeddedTenseReading.shifted, Tense.EmbeddedTenseReading.simultaneous]
• Tense.availableReadings Tense.SOTParameter.absolute = [Tense.EmbeddedTenseReading.shifted]

Upper Limit Constraint

[Abu97] §7 (p. 25): "the now of an epistemic alternative is an upper limit for the denotation of tenses" — at the now of an intensional context, future branches diverge across epistemic alternatives, so forward reference past the now is unsupported. The presuppositional construal (ULC as a definedness constraint, projecting via Karttunen-Heim) is due to [Hei94a]; [Abu97] fn 20 endorses it. The value-level reduction embeddedR ≤ matrixE strips the modal-alternative quantification of Abusch's formulation (the "now of an epistemic alternative" quantifies over doxastic alternatives); a modal-layer formulation would be more faithful.

@[reducible, inline]

abbrev Tense.upperLimitConstraint {Time : Type u_1} [LE Time] (embeddedR matrixE : Time) : Prop

The Upper Limit Constraint ([Abu97] §7, presuppositional construal per [Hei94a]): the embedded reference time may not exceed the matrix event time (= the embedded perspective).

Equations

• Tense.upperLimitConstraint embeddedR matrixE = (embeddedR ≤ matrixE)

theorem Tense.shifted_satisfies_ulc {Time : Type u_1} [Preorder Time] (embeddedR matrixE : Time) (h : embeddedR < matrixE) : upperLimitConstraint embeddedR matrixE

The shifted reading satisfies the ULC.

theorem Tense.simultaneous_satisfies_ulc {Time : Type u_1} [Preorder Time] (embeddedR matrixE : Time) (h : embeddedR = matrixE) : upperLimitConstraint embeddedR matrixE

The simultaneous reading satisfies the ULC.

Pronoun resolution into frames

def Tense.TensePronoun.toFrame {Time : Type u_1} (tp : TensePronoun) (g : TemporalAssignment Time) (speechTime perspectiveTime eventTime : Time) : _root_.Time.ReichenbachFrame Time

Assemble the Reichenbach frame a resolved tense pronoun determines: R = the pronoun's referent under g, with perspective, speech, and event times supplied by the embedding context.

Equations

• tp.toFrame g speechTime perspectiveTime eventTime = { speechTime := speechTime, perspectiveTime := perspectiveTime, referenceTime := tp.resolve g, eventTime := eventTime }

theorem Tense.TensePronoun.bound_present_simultaneous {Time : Type u_1} (tp : TensePronoun) (g : TemporalAssignment Time) (speechTime perspTime eventTime : Time) (hBind : tp.resolve g = perspTime) (_hPres : tp.constraint = present) : (tp.toFrame g speechTime perspTime eventTime).isPresent

A present-constraint bound tense under binding gives R = P — the simultaneous reading as pronoun resolution: binding the variable to the perspective time yields a PRESENT frame.

def Tense.doubleAccess {Time : Type u_1} (p : Time → Prop) (speechTime matrixEventTime : Time) : Prop

Double-access: present-under-past requires the complement to hold at BOTH speech time (indexical rigidity) AND matrix event time (attitude accessibility).

Equations

• Tense.doubleAccess p speechTime matrixEventTime = (p speechTime ∧ p matrixEventTime)