@cite{zeijlstra-2012}: SOT as Upward Agree

@cite{chomsky-2000} @cite{zeijlstra-2012}

Zeijlstra's theory: Sequence of Tense is syntactic concord, structurally parallel to Negative Concord. Subordinate past morphemes carry uninterpretable [uPAST]; they Agree upward with matrix [iPAST]. The subordinate verb's past morphology is semantically vacuous -- it is Agree spell-out, not semantic past.

Core Mechanisms

1. Tense feature interpretability: [iPAST] contributes past semantics; [uPAST] is checked by Agree, semantically vacuous
2. Upward Agree: the goal c-commands the probe (reverse of standard @cite{chomsky-2000} Agree where probe c-commands goal)
3. SOT as concord: SOT languages allow [uT] on embedded T; non-SOT languages do not, so embedded tense is always interpretable
4. Parametric variation: whether a language has SOT = whether it allows uninterpretable tense features on embedded T heads

Derivation Theorems

• Simultaneous reading: [uPAST] is semantically vacuous, so the embedded clause is interpreted at matrix event time
• Shifted reading: embedded T has [iPAST] (independent tense, no Agree)
• SOT parameter: SOT languages allow [uT]; non-SOT do not
• SOT is concord: structural parallel with Negative Concord

Limitations

• Temporal de re: not addressed (syntactic, not semantic mechanism)
• Counterfactual tense: not directly handled
• Relative clause tense: would require extending Agree domain

inductive Minimalism.Tense.Zeijlstra.TenseFeatureStatus : Type

Tense feature interpretability. Following @cite{zeijlstra-2012}:

• Interpretable [iPAST]: contributes past semantics
• Uninterpretable [uPAST]: checked by Agree, semantically vacuous

• interpretable : TenseFeatureStatus

  [iT] -- semantically active

• uninterpretable : TenseFeatureStatus

  [uT] -- checked by Agree, semantically vacuous

instance Minimalism.Tense.Zeijlstra.instDecidableEqTenseFeatureStatus : DecidableEq TenseFeatureStatus

Equations

• Minimalism.Tense.Zeijlstra.instDecidableEqTenseFeatureStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Minimalism.Tense.Zeijlstra.instReprTenseFeatureStatus : Repr TenseFeatureStatus

Equations

• Minimalism.Tense.Zeijlstra.instReprTenseFeatureStatus = { reprPrec := Minimalism.Tense.Zeijlstra.instReprTenseFeatureStatus.repr }

def Minimalism.Tense.Zeijlstra.instReprTenseFeatureStatus.repr : TenseFeatureStatus → ℕ → Std.Format

Equations

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

instance Minimalism.Tense.Zeijlstra.instBEqTenseFeatureStatus : BEq TenseFeatureStatus

Equations

• Minimalism.Tense.Zeijlstra.instBEqTenseFeatureStatus = { beq := Minimalism.Tense.Zeijlstra.instBEqTenseFeatureStatus.beq }

def Minimalism.Tense.Zeijlstra.instBEqTenseFeatureStatus.beq : TenseFeatureStatus → TenseFeatureStatus → Bool

Equations

• Minimalism.Tense.Zeijlstra.instBEqTenseFeatureStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Minimalism.Tense.Zeijlstra.TenseHead : Type

A tense head with its feature specification.

• tense : Core.Tense.GramTense

  The tense value (past/present/future)

• status : TenseFeatureStatus

  Whether this tense feature is interpretable or uninterpretable

instance Minimalism.Tense.Zeijlstra.instDecidableEqTenseHead : DecidableEq TenseHead

Equations

• Minimalism.Tense.Zeijlstra.instDecidableEqTenseHead = Minimalism.Tense.Zeijlstra.instDecidableEqTenseHead.decEq

def Minimalism.Tense.Zeijlstra.instDecidableEqTenseHead.decEq (x✝ x✝¹ : TenseHead) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalism.Tense.Zeijlstra.instReprTenseHead.repr : TenseHead → ℕ → Std.Format

Equations

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

instance Minimalism.Tense.Zeijlstra.instReprTenseHead : Repr TenseHead

Equations

• Minimalism.Tense.Zeijlstra.instReprTenseHead = { reprPrec := Minimalism.Tense.Zeijlstra.instReprTenseHead.repr }

def Minimalism.Tense.Zeijlstra.instBEqTenseHead.beq : TenseHead → TenseHead → Bool

