@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

structure Minimalist.Tense.AgreeSOT.TenseHead : Type

A tense head with its feature specification.

Uses the unified Interpretability type from Features.lean rather than a local reinvention. Following @cite{zeijlstra-2012}:

• .interpretable [iPAST]: contributes past semantics
• .uninterpretable [uPAST]: checked by Agree, semantically vacuous

• tense : Core.Time.Tense.GramTense

  The tense value (past/present/future)

• status : Interpretability

  Whether this tense feature is interpretable or uninterpretable

@[implicit_reducible]

instance Minimalist.Tense.AgreeSOT.instDecidableEqTenseHead : DecidableEq TenseHead

Equations

• Minimalist.Tense.AgreeSOT.instDecidableEqTenseHead = Minimalist.Tense.AgreeSOT.instDecidableEqTenseHead.decEq

def Minimalist.Tense.AgreeSOT.instDecidableEqTenseHead.decEq (x✝ x✝¹ : TenseHead) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalist.Tense.AgreeSOT.instReprTenseHead.repr : TenseHead → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.Tense.AgreeSOT.instReprTenseHead : Repr TenseHead

Equations

• Minimalist.Tense.AgreeSOT.instReprTenseHead = { reprPrec := Minimalist.Tense.AgreeSOT.instReprTenseHead.repr }

def Minimalist.Tense.AgreeSOT.TenseHead.isSemanticallyActive (th : TenseHead) : Bool

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

Equations

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

structure Minimalist.Tense.AgreeSOT.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 = Interpretability.uninterpretable

  The probe carries an uninterpretable feature

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

  The goal carries an interpretable feature

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

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

@[implicit_reducible]

instance Minimalist.Tense.AgreeSOT.instReprUpwardAgree : Repr UpwardAgree

Equations

• Minimalist.Tense.AgreeSOT.instReprUpwardAgree = { reprPrec := Minimalist.Tense.AgreeSOT.instReprUpwardAgree.repr }

def Minimalist.Tense.AgreeSOT.instReprUpwardAgree.repr : UpwardAgree → ℕ → Std.Format

Equations

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

theorem Minimalist.Tense.AgreeSOT.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 Minimalist.Tense.AgreeSOT.upwardAgree_goal_active (ua : UpwardAgree) : ua.goal.isSemanticallyActive = true

The goal's tense IS semantically active.

structure Minimalist.Tense.AgreeSOT.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 = Interpretability.interpretable

  Matrix T is interpretable

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

  All embedded T heads are uninterpretable

def Minimalist.Tense.AgreeSOT.instReprSOTAgreeConfig.repr : SOTAgreeConfig → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.Tense.AgreeSOT.instReprSOTAgreeConfig : Repr SOTAgreeConfig

Equations

• Minimalist.Tense.AgreeSOT.instReprSOTAgreeConfig = { reprPrec := Minimalist.Tense.AgreeSOT.instReprSOTAgreeConfig.repr }

