Lakoff (1970): Tense and Its Relation to Participants

This file formalizes the claim of [Lak70] that the choice of a tense answers to the participants and not only to the times: a past tense may report a present state the speaker no longer treats as salient, a present tense survives under a past matrix when its content is new to the hearer, the present perfect asks for a relevance the speaker grants, and a present tense stands for a future one when the event is scheduled. Perspective extends the library's Reichenbach frame with the two participant dimensions, the salience of the event to the speaker and the novelty of the content to the hearer, and each of the paper's uses is a condition on such a frame. A use of a tense is true when the relation of the event to the speech time lies in the cell of the tense chosen (IsTrueUse) and false otherwise; the paper's judgments are predicted by true use or by a licensed false use in a synthetic form (predicted_iff_acceptable), the periphrastic used to being confined to true pasts (false_use_synthetic).

Implementation notes

The participant dimensions are propositions on the frame, and the frame is Reichenbach's; the evidential refinement of the frame belongs to the later literature and is not used. The false future of the paper's (4b) and (10a), a will for a present state not yet real to the speaker, would need a second direction of salience and is not represented, nor is the ban on used to under sequence of tense, (11b).

References

• [Lak70]
• [Rei47]

The participant frame

structure Lakoff1970.Perspective (T : Type u_2) extends Tense.ReichenbachFrame T : Type u_2

Reichenbach's frame with the two participant dimensions: whether the event is salient to the speaker at speech time, and whether the content is new to the hearer.

• speechTime : T
• perspectiveTime : T
• referenceTime : T
• eventTime : T
• Salient : Prop

  The event is psychologically salient to the speaker at speech time.

• Novel : Prop

  The content is new to the hearer.

• decSalient : Decidable self.Salient
• decNovel : Decidable self.Novel

def Lakoff1970.IsTrueUse {T : Type u_1} [LinearOrder T] (cell : Finset Ordering) (f : Perspective T) : Prop

A use of a tense cell is true when the relation of the event to the speech time lies in the cell: the past, present, future, and nonpast table.

Equations

• Lakoff1970.IsTrueUse cell f = (compare f.eventTime f.speechTime ∈ cell)

@[instance_reducible]

instance Lakoff1970.instDecidableIsTrueUse {T : Type u_1} [LinearOrder T] (cell : Finset Ordering) (f : Perspective T) : Decidable (IsTrueUse cell f)

Equations

• Lakoff1970.instDecidableIsTrueUse cell f = Lakoff1970.instDecidableIsTrueUse._aux_1 cell f

def Lakoff1970.FalsePast {T : Type u_1} [DecidableEq T] (f : Perspective T) : Prop

False past (§1): a past tense on a present state the speaker no longer finds salient, as The animal you saw was a chipmunk of an animal that still is one.

Equations

• Lakoff1970.FalsePast f = (f.eventTime = f.speechTime ∧ ¬f.Salient)

@[instance_reducible]

instance Lakoff1970.instDecidableFalsePast {T : Type u_1} [DecidableEq T] (f : Perspective T) : Decidable (FalsePast f)

Equations

• Lakoff1970.instDecidableFalsePast f = { decide := decide (f.eventTime = f.speechTime) && decide ¬f.Salient, reflects_decide := ⋯ }

def Lakoff1970.NovelPresent {T : Type u_1} (f : Perspective T) : Prop

Novel present (§2): a present tense under a past matrix, licensed by content new to the hearer, as He discovered that the boy has blue eyes.

Equations

• Lakoff1970.NovelPresent f = (f.Novel ∧ f.eventTime = f.speechTime)

def Lakoff1970.RelevantPerfect {T : Type u_1} [LinearOrder T] (f : Perspective T) : Prop

Relevant perfect (§4): the present perfect, a past event at a present reference time, requires the event to be salient, as Shakespeare has written thirty-seven plays against Shakespeare has quarreled with Bacon.

Equations

• Lakoff1970.RelevantPerfect f = (f.eventPosition = Ordering.lt ∧ f.referenceTime = f.speechTime ∧ f.Salient)

def Lakoff1970.WillDeletion {T : Type u_1} [LinearOrder T] (f : Perspective T) : Prop

Will-deletion (§5): a present tense for a future event the speaker treats as scheduled and salient, as John dies tomorrow against It rains Thursday.