Equations

• Minimalism.Tense.Zeijlstra.instBEqTenseHead.beq { tense := a, status := a_1 } { tense := b, status := b_1 } = (a == b && a_1 == b_1)
• Minimalism.Tense.Zeijlstra.instBEqTenseHead.beq x✝¹ x✝ = false

instance Minimalism.Tense.Zeijlstra.instBEqTenseHead : BEq TenseHead

Equations

• Minimalism.Tense.Zeijlstra.instBEqTenseHead = { beq := Minimalism.Tense.Zeijlstra.instBEqTenseHead.beq }

def Minimalism.Tense.Zeijlstra.TenseHead.isSemanticallyActive (th : TenseHead) : Bool

Is a tense head semantically active? Only interpretable features contribute to meaning.

Equations

• th.isSemanticallyActive = (th.status == Minimalism.Tense.Zeijlstra.TenseFeatureStatus.interpretable)

structure Minimalism.Tense.Zeijlstra.UpwardAgree : Type

Zeijlstra's upward Agree: the goal c-commands the probe. Standard Agree: probe c-commands goal. Zeijlstra: reverse -- [uF] is valued by a c-commanding [iF].

This is the key innovation: the c-command direction is reversed. The uninterpretable feature (probe) sits low in the structure and is valued by a c-commanding interpretable feature (goal).

• probe : TenseHead

  The embedded T with [uT] (probe)

• goal : TenseHead

  The matrix T with [iT] (goal)

• probe_uninterpretable : self.probe.status = TenseFeatureStatus.uninterpretable

  The probe carries an uninterpretable feature

• goal_interpretable : self.goal.status = TenseFeatureStatus.interpretable

  The goal carries an interpretable feature

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

  The tense values match (both past, both present, etc.)

def Minimalism.Tense.Zeijlstra.instReprUpwardAgree.repr : UpwardAgree → ℕ → Std.Format

Equations

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

instance Minimalism.Tense.Zeijlstra.instReprUpwardAgree : Repr UpwardAgree

Equations

• Minimalism.Tense.Zeijlstra.instReprUpwardAgree = { reprPrec := Minimalism.Tense.Zeijlstra.instReprUpwardAgree.repr }

theorem Minimalism.Tense.Zeijlstra.upwardAgree_probe_vacuous (ua : UpwardAgree) : ua.probe.isSemanticallyActive = false

Upward Agree makes the probe semantically vacuous: since the probe's feature is uninterpretable, it does not contribute to LF interpretation.

theorem Minimalism.Tense.Zeijlstra.upwardAgree_goal_active (ua : UpwardAgree) : ua.goal.isSemanticallyActive = true

The goal's tense IS semantically active.

structure Minimalism.Tense.Zeijlstra.SOTAgreeConfig : Type

SOT configuration: [iPAST] > [uPAST] > [uPAST] (@cite{zeijlstra-2012}, ex. 22--23).

In an SOT language, the matrix T carries [iPAST] (the only semantically active past), and all embedded T heads carry [uPAST] (semantically vacuous, valued by upward Agree with [iPAST]).

• matrixT : TenseHead

  Matrix T head with [iPAST]

• embeddedTs : List TenseHead

  Embedded T heads with [uPAST]

• matrix_is_interpretable : self.matrixT.status = TenseFeatureStatus.interpretable

  Matrix T is interpretable

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

  All embedded T heads are uninterpretable

instance Minimalism.Tense.Zeijlstra.instReprSOTAgreeConfig : Repr SOTAgreeConfig

Equations

• Minimalism.Tense.Zeijlstra.instReprSOTAgreeConfig = { reprPrec := Minimalism.Tense.Zeijlstra.instReprSOTAgreeConfig.repr }

def Minimalism.Tense.Zeijlstra.instReprSOTAgreeConfig.repr : SOTAgreeConfig → ℕ → Std.Format

Equations

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

theorem Minimalism.Tense.Zeijlstra.sotConfig_only_matrix_active (cfg : SOTAgreeConfig) : cfg.matrixT.isSemanticallyActive = true ∧ ∀ t ∈ cfg.embeddedTs, t.isSemanticallyActive = false

In an SOT configuration, only the matrix T contributes past semantics. All embedded past morphology is concord (semantically vacuous).

def Minimalism.Tense.Zeijlstra.allowsUninterpretableTense (param : Core.Tense.SOTParameter) : Bool

