[Zei12]: sequence of tense as upward Agree

[Zei12] analyzes Sequence of Tense (SOT) as syntactic concord, structurally parallel to Negative Concord. Subordinate past morphemes carry uninterpretable [uPAST]; they Agree upward with a c-commanding interpretable [iPAST]. The subordinate past morphology is semantically vacuous — it is Agree spell-out, not semantic past. The account builds on [Cho00]'s Agree, reversing its c-command direction.

Main declarations

• TenseHead — a tense head carrying a Finset Ordering comparison cell and an Interpretability.
• TenseHead.IsSemanticallyActive — only interpretable heads contribute to LF.
• UpwardAgree — the reverse-Agree configuration: the goal c-commands the probe.
• SOTAgreeConfig — one interpretable [iPAST] over a list of [uPAST] heads.
• TenseHead.toGramFeature — maps a tense head into the Minimalist GramFeature infrastructure (interpretable ↦ valued, uninterpretable ↦ unvalued).

Implementation notes

• The interpretable past is an abstract operator, not the matrix verb. In [Zei12] (§5.3) the [iPAST] sits on an abstract operator (Op_PAST, after von Stechow); all finite verbal morphology, the matrix verb included, is [uPAST]. SOTAgreeConfig simplifies by treating matrixT as the [iPAST] bearer and abstracting the matrix verb's own [uPAST].
• SOT crosses CP. [Zei12] (§5.3) holds SOT to be not clause-bounded — unlike Negative Concord it crosses a CP, because the embedding C itself carries [uT] and so participates in the phase edge.
• Embedded [uPAST] is modeled as pure simultaneity. zeijlstra_derives_simultaneous yields simultaneousFrame (R' = P' = matrix E). [Zei12] fn. 9 treats embedded [uPAST] as a relative non-future ("no later than") licensing both the simultaneous and a back-shifted reading (not forward); that refinement is not formalized here.
• zeijlstra_derives_shifted derives the back-shifted reading from an independent embedded [iPAST] — one source of back-shift, distinct from the fn. 9 [uPAST]-as-non-future route.
• Zeijlstra's parameter — whether embedded T may carry [uPAST] — is the substrate SOTParameter; that SOT languages (relative) license the simultaneous reading is Tense.sot_simultaneous_available.

Todo

• Temporal de re, counterfactual tense, and relative-clause tense are not addressed.

Tense feature interpretability

structure Zeijlstra2012.TenseHead : Type

A tense head: a Finset Ordering comparison cell together with an Interpretability status. Following [Zei12], [iPAST] (.interpretable) contributes past semantics; [uPAST] (.uninterpretable) is checked by Agree and is semantically vacuous.

• tense : Finset Ordering

  The tense value (past/present/future) as a Finset Ordering comparison cell.

• status : Minimalist.Interpretability

  Whether this tense feature is interpretable or uninterpretable.

def Zeijlstra2012.instDecidableEqTenseHead.decEq (x✝ x✝¹ : TenseHead) : Decidable (x✝ = x✝¹)

Equations

