Pronominal tense

Read pronominally, after Partee, a tense refers to a time as a pronoun refers to an individual. It denotes the value of a temporal variable and presupposes that this time stands to the evaluation time, the value of a second variable, in a position of its cell, as a pronoun presupposes that its referent has its φ-features. Tense.pronoun C k j is this denotation, a nominal over times (Reference.Nominal) as the denotation of a personal pronoun is a nominal over individuals. The past and the present are the pronouns of their cells, and the zero tense of Kratzer, a variable with no presupposition, is the pronoun of the unconstrained cell ⊤. One denotation serves the deictic, the anaphoric and the bound use, binding being abstraction over the assignment (HeimKratzer.lambdaAbsG), and a free evaluation index is by convention the utterance time. Bound by an existential quantifier, a pronominal tense is the quantificational tense of its cell.

Main definitions

• Tense.pronoun: the pronominal tense of a cell, with a referential and an evaluation index.

Main statements

• Tense.exists_pronoun_iff_diamond: the existential closure of a pronominal tense is the quantificational tense of its cell at the evaluation time.

References

• [Par73]
• [Hei94a]
• [Kra98a]
• [Sha14]

def Tense.pronoun {W : Type u_1} {T : Type u_2} [LT T] (C : Finset Ordering) (k j : ℕ) : Reference.Nominal (Assignment T) W T

The pronominal tense with cell C, referential index k and evaluation index j denotes the time of k and presupposes that it stands to the time of j in a position of C.

Equations

• Tense.pronoun C k j = { presup := fun (g : Assignment T) (x : W) => (g j, g k) ∈ Tense.toSetRel C, selector := fun (g : Assignment T) (x : W) => some (HeimKratzer.interpPronoun k g) }

@[simp]

theorem Tense.pronoun_presup {W : Type u_1} {T : Type u_2} {C : Finset Ordering} {k j : ℕ} {g : Assignment T} {w : W} [LT T] : (pronoun C k j).presup g w = ((g j, g k) ∈ toSetRel C)

@[simp]

theorem Tense.pronoun_selector {W : Type u_1} {T : Type u_2} {C : Finset Ordering} {k j : ℕ} {g : Assignment T} {w : W} [LT T] : (pronoun C k j).selector g w = some (g k)

theorem Tense.exists_pronoun_iff_diamond {W : Type u_1} {T : Type u_2} {C : Finset Ordering} {k j : ℕ} {g : Assignment T} {w : W} [LT T] (hkj : k ≠ j) (P : T → Prop) : (∃ (t : T), HeimKratzer.lambdaAbsG k (fun (g : Assignment T) => (pronoun C k j).presup g w ∧ P (HeimKratzer.interpPronoun k g)) g t) ↔ ModalLogic.Diamond (toSetRel C) P (g j)

A pronominal tense with its referential index bound by an existential quantifier is the quantificational tense of its cell at the evaluation time.

@[instance_reducible]

instance Tense.instDecidablePresupAssignmentPronoun {W : Type u_1} {T : Type u_2} {C : Finset Ordering} {k j : ℕ} {g : Assignment T} {w : W} [LinearOrder T] : Decidable ((pronoun C k j).presup g w)

Equations

• Tense.instDecidablePresupAssignmentPronoun = { decide := decide (compare (g k) (g j) ∈ C), reflects_decide := ⋯ }

@[simp]

theorem Tense.pronoun_presup_const {W : Type u_1} {T : Type u_2} {C : Finset Ordering} {k j : ℕ} {w : W} [LinearOrder T] (t₀ : T) : (pronoun C k j).presup (Function.const ℕ t₀) w ↔ Ordering.eq ∈ C

With every index at one time, a pronominal tense is defined iff its cell admits coincidence.