[Lak70]: Tense and Its Relation to Participants

[Lak70]

[Lak70] argues that tense selection is sensitive to speaker/hearer epistemic states, not just temporal ordering: past tense can apply to a present-time event that has lost psychological salience ("The animal you saw WAS a chipmunk" — it still is one), and embedded present survives a past matrix when the content is novel to the hearer. The TensePerspective frame extends the evidential-tense substrate's EvidentialFrame (Semantics/Tense/Evidential.lean) with these two participant dimensions; the paper's acceptability judgments are collected as TenseJudgment data, and the paper's synthetic vs periphrastic form contrast (TenseFormType) with its English exemplar entries lives here as study-local apparatus.

Key Minimal Pairs

• §1 False tense: synthetic forms (WAS, IS) can express non-temporal tense; periphrastic forms (USED TO) cannot.
• §2 SOT/novelty: present tense survives under past matrix when content is novel to hearer ("discovered that the boy HAS blue eyes").
• §4 Perfect/salience: present perfect requires current relevance (*"Shakespeare has quarreled with Bacon" vs "Shakespeare has written...").
• §5 Will-deletion: scheduled events allow present-for-future ("The meeting starts at 3"), but unscheduled events do not (*"It rains Thursday").

inductive Lakoff1970.TenseFormType : Type

Morphological form type of a tense: synthetic (inflectional: walked) vs periphrastic (auxiliary-based: used to walk). Lakoff §1's licensing contrast: only synthetic forms permit false tense.

• synthetic : TenseFormType
• periphrastic : TenseFormType

@[instance_reducible]

instance Lakoff1970.instDecidableEqTenseFormType : DecidableEq TenseFormType

Equations

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

def Lakoff1970.instReprTenseFormType.repr : TenseFormType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Lakoff1970.instReprTenseFormType : Repr TenseFormType

Equations

• Lakoff1970.instReprTenseFormType = { reprPrec := Lakoff1970.instReprTenseFormType.repr }

def Lakoff1970.instBEqTenseFormType.beq : TenseFormType → TenseFormType → Bool

Equations

• Lakoff1970.instBEqTenseFormType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance Lakoff1970.instBEqTenseFormType : BEq TenseFormType

Equations

• Lakoff1970.instBEqTenseFormType = { beq := Lakoff1970.instBEqTenseFormType.beq }

inductive Lakoff1970.Acceptability : Type

Acceptability judgment for a tense example.

• grammatical : Acceptability
• ungrammatical : Acceptability
• marginal : Acceptability

@[instance_reducible]

instance Lakoff1970.instDecidableEqAcceptability : DecidableEq Acceptability

Equations

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

@[instance_reducible]

instance Lakoff1970.instReprAcceptability : Repr Acceptability

Equations

• Lakoff1970.instReprAcceptability = { reprPrec := Lakoff1970.instReprAcceptability.repr }

def Lakoff1970.instReprAcceptability.repr : Acceptability → ℕ → Std.Format

Equations

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

inductive Lakoff1970.TenseUseType : Type

Whether the tense use is "true" (temporal) or "false" (psychological).

• trueTense : TenseUseType
• falseTense : TenseUseType

@[instance_reducible]

instance Lakoff1970.instDecidableEqTenseUseType : DecidableEq TenseUseType

Equations

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

@[instance_reducible]

instance Lakoff1970.instReprTenseUseType : Repr TenseUseType

Equations

• Lakoff1970.instReprTenseUseType = { reprPrec := Lakoff1970.instReprTenseUseType.repr }

def Lakoff1970.instReprTenseUseType.repr : TenseUseType → ℕ → Std.Format

Equations

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

structure Lakoff1970.TenseJudgment : Type

A grammaticality judgment from [Lak70].

• exNumber : String

  Example number in the paper (e.g., "4a", "8a")

• sentence : String

  The sentence (abbreviated)

• tenseUse : TenseUseType

  True or false tense use

• formType : TenseFormType

  Synthetic or periphrastic form

• acceptability : Acceptability

  The paper's acceptability judgment

@[instance_reducible]

