Tense as a typed lexical object

[Sha14] argues tense comes in two cross-linguistic semantic types ((30), p. 274): pronominal (after [Par73]; an element of D_i) and quantificational (a Priorean operator over time-predicates). They diverge on past-under-past in before-clauses, where quantificational past triggers Inherent Presupposition Failure under [BC03]'s before (Tense.TemporalConnectives.Before); the cross-linguistic typology ((98), (99)) is in Studies.Sharvit2014.

Main definitions

• Tense.LexicalType — pronominal vs quantificational tense.
• Tense.pronominalLookup — the pronominal-past partial lookup ((30a)).
• Tense.quantificationalPast — the quantificational past, the GQ some over K ((30b)).

inductive Tense.LexicalType : Type

[Sha14]'s two semantic types of tense ((30)).

• pronominal : LexicalType

  Pronominal: an element of D_i, two-indexed past_{j,k}.

• quantificational : LexicalType

  Quantificational: an operator over time-predicates.

@[implicit_reducible]

instance Tense.instDecidableEqLexicalType : DecidableEq LexicalType

Equations

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

@[implicit_reducible]

instance Tense.instReprLexicalType : Repr LexicalType

Equations

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

def Tense.instReprLexicalType.repr : LexicalType → ℕ → Std.Format

Equations

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

theorem Tense.LexicalType.pronominal_ne_quantificational : pronominal ≠ quantificational

The two semantic types are distinct. ([Sha14]'s language-level no-mixing constraint — a language has tenses of just one type — lives in Studies.Sharvit2014.)

def Tense.pronominalLookup {Time : Type u_1} [LT Time] [DecidableLT Time] (g : ℕ → Time) (j k : ℕ) : Option Time

[Sha14] (30a): pronominal-past lookup [[past_{j,k}]]^g. Indices j (evaluation), k (referential); defined iff g k < g j, then g k. Uses Option (not Part/PFun) as the domain is decidable; the shape is Option.guard.

Equations

• Tense.pronominalLookup g j k = if g k < g j then some (g k) else none

@[simp]

theorem Tense.pronominalLookup_eq_some_iff {Time : Type u_1} [LT Time] [DecidableLT Time] (g : ℕ → Time) (j k : ℕ) (t : Time) : pronominalLookup g j k = some t ↔ g k < g j ∧ g k = t

The pronominal past denotes the referential index when defined.

@[simp]

theorem Tense.pronominalLookup_eq_none_iff {Time : Type u_1} [LT Time] [DecidableLT Time] (g : ℕ → Time) (j k : ℕ) : pronominalLookup g j k = none ↔ ¬g k < g j

The pronominal past is undefined exactly when the constraint fails.

def Tense.TensePronoun.toNominalDenot {Time : Type u_1} [LinearOrder Time] (tp : TensePronoun) : Semantics.Reference.NominalDenot (TemporalAssignment Time) PUnit.{u_2 + 1} Time

A tense pronoun is a nominal denotation over Time ([Par73]): the referent selector is the total assignment lookup resolve, the intrinsic presupposition is the tense constraint. Entity pronouns (Semantics.Reference.PronounDenotation) are the same NominalDenot construction over Entity, so "tense is a pronoun" holds by construction.

Equations

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

@[simp]

theorem Tense.TensePronoun.toNominalDenot_presup {Time : Type u_1} [LinearOrder Time] (tp : TensePronoun) (g : TemporalAssignment Time) (w : PUnit.{u_2 + 1}) : tp.toNominalDenot.presup g w = tp.fullPresupposition g

@[simp]

theorem Tense.TensePronoun.toNominalDenot_selector {Time : Type u_1} [LinearOrder Time] (tp : TensePronoun) (g : TemporalAssignment Time) (w : PUnit.{u_2 + 1}) : tp.toNominalDenot.selector g w = some (tp.resolve g)

theorem Tense.pronominalLookup_eq_some_iff_tensePronoun {Time : Type u_1} [LinearOrder Time] (g : TemporalAssignment Time) (j k : ℕ) (t : Time) (mode : TenseInterpretation) : pronominalLookup g j k = some t ↔ { varIndex := k, constraint := past, mode := mode, evalTimeIndex := j }.toNominalDenot.presup g PUnit.unit ∧ { varIndex := k, constraint := past, mode := mode, evalTimeIndex := j }.toNominalDenot.selector g PUnit.unit = some t

The two codebase formalizations of [Par73] pronominal tense coincide: pronominalLookup is the presupposition-gated referent of the tense pronoun's NominalDenot (TensePronoun.toNominalDenot), for any binding mode.

def Tense.quantificationalPast {Time : Type u_1} [LT Time] (K : Set Time) (p : Time → Prop) (t : Time) : Prop

[Sha14] (30b): quantificational past as the generalized quantifier some (Quantification.some_sem) over the contextual restrictor K, with scope "precedes t and satisfies p". Definitionally ∃ t' ∈ K, t' < t ∧ p t'.

Equations

• Tense.quantificationalPast K p t = Quantification.some_sem (fun (x : Time) => x ∈ K) fun (t' : Time) => t' < t ∧ p t'

theorem Tense.quantificationalPast_mono {Time : Type u_1} [LT Time] {K : Set Time} {p q : Time → Prop} (h : ∀ (t : Time), p t → q t) {t : Time} : quantificationalPast K p t → quantificationalPast K q t

Monotone in the body predicate — inherited from scope-monotonicity of some (Quantification.some_scope_up), not reproved.