Declerck (1991): Time-Spheres, TO-Chains, and Temporal Domains

[Dec91b] organizes English tense around two time-spheres — past and present, the latter divided into pre-present, present, and post-present sectors — and chains of times of orientation (TOs): an absolute tense establishes a temporal domain, relative tenses bind further TOs within it, and the time of the situation always coincides with a TO (TS = TO_sit). Example sentences in the generated block are drawn from Declerck's companion volume, [Dec91a].

Main declarations

• TOChain.DeclercianSchema: a tense as a chain of TOs plus a time-sphere
• TOChain.preterit … TOChain.conditionalPerfect: the eight English tenses
• TOChain.DeclercianSchema.toFrame, toDomain, declercianToTower: projections to the shared Reichenbach, Domain, and ContextTower substrates
• TOChain.DeclercianSchema.zoneOf: project-side zone classifier
• putiDefault: Declerck's principle of unmarked temporal interpretation

Time-spheres

inductive Declerck1991.TOChain.TimeSphere : Type

The two time-spheres of English ([Dec91b]): the tense system divides time into a past time-sphere lying wholly before t₀ (preterit, past perfect, conditional, conditional perfect) and a present time-sphere including t₀ (present, present perfect, future, future perfect).

This is a conceptual partition, not a temporal relation: both "I visited Paris" and "I have visited Paris" can refer to the same objective event, but differ in time-sphere membership.

• past : TimeSphere

  wholly before t₀

• present : TimeSphere

  includes t₀

@[implicit_reducible]

instance Declerck1991.TOChain.instDecidableEqTimeSphere : DecidableEq TimeSphere

Equations

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

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

Equations

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

@[implicit_reducible]

instance Declerck1991.TOChain.instReprTimeSphere : Repr TimeSphere

Equations

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

TO-chain architecture

structure Declerck1991.TOChain.TOLink (Time : Type u_1) : Type u_1

A single link in a TO chain: a Tense.Orientation-labelled time of orientation related to the next TO inward by a temporal relation.

Example: in the past perfect schema TS simul TO_sit before TO₂ before TO₁, the link for TO₂ is ⟨.sub 0, .lt, t₂⟩ — meaning TO₂ (= .sub 0, one step out from the binding TO₁ = .perspective) stands in the before relation to the next TO outward. The .situation role labels TO_sit.

• name : Tense.Orientation

  The orientation-time role of this link (.situation for TO_sit; .sub n for an intermediate TO).

• relation : Ordering

  How this TO relates to the next TO inward toward TO₁, as a point comparison (Ordering): .lt = this TO precedes the next (before); .gt = this TO follows it (after); .eq = simultaneous (overlapping).

• time : Time

  The resolved time value.

structure Declerck1991.TOChain.DeclercianSchema (Time : Type u_1) : Type u_1

Declerck's tense schema: a chain of TOs from TO₁ outward to TO_sit, with a time-sphere classification.