Whether a language allows uninterpretable tense on embedded T. SOT languages (English): yes → simultaneous reading available. Non-SOT languages (Japanese): no → all tense is interpretable.

Equations

• Minimalism.Tense.Zeijlstra.allowsUninterpretableTense Core.Tense.SOTParameter.relative = true
• Minimalism.Tense.Zeijlstra.allowsUninterpretableTense Core.Tense.SOTParameter.absolute = false

theorem Minimalism.Tense.Zeijlstra.sot_allows_uT : allowsUninterpretableTense Core.Tense.SOTParameter.relative = true

SOT languages allow uninterpretable tense.

theorem Minimalism.Tense.Zeijlstra.nonSOT_no_uT : allowsUninterpretableTense Core.Tense.SOTParameter.absolute = false

Non-SOT languages do not allow uninterpretable tense.

theorem Minimalism.Tense.Zeijlstra.zeijlstra_derives_simultaneous {Time : Type u_1} (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (embeddedE : Time) (embeddedT : TenseHead) (h_u : embeddedT.status = TenseFeatureStatus.uninterpretable) : embeddedT.isSemanticallyActive = false ∧ (Semantics.Tense.simultaneousFrame matrixFrame embeddedE).isPresent

Zeijlstra derives the simultaneous reading: [uPAST] is semantically vacuous → the embedded clause has no independent past semantics → it is interpreted at the matrix event time → R' = P' (simultaneous).

Concretely: the embedded frame with a vacuous [uPAST] has R' = P' = matrix E, which is simultaneousFrame.

theorem Minimalism.Tense.Zeijlstra.zeijlstra_derives_shifted {Time : Type u_1} [LinearOrder Time] (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (embeddedR embeddedE : Time) (embeddedT : TenseHead) (h_i : embeddedT.status = TenseFeatureStatus.interpretable) (h_past : embeddedT.tense = Core.Tense.GramTense.past) (h_shifted : embeddedR < matrixFrame.eventTime) : embeddedT.isSemanticallyActive = true ∧ (Semantics.Tense.shiftedFrame matrixFrame embeddedR embeddedE).isPast

Zeijlstra derives the shifted reading: When embedded T has [iPAST] (independent tense, no Agree), it contributes genuine past semantics → R' < P' (shifted).

theorem Minimalism.Tense.Zeijlstra.zeijlstra_SOT_parametric : allowsUninterpretableTense Core.Tense.SOTParameter.relative = true ∧ allowsUninterpretableTense Core.Tense.SOTParameter.absolute = false

SOT is parametric: SOT languages allow [uT] on embedded T; non-SOT languages do not. This bridges Zeijlstra's feature-based account to the SOTParameter type.

theorem Minimalism.Tense.Zeijlstra.zeijlstra_upward_direction (ua : UpwardAgree) : ua.goal.isSemanticallyActive = true ∧ ua.probe.isSemanticallyActive = false

Upward Agree explains the directionality: embedded tense depends on matrix (not reverse) because [uPAST] must be c-commanded by [iPAST]. The c-command relation is asymmetric: matrix c-commands embedded.

structure Minimalism.Tense.Zeijlstra.ConcordParallel : Type

The structural parallel between SOT and Negative Concord.

Just as Negative Concord languages have [uNEG] on n-words that Agree with [iNEG] on the sentential negation, SOT languages have [uPAST] on embedded T heads that Agree with [iPAST] on matrix T.

Both involve:

• One interpretable feature (semantically active)
• Multiple uninterpretable copies (concord, semantically vacuous)
• Upward Agree as the licensing mechanism

• iFeatureBearer : String

  The interpretable feature bearer

• uFeatureBearers : List String

  The uninterpretable concord items

• domain : String

  The domain

instance Minimalism.Tense.Zeijlstra.instReprConcordParallel : Repr ConcordParallel

Equations

• Minimalism.Tense.Zeijlstra.instReprConcordParallel = { reprPrec := Minimalism.Tense.Zeijlstra.instReprConcordParallel.repr }

def Minimalism.Tense.Zeijlstra.instReprConcordParallel.repr : ConcordParallel → ℕ → Std.Format

Equations

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

def Minimalism.Tense.Zeijlstra.sotAsConcord : ConcordParallel

SOT as tense concord.

Equations

• Minimalism.Tense.Zeijlstra.sotAsConcord = { iFeatureBearer := "matrix T [iPAST]", uFeatureBearers := ["embedded T [uPAST]"], domain := "tense" }

def Minimalism.Tense.Zeijlstra.negativeConcord : ConcordParallel

Negative Concord parallel.

Equations

• Minimalism.Tense.Zeijlstra.negativeConcord = { iFeatureBearer := "sentential negation [iNEG]", uFeatureBearers := ["n-word [uNEG]"], domain := "negation" }

def Minimalism.Tense.Zeijlstra.TenseHead.toGramFeature (th : TenseHead) : GramFeature

Map a TenseHead to the Minimalism Agree infrastructure. An interpretable [iPAST] maps to GramFeature.valued (.tense true); an uninterpretable [uPAST] maps to GramFeature.unvalued (.tense true).

Equations

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

theorem Minimalism.Tense.Zeijlstra.zeijlstra_bridge_interpretable (th : TenseHead) (h : th.status = TenseFeatureStatus.interpretable) : th.toGramFeature = GramFeature.valued (FeatureVal.tense true)

Interpretable tense heads map to valued features.

theorem Minimalism.Tense.Zeijlstra.zeijlstra_bridge_uninterpretable (th : TenseHead) (h : th.status = TenseFeatureStatus.uninterpretable) : th.toGramFeature = GramFeature.unvalued (FeatureVal.tense true)

Uninterpretable tense heads map to unvalued features.

theorem Minimalism.Tense.Zeijlstra.zeijlstra_simultaneousFrame {Time : Type u_1} (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (embeddedE : Time) : (Semantics.Tense.simultaneousFrame matrixFrame embeddedE).referenceTime = (Semantics.Tense.simultaneousFrame matrixFrame embeddedE).perspectiveTime

Agree-valued [uPAST] produces the same Reichenbach frame as simultaneousFrame: the embedded tense contributes no independent temporal ordering, so R' = P' = matrix E.

Size-Sensitive SOT

@cite{egressy-2026} shows that Hungarian is a partial SOT language: the simultaneous reading is available in TP complements but blocked in CP complements. This follows from PIC blocking upward Agree for [uPAST] across the CP phase boundary.

The key insight: Zeijlstra's UpwardAgree succeeds only when no phase boundary intervenes between probe ([uPAST] on embedded T) and goal ([iPAST] on matrix T). CP is a phase (Phase.lean), so [uPAST] inside a CP complement cannot reach matrix [iPAST].

def Minimalism.Tense.Zeijlstra.availableReadingsBySize (cs : ComplementSize) : List Semantics.Tense.EmbeddedTenseReading

Available embedded tense readings given complement size.

In a size-sensitive SOT language:

• Small complements (< CP): both shifted and simultaneous
• Large complements (≥ CP): shifted only (simultaneous blocked)

Equations

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

theorem Minimalism.Tense.Zeijlstra.tp_both_readings : availableReadingsBySize ComplementSize.tP = [Semantics.Tense.EmbeddedTenseReading.shifted, Semantics.Tense.EmbeddedTenseReading.simultaneous]

TP complements yield both readings.

theorem Minimalism.Tense.Zeijlstra.cp_shifted_only : availableReadingsBySize ComplementSize.cP = [Semantics.Tense.EmbeddedTenseReading.shifted]

CP complements yield only the shifted reading.

theorem Minimalism.Tense.Zeijlstra.simultaneous_available_in_tp : Semantics.Tense.EmbeddedTenseReading.simultaneous ∈ availableReadingsBySize ComplementSize.tP

The simultaneous reading is available in TP complements.

theorem Minimalism.Tense.Zeijlstra.simultaneous_blocked_in_cp : Semantics.Tense.EmbeddedTenseReading.simultaneous ∉ availableReadingsBySize ComplementSize.cP

The simultaneous reading is blocked in CP complements.

The Williams Cycle

The Williams Cycle is the diachronic process by which formerly transparent clause boundaries become opaque. A language at stage N of the cycle has some complement types that are transparent to tense Agree and others that are opaque.

• Stage 0 (non-SOT, e.g., Japanese): all boundaries opaque
• Stage 1 (partial SOT, e.g., Hungarian): CP opaque, TP transparent
• Stage 2 (full SOT, e.g., English): all boundaries transparent

@cite{egressy-2026} argues Hungarian is at Stage 1: mid-cycle, with the CP boundary having become opaque while TP remains transparent.

inductive Minimalism.Tense.Zeijlstra.WilliamsCycleStage : Type

Williams Cycle stage for SOT.

Classifies a language by how many complement boundaries are transparent to upward tense Agree.

• noSOT : WilliamsCycleStage

  No SOT: all boundaries opaque (Japanese)

• partialSOT : WilliamsCycleStage

  Partial SOT: CP opaque, TP transparent (Hungarian)

• fullSOT : WilliamsCycleStage

  Full SOT: all boundaries transparent (English)

instance Minimalism.Tense.Zeijlstra.instDecidableEqWilliamsCycleStage : DecidableEq WilliamsCycleStage

Equations

• Minimalism.Tense.Zeijlstra.instDecidableEqWilliamsCycleStage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalism.Tense.Zeijlstra.instReprWilliamsCycleStage.repr : WilliamsCycleStage → ℕ → Std.Format

Equations

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

instance Minimalism.Tense.Zeijlstra.instReprWilliamsCycleStage : Repr WilliamsCycleStage

Equations

• Minimalism.Tense.Zeijlstra.instReprWilliamsCycleStage = { reprPrec := Minimalism.Tense.Zeijlstra.instReprWilliamsCycleStage.repr }

instance Minimalism.Tense.Zeijlstra.instBEqWilliamsCycleStage : BEq WilliamsCycleStage

Equations

• Minimalism.Tense.Zeijlstra.instBEqWilliamsCycleStage = { beq := Minimalism.Tense.Zeijlstra.instBEqWilliamsCycleStage.beq }

def Minimalism.Tense.Zeijlstra.instBEqWilliamsCycleStage.beq : WilliamsCycleStage → WilliamsCycleStage → Bool

Equations

• Minimalism.Tense.Zeijlstra.instBEqWilliamsCycleStage.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Minimalism.Tense.Zeijlstra.readingsByStage (stage : WilliamsCycleStage) (cs : ComplementSize) : List Semantics.Tense.EmbeddedTenseReading

Map Williams Cycle stage to available readings by complement size.

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.Tense.Zeijlstra.readingsByStage Minimalism.Tense.Zeijlstra.WilliamsCycleStage.noSOT cs = [Semantics.Tense.EmbeddedTenseReading.shifted]
• Minimalism.Tense.Zeijlstra.readingsByStage Minimalism.Tense.Zeijlstra.WilliamsCycleStage.partialSOT cs = Minimalism.Tense.Zeijlstra.availableReadingsBySize cs

theorem Minimalism.Tense.Zeijlstra.fullSOT_both_readings (cs : ComplementSize) : readingsByStage WilliamsCycleStage.fullSOT cs = [Semantics.Tense.EmbeddedTenseReading.shifted, Semantics.Tense.EmbeddedTenseReading.simultaneous]

Full-SOT languages get both readings regardless of complement size.

theorem Minimalism.Tense.Zeijlstra.noSOT_shifted_only (cs : ComplementSize) : readingsByStage WilliamsCycleStage.noSOT cs = [Semantics.Tense.EmbeddedTenseReading.shifted]

Non-SOT languages get only shifted regardless of complement size.

theorem Minimalism.Tense.Zeijlstra.partialSOT_size_sensitive : readingsByStage WilliamsCycleStage.partialSOT ComplementSize.tP = [Semantics.Tense.EmbeddedTenseReading.shifted, Semantics.Tense.EmbeddedTenseReading.simultaneous] ∧ readingsByStage WilliamsCycleStage.partialSOT ComplementSize.cP = [Semantics.Tense.EmbeddedTenseReading.shifted]

Partial-SOT languages show size sensitivity.

theorem Minimalism.Tense.Zeijlstra.williams_bridges_sotparam : allowsUninterpretableTense Core.Tense.SOTParameter.relative = true ∧ allowsUninterpretableTense Core.Tense.SOTParameter.absolute = false

Bridge to SOTParameter: full SOT =.relative, no SOT =.absolute. Partial SOT has no SOTParameter equivalent — it is genuinely a third option that the binary parameter cannot express.

def Minimalism.Tense.Zeijlstra.Zeijlstra : Semantics.Tense.TenseTheory

@cite{zeijlstra-2012} identity card, extended with @cite{egressy-2026} size-sensitive SOT prediction.

Equations

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