instance Lakoff1970.instReprTenseJudgment : Repr TenseJudgment

Equations

• Lakoff1970.instReprTenseJudgment = { reprPrec := Lakoff1970.instReprTenseJudgment.repr }

def Lakoff1970.instReprTenseJudgment.repr : TenseJudgment → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Lakoff1970.instBEqTenseJudgment : BEq TenseJudgment

Equations

• Lakoff1970.instBEqTenseJudgment = { beq := Lakoff1970.instBEqTenseJudgment.beq }

def Lakoff1970.instBEqTenseJudgment.beq : TenseJudgment → TenseJudgment → Bool

Equations

• One or more equations did not get rendered due to their size.
• Lakoff1970.instBEqTenseJudgment.beq x✝¹ x✝ = false

def Lakoff1970.ex4a : TenseJudgment

(4a) "The animal you saw WAS a chipmunk" — false past, synthetic, OK.

Equations

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

def Lakoff1970.ex6a : TenseJudgment

(6a) "The animal you saw IS a chipmunk" — true present, synthetic, OK.

Equations

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

def Lakoff1970.ex8a : TenseJudgment

(8a) *"The animal you saw USED TO BE a chipmunk" — false past, periphrastic, ungrammatical. The periphrastic form forces true-past reading, which conflicts with the present-time event.

Equations

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

def Lakoff1970.ex9a : TenseJudgment

(9a) "The animal you saw USED TO BE a chipmunk" — true past, periphrastic, grammatical. It genuinely WAS a chipmunk before.

Equations

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

def Lakoff1970.ex13a : TenseJudgment

(13a) "He discovered that the boy HAD blue eyes" — SOT past-under-past, OK.

Equations

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

def Lakoff1970.ex13b : TenseJudgment

(13b) "He discovered that the boy HAS blue eyes" — novel-info present survives under past matrix, grammatical when content is new to hearer.

Equations

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

def Lakoff1970.ex22a : TenseJudgment

(22a) "Shakespeare has written 37 plays" — salient (enduring relevance), OK.

Equations

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

def Lakoff1970.ex22b : TenseJudgment

(22b) *"Shakespeare has quarreled with Bacon" — not salient (no current relevance), ungrammatical with present perfect.

Equations

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

def Lakoff1970.ex27a : TenseJudgment

(27a) "John will die" — overt future, grammatical (control).

Equations

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

def Lakoff1970.ex27b : TenseJudgment

(27b) "John dies tomorrow" — will-deletion with scheduled/salient event, OK.

Equations

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

def Lakoff1970.ex25b : TenseJudgment

(25b) *"It rains Thursday" — will-deletion without salience/schedule, ungrammatical. Weather events are not scheduled.

Equations

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

def Lakoff1970.allJudgments : List TenseJudgment

All judgments from the paper.

Equations

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

def Lakoff1970.falseTenseJudgments : List TenseJudgment

False-tense judgments only.

Equations

• Lakoff1970.falseTenseJudgments = List.filter (fun (x : Lakoff1970.TenseJudgment) => x.tenseUse == Lakoff1970.TenseUseType.falseTense) Lakoff1970.allJudgments

def Lakoff1970.periphrasticJudgments : List TenseJudgment

Periphrastic judgments only.

Equations

• Lakoff1970.periphrasticJudgments = List.filter (fun (x : Lakoff1970.TenseJudgment) => x.formType == Lakoff1970.TenseFormType.periphrastic) Lakoff1970.allJudgments

theorem Lakoff1970.total_count : allJudgments.length = 11

There are 11 total judgments.

theorem Lakoff1970.false_tense_count : falseTenseJudgments.length = 4

There are 4 false-tense judgments.

theorem Lakoff1970.periphrastic_count : periphrasticJudgments.length = 2

There are 2 periphrastic judgments.

theorem Lakoff1970.false_periphrastic_ungrammatical : (List.filter (fun (x : TenseJudgment) => x.formType == TenseFormType.periphrastic) falseTenseJudgments).length = 1

The only ungrammatical false-tense-with-periphrastic example is ex8a.