• Zeijlstra2012.instDecidableEqTenseHead.decEq { tense := a, status := a_1 } { tense := b, status := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Zeijlstra2012.instDecidableEqTenseHead : DecidableEq TenseHead

Equations

• Zeijlstra2012.instDecidableEqTenseHead = Zeijlstra2012.instDecidableEqTenseHead.decEq

def Zeijlstra2012.TenseHead.IsSemanticallyActive (th : TenseHead) : Prop

A tense head is semantically active iff its feature is interpretable.

Equations

• th.IsSemanticallyActive = (th.status = Minimalist.Interpretability.interpretable)

@[implicit_reducible]

instance Zeijlstra2012.instDecidableIsSemanticallyActive (th : TenseHead) : Decidable th.IsSemanticallyActive

Equations

• Zeijlstra2012.instDecidableIsSemanticallyActive th = Zeijlstra2012.instDecidableIsSemanticallyActive._aux_1 th

Upward Agree

structure Zeijlstra2012.UpwardAgree : Type

Zeijlstra's upward Agree: the goal c-commands the probe, reversing standard [Cho00] Agree. The uninterpretable [uF] probe sits low and is valued by a c-commanding interpretable [iF] goal.

• probe : TenseHead

  The embedded T with [uT] (probe).

• goal : TenseHead

  The matrix T with [iT] (goal).

• probe_uninterpretable : self.probe.status = Minimalist.Interpretability.uninterpretable

  The probe carries an uninterpretable feature.

• goal_interpretable : self.goal.status = Minimalist.Interpretability.interpretable

  The goal carries an interpretable feature.

• tense_match : self.probe.tense = self.goal.tense

  The tense values match.

theorem Zeijlstra2012.upwardAgree_probe_vacuous (ua : UpwardAgree) : ¬ua.probe.IsSemanticallyActive

Upward Agree makes the probe semantically vacuous: its feature is uninterpretable, so it does not contribute to LF.

theorem Zeijlstra2012.upwardAgree_goal_active (ua : UpwardAgree) : ua.goal.IsSemanticallyActive

The goal's tense is semantically active.

SOT Agree configuration

structure Zeijlstra2012.SOTAgreeConfig : Type

An SOT configuration: one interpretable [iPAST] head over a list of uninterpretable [uPAST] heads ([Zei12], ex. 22–23) — the [iF] > [uF] (> [uF]) upward-Agree schema. See the module notes: the interpretable head is really an abstract operator, and matrix verbal morphology is itself [uPAST].

• matrixT : TenseHead

  Matrix head bearing [iPAST].

• embeddedTs : List TenseHead

  Embedded heads bearing [uPAST].

• matrix_is_interpretable : self.matrixT.status = Minimalist.Interpretability.interpretable

  The matrix head is interpretable.

• embedded_all_uninterpretable (t : TenseHead) : t ∈ self.embeddedTs → t.status = Minimalist.Interpretability.uninterpretable

  All embedded heads are uninterpretable.

theorem Zeijlstra2012.sotConfig_only_matrix_active (cfg : SOTAgreeConfig) : cfg.matrixT.IsSemanticallyActive ∧ ∀ t ∈ cfg.embeddedTs, ¬t.IsSemanticallyActive

In an SOT configuration only the matrix head contributes past semantics; all embedded past morphology is vacuous concord.

Derivation theorems

theorem Zeijlstra2012.zeijlstra_derives_simultaneous {Time : Type u_1} (matrixFrame : _root_.Time.ReichenbachFrame Time) (embeddedE : Time) (embeddedT : TenseHead) (h_u : embeddedT.status = Minimalist.Interpretability.uninterpretable) : ¬embeddedT.IsSemanticallyActive ∧ (Tense.simultaneousFrame matrixFrame embeddedE).isPresent

The simultaneous reading: embedded [uPAST] is vacuous, so the embedded clause has no independent past — it is interpreted at the matrix event time, giving simultaneousFrame (R' = P' = matrix E). See the module notes on the fn. 9 non-future refinement.

theorem Zeijlstra2012.zeijlstra_derives_shifted {Time : Type u_1} [LinearOrder Time] (matrixFrame : _root_.Time.ReichenbachFrame Time) (embeddedR embeddedE : Time) (embeddedT : TenseHead) (h_i : embeddedT.status = Minimalist.Interpretability.interpretable) (h_shifted : embeddedR < matrixFrame.eventTime) : embeddedT.IsSemanticallyActive ∧ (Tense.shiftedFrame matrixFrame embeddedR embeddedE).isPast

The back-shifted reading: when embedded T bears an independent [iPAST] (no Agree), it contributes genuine past semantics, giving shiftedFrame (R' < P').

theorem Zeijlstra2012.zeijlstra_upward_direction (ua : UpwardAgree) : ua.goal.IsSemanticallyActive ∧ ¬ua.probe.IsSemanticallyActive

Upward Agree fixes the directionality: the goal [iPAST] is active and the probe [uPAST] is vacuous.

Mapping to the Minimalist Agree features

def Zeijlstra2012.TenseHead.toGramFeature (th : TenseHead) : Minimalist.GramFeature

Map a TenseHead into the Minimalist GramFeature infrastructure: interpretable ↦ valued, uninterpretable ↦ unvalued. In the SOT domain the ±interpretable and ±valued axes coincide ([Cho95]); they are orthogonal in general (see Minimalist.Features).

Equations

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

theorem Zeijlstra2012.zeijlstra_bridge_interpretable (th : TenseHead) (h : th.status = Minimalist.Interpretability.interpretable) : th.toGramFeature = Minimalist.GramFeature.valued (Minimalist.FeatureVal.tense true)

Interpretable tense heads map to valued features.

theorem Zeijlstra2012.zeijlstra_bridge_uninterpretable (th : TenseHead) (h : th.status = Minimalist.Interpretability.uninterpretable) : th.toGramFeature = Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.tense true)

Uninterpretable tense heads map to unvalued features.