Declerck (1991): Tense in English

This file formalizes the tense system of [Dec91b]. Time divides into two time-spheres, the past, lying wholly before the temporal zero-point t₀, and the present, which contains t₀ and is thereby divided into a pre-present, a present and a post-present sector; with the past sector these are the four absolute sectors, and each has its absolute tense, the preterit, the present perfect, the present tense and the future tense, so that the preterit and the present perfect differ in sphere and not in the time of the situation. Every tense represents the time of the situation as coinciding with a time of orientation, the situation-TO, and relates it by a chain of anteriority, simultaneity and posteriority relations to a binding TO, ultimately t₀: the four relative tenses, the past perfect, the conditional, the future perfect and the conditional perfect, relate the situation to a TO already established in a temporal domain. Where the chain relates the situation-TO only to an intermediate TO, its relation to t₀ is not expressed, so the conditional, the future perfect and the conditional perfect are vague, not ambiguous, among the three orderings of the situation against t₀ that [Rei47]'s format distinguishes as separate tenses. The tenses are chains, a realization assigns times along a chain from a binding TO, t₀ or the pseudo-t₀ of a post-present domain, and the projection onto the shared Reichenbach frame shows the vagueness as three orderings of R against S.

Implementation notes

Temporal subordination against shift of domain, the Present and Future Perspective Systems, the principle of unmarked temporal interpretation and the modal past are matters of discourse the chains do not decide; the companion grammar's examples of them, [Dec91a], are the rows of Data/Examples/Declerck1991.json.

References

• [Dec91b]
• [Dec91a]
• [Rei47]

Time-spheres, sectors and tenses

inductive Declerck1991.TimeSphere : Type

The two time-spheres: the past, lying wholly before t₀, and the present, which contains it.

• past : TimeSphere
• present : TimeSphere

@[instance_reducible]

instance Declerck1991.instDecidableEqTimeSphere : DecidableEq TimeSphere

Equations

• Declerck1991.instDecidableEqTimeSphere x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Declerck1991.instReprTimeSphere : Repr TimeSphere

Equations

• Declerck1991.instReprTimeSphere = { reprPrec := Declerck1991.instReprTimeSphere.repr }

def Declerck1991.instReprTimeSphere.repr : TimeSphere → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Declerck1991.instFintypeTimeSphere : Fintype TimeSphere

Equations

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

inductive Declerck1991.Sector : Type

The four absolute sectors, defined in direct relation to t₀: the past sphere as one sector, and the three sectors t₀ divides the present sphere into.

• past : Sector
• prePresent : Sector
• present : Sector
• postPresent : Sector

@[instance_reducible]

instance Declerck1991.instDecidableEqSector : DecidableEq Sector

Equations

• Declerck1991.instDecidableEqSector x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Declerck1991.instReprSector : Repr Sector

Equations

• Declerck1991.instReprSector = { reprPrec := Declerck1991.instReprSector.repr }

def Declerck1991.instReprSector.repr : Sector → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Declerck1991.instReprSector.repr Declerck1991.Sector.past prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Declerck1991.Sector.past")).group prec✝

@[instance_reducible]

instance Declerck1991.instFintypeSector : Fintype Sector

Equations

• Declerck1991.instFintypeSector = { elems := { val := ↑Declerck1991.Sector.enumList, nodup := Declerck1991.Sector.enumList_nodup }, complete := Declerck1991.instFintypeSector._proof_1 }

inductive Declerck1991.Tense : Type

The eight tenses of English.

• preterit : Tense
• present : Tense
• presentPerfect : Tense
• future : Tense
• pastPerfect : Tense
• conditional : Tense
• futurePerfect : Tense
• conditionalPerfect : Tense

@[instance_reducible]

instance Declerck1991.instDecidableEqTense : DecidableEq Tense

Equations

• Declerck1991.instDecidableEqTense x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Declerck1991.instReprTense.repr : Tense → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Declerck1991.instReprTense.repr Declerck1991.Tense.present prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Declerck1991.Tense.present")).group prec✝
• Declerck1991.instReprTense.repr Declerck1991.Tense.future prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Declerck1991.Tense.future")).group prec✝

@[instance_reducible]

instance Declerck1991.instReprTense : Repr Tense

Equations

• Declerck1991.instReprTense = { reprPrec := Declerck1991.instReprTense.repr }

@[instance_reducible]

instance Declerck1991.instFintypeTense : Fintype Tense

Equations

• Declerck1991.instFintypeTense = { elems := { val := ↑Declerck1991.Tense.enumList, nodup := Declerck1991.Tense.enumList_nodup }, complete := Declerck1991.instFintypeTense._proof_1 }

def Declerck1991.Tense.sphere : Tense → TimeSphere

The time-sphere a tense locates its situation in: the preterit and the present perfect differ only here, the same situation lying in the past sector or in the pre-present as the speaker conceives it.

Equations

• Declerck1991.Tense.preterit.sphere = Declerck1991.TimeSphere.past
• Declerck1991.Tense.pastPerfect.sphere = Declerck1991.TimeSphere.past
• Declerck1991.Tense.conditional.sphere = Declerck1991.TimeSphere.past
• Declerck1991.Tense.conditionalPerfect.sphere = Declerck1991.TimeSphere.past
• Declerck1991.Tense.present.sphere = Declerck1991.TimeSphere.present
• Declerck1991.Tense.presentPerfect.sphere = Declerck1991.TimeSphere.present
• Declerck1991.Tense.future.sphere = Declerck1991.TimeSphere.present
• Declerck1991.Tense.futurePerfect.sphere = Declerck1991.TimeSphere.present