structure Lakoff1970.TensePerspective (Time : Type u_1) extends Tense.Evidential.EvidentialFrame Time : Type u_1

Lakoff's participant-sensitive tense frame. Extends the substrate's EvidentialFrame (which extends ReichenbachFrame with acquisition time A) with two psychological dimensions. Lakoff's observations are orthogonal to the evidential constraint: "false past" arises even when evidence is downstream (the chipmunk is still there, so T ≤ A holds) because the event has lost psychological salience.

• speechTime : Time
• perspectiveTime : Time
• referenceTime : Time
• eventTime : Time
• acquisitionTime : Time
• speakerSalience : Bool

  Is the event psychologically salient to the speaker at S?

• hearerNovelty : Bool

  Is the propositional content new to the hearer?

def Lakoff1970.falsePast {Time : Type u_1} (f : TensePerspective Time) : Prop

False tense (Lakoff §1): past (or future) morphology applied to a present-time event because the speaker does not find it salient.

Past example: "The animal you saw WAS a chipmunk" (it still IS one). Future example: "That thing WILL be a chipmunk" (it already IS one). The licensing condition is the same for both; the surface-form divergence is recorded in the perspective entries (formType).

Equations

• Lakoff1970.falsePast f = (f.eventTime = f.speechTime ∧ ¬f.speakerSalience = true)

def Lakoff1970.novelInfoPresent {Time : Type u_1} (f : TensePerspective Time) : Prop

Novel-information present (Lakoff §2): present tense survives under a past-tense matrix verb because the embedded content is new to the hearer ("He discovered that the boy HAS blue eyes").

Equations

• Lakoff1970.novelInfoPresent f = (f.hearerNovelty = true ∧ f.eventTime = f.speechTime)

def Lakoff1970.perfectRequiresSalience {Time : Type u_1} (f : TensePerspective Time) : Prop

Perfect requires salience (Lakoff §4): the present perfect is infelicitous when the event lacks current relevance to the speaker (*"Shakespeare has quarreled with Bacon").

Equations

• Lakoff1970.perfectRequiresSalience f = (f.speakerSalience = true)

def Lakoff1970.willDeletion {Time : Type u_1} [LT Time] (f : TensePerspective Time) : Prop

Will-deletion (Lakoff §5): future-time events can appear in present tense (deleting will) when the speaker treats them as salient and scheduled ("The meeting starts at 3").

Equations

• Lakoff1970.willDeletion f = (f.speechTime < f.eventTime ∧ f.speakerSalience = true)

def Lakoff1970.classifyUse {Time : Type u_1} [LinearOrder Time] (gramTense : Finset Ordering) (f : TensePerspective Time) : TenseUseType

Classify a tense use as true (grammatical tense matches the temporal relation) or false (tense encodes psychological perspective instead), reusing the TenseUseType classification of the judgment data.

Derived, not stipulated: the use is true exactly when the event-vs-speech comparison falls in the tense's Finset Ordering cell (Core.Order.holds gramTense f.eventTime f.speechTime), reproducing the four-way past/present/future/nonpast table (before: E < S; overlapping: E = S; after: S < E; notBefore: S ≤ E).

Equations

• Lakoff1970.classifyUse gramTense f = if Core.Order.holds gramTense f.eventTime f.speechTime then Lakoff1970.TenseUseType.trueTense else Lakoff1970.TenseUseType.falseTense

def Lakoff1970.FalseTenseLicensed (use : TenseUseType) (form : TenseFormType) : Prop

Periphrastic forms block false tense (Lakoff §1, ex. 8a vs 9a): a false tense use demands a synthetic form; true tense is compatible with any form.

Equations

• Lakoff1970.FalseTenseLicensed use form = (use = Lakoff1970.TenseUseType.falseTense → form = Lakoff1970.TenseFormType.synthetic)

structure Lakoff1970.TensePerspectiveEntryextends Tense.Evidential.TAMEEntry : Type

A tense paradigm entry enriched with Lakoff's perspective dimensions: grammatical tense and morphological form type (synthetic vs periphrastic). Study-local: the classification is this paper's analytical frame over the Fragment's TAMEEntry data.