Equations

• Lakoff1970.WillDeletion f = (f.speechTime < f.eventTime ∧ f.Salient)

@[instance_reducible]

instance Lakoff1970.instDecidableWillDeletion {T : Type u_1} [LinearOrder T] (f : Perspective T) : Decidable (WillDeletion f)

Equations

• Lakoff1970.instDecidableWillDeletion f = { decide := decide (f.speechTime < f.eventTime) && decide f.Salient, reflects_decide := ⋯ }

theorem Lakoff1970.falsePast_not_trueUse {T : Type u_1} [LinearOrder T] {f : Perspective T} (h : FalsePast f) : ¬IsTrueUse (Semantics.Denotes.denote Tense.past) f

A false past is a false use of the past cell.

theorem Lakoff1970.willDeletion_not_trueUse {T : Type u_1} [LinearOrder T] {f : Perspective T} (h : WillDeletion f) : ¬IsTrueUse (Semantics.Denotes.denote Tense.present) f

Will-deletion is a false use of the present cell.

Forms and judgments

inductive Lakoff1970.Form : Type

The morphology of a tense form: synthetic, as walked, or periphrastic, as used to walk.

• synthetic : Form
• periphrastic : Form

@[instance_reducible]

instance Lakoff1970.instDecidableEqForm : DecidableEq Form

Equations

• Lakoff1970.instDecidableEqForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Lakoff1970.TenseForm : Type

An English tense form: the cell it realizes and its morphology.

• cell : Finset Ordering
• form : Form

def Lakoff1970.simplePast : TenseForm

The simple past.

Equations

• Lakoff1970.simplePast = { cell := Semantics.Denotes.denote Tense.past, form := Lakoff1970.Form.synthetic }

def Lakoff1970.simplePresent : TenseForm

The simple present.

Equations

• Lakoff1970.simplePresent = { cell := Semantics.Denotes.denote Tense.present, form := Lakoff1970.Form.synthetic }

def Lakoff1970.will : TenseForm

The future with will.

Equations

• Lakoff1970.will = { cell := Semantics.Denotes.denote Tense.future, form := Lakoff1970.Form.synthetic }

def Lakoff1970.usedTo : TenseForm

The periphrastic past used to.

Equations

• Lakoff1970.usedTo = { cell := Semantics.Denotes.denote Tense.past, form := Lakoff1970.Form.periphrastic }

def Lakoff1970.frame (e : ℤ) (Salient : Prop) [Decidable Salient] : Perspective ℤ

A frame at speech time zero with the event at e.

Equations

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

structure Lakoff1970.Judgment : Type

A judgment of the paper: the form used, the frame of the utterance, and the verdict.

• form : TenseForm
• frame : Perspective ℤ
• verdict : _root_.Judgment

def Lakoff1970.Judgment.Predicted (j : Judgment) : Prop

The paper licenses a form in a frame when its use is true, or when it is a synthetic form in one of the false uses the paper describes: a false past, or will-deletion.

Equations

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

@[instance_reducible]

instance Lakoff1970.instDecidablePredicted (j : Judgment) : Decidable j.Predicted

Equations

• Lakoff1970.instDecidablePredicted j = id inferInstance

def Lakoff1970.rows : List Judgment

The judgments of the paper's first and fifth sections: (4a) the animal you saw was a chipmunk, of an animal still running up a tree; (6a) the animal you saw is a chipmunk; (8a) the animal you saw used to be a chipmunk, of the same animal; (9a) the animal the sorcerer got hold of used to be a chipmunk, but now he's a badger; (27a) John will die tomorrow, said by his doctor; (27b) John dies tomorrow, said by his executioner; and (25b) it rains Thursday, because the weatherman predicted it.

Equations

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

theorem Lakoff1970.predicted_iff_acceptable (j : Judgment) : j ∈ rows → (j.Predicted ↔ j.verdict = Judgment.acceptable)

The account predicts exactly the acceptable judgments.

theorem Lakoff1970.false_use_synthetic (j : Judgment) (hj : j ∈ rows) (ha : j.verdict = Judgment.acceptable) (hf : ¬IsTrueUse j.form.cell j.frame) : j.form.form = Form.synthetic

§1: an acceptable false use is in a synthetic form; the periphrastic used to is confined to true pasts.