def Declerck1991.Tense.chain : Tense → List Ordering

A tense's chain of relations from the binding TO outward to the situation-TO, each link relating a TO to the one before: .lt anteriority, .eq simultaneity, .gt posteriority. The past perfect is anteriority to a past TO, the conditional posteriority to one, the future perfect anteriority to a post-present TO, and the conditional perfect anteriority to a TO posterior to a past one.

Equations

• Declerck1991.Tense.preterit.chain = [Ordering.lt]
• Declerck1991.Tense.presentPerfect.chain = [Ordering.lt]
• Declerck1991.Tense.present.chain = [Ordering.eq]
• Declerck1991.Tense.future.chain = [Ordering.gt]
• Declerck1991.Tense.pastPerfect.chain = [Ordering.lt, Ordering.lt]
• Declerck1991.Tense.conditional.chain = [Ordering.lt, Ordering.gt]
• Declerck1991.Tense.futurePerfect.chain = [Ordering.gt, Ordering.lt]
• Declerck1991.Tense.conditionalPerfect.chain = [Ordering.lt, Ordering.gt, Ordering.lt]

def Declerck1991.Tense.IsAbsolute (t : Tense) : Prop

An absolute tense relates the situation-TO to t₀ directly; a relative tense relates it to a TO already established in a domain.

Equations

• t.IsAbsolute = (t.chain.length = 1)

@[instance_reducible]

instance Declerck1991.instDecidablePredTenseIsAbsolute : DecidablePred Tense.IsAbsolute

Equations

• Declerck1991.instDecidablePredTenseIsAbsolute x✝ = { decide := x✝.chain.length.beq 1, reflects_decide := ⋯ }

def Declerck1991.Tense.sector (t : Tense) : Sector

The absolute sector of the domain a tense's situation lies in: the past sphere is one sector, and in the present sphere the first link places the domain before, at or after t₀.

Equations

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

theorem Declerck1991.absolute_sector_bijective : (∀ (s : Sector), ∃ (t : Tense), t.IsAbsolute ∧ t.sector = s) ∧ ∀ (t u : Tense), t.IsAbsolute → u.IsAbsolute → t.sector = u.sector → t = u

Each absolute sector has exactly one absolute tense to locate a situation in it.

Realizations

def Declerck1991.Realizes {T : Type u_1} [LinearOrder T] (t : Tense) (binding : T) (tos : List T) : Prop

Times realizing a tense from a binding TO: each TO stands to the one before in the relation the chain gives, the last being the situation-TO. The binding TO is t₀ in an absolute use and, in the Present Perspective System, the pseudo-t₀ of a post-present domain.

Equations

• Declerck1991.Realizes t binding tos = (List.zipWith compare tos (binding :: tos) = t.chain)

@[instance_reducible]

instance Declerck1991.instDecidableRealizes {T : Type u_1} [LinearOrder T] (t : Tense) (binding : T) (tos : List T) : Decidable (Realizes t binding tos)

Equations

• Declerck1991.instDecidableRealizes t binding tos = Declerck1991.instDecidableRealizes._aux_1 t binding tos

def Declerck1991.toFrame {T : Type u_1} (t0 : T) (tos : List T) : Tense.ReichenbachFrame T

The Reichenbach frame of a realization from t₀: S = P = t₀ and R = E = the situation-TO, since every tense represents the time of the situation as coinciding with its TO.

Equations

• Declerck1991.toFrame t0 tos = Tense.ReichenbachFrame.root t0 (tos.getLast?.getD t0) (tos.getLast?.getD t0)

theorem Declerck1991.toFrame_eventPosition {T : Type u_1} [LinearOrder T] (t0 : T) (tos : List T) : (toFrame t0 tos).eventPosition = Ordering.eq

Every frame of a realization is simple in Reichenbach's sense, its event at its reference: the perfect lives in the chain, as anteriority to a TO, not in the relation of E to R.

theorem Declerck1991.pastPerfect_lt {T : Type u_1} [LinearOrder T] (t0 to2 ts : T) (h : Realizes Tense.pastPerfect t0 [to2, ts]) : ts < t0

A chain of anteriorities does fix the situation against t₀: the past perfect's situation lies before t₀.

theorem Declerck1991.vague (o : Ordering) : (∃ (to2 : ℤ) (ts : ℤ), Realizes Tense.conditional 0 [to2, ts] ∧ (toFrame 0 [to2, ts]).referencePosition = o) ∧ (∃ (to2 : ℤ) (ts : ℤ), Realizes Tense.futurePerfect 0 [to2, ts] ∧ (toFrame 0 [to2, ts]).referencePosition = o) ∧ ∃ (to2 : ℤ) (to3 : ℤ) (ts : ℤ), Realizes Tense.conditionalPerfect 0 [to2, to3, ts] ∧ (toFrame 0 [to2, to3, ts]).referencePosition = o

The conditional, the future perfect and the conditional perfect relate the situation-TO to an intermediate TO only, so its relation to t₀ is not expressed: each has realizations with the situation before, at and after t₀, three orderings of R against S that [Rei47]'s format can tell apart, and the tense is vague among them rather than ambiguous.