• label : String
• ep : EPCondition
• up : UPCondition
• mood : Option Mood.Grammatical
• mirative : Option Features.Mirativity.MirativityValue
• gramTense : Finset Ordering

  The grammatical tense this form realizes

• formType : TenseFormType

  Synthetic (inflectional) or periphrastic (auxiliary-based)

def Lakoff1970.TensePerspectiveEntry.allowsFalseTense (e : TensePerspectiveEntry) : Bool

Does this form allow false-tense interpretations? Derived from formType: only synthetic forms can.

Equations

• e.allowsFalseTense = (e.formType == Lakoff1970.TenseFormType.synthetic)

def Lakoff1970.simplePastPerspective : TensePerspectiveEntry

English simple past with perspective: synthetic, allows false past.

Equations

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

def Lakoff1970.simplePresentPerspective : TensePerspectiveEntry

English simple present with perspective: synthetic, allows false uses.

Equations

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

def Lakoff1970.usedTo : TensePerspectiveEntry

English periphrastic past "used to V": cannot express false past.

Equations

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

def Lakoff1970.goingTo : TensePerspectiveEntry

English periphrastic future "going to V": cannot express false future.

Equations

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

theorem Lakoff1970.simplePast_allows_false : simplePastPerspective.allowsFalseTense = true

Synthetic entries allow false tense.

theorem Lakoff1970.simplePresent_allows_false : simplePresentPerspective.allowsFalseTense = true

theorem Lakoff1970.usedTo_blocks_false : usedTo.allowsFalseTense = false

Periphrastic entries block false tense.

theorem Lakoff1970.goingTo_blocks_false : goingTo.allowsFalseTense = false

theorem Lakoff1970.ex4a_formType : ex4a.formType = simplePastPerspective.formType

theorem Lakoff1970.ex8a_formType : ex8a.formType = usedTo.formType

theorem Lakoff1970.ex9a_formType : ex9a.formType = usedTo.formType

theorem Lakoff1970.synthetic_allows_false_tense : FalseTenseLicensed TenseUseType.falseTense TenseFormType.synthetic

theorem Lakoff1970.periphrastic_blocks_false_tense : ¬FalseTenseLicensed TenseUseType.falseTense TenseFormType.periphrastic

theorem Lakoff1970.true_tense_any_form : FalseTenseLicensed TenseUseType.trueTense TenseFormType.periphrastic

theorem Lakoff1970.usedTo_entry_blocks_false : usedTo.allowsFalseTense = false

theorem Lakoff1970.simplePast_entry_allows_false : simplePastPerspective.allowsFalseTense = true

theorem Lakoff1970.false_past_is_temporally_present {Time : Type u_1} (f : TensePerspective Time) (h : falsePast f) : f.eventTime = f.speechTime

A false past is temporally present — the mismatch is purely psychological (salience), not temporal.

theorem Lakoff1970.false_past_satisfies_up_present (f : TensePerspective ℤ) (h : falsePast f) : Tense.Evidential.UPCondition.present.toConstraint f.toEvidentialFrame

When falsePast holds, the evidential substrate's present-tense UP constraint (T = S, UPCondition.present) is satisfied.

theorem Lakoff1970.false_past_classified_correctly {Time : Type u_1} [LinearOrder Time] (f : TensePerspective Time) (h : falsePast f) : classifyUse Tense.past f = TenseUseType.falseTense

theorem Lakoff1970.will_deletion_requires_future_and_salience (f : TensePerspective ℤ) (h : willDeletion f) : f.speechTime < f.eventTime ∧ f.speakerSalience = true

theorem Lakoff1970.grammatical_false_tense_all_synthetic : ((List.filter (fun (j : TenseJudgment) => j.acceptability == Acceptability.grammatical) falseTenseJudgments).all fun (j : TenseJudgment) => j.formType == TenseFormType.synthetic) = true

theorem Lakoff1970.false_periphrastic_is_ungrammatical : (ex8a.tenseUse == TenseUseType.falseTense && ex8a.formType == TenseFormType.periphrastic && ex8a.acceptability == Acceptability.ungrammatical) = true