Tense licensing by transmitted temporal relations

This file defines the semantics of tense in intensional contexts on which sequence of tense rests. Every temporal argument carries a relation variable relating its time to its local evaluation time; an intensional operator transmits its temporal argument's relation to its complement, so an embedded tense has access to a set of relations; and a tense constrains that whole set — past tense requires some accessible relation to be temporal precedence, present tense requires every accessible relation to exclude it. A past tense is locally licensed when its own relation is precedence and non-locally licensed when a transmitted one is; the upper limit constraint bounds every temporal argument by its local evaluation time.

Main definitions

• Tense.TemporalArgument: a temporal argument with its relation variable, time index, and local evaluation index; TemporalArgument.Con is its relational constraint and TemporalArgument.UpperLimit the upper limit constraint on it.
• Tense.PastConstraint, Tense.PresentConstraint: the tense constraints on an accessible set of relation variables.
• Tense.TemporalArgument.LocallyLicensed, Tense.TemporalArgument.NonLocallyLicensed.

Main statements

• Tense.TemporalArgument.not_locallyLicensed_of_coindexed, Tense.PastConstraint.nonLocallyLicensed_of_coindexed: a past tense coindexed with its evaluation time is licensed only non-locally.
• Tense.PresentConstraint.ne_lt: a present-constrained relation that holds somewhere is not precedence, so a past tense transmitted only such relations is licensed locally.
• Tense.PastConstraint.false_of_presentConstraint: no relation both licenses a past tense and satisfies a present constraint at an instantiated argument.

References

• [abusch-1997]

structure Tense.TemporalArgument (ι : Type u_3) : Type u_3

A temporal argument: its relation variable, the index of its time, and the index of its local evaluation time.

• rel : ι

  The relation variable.

• index : ℕ

  The index of the argument's time.

• evalIndex : ℕ

  The index of the local evaluation time.

@[reducible, inline]

abbrev Tense.RelationAssignment (ι : Type u_3) (T : Type u_4) : Type (max u_3 u_4)

An assignment of temporal relations to relation variables.

Equations

• Tense.RelationAssignment ι T = (ι → T → T → Prop)

def Tense.TemporalArgument.Con {ι : Type u_1} {T : Type u_2} (a : TemporalArgument ι) (ρ : RelationAssignment ι T) (g : ℕ → T) : Prop

The constraint con: the argument's relation holds between its time and its local evaluation time.

Equations

• a.Con ρ g = ρ a.rel (g a.index) (g a.evalIndex)

def Tense.TemporalArgument.UpperLimit {ι : Type u_1} {T : Type u_2} (a : TemporalArgument ι) (g : ℕ → T) [LE T] : Prop

The upper limit constraint: the argument's time does not follow its local evaluation time.

Equations

• a.UpperLimit g = Tense.upperLimitConstraint (g a.index) (g a.evalIndex)

def Tense.TemporalArgument.LocallyLicensed {ι : Type u_1} {T : Type u_2} (a : TemporalArgument ι) (ρ : RelationAssignment ι T) [LT T] : Prop

Locally licensed: the argument's own relation is temporal precedence.

Equations

• a.LocallyLicensed ρ = (ρ a.rel = fun (x1 x2 : T) => x1 < x2)

def Tense.TemporalArgument.NonLocallyLicensed {ι : Type u_1} {T : Type u_2} (a : TemporalArgument ι) (ρ : RelationAssignment ι T) [LT T] (acc : Finset ι) : Prop

Non-locally licensed: a transmitted relation other than the argument's own is precedence.

Equations

• a.NonLocallyLicensed ρ acc = ∃ r ∈ acc, r ≠ a.rel ∧ ρ r = fun (x1 x2 : T) => x1 < x2

def Tense.PastConstraint {ι : Type u_1} {T : Type u_2} [LT T] (ρ : RelationAssignment ι T) (acc : Finset ι) : Prop

The past tense constraint on the relations a tense has access to: at least one is temporal precedence.

Equations

• Tense.PastConstraint ρ acc = ∃ r ∈ acc, ρ r = fun (x1 x2 : T) => x1 < x2

def Tense.PresentConstraint {ι : Type u_1} {T : Type u_2} [LT T] (ρ : RelationAssignment ι T) (acc : Finset ι) : Prop

The present tense constraint: every accessible relation entails the negation of temporal precedence.

Equations

• Tense.PresentConstraint ρ acc = ∀ r ∈ acc, ∀ (a b : T), ρ r a b → ¬a < b

theorem Tense.pastConstraint_singleton {ι : Type u_1} {T : Type u_2} {ρ : RelationAssignment ι T} {r : ι} [LT T] : PastConstraint ρ {r} ↔ ρ r = fun (x1 x2 : T) => x1 < x2

theorem Tense.PastConstraint.of_mem {ι : Type u_1} {T : Type u_2} {ρ : RelationAssignment ι T} {acc : Finset ι} {r : ι} [LT T] (hr : r ∈ acc) (h : ρ r = fun (x1 x2 : T) => x1 < x2) : PastConstraint ρ acc

theorem Tense.PresentConstraint.ne_lt {ι : Type u_1} {T : Type u_2} {ρ : RelationAssignment ι T} {acc : Finset ι} {r : ι} [LT T] (hq : PresentConstraint ρ acc) (hr : r ∈ acc) {a b : T} (hab : ρ r a b) : ρ r ≠ fun (x1 x2 : T) => x1 < x2

A present-constrained relation that holds somewhere is not temporal precedence.

theorem Tense.PastConstraint.false_of_presentConstraint {ι : Type u_1} {T : Type u_2} {ρ : RelationAssignment ι T} {r : ι} [LT T] (hp : PastConstraint ρ {r}) {acc : Finset ι} (hq : PresentConstraint ρ acc) (hr : r ∈ acc) {a b : T} (hab : ρ r a b) : False

No relation both licenses a past tense and satisfies a present constraint at an instantiated argument.

theorem Tense.TemporalArgument.not_locallyLicensed_of_coindexed {ι : Type u_1} {T : Type u_2} {ρ : RelationAssignment ι T} [Preorder T] {a : TemporalArgument ι} {g : ℕ → T} (hcon : a.Con ρ g) (h : a.index = a.evalIndex) : ¬a.LocallyLicensed ρ

theorem Tense.PastConstraint.nonLocallyLicensed_of_coindexed {ι : Type u_1} {T : Type u_2} {ρ : RelationAssignment ι T} {acc : Finset ι} [Preorder T] {a : TemporalArgument ι} {g : ℕ → T} (hp : PastConstraint ρ acc) (hcon : a.Con ρ g) (h : a.index = a.evalIndex) : a.NonLocallyLicensed ρ acc

A past tense coindexed with its local evaluation time is licensed non-locally.