theorem Minimalist.Tense.AgreeSOT.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 Minimalist.Tense.AgreeSOT.allowsUninterpretableTense (param : Core.Time.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

• Minimalist.Tense.AgreeSOT.allowsUninterpretableTense Core.Time.Tense.SOTParameter.relative = true
• Minimalist.Tense.AgreeSOT.allowsUninterpretableTense Core.Time.Tense.SOTParameter.absolute = false

theorem Minimalist.Tense.AgreeSOT.sot_allows_uT : allowsUninterpretableTense Core.Time.Tense.SOTParameter.relative = true

SOT languages allow uninterpretable tense.

theorem Minimalist.Tense.AgreeSOT.nonSOT_no_uT : allowsUninterpretableTense Core.Time.Tense.SOTParameter.absolute = false

Non-SOT languages do not allow uninterpretable tense.

theorem Minimalist.Tense.AgreeSOT.zeijlstra_derives_simultaneous {Time : Type u_1} (matrixFrame : Core.Time.Reichenbach.ReichenbachFrame Time) (embeddedE : Time) (embeddedT : TenseHead) (h_u : embeddedT.status = Interpretability.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 Minimalist.Tense.AgreeSOT.zeijlstra_derives_shifted {Time : Type u_1} [LinearOrder Time] (matrixFrame : Core.Time.Reichenbach.ReichenbachFrame Time) (embeddedR embeddedE : Time) (embeddedT : TenseHead) (h_i : embeddedT.status = Interpretability.interpretable) (h_past : embeddedT.tense = Core.Time.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 Minimalist.Tense.AgreeSOT.zeijlstra_SOT_parametric : allowsUninterpretableTense Core.Time.Tense.SOTParameter.relative = true ∧ allowsUninterpretableTense Core.Time.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 Minimalist.Tense.AgreeSOT.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 Minimalist.Tense.AgreeSOT.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

def Minimalist.Tense.AgreeSOT.instReprConcordParallel.repr : ConcordParallel → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.Tense.AgreeSOT.instReprConcordParallel : Repr ConcordParallel

Equations

• Minimalist.Tense.AgreeSOT.instReprConcordParallel = { reprPrec := Minimalist.Tense.AgreeSOT.instReprConcordParallel.repr }

def Minimalist.Tense.AgreeSOT.sotAsConcord : ConcordParallel

SOT as tense concord.

Equations

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

def Minimalist.Tense.AgreeSOT.negativeConcord : ConcordParallel

Negative Concord parallel.

Equations

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

def Minimalist.Tense.AgreeSOT.TenseHead.toGramFeature (th : TenseHead) : GramFeature

Map a TenseHead to the Minimalism Agree infrastructure.

In the SOT domain, the ±Interpretable and ±Valued axes coincide:

• [iPAST] is both interpretable AND valued (contributes semantics)
• [uPAST] is both uninterpretable AND unvalued (probe, needs Agree)

This is the typical pairing (@cite{chomsky-1995} Ch 4 §4.5), but the two distinctions are in principle orthogonal — see Features.lean for the general case.

Equations

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

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

Interpretable tense heads map to valued features.

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

Uninterpretable tense heads map to unvalued features.

theorem Minimalist.Tense.AgreeSOT.zeijlstra_simultaneousFrame {Time : Type u_1} (matrixFrame : Core.Time.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 Minimalist.Tense.AgreeSOT.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 Minimalist.Tense.AgreeSOT.tp_both_readings : availableReadingsBySize ComplementSize.tP = [Semantics.Tense.EmbeddedTenseReading.shifted, Semantics.Tense.EmbeddedTenseReading.simultaneous]

TP complements yield both readings.

theorem Minimalist.Tense.AgreeSOT.cp_shifted_only : availableReadingsBySize ComplementSize.cP = [Semantics.Tense.EmbeddedTenseReading.shifted]

CP complements yield only the shifted reading.

theorem Minimalist.Tense.AgreeSOT.simultaneous_available_in_tp : Semantics.Tense.EmbeddedTenseReading.simultaneous ∈ availableReadingsBySize ComplementSize.tP

The simultaneous reading is available in TP complements.

theorem Minimalist.Tense.AgreeSOT.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 Minimalist.Tense.AgreeSOT.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)

@[implicit_reducible]

instance Minimalist.Tense.AgreeSOT.instDecidableEqWilliamsCycleStage : DecidableEq WilliamsCycleStage

Equations

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

def Minimalist.Tense.AgreeSOT.instReprWilliamsCycleStage.repr : WilliamsCycleStage → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.Tense.AgreeSOT.instReprWilliamsCycleStage : Repr WilliamsCycleStage

Equations

• Minimalist.Tense.AgreeSOT.instReprWilliamsCycleStage = { reprPrec := Minimalist.Tense.AgreeSOT.instReprWilliamsCycleStage.repr }

def Minimalist.Tense.AgreeSOT.readingsByStage (stage : WilliamsCycleStage) (cs : ComplementSize) : List Semantics.Tense.EmbeddedTenseReading

Map Williams Cycle stage to available readings by complement size.

Equations

• Minimalist.Tense.AgreeSOT.readingsByStage Minimalist.Tense.AgreeSOT.WilliamsCycleStage.noSOT cs = [Semantics.Tense.EmbeddedTenseReading.shifted]
• Minimalist.Tense.AgreeSOT.readingsByStage Minimalist.Tense.AgreeSOT.WilliamsCycleStage.partialSOT cs = Minimalist.Tense.AgreeSOT.availableReadingsBySize cs
• Minimalist.Tense.AgreeSOT.readingsByStage Minimalist.Tense.AgreeSOT.WilliamsCycleStage.fullSOT cs = [Semantics.Tense.EmbeddedTenseReading.shifted, Semantics.Tense.EmbeddedTenseReading.simultaneous]

theorem Minimalist.Tense.AgreeSOT.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 Minimalist.Tense.AgreeSOT.noSOT_shifted_only (cs : ComplementSize) : readingsByStage WilliamsCycleStage.noSOT cs = [Semantics.Tense.EmbeddedTenseReading.shifted]

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

theorem Minimalist.Tense.AgreeSOT.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 Minimalist.Tense.AgreeSOT.williams_bridges_sotparam : allowsUninterpretableTense Core.Time.Tense.SOTParameter.relative = true ∧ allowsUninterpretableTense Core.Time.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.