The chain runs from TO₁ (innermost, adjacent to t₀) outward through intermediate TOs to TO_sit. The situation time TS is always simultaneous with TO_sit (Declerck's universal principle: every tense represents TS as coinciding with some TO), so there is no separate ts field — both E and R in the Reichenbach projection are derived from TO_sit.

The chain captures only adjacent relations. Non-adjacent TOs (e.g., TO_sit and TO₁ in the conditional tense) have no asserted relation — this is Declerck's account of temporal vagueness.

• t0 : Time

  Temporal zero-point (usually = speech time)

• to1 : Time

  Basic TO (TO₁): the starting point for temporal relations. Usually = t₀, but can be a future or past time in embedded contexts.

• chain : List (TOLink Time)

  Chain of TOs from TO₁ outward. Each link's relation connects it to the previous link (or to TO₁ for the first link). The last element is TO_sit, which TS is simultaneous with.

• timeSphere : TimeSphere

  Which time-sphere the tense belongs to

def Declerck1991.TOChain.DeclercianSchema.toSit {Time : Type u_1} (s : DeclercianSchema Time) : Time

The situation-TO (= TS): the TO with which the situation time coincides. This is the last element of the chain, or TO₁ if the chain is empty.

Equations

• s.toSit = match s.chain.getLast? with | some link => link.time | none => s.to1

def Declerck1991.TOChain.DeclercianSchema.depth {Time : Type u_1} (s : DeclercianSchema Time) : ℕ

Number of TOs in the schema (including TO₁).

Equations

• s.depth = s.chain.length + 1

Projection to ReichenbachFrame

def Declerck1991.TOChain.DeclercianSchema.toFrame {Time : Type u_1} (s : DeclercianSchema Time) : _root_.Time.ReichenbachFrame Time

Project a Declercian schema to a Reichenbach frame: S = t₀, P = TO₁, R = E = TO_sit (by Declerck's universal principle TS = TO_sit).

Since R = E always, no Declercian frame satisfies isPerfect (E < R) — see toFrame_not_isPerfect. The "perfect" in Declerck's system is a chain property (TO_sit before TO₂), not an E/R relation. The projection is lossy: intermediate TOs and temporal vagueness are collapsed.

Equations

• s.toFrame = { speechTime := s.t0, perspectiveTime := s.to1, referenceTime := s.toSit, eventTime := s.toSit }

theorem Declerck1991.TOChain.DeclercianSchema.eventTime_eq_referenceTime {Time : Type u_1} (s : DeclercianSchema Time) : s.toFrame.eventTime = s.toFrame.referenceTime

Every Declercian frame has E = R (Declerck's TS = TO_sit principle).

The eight English tense schemata

Each schema is parameterized by concrete times so that bridge theorems can verify the structural relations.

def Declerck1991.TOChain.preterit {Time : Type u_1} (t0 toSit : Time) : DeclercianSchema Time

Preterit: TS simul TO_sit, TO_sit before TO₁. Past time-sphere.

Example: "John was ill yesterday." — TO₁ = t₀ (absolute use), TO_sit before TO₁, TS = TO_sit.

Equations

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

def Declerck1991.TOChain.present {Time : Type u_1} (t0 toSit : Time) : DeclercianSchema Time

Present tense: TS simul TO_sit, TO_sit includes t₀. Present time-sphere.

Declerck's key claim: the present tense does NOT assert TO_sit = t₀ but rather TO_sit includes t₀. For point times this degenerates to equality (captured by .eq); interval-level inclusion is handled by NonemptyInterval.le_def.

Example: "John is in London."

Equations

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

def Declerck1991.TOChain.presentPerfect {Time : Type u_1} (t0 toSit : Time) : DeclercianSchema Time

Present perfect: TS simul TO_sit, TO_sit before TO₁. Present time-sphere (the crucial difference from the preterit).

Declerck's distinctive claim: the present perfect and preterit differ in time-sphere membership, not in definiteness or current relevance (current relevance is "no more than an implicature"). Both can refer to the same event; the perfect places it in the pre-present sector.

Example: "I have visited Paris."

Scope note: the schema represents the predicated situation's TO_sit; the continuative reading ("I have lived here for ten years"), where the full situation extends through t₀, is not representable here.

Equations

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

def Declerck1991.TOChain.pastPerfect {Time : Type u_1} (t0 to2 toSit : Time) : DeclercianSchema Time

Past perfect: TS simul TO_sit, TO_sit before TO₂, TO₂ before TO₁. Past time-sphere. "The past of the preterit" or "the past of the present perfect": TO₂ lies in the past time-sphere relative to TO₁, and TO_sit is anterior to TO₂.

Example: "John had left before we arrived."

Equations

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

def Declerck1991.TOChain.future {Time : Type u_1} (t0 toSit : Time) : DeclercianSchema Time

Future tense: TS simul TO_sit, TO_sit after TO₁. Present time-sphere. TO_sit lies in the post-present sector.

Example: "I will do it next week."

Equations

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

def Declerck1991.TOChain.futurePerfect {Time : Type u_1} (t0 to2 toSit : Time) : DeclercianSchema Time

Future perfect: TS simul TO_sit, TO_sit before TO₂, TO₂ after TO₁. Present time-sphere.

The future perfect is vague about the relation between TO_sit and TO₁: John may have already left, may be leaving now, or may leave later. The chain captures this by NOT asserting a TO_sit–TO₁ relation.

Example: "John will have left when we arrive."

Equations

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

def Declerck1991.TOChain.conditional {Time : Type u_1} (t0 to2 toSit : Time) : DeclercianSchema Time

Conditional tense: TS simul TO_sit, TO_sit after TO₂, TO₂ before TO₁. Past time-sphere (for TO₂). The mirror image of the future perfect: "future in the past". Like the future perfect, it is vague about TO_sit's relation to TO₁ — the situation may or may not have occurred by speech time.

Example (from [Dec91b]): "The faded red brick of the house had weathered many London storms and would weather many more."

Equations

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

def Declerck1991.TOChain.conditionalPerfect {Time : Type u_1} (t0 to2 to3 toSit : Time) : DeclercianSchema Time

Conditional perfect: TS simul TO_sit, TO_sit before TO₃, TO₃ after TO₂, TO₂ before TO₁. Past time-sphere. The most intricate English tense: "past in the future in the past".

Example: "He would have left by then."

Equations

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

Bridge theorems: Declercian schema → Reichenbach frame

Each bridge theorem shows that a Declercian schema, when resolved to concrete times satisfying the chain constraints, projects to a ReichenbachFrame satisfying the expected Reichenbach tense predicate. This connects Declerck's chain architecture to the Reichenbach infrastructure used by the other tense theories in linglib.

theorem Declerck1991.TOChain.DeclercianSchema.toFrame_not_isPerfect {Time : Type u_1} [LinearOrder Time] (s : DeclercianSchema Time) : ¬s.toFrame.isPerfect

No Declercian frame is isPerfect (E < R): the TS = TO_sit principle forces E = R. The perfect lives in the chain, not in the E/R relation.

theorem Declerck1991.TOChain.preterit_isPast {Time : Type u_1} [LinearOrder Time] (t0 toSit : Time) (h : toSit < t0) : (preterit t0 toSit).toFrame.isPast

Preterit projects to a frame satisfying PAST (R < P).

theorem Declerck1991.TOChain.present_isPresent {Time : Type u_1} (t0 : Time) : (present t0 t0).toFrame.isPresent

Present projects to a frame satisfying PRESENT (R = P) for point times.

theorem Declerck1991.TOChain.presentPerfect_frame_isPast {Time : Type u_1} [LinearOrder Time] (t0 toSit : Time) (h : toSit < t0) : (presentPerfect t0 toSit).toFrame.isPast

Present perfect projects to PAST (R < P) — because TO_sit (= R) < TO₁ (= P). The present-sphere membership is tracked by timeSphere, not by the Reichenbach R/P relation.

theorem Declerck1991.TOChain.preterit_presentPerfect_same_frame {Time : Type u_1} (t0 toSit : Time) : (preterit t0 toSit).toFrame = (presentPerfect t0 toSit).toFrame

Preterit and present perfect produce identical Reichenbach frames for the same times — they differ ONLY in time-sphere. This is Declerck's central thesis about the perfect/preterit distinction: the contrast is sphere membership, not R/P configuration.

theorem Declerck1991.TOChain.preterit_presentPerfect_differ_sphere {Time : Type u_1} (t0 toSit : Time) : (preterit t0 toSit).timeSphere ≠ (presentPerfect t0 toSit).timeSphere

… but they differ in time-sphere.

theorem Declerck1991.TOChain.pastPerfect_isPast {Time : Type u_1} [LinearOrder Time] (t0 to2 toSit : Time) (h₁ : toSit < to2) (h₂ : to2 < t0) : (pastPerfect t0 to2 toSit).toFrame.isPast

Past perfect projects to PAST (R < P): the chain gives TO_sit < TO₂ < TO₁, so R (= TO_sit) < P (= TO₁).

theorem Declerck1991.TOChain.future_isFuture {Time : Type u_1} [LinearOrder Time] (t0 toSit : Time) (h : t0 < toSit) : (future t0 toSit).toFrame.isFuture

Future projects to FUTURE (P < R).

Temporal vagueness

When a schema's chain has no direct link between two TOs, their relation is genuinely unspecified. The future perfect and conditional tense are both vague about TO_sit's relation to TO₁. [Dec91b] argues this against the [Rei47] format, which generates three orderings for the posterior past (R–E–S; R–S,E; R–S–E): if one tense form realizes three configurations, the form would have to be three-ways ambiguous, and there is no evidence that the English conditional (or future perfect) is ambiguous rather than vague.

theorem Declerck1991.TOChain.futurePerfect_vague_sit_t0 : ∃ (toSit₁ : ℤ) (toSit₂ : ℤ) (toSit₃ : ℤ), ∃ to2 > 0, toSit₁ < to2 ∧ toSit₂ < to2 ∧ toSit₃ < to2 ∧ toSit₁ < 0 ∧ toSit₂ = 0 ∧ toSit₃ > 0

The future perfect is vague about TO_sit's relation to t₀: the chain relates TO_sit to TO₂ and TO₂ to TO₁, but NOT TO_sit to TO₁. All three scenarios are consistent.

theorem Declerck1991.TOChain.conditional_vague_sit_t0 : ∃ (toSit₁ : ℤ) (toSit₂ : ℤ) (toSit₃ : ℤ), ∃ to2 < 0, toSit₁ > to2 ∧ toSit₂ > to2 ∧ toSit₃ > to2 ∧ toSit₁ < 0 ∧ toSit₂ = 0 ∧ toSit₃ > 0

The conditional tense is vague about TO_sit's relation to t₀: the chain relates TO_sit to TO₂ and TO₂ to TO₁, but NOT TO_sit to TO₁. The three Reichenbach orderings for the posterior past are instances of a single vague schema, not distinct tenses.

Tower bridge: TO-chain as context tower

Each link in a TO-chain corresponds to a temporal shift in a context tower: TO₁ is the tower origin, and each subsequent TO maps to a push with a temporalShift. DeclercianSchema.depth counts TOs including TO₁, while the tower counts shifts, so schema.depth = tower.depth + 1.

def Declerck1991.TOChain.declercianToShifts {Time : Type u_1} {E : Type u_2} {P : Type u_3} (chain : List (TOLink Time)) : List (Semantics.Context.ContextShift (Semantics.Context.KContext Time E P Time))

Convert a Declercian TO-chain to a list of temporal shifts. Each TOLink becomes a temporal shift with .temporal label. The relation in the link is not encoded in the shift itself — it is a constraint on the times, not a transformation.

Equations

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

def Declerck1991.TOChain.declercianToTower {Time : Type u_1} {E : Type u_2} {P : Type u_3} (s : DeclercianSchema Time) (agent addressee : E) (world : Time) (pos : P) : Semantics.Context.ContextTower (Semantics.Context.KContext Time E P Time)

Convert a Declercian schema to a context tower: the origin context has time := to1 (the basic TO), and each chain link becomes a temporal shift.

Equations

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

theorem Declerck1991.TOChain.declercianToTower_depth {Time : Type u_1} {E : Type u_2} {P : Type u_3} (s : DeclercianSchema Time) (agent addr : E) (world : Time) (pos : P) : (declercianToTower s agent addr world pos).depth = s.chain.length

The tower depth equals the chain length.

theorem Declerck1991.TOChain.declerck_depth_is_tower_depth_plus_one {Time : Type u_1} {E : Type u_2} {P : Type u_3} (s : DeclercianSchema Time) (agent addr : E) (world : Time) (pos : P) : s.depth = (declercianToTower s agent addr world pos).depth + 1

Declerck's depth = tower depth + 1: Declerck counts TO₁ as part of the depth (number of TOs), while the tower counts only shifts (pushes).

theorem Declerck1991.TOChain.preterit_tower_depth {Time : Type u_1} (t0 toSit : Time) {E : Type u_2} {P : Type u_3} (agent addr : E) (world : Time) (pos : P) : (declercianToTower (preterit t0 toSit) agent addr world pos).depth = 1

For simple tenses (chain length 1), the tower has depth 1.

theorem Declerck1991.TOChain.pastPerfect_tower_depth {Time : Type u_1} (t0 to2 toSit : Time) {E : Type u_2} {P : Type u_3} (agent addr : E) (world : Time) (pos : P) : (declercianToTower (pastPerfect t0 to2 toSit) agent addr world pos).depth = 2

For compound tenses (chain length 2), the tower has depth 2.

theorem Declerck1991.TOChain.conditionalPerfect_tower_depth {Time : Type u_1} (t0 to2 to3 toSit : Time) {E : Type u_2} {P : Type u_3} (agent addr : E) (world : Time) (pos : P) : (declercianToTower (conditionalPerfect t0 to2 to3 toSit) agent addr world pos).depth = 3

For the conditional perfect (chain length 3), the tower has depth 3.

Domain bridge: TO-chain as Tense.Domain

Re-express DeclercianSchema via the framework-agnostic Tense.Domain substrate (central TO + list of sub-TOs, with Allen relations computed on demand from the underlying linear order). Additive: the schema structure and named-tense constructors stay unchanged; domain-level tooling can work uniformly with s.toDomain.relatedByName, while Reichenbach-projecting code continues to use s.toFrame.

def Declerck1991.TOChain.DeclercianSchema.toDomain {Time : Type u_1} [LinearOrder Time] (s : DeclercianSchema Time) : Tense.Domain Time Tense.Orientation

The schema as a Tense.Domain over the universal Orientation role vocabulary: central = .utterance (t₀), sub-TOs = .perspective (TO₁) followed by every chain link as a point interval.

The Allen relations between any pair of TOs are computed from the underlying LinearOrder Time via NonemptyInterval.allenRel; nothing is stored. The chain's relation field encodes the intended Declercian temporal relation but is not consulted here — its job is to constrain admissible time assignments at the call site.

Equations

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

@[simp]

theorem Declerck1991.TOChain.DeclercianSchema.toDomain_central {Time : Type u_1} [LinearOrder Time] (s : DeclercianSchema Time) : s.toDomain.central = Tense.NamedTO.ofPoint Tense.Orientation.utterance s.t0

@[simp]

theorem Declerck1991.TOChain.DeclercianSchema.toDomain_subTOs {Time : Type u_1} [LinearOrder Time] (s : DeclercianSchema Time) : s.toDomain.subTOs = Tense.NamedTO.ofPoint Tense.Orientation.perspective s.to1 :: List.map (fun (link : TOLink Time) => Tense.NamedTO.ofPoint link.name link.time) s.chain

theorem Declerck1991.TOChain.DeclercianSchema.toDomain_labels {Time : Type u_1} [LinearOrder Time] (s : DeclercianSchema Time) : s.toDomain.labels = Tense.Orientation.utterance :: Tense.Orientation.perspective :: List.map TOLink.name s.chain

The schema's domain labels: utterance first, then perspective, then every chain link's role. Useful for stating role-set invariants.

Zone classifier

Zone crosses the two time-spheres with three positions (anterior, central, posterior). Project-side caveat: Declerck's own inventory of absolute sectors is four — pre-present, present, and post-present sectors of the present time-sphere, plus a single undivided past sector. prePast and postPast are not Declercian sectors but domain-internal positions (anteriority/posteriority to a TO inside a past temporal domain); the symmetric 2×3 cross is this file's classifier, not the book's taxonomy.

DeclercianSchema.zoneOf classifies by (timeSphere, chain length, last link's relation). The classifier is not the inverse of the chain — vague tenses (future perfect, conditional) under-determine TO_sit's zone, and the classifier returns the zone of the immediate anchor.

inductive Declerck1991.TOChain.Zone : Type

The two time-spheres crossed with three positions: Declerck's four absolute sectors (past, prePresent, present, postPresent) plus the domain-internal positions prePast and postPast (see the section docstring caveat).

• prePast : Zone
• past : Zone
• postPast : Zone
• prePresent : Zone
• present : Zone
• postPresent : Zone

@[implicit_reducible]

instance Declerck1991.TOChain.instDecidableEqZone : DecidableEq Zone

Equations

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

@[implicit_reducible]

instance Declerck1991.TOChain.instReprZone : Repr Zone

Equations

• Declerck1991.TOChain.instReprZone = { reprPrec := Declerck1991.TOChain.instReprZone.repr }

def Declerck1991.TOChain.instReprZone.repr : Zone → ℕ → Std.Format

Equations

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

def Declerck1991.TOChain.DeclercianSchema.zoneOf {Time : Type u_1} (s : DeclercianSchema Time) : Zone

Classify a schema's TO_sit by zone, based on (timeSphere, chain length, last chain link's relation). Simple past-sphere tenses (chain length 1) classify as past; deeper past-sphere chains land in the domain-internal prePast/postPast positions. Defaults to the sphere's center for empty chains and non-strict relations.

Equations

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

Each named English tense classifies to its expected zone; these exercise the zoneOf match against all eight constructors.

theorem Declerck1991.TOChain.preterit_zone {Time : Type u_1} (t0 toSit : Time) : (preterit t0 toSit).zoneOf = Zone.past

theorem Declerck1991.TOChain.present_zone {Time : Type u_1} (t0 toSit : Time) : (present t0 toSit).zoneOf = Zone.present

theorem Declerck1991.TOChain.presentPerfect_zone {Time : Type u_1} (t0 toSit : Time) : (presentPerfect t0 toSit).zoneOf = Zone.prePresent

theorem Declerck1991.TOChain.future_zone {Time : Type u_1} (t0 toSit : Time) : (future t0 toSit).zoneOf = Zone.postPresent

theorem Declerck1991.TOChain.pastPerfect_zone {Time : Type u_1} (t0 to2 toSit : Time) : (pastPerfect t0 to2 toSit).zoneOf = Zone.prePast

theorem Declerck1991.TOChain.conditional_zone {Time : Type u_1} (t0 to2 toSit : Time) : (conditional t0 to2 toSit).zoneOf = Zone.postPast

theorem Declerck1991.TOChain.futurePerfect_zone {Time : Type u_1} (t0 to2 toSit : Time) : (futurePerfect t0 to2 toSit).zoneOf = Zone.prePresent

theorem Declerck1991.TOChain.conditionalPerfect_zone {Time : Type u_1} (t0 to2 to3 toSit : Time) : (conditionalPerfect t0 to2 to3 toSit).zoneOf = Zone.prePast

theorem Declerck1991.TOChain.preterit_presentPerfect_differ_zone {Time : Type u_1} (t0 toSit : Time) : (preterit t0 toSit).zoneOf ≠ (presentPerfect t0 toSit).zoneOf

Preterit and present perfect classify to different zones (past vs prePresent) despite projecting to identical Reichenbach frames (preterit_presentPerfect_same_frame). The Zone classifier surfaces what toFrame flattens.

TenseSystem and AspectSystem instances

The aspect instance collapses event and reference roles both to .situation — Declerck's universal TS = TO_sit principle means E = R always holds, so "event precedes reference" can never hold and the perfect lives in the chain structure instead. Exactly Declerck's claim.

@[implicit_reducible]

instance Declerck1991.TOChain.declercianSchema_tenseSystem {Time : Type u_1} [LinearOrder Time] : TenseSystem (DeclercianSchema Time) Time Tense.Orientation

Equations

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

@[implicit_reducible]

instance Declerck1991.TOChain.declercianSchema_aspectSystem {Time : Type u_1} [LinearOrder Time] : AspectSystem (DeclercianSchema Time) Time Tense.Orientation

Equations

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

Temporal domain: subordination vs shift

A stretch of discourse may either incorporate each new clause into an existing temporal domain (relative tenses expressing anteriority, simultaneity, posteriority — Declerck's "temporal subordination") or shift to a new absolute domain. Subordination keeps the perspective on the existing domain anchor; shift resets the perspective to S.

See Examples.domainShift1a (subordination) and Examples.domainShift1b (shift) for the book's examples.

def Declerck1991.domainLeft : Time.ReichenbachFrame ℤ

"He left…" — past domain anchor. Serves both discourse continuations below: temporal subordination ("…and would never come back") and domain shift ("…and never came back").

Equations

• Declerck1991.domainLeft = { speechTime := 0, perspectiveTime := 0, referenceTime := -5, eventTime := -5 }

def Declerck1991.domainSubordWouldReturn : Time.ReichenbachFrame ℤ

"…and would never come back" — relative tense within the past domain established by left. Constructed via shiftedFrame so the perspective is taken from domainLeft.eventTime.

Equations

• Declerck1991.domainSubordWouldReturn = Tense.shiftedFrame Declerck1991.domainLeft (-3) (-3)

def Declerck1991.domainShiftCameBack : Time.ReichenbachFrame ℤ

"…and never came back" — independent past domain (shift): an absolute preterit, perspective reset to S.

Equations

• Declerck1991.domainShiftCameBack = { speechTime := 0, perspectiveTime := 0, referenceTime := -3, eventTime := -3 }

theorem Declerck1991.domainLeft_isPast : domainLeft.isPast

The domain anchor is past (R < P).

theorem Declerck1991.domainSubordWouldReturn_posterior : domainSubordWouldReturn.referenceTime > domainLeft.eventTime

Subordination: wouldReturn is posterior within the domain.

theorem Declerck1991.domainShiftCameBack_absolute : domainShiftCameBack.isSimpleCase

Shift: the shifted continuation has absolute perspective (P = S).

theorem Declerck1991.domainSubordWouldReturn_shifted : ¬domainSubordWouldReturn.isSimpleCase

Subordination: wouldReturn has a shifted (non-absolute) perspective.

Modal (false) past

Some uses of the past tense have non-past reference: the past morphology marks modal remoteness (tentativeness, politeness, hypotheticality) rather than past temporal location — Declerck's "modal past".

A bare ReichenbachFrame cannot encode this phenomenon: a single (R, E) pair represents either the morphology or the interpretation, not their divergence. The data therefore live as Examples.modalPastWish and Examples.modalPastIfWas; no frames are stipulated here.

Future-time subclauses: Present vs Future Perspective System

[Dec91b] distinguishes two systems for tense in clauses about post-present time. The FPS (Future Perspective System) uses tenses that establish post-present domains directly from t₀: the future tense (as absolute tense) and the future perfect. The PPS (Present Perspective System) consists of relative tenses binding into an established post-present domain whose binding TO behaves as a pseudo-t₀: present tense for simultaneity, preterit or present perfect for anteriority, future for posteriority. In "If the weather is good, John will go to the seaside", the matrix is FPS (absolute future) and the protasis is PPS (relative present against the pseudo-t₀); will in a pure-future protasis is the marked FPS option.

Encoded via shiftedFrame: PPS = relative present against a shifted perspective, FPS = absolute frame (P = S). Examples.whenPresent is the same phenomenon in a when-clause.

def Declerck1991.fpsSeaside : Time.ReichenbachFrame ℤ

"John will go to the seaside" — FPS: absolute future establishing a post-present domain.

Equations

• Declerck1991.fpsSeaside = { speechTime := 0, perspectiveTime := 0, referenceTime := 3, eventTime := 3 }

def Declerck1991.ppsWeatherGood : Time.ReichenbachFrame ℤ

"…if the weather is good" — PPS: present tense binding into the post-present domain, simultaneous with the pseudo-t₀.

Equations

• Declerck1991.ppsWeatherGood = Tense.shiftedFrame Declerck1991.fpsSeaside 3 3

theorem Declerck1991.fpsSeaside_absolute_future : fpsSeaside.isSimpleCase ∧ fpsSeaside.isFuture

The FPS matrix is an absolute future: P = S and P < R.

theorem Declerck1991.ppsWeatherGood_relative_present : ppsWeatherGood.isPresent

The PPS protasis is a relative present: R = P at the shifted perspective, even though the situation is post-present.

theorem Declerck1991.ppsWeatherGood_pseudo_t0 : ppsWeatherGood.perspectiveTime = fpsSeaside.eventTime ∧ ¬ppsWeatherGood.isSimpleCase

The PPS perspective is the pseudo-t₀ — the post-present domain anchor, not speech time.

Past perfect in before-clauses

The past perfect encodes an event anterior to a past reference point. The frames below use the orthodox Reichenbach convention (E < R for the perfect) — the convention DeclercianSchema.toFrame deliberately cannot express; see the perfect-vs-preterit section for the explicit divergence.

The future-perfect counterpart (Examples.futurePerfect) and the future-referring present in when-clauses (Examples.whenPresent, the PPS phenomenon above) are kept as examples only: frame-encoding the latter would conflate morphology with interpretation.

def Declerck1991.hadLeftBefore : Time.ReichenbachFrame ℤ

"I had left before he arrived" — past perfect, event anterior to a past reference point (orthodox convention: E < R).

Equations

• Declerck1991.hadLeftBefore = { speechTime := 0, perspectiveTime := 0, referenceTime := -3, eventTime := -5 }

def Declerck1991.beforeArrived : Time.ReichenbachFrame ℤ

"…before he arrived" — past time-sphere reference point.

Equations

• Declerck1991.beforeArrived = { speechTime := 0, perspectiveTime := 0, referenceTime := -3, eventTime := -3 }

theorem Declerck1991.hadLeftBefore_event_lt_arrival : hadLeftBefore.eventTime < beforeArrived.eventTime

Before-clause: leaving precedes arrival.

theorem Declerck1991.hadLeftBefore_isPerfect : hadLeftBefore.isPerfect

The past-perfect frame has E < R (perfect, orthodox convention).

Boundedness and unmarked temporal interpretation

Declerck's principle of unmarked temporal interpretation (his label, building on earlier work on temporal anaphora in discourse): in a sequence of clauses each establishing its own domain, (a) bounded + bounded → interpreted as sequential, in report order; (b) unbounded + unbounded → interpreted as simultaneous; (c) mixed → the bounded situation is included in the unbounded one.

Boundedness is sentence-level and distinct from telicity: Bill ran five miles is bounded but Bill was running five miles is unbounded, with the same telic VP. These are pragmatic defaults, not entailments.

inductive Declerck1991.TemporalArrangement : Type

The three default temporal arrangements of Declerck's principle of unmarked temporal interpretation.

• sequential : TemporalArrangement
• simultaneous : TemporalArrangement
• inclusion : TemporalArrangement

@[implicit_reducible]

instance Declerck1991.instDecidableEqTemporalArrangement : DecidableEq TemporalArrangement

Equations

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

def Declerck1991.instReprTemporalArrangement.repr : TemporalArrangement → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Declerck1991.instReprTemporalArrangement : Repr TemporalArrangement

Equations

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

def Declerck1991.putiDefault : Semantics.Aspect.SituationBoundedness → Semantics.Aspect.SituationBoundedness → TemporalArrangement

Declerck's unmarked-interpretation default for a pair of juxtaposed situations, by boundedness.

Equations

• Declerck1991.putiDefault Semantics.Aspect.SituationBoundedness.bounded Semantics.Aspect.SituationBoundedness.bounded = Declerck1991.TemporalArrangement.sequential
• Declerck1991.putiDefault Semantics.Aspect.SituationBoundedness.unbounded Semantics.Aspect.SituationBoundedness.unbounded = Declerck1991.TemporalArrangement.simultaneous
• Declerck1991.putiDefault x✝¹ x✝ = Declerck1991.TemporalArrangement.inclusion

def Declerck1991.TemporalArrangement.holdsAt : TemporalArrangement → Time.ReichenbachFrame ℤ → Time.ReichenbachFrame ℤ → Prop

An arrangement holding of two point-time frames. For point times, inclusion degenerates to coincidence of event times (genuine interval inclusion would need interval-valued frames).

Equations

• Declerck1991.TemporalArrangement.sequential.holdsAt x✝¹ x✝ = (x✝¹.eventTime < x✝.eventTime)
• Declerck1991.TemporalArrangement.simultaneous.holdsAt x✝¹ x✝ = (x✝¹.eventTime = x✝.eventTime)
• Declerck1991.TemporalArrangement.inclusion.holdsAt x✝¹ x✝ = (x✝¹.eventTime = x✝.eventTime)

def Declerck1991.arrivedFrame : Time.ReichenbachFrame ℤ

"He arrived." — bounded (achievement).

Equations

• Declerck1991.arrivedFrame = { speechTime := 0, perspectiveTime := 0, referenceTime := -5, eventTime := -5 }

def Declerck1991.satDownFrame : Time.ReichenbachFrame ℤ

"He sat down." — bounded (achievement), after arriving by default.

Equations

• Declerck1991.satDownFrame = { speechTime := 0, perspectiveTime := 0, referenceTime := -4, eventTime := -4 }

def Declerck1991.rainingFrame : Time.ReichenbachFrame ℤ

"It was raining." — unbounded (state/activity).

Equations

• Declerck1991.rainingFrame = { speechTime := 0, perspectiveTime := 0, referenceTime := -3, eventTime := -3 }

def Declerck1991.windBlowingFrame : Time.ReichenbachFrame ℤ

"The wind was blowing." — unbounded (activity), simultaneous with raining by default.

Equations

• Declerck1991.windBlowingFrame = { speechTime := 0, perspectiveTime := 0, referenceTime := -3, eventTime := -3 }

def Declerck1991.readingFrame : Time.ReichenbachFrame ℤ

"He was reading." — unbounded (activity).

Equations

• Declerck1991.readingFrame = { speechTime := 0, perspectiveTime := 0, referenceTime := -3, eventTime := -3 }

def Declerck1991.phoneRangFrame : Time.ReichenbachFrame ℤ

"The phone rang." — bounded (achievement), included in the reading interval by default.

Equations

• Declerck1991.phoneRangFrame = { speechTime := 0, perspectiveTime := 0, referenceTime := -3, eventTime := -3 }

theorem Declerck1991.arrived_satDown_puti : (putiDefault Semantics.Aspect.SituationBoundedness.bounded Semantics.Aspect.SituationBoundedness.bounded).holdsAt arrivedFrame satDownFrame

Bounded + bounded → sequential: the constructed frames instantiate the unmarked-interpretation default.

theorem Declerck1991.raining_windBlowing_puti : (putiDefault Semantics.Aspect.SituationBoundedness.unbounded Semantics.Aspect.SituationBoundedness.unbounded).holdsAt rainingFrame windBlowingFrame

Unbounded + unbounded → simultaneous.

theorem Declerck1991.phoneRang_reading_puti : (putiDefault Semantics.Aspect.SituationBoundedness.bounded Semantics.Aspect.SituationBoundedness.unbounded).holdsAt phoneRangFrame readingFrame

Mixed → inclusion (point-degenerate: coincidence).

Present perfect vs preterit: time-sphere, and two frame conventions

Declerck's distinctive claim: the present perfect and preterit differ in time-sphere membership, not in definiteness or current relevance (an implicature, for Declerck). Both can refer to the same objective event. The companion grammar's minimal pair (Examples.perfectOverslept): "I have overslept this morning" requires that the morning not be over; "I overslept this morning" does not.

Two Reichenbach encodings of the perfect coexist in this file:

• DeclercianSchema.toFrame (TS = TO_sit, so E = R always): perfect and preterit project to the same frame (preterit_presentPerfect_same_frame); the contrast lives in timeSphere/zoneOf.
• The orthodox convention below (R at the sphere anchor): the perfect has E < R = P, making the contrast frame-visible.

perfect_frame_conventions_diverge states the discrepancy explicitly: the orthodox perfect frame is unreachable from any Declercian schema.

def Declerck1991.perfectOversleptFrame : Time.ReichenbachFrame ℤ

"I have overslept this morning." — present perfect in the orthodox convention: E < R and R = P (pre-present, present orientation).

Equations

• Declerck1991.perfectOversleptFrame = { speechTime := 0, perspectiveTime := 0, referenceTime := 0, eventTime := -3 }

def Declerck1991.preteritOversleptFrame : Time.ReichenbachFrame ℤ

"I overslept this morning." — simple preterit: E = R < P.

Equations

• Declerck1991.preteritOversleptFrame = { speechTime := 0, perspectiveTime := 0, referenceTime := -3, eventTime := -3 }

theorem Declerck1991.oversleptFrames_eventTime_eq : perfectOversleptFrame.eventTime = preteritOversleptFrame.eventTime

Same event time — the difference is structural, not temporal.

theorem Declerck1991.perfectOversleptFrame_isPerfect_isPresent : perfectOversleptFrame.isPerfect ∧ perfectOversleptFrame.isPresent

The perfect frame is perfect (E < R) with present orientation (R = P).

theorem Declerck1991.preteritOversleptFrame_isPast_isPerfective : preteritOversleptFrame.isPast ∧ preteritOversleptFrame.isPerfective

The preterit frame is past (R < P) and perfective (E = R).

theorem Declerck1991.perfect_frame_conventions_diverge : (TOChain.presentPerfect 0 (-3)).toFrame ≠ perfectOversleptFrame ∧ ¬(TOChain.presentPerfect 0 (-3)).toFrame.isPerfect ∧ perfectOversleptFrame.isPerfect

The two perfect conventions diverge: Declerck's toFrame projection of the present perfect is not the orthodox perfect frame, and no Declercian projection can be isPerfect — while the orthodox frame is. This is the visible fault line between R-as-TO_sit (Declerck) and R-as-extended-now (the orthodox reading of the perfect).