Tense and Participant Perspective

@cite{cumming-2026} @cite{lakoff-1970}

Participant perspective — psychological salience and hearer novelty — is distinct from temporal perspective (Kiparsky's π / @cite{tsilia-zhao-2026}), which concerns the tense anchor point. This module handles the former; TsiliaZhao2026.lean handles the latter.

@cite{lakoff-1970} "Tense and Its Relation to Participants" argues that tense selection is sensitive to speaker/hearer epistemic states, not just temporal ordering. The chipmunk IS still there, but the speaker uses past tense because the event is no longer psychologically salient. Likewise, present tense can survive under a past-tense matrix verb when the embedded content is novel to the hearer ("He discovered that the boy has blue eyes").

This module extends EvidentialFrame with two orthogonal Boolean participant dimensions — speakerSalience and hearerNovelty — and defines Lakoff's five key predicates on this enriched structure.

Relationship to @cite{cumming-2026}

Cumming's EvidentialFrame adds acquisition time A to Reichenbach's (S, R, E), capturing the constraint that nonfuture evidence is downstream of the event. Lakoff's observations are orthogonal: "false past" arises even when evidence IS downstream (the chipmunk is still there = T ≤ A holds), because the event has lost psychological salience. TensePerspective inherits the full (S, R, E, A) frame and adds the participant-psychological layer on top.

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

Lakoff's participant-sensitive tense frame. Extends EvidentialFrame (which already extends ReichenbachFrame) with two psychological dimensions:

• speakerSalience: is the event psychologically salient to the speaker at speech time S?
• hearerNovelty: is the propositional content new to the hearer?

• 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 Semantics.Tense.ParticipantPerspective.falsePast (f : TensePerspective ℤ) : Prop

False past (Lakoff §1): past tense applied to a present-time event because the speaker no longer finds it salient.

Example: "The animal you saw WAS a chipmunk" (it still IS one). The event time equals speech time, but salience is absent.

Equations

• Semantics.Tense.ParticipantPerspective.falsePast f = (f.eventTime = f.speechTime ∧ ¬f.speakerSalience = true)

def Semantics.Tense.ParticipantPerspective.falseFuture (f : TensePerspective ℤ) : Prop

False future (Lakoff §1): future tense applied to a present-time event because the speaker treats it as not yet salient.

Example: "That thing WILL be a chipmunk" (it already IS one). Same licensing condition as false past — the divergence is in surface morphology (a Fragment-level concern).

Equations

• Semantics.Tense.ParticipantPerspective.falseFuture f = (f.eventTime = f.speechTime ∧ ¬f.speakerSalience = true)

def Semantics.Tense.ParticipantPerspective.novelInfoPresent (f : TensePerspective ℤ) : Prop

Novel-information present (Lakoff §2): present tense survives under a past-tense matrix verb because the embedded content is new to the hearer.

Example: "He discovered that the boy HAS blue eyes." The event time equals speech time and the content is novel.

Equations

• Semantics.Tense.ParticipantPerspective.novelInfoPresent f = (f.hearerNovelty = true ∧ f.eventTime = f.speechTime)

def Semantics.Tense.ParticipantPerspective.perfectRequiresSalience (f : TensePerspective ℤ) : Prop

Perfect requires salience (Lakoff §4): the present perfect is infelicitous when the event lacks current relevance to the speaker.

Example: *"Einstein has visited Princeton" — infelicitous because Einstein is dead and the event has no current relevance.

Equations

• Semantics.Tense.ParticipantPerspective.perfectRequiresSalience f = (f.speakerSalience = true)

def Semantics.Tense.ParticipantPerspective.willDeletion (f : TensePerspective ℤ) : Prop

Will-deletion (Lakoff §5): future-time events can appear in present tense (deleting will) when the speaker treats them as salient and controlled/scheduled.

Example: "The meeting starts at 3" (= will start, but scheduled). The event is future (S < T) but salient.

Equations

• Semantics.Tense.ParticipantPerspective.willDeletion f = (f.speechTime < f.eventTime ∧ f.speakerSalience = true)

inductive Semantics.Tense.ParticipantPerspective.TenseUse : Type

Lakoff's central classification: a tense use is true when the grammatical tense matches the temporal relation, false when there is a mismatch (tense encodes psychological perspective instead).

• trueTense : TenseUse
• falseTense : TenseUse

instance Semantics.Tense.ParticipantPerspective.instDecidableEqTenseUse : DecidableEq TenseUse

Equations

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

def Semantics.Tense.ParticipantPerspective.instReprTenseUse.repr : TenseUse → ℕ → Std.Format

Equations

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

instance Semantics.Tense.ParticipantPerspective.instReprTenseUse : Repr TenseUse

Equations

• Semantics.Tense.ParticipantPerspective.instReprTenseUse = { reprPrec := Semantics.Tense.ParticipantPerspective.instReprTenseUse.repr }

instance Semantics.Tense.ParticipantPerspective.instBEqTenseUse : BEq TenseUse

Equations

• Semantics.Tense.ParticipantPerspective.instBEqTenseUse = { beq := Semantics.Tense.ParticipantPerspective.instBEqTenseUse.beq }

def Semantics.Tense.ParticipantPerspective.instBEqTenseUse.beq : TenseUse → TenseUse → Bool

Equations

• Semantics.Tense.ParticipantPerspective.instBEqTenseUse.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Tense.ParticipantPerspective.classifyUse (gramTense : GramTense) (f : TensePerspective ℤ) : TenseUse

Classify a tense use based on whether the grammatical tense matches the temporal reality. A GramTense.past with eventTime = speechTime is false (the event is present-time despite past morphology).

Equations

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

def Semantics.Tense.ParticipantPerspective.falseTenseRequiresSynthetic (use : TenseUse) (form : Core.Morphology.Tense.TenseFormType) : Bool

Periphrastic forms block false tense (Lakoff §1, ex. 8a vs 9a): if the tense use is false and the form is periphrastic, the result is unacceptable. Only synthetic forms can carry false-tense interpretations.

This is stated as: false tense requires synthetic form.

Equations

• Semantics.Tense.ParticipantPerspective.falseTenseRequiresSynthetic Semantics.Tense.ParticipantPerspective.TenseUse.trueTense form = true
• Semantics.Tense.ParticipantPerspective.falseTenseRequiresSynthetic Semantics.Tense.ParticipantPerspective.TenseUse.falseTense form = (form == Core.Morphology.Tense.TenseFormType.synthetic)

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

When falsePast holds, the UP present-tense constraint (T = S) is satisfied. The event IS at speech time, despite the past surface tense — the mismatch is purely psychological (salience), not temporal.

theorem Semantics.Tense.ParticipantPerspective.salience_with_downstream (f : TensePerspective ℤ) (h_sal : f.speakerSalience = true) (h_down : Evidential.downstreamEvidence f.toEvidentialFrame) : f.speakerSalience = true ∧ Evidential.downstreamEvidence f.toEvidentialFrame

Speaker salience strictly exceeds bare downstream evidence: when both hold, we have the conjunction. This captures Lakoff's insight that salience is an additional dimension beyond Cumming's evidential constraint.