Grammatical tense

A tense, past, present or future (Tense, from Syntax/Category/Verb/Tense.lean), denotes a comparison cell, a Finset Ordering of the positions in which a reference time may stand to a perspective time, so the constraint a tense imposes on times r and p is compare r p ∈ ⟦t⟧. Following Kiparsky, tense locates the reference time relative to the perspective time, not the speech time. Cells are the elements of the Boolean algebra 𝒫 {lt, eq, gt}, so the derived categories are joins and complements of tense denotations rather than further tenses: Klecha's nonpast is ⟦present⟧ ⊔ ⟦future⟧, the nonfuture is ⟦future⟧ᶜ, and the unconstrained cell is ⊤.

Cells compose: comp R S collects the positions of a to c compatible with a to b in R and b to c in S. A cell is also a relation between times (toSetRel), the union of the relations <, = and > of its positions. The relation is defined on any order, so the past relates a moment of branching time to the moments below it. On linear time it is the constraint compare r p ∈ C, and the relation of a composed cell contains the composite of the relations, with equality when time is dense and has no first or last moment.

Main declarations

• Tense.denote: the cell a tense denotes, written ⟦t⟧.
• Tense.nonpast: the cell of the present or future.
• Tense.comp: the composition of two cells.
• Tense.toSetRel: a cell as a relation between times.

Main statements

• Tense.inv_toSetRel: the converse of a cell's relation is the relation of its mirror image.
• Tense.toSetRel_comp_subset, Tense.toSetRel_comp: the composite of two cells' relations lies in the relation of the composed cell, and is that relation on dense time without endpoints.

References

• [Kip02]
• [Kle16]

def Tense.denote : Tense → Finset Ordering

A tense denotes the cell of orderings in which the reference time may stand to the perspective time, before it for the past, at it for the present and after it for the future.

Equations

• Tense.past.denote = {Ordering.lt}
• Tense.present.denote = {Ordering.eq}
• Tense.future.denote = {Ordering.gt}

@[instance_reducible]

instance Tense.instDenotesFinsetOrdering : Semantics.Denotes Tense (Finset Ordering)

Equations

• Tense.instDenotesFinsetOrdering = { denote := Tense.denote }

theorem Tense.denote_past : Semantics.Denotes.denote past = {Ordering.lt}

theorem Tense.denote_present : Semantics.Denotes.denote present = {Ordering.eq}

theorem Tense.denote_future : Semantics.Denotes.denote future = {Ordering.gt}

def Tense.nonpast : Finset Ordering

The nonpast is the cell of a reference time at or after the perspective time.

Equations

• Tense.nonpast = {Ordering.eq, Ordering.gt}

theorem Tense.nonpast_eq_present_sup_future : nonpast = Semantics.Denotes.denote present ⊔ Semantics.Denotes.denote future

The nonpast is the join of the present and the future, not a fourth tense.

theorem Tense.nonpast_eq_compl_past : nonpast = (Semantics.Denotes.denote past)ᶜ

theorem Tense.past_sup_present : Semantics.Denotes.denote past ⊔ Semantics.Denotes.denote present = (Semantics.Denotes.denote future)ᶜ

The nonfuture is the join of the past and the present.

def Tense.comp (R S : Finset Ordering) : Finset Ordering

The composition of two cells collects the orderings of a to c compatible with a to b in R and b to c in S.

Equations

• Tense.comp R S = {o : Ordering | ∃ r ∈ R, ∃ s ∈ S, o ∈ r.comp s}

theorem Tense.mem_comp {R S : Finset Ordering} {o : Ordering} : o ∈ comp R S ↔ ∃ r ∈ R, ∃ s ∈ S, o ∈ r.comp s

theorem Tense.comp_sup_left (R R' S : Finset Ordering) : comp (R ⊔ R') S = comp R S ⊔ comp R' S

theorem Tense.comp_sup_right (R S S' : Finset Ordering) : comp R (S ⊔ S') = comp R S ⊔ comp R S'

@[simp]

theorem Tense.comp_present_left (S : Finset Ordering) : comp (Semantics.Denotes.denote present) S = S

@[simp]

theorem Tense.comp_present_right (R : Finset Ordering) : comp R (Semantics.Denotes.denote present) = R

@[simp]

theorem Tense.comp_past_past : comp (Semantics.Denotes.denote past) (Semantics.Denotes.denote past) = Semantics.Denotes.denote past

@[simp]

theorem Tense.comp_future_future : comp (Semantics.Denotes.denote future) (Semantics.Denotes.denote future) = Semantics.Denotes.denote future

@[simp]

theorem Tense.comp_past_future : comp (Semantics.Denotes.denote past) (Semantics.Denotes.denote future) = ⊤

A past followed by a future leaves the relation of the outer times open.

@[simp]

theorem Tense.comp_future_past : comp (Semantics.Denotes.denote future) (Semantics.Denotes.denote past) = ⊤

A future followed by a past leaves the relation of the outer times open.

Cells on linear time

@[simp]

theorem Tense.compare_mem_past {T : Type u_1} [LinearOrder T] (r p : T) : compare r p ∈ Semantics.Denotes.denote past ↔ r < p

@[simp]

theorem Tense.compare_mem_present {T : Type u_1} [LinearOrder T] (r p : T) : compare r p ∈ Semantics.Denotes.denote present ↔ r = p

@[simp]

theorem Tense.compare_mem_future {T : Type u_1} [LinearOrder T] (r p : T) : compare r p ∈ Semantics.Denotes.denote future ↔ p < r

@[simp]

theorem Tense.compare_mem_nonpast {T : Type u_1} [LinearOrder T] (r p : T) : compare r p ∈ nonpast ↔ p ≤ r

@[simp]

theorem Tense.compare_mem_compl_future {T : Type u_1} [LinearOrder T] (r p : T) : compare r p ∈ (Semantics.Denotes.denote future)ᶜ ↔ r ≤ p

theorem Tense.compare_mem_comp {T : Type u_1} [LinearOrder T] {R S : Finset Ordering} {a b c : T} (h₁ : compare a b ∈ R) (h₂ : compare b c ∈ S) : compare a c ∈ comp R S

theorem Tense.compare_mem_comp_iff {T : Type u_1} {C D : Finset Ordering} [LinearOrder T] [DenselyOrdered T] [NoMinOrder T] [NoMaxOrder T] {a c : T} : compare a c ∈ comp C D ↔ ∃ (b : T), compare a b ∈ C ∧ compare b c ∈ D

On dense time without endpoints a cell composition is realized through an intermediate time.

The relation of a cell

def Tense.toSetRel {T : Type u_1} [LT T] (C : Finset Ordering) : SetRel T T

The relation of a cell relates a perspective time to the reference times that stand to it in one of the cell's positions.

Equations

• Tense.toSetRel C = {x : T × T | ∃ o ∈ C, o.Compares x.2 x.1}

theorem Tense.mem_toSetRel {T : Type u_1} {C : Finset Ordering} {p r : T} [LT T] : (p, r) ∈ toSetRel C ↔ ∃ o ∈ C, o.Compares r p

@[simp]

theorem Tense.mem_toSetRel_past {T : Type u_1} {p r : T} [LT T] : (p, r) ∈ toSetRel (Semantics.Denotes.denote past) ↔ r < p

@[simp]

theorem Tense.mem_toSetRel_present {T : Type u_1} {p r : T} [LT T] : (p, r) ∈ toSetRel (Semantics.Denotes.denote present) ↔ r = p

@[simp]

theorem Tense.mem_toSetRel_future {T : Type u_1} {p r : T} [LT T] : (p, r) ∈ toSetRel (Semantics.Denotes.denote future) ↔ p < r

@[simp]

theorem Tense.toSetRel_bot {T : Type u_1} [LT T] : toSetRel ⊥ = ∅

theorem Tense.toSetRel_sup {T : Type u_1} [LT T] (C D : Finset Ordering) : toSetRel (C ⊔ D) = toSetRel C ∪ toSetRel D

theorem Tense.toSetRel_subset_toSetRel {T : Type u_1} {C D : Finset Ordering} [LT T] (h : C ⊆ D) : toSetRel C ⊆ toSetRel D

theorem Tense.inv_toSetRel {T : Type u_1} [LT T] (C : Finset Ordering) : (toSetRel C).inv = toSetRel (Finset.image Ordering.swap C)

The converse of a cell's relation is the relation of its mirror image, which exchanges the past with the future.

@[simp]

theorem Tense.inv_toSetRel_past {T : Type u_1} [LT T] : (toSetRel (Semantics.Denotes.denote past)).inv = toSetRel (Semantics.Denotes.denote future)

@[simp]

theorem Tense.inv_toSetRel_future {T : Type u_1} [LT T] : (toSetRel (Semantics.Denotes.denote future)).inv = toSetRel (Semantics.Denotes.denote past)

theorem Tense.mem_toSetRel_iff_compare {T : Type u_1} [LinearOrder T] {C : Finset Ordering} {p r : T} : (p, r) ∈ toSetRel C ↔ compare r p ∈ C

On linear time a cell relates a perspective time to a reference time exactly when the position of the reference time is in the cell.

theorem Tense.toSetRel_past_comp_self {T : Type u_1} [Preorder T] [DenselyOrdered T] : (toSetRel (Semantics.Denotes.denote past)).comp (toSetRel (Semantics.Denotes.denote past)) = toSetRel (Semantics.Denotes.denote past)

On dense time the past relation composed with itself is the past relation, since a time before an earlier time is earlier and an earlier time has a time between.

@[simp]

theorem Tense.mem_toSetRel_iff {T : Type u_1} {C : Finset Ordering} {p r : T} [LinearOrder T] : (p, r) ∈ toSetRel C ↔ compare r p ∈ C

On linear time the relation of a cell is the constraint the cell imposes.

@[instance_reducible]

instance Tense.instDecidableMemProdSetRelToSetRelMk {T : Type u_1} {C : Finset Ordering} {p r : T} [LinearOrder T] : Decidable ((p, r) ∈ toSetRel C)

Equations

• Tense.instDecidableMemProdSetRelToSetRelMk = decidable_of_iff (compare r p ∈ C) ⋯

@[simp]

theorem Tense.toSetRel_top {T : Type u_1} [LinearOrder T] : toSetRel ⊤ = Set.univ

theorem Tense.toSetRel_compl {T : Type u_1} [LinearOrder T] (C : Finset Ordering) : toSetRel Cᶜ = (toSetRel C)ᶜ

theorem Tense.toSetRel_comp_subset {T : Type u_1} [LinearOrder T] (C D : Finset Ordering) : (toSetRel C).comp (toSetRel D) ⊆ toSetRel (comp D C)

theorem Tense.toSetRel_comp {T : Type u_1} [LinearOrder T] [DenselyOrdered T] [NoMinOrder T] [NoMaxOrder T] (C D : Finset Ordering) : (toSetRel C).comp (toSetRel D) = toSetRel (comp D C)

On dense time without endpoints the composite of two cells' relations is the relation of the composed cell.