[Egr26]: Size-Sensitive Sequence of Tense in Hungarian

[Egr26]

János Egressy shows that the availability of the simultaneous reading of a past-under-past configuration in Hungarian depends on a clause-internal property of the embedded clause, not on the matrix verb or on the complementizer hogy (which is an edge marker, not a C head — Hungarian has no CP, [EK23]):

• Non-speech-reporting clauses (perception, dreaming, belief — clauses that do not encode the content of a verbal/representational sign) pattern like English: a past-under-past clause has a simultaneous reading (and, pragmatics permitting, a back-shifted one).
• Speech-reporting clauses (the content of say/shout/growl) pattern like Japanese: only the back-shifted reading.

The analysis: speech-reporting clauses carry an extra Say layer (Say > Foc > T) above the bare TP of non-speech-reporting clauses ([Maj21], [Kri23]). The simultaneous reading comes from the optional LF deletion of the embedded PAST under an agreeing matrix PAST — the Sequence of Tense Rule of [Ogi96] / [OS12]. Crucially this SOT-Agree obeys the Williams Cycle ([Wil03a]), i.e. [Kei19]'s selective opacity generalized from movement to Agree: an Agree dependency from T cannot cross a larger Say projection. So it crosses a TP (simultaneous available) but is blocked by a SayP (back-shift only). Williams-Cycle sensitivity favors the SOT-Agree analysis over a res-movement (de re) account of simultaneity ([Abu88], [Abu97]), which would be unboundedly free (see de_re_overgenerates).

Formalization strategy

The opacity is derived, not stipulated: the Say head sits at fValue 5 in the shared functional sequence (Syntax.Minimalist), and the SOT transparency of a complement is exactly ComplementSize.transparentToSOTAgree (fLevel < fValue .Say). This reuses the very machinery that derives the ban on hyperraising and Hindi long-distance Agree ([Kei20]); see sot_is_selective_opacity. There is no language-wide "SOT stage" parameter — the two Hungarian clause types reproduce the two values of the binary SOTParameter clause-internally (nonSpeech_eq_relative, speech_eq_absolute).

The two clause types and their size

inductive Egressy2026.ClauseType : Type

The clause-internal distinction [Egr26] draws: whether an embedded clause encodes the content of a verbal/representational sign. This is a property of the clause, independent of the matrix verb (hall 'hear' and gondol 'think' embed either type) and of hogy.

• nonSpeechReporting : ClauseType

  Perception, dreaming, belief: no Say layer, a bare TP.

• speechReporting : ClauseType

  The content of a verbal/representational sign: an extra Say layer (SayP).

@[implicit_reducible]

instance Egressy2026.instDecidableEqClauseType : DecidableEq ClauseType

Equations

• Egressy2026.instDecidableEqClauseType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Egressy2026.instReprClauseType : Repr ClauseType

Equations

• Egressy2026.instReprClauseType = { reprPrec := Egressy2026.instReprClauseType.repr }

def Egressy2026.instReprClauseType.repr : ClauseType → ℕ → Std.Format

Equations

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

def Egressy2026.ClauseType.complementSize : ClauseType → Minimalist.ComplementSize

The structural size of each clause type in the shared functional sequence: non-speech-reporting = TP, speech-reporting = SayP (Say > Foc > T).

Equations

• Egressy2026.ClauseType.nonSpeechReporting.complementSize = Minimalist.ComplementSize.tP
• Egressy2026.ClauseType.speechReporting.complementSize = Minimalist.ComplementSize.sayP

theorem Egressy2026.speech_larger_than_nonspeech : ClauseType.nonSpeechReporting.complementSize.fLevel < ClauseType.speechReporting.complementSize.fLevel

Speech-reporting clauses are strictly larger than non-speech-reporting ones (SayP dominates TP).

SOT-Agree opacity is selective opacity (the Williams Cycle)

def Egressy2026.sotProbe : Minimalist.Probe.Profile

The Sequence-of-Tense probe: a T-probe whose horizon is the Say layer. Deletion-under-Agree of an embedded PAST searches down from a matrix T and is terminated by a Say head ([Egr26], generalizing [Kei19]).

Equations

• Egressy2026.sotProbe = { probeHead := Minimalist.Cat.T, horizon := some Minimalist.Cat.Say }

def Egressy2026.nonSpeechSpine : List Minimalist.Cat

Projected heads of a non-speech-reporting clause (a bare TP): no Say.

Equations

• Egressy2026.nonSpeechSpine = [Minimalist.Cat.V, Minimalist.Cat.v, Minimalist.Cat.T]

def Egressy2026.speechSpine : List Minimalist.Cat

Projected heads of a speech-reporting clause (a SayP): contains Say.

Equations

• Egressy2026.speechSpine = [Minimalist.Cat.V, Minimalist.Cat.v, Minimalist.Cat.T, Minimalist.Cat.Say]

theorem Egressy2026.sot_crosses_TP : sotProbe.transparentToLabel nonSpeechSpine = true

The SOT probe crosses a TP: a non-speech-reporting clause is transparent.

theorem Egressy2026.sot_blocked_by_SayP : sotProbe.transparentToLabel speechSpine = false

The SOT probe is blocked by a SayP: a speech-reporting clause is opaque.

theorem Egressy2026.sot_is_selective_opacity : ClauseType.nonSpeechReporting.complementSize.transparentToSOTAgree = sotProbe.transparentToLabel nonSpeechSpine ∧ ClauseType.speechReporting.complementSize.transparentToSOTAgree = sotProbe.transparentToLabel speechSpine

The unification. SOT-Agree opacity is the same selective-opacity mechanism that the syntax layer uses for movement and Agree: the fValue-keyed ComplementSize.transparentToSOTAgree agrees with the horizon-keyed Probe.transparentToLabel of sotProbe on both clause types. (Compare Minimalist.Probe a_movement_typology for hyperraising.)

theorem Egressy2026.sot_opaque_above_say (cs : Minimalist.ComplementSize) (h : Minimalist.fValue Minimalist.Cat.Say ≤ cs.fLevel) : cs.transparentToSOTAgree = false

Upward entailment ([Kei20]): the SayP boundary is monotone — any complement at or above the Say layer is opaque to SOT-Agree. (Speas–Tenny SA, Force, and C all sit at or above Say.)

The Egressy license and the predictions

The Sequence-of-Tense rule is a SequenceOfTense.LocalLicense: the Say-boundary size gate, refined by an agreeing-past gate (SOT deletion needs an agreeing PAST). Built from the shared schemas, so the predictions are the foundation's Simultaneous/Backshifted, not a study-local reading function.

def Egressy2026.sayBoundary : Clause.Size

The Say boundary as a framework-neutral Clause.Size.

Equations

• Egressy2026.sayBoundary = Minimalist.ComplementSize.sayP.toClauseSize

def Egressy2026.clauseNode (tense : Finset Ordering) (ct : ClauseType) : SequenceOfTense.Node

A clause node: a tense cell (notAfter = past, after = future — the ungated reading set of [KZ18]) and the neutral size of its ClauseType.

Equations

• Egressy2026.clauseNode tense ct = { tense := tense, size := ct.complementSize.toClauseSize }

def Egressy2026.pastMatrix : SequenceOfTense.Node

A past matrix clause (the container; only its tense matters to licensing).

Equations

• Egressy2026.pastMatrix = { tense := Core.Order.notAfter, size := 0 }

def Egressy2026.agreeingPast : SequenceOfTense.Node → SequenceOfTense.Node → Bool

The agreeing-past gate: SOT deletion needs both the container and the contained clause to be morphologically past ([Ogi96]).

Equations

• Egressy2026.agreeingPast a c = (a.tense == Core.Order.notAfter && c.tense == Core.Order.notAfter)

def Egressy2026.egressyLicense : SequenceOfTense.LocalLicense

[Egr26]'s license: the Say-boundary size gate refined by the agreeing-past gate. The size gate blocks simultaneity in speech-reporting (SayP) clauses; the agreeing-past refinement additionally blocks it under an intervening future (see ex18).

Equations

• Egressy2026.egressyLicense = (SequenceOfTense.sizeGatedLicense Egressy2026.sayBoundary).gate Egressy2026.agreeingPast

theorem Egressy2026.transparentToSOTAgree_iff_clause (cs : Minimalist.ComplementSize) : cs.transparentToSOTAgree = true ↔ Clause.transparentTo cs.toClauseSize sayBoundary

The framework-neutral Clause.transparentTo at the Say boundary reproduces the Minimalist ComplementSize.transparentToSOTAgree — the bridge that justifies stating SOT over Clause.Size rather than Cat.

def Egressy2026.toReadings (s : Finset Ordering) : List Tense.EmbeddedTenseReading

Bridge from licensed atoms to the legacy EmbeddedTenseReading (atoms are canonical; this adapter feeds the binary SOTParameter comparison).

Equations

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

theorem Egressy2026.nonSpeech_both : SequenceOfTense.Simultaneous (egressyLicense pastMatrix (clauseNode Core.Order.notAfter ClauseType.nonSpeechReporting)) ∧ SequenceOfTense.Backshifted (egressyLicense pastMatrix (clauseNode Core.Order.notAfter ClauseType.nonSpeechReporting))

Non-speech-reporting (TP) clauses license both readings.

theorem Egressy2026.speech_backshift_only : ¬SequenceOfTense.Simultaneous (egressyLicense pastMatrix (clauseNode Core.Order.notAfter ClauseType.speechReporting)) ∧ SequenceOfTense.Backshifted (egressyLicense pastMatrix (clauseNode Core.Order.notAfter ClauseType.speechReporting))

Speech-reporting (SayP) clauses license only the back-shifted reading.

theorem Egressy2026.simultaneous_iff_nonSpeech (ct : ClauseType) : SequenceOfTense.Simultaneous (egressyLicense pastMatrix (clauseNode Core.Order.notAfter ct)) ↔ ct = ClauseType.nonSpeechReporting

The core asymmetry: simultaneity is blocked exactly in speech-reporting clauses.

Unification with the binary SOT parameter

Hungarian is not at a language-wide "SOT stage": its two clause types realize the two values of the binary SOTParameter ([OS12]) clause-internally — a non-speech-reporting clause behaves like an English (.relative) complement, a speech-reporting one like a Japanese (.absolute) one.

theorem Egressy2026.nonSpeech_eq_relative : toReadings (egressyLicense pastMatrix (clauseNode Core.Order.notAfter ClauseType.nonSpeechReporting)) = Tense.availableReadings Tense.SOTParameter.relative

A non-speech-reporting clause reproduces the English (.relative) parameter.

theorem Egressy2026.speech_eq_absolute : toReadings (egressyLicense pastMatrix (clauseNode Core.Order.notAfter ClauseType.speechReporting)) = Tense.availableReadings Tense.SOTParameter.absolute

A speech-reporting clause reproduces the Japanese (.absolute) parameter.

Empirical data ([Egr26], §2)

The verbs are grounded in Hungarian.Predicates; clause types are assigned by the embedding predicate (perception/cognition → non-speech-reporting; communication → speech-reporting). All examples are past-under-past with the embedded copula volt 'was'.

structure Egressy2026.SOTDatum : Type

A past-under-past judgment: matrix verb, the embedded clause type, and whether the simultaneous reading is observed.

• matrixVerb : String

  Matrix verb (Hungarian surface form)

• matrixGloss : String

  English gloss of the matrix verb

• clauseType : ClauseType

  The embedded clause type

• example_ : String

  Example sentence

• simultaneousObserved : Bool

  Is the simultaneous reading observed?

@[implicit_reducible]

instance Egressy2026.instReprSOTDatum : Repr SOTDatum

Equations

• Egressy2026.instReprSOTDatum = { reprPrec := Egressy2026.instReprSOTDatum.repr }

def Egressy2026.instReprSOTDatum.repr : SOTDatum → ℕ → Std.Format

Equations

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

def Egressy2026.ex4_lat : SOTDatum

ex. (4): direct perception with lát 'see' — simultaneous (only).

Equations

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

def Egressy2026.ex5_hall : SOTDatum

ex. (5): direct perception with hall 'hear' — simultaneous (only).

Equations

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

def Egressy2026.ex6_almodik : SOTDatum

ex. (6): dreaming with álmodik — simultaneous (only).

Equations

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

def Egressy2026.ex7_gondol : SOTDatum

ex. (7): belief with gondol 'think' — simultaneous and back-shifted.

Equations

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

def Egressy2026.ex8_aggaszt : SOTDatum

ex. (8): subject clause with aggaszt 'worry' — simultaneous and back-shifted.

Equations

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

def Egressy2026.ex11_mond : SOTDatum

ex. (11a): saying with mond 'say' — back-shifted only.

Equations

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

def Egressy2026.ex11_rikolt : SOTDatum

ex. (11b): shouting with rikolt 'shout' — back-shifted only.

Equations

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

def Egressy2026.ex11_morog : SOTDatum

ex. (11c): growling with morog 'growl' — back-shifted only.

Equations

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

def Egressy2026.allData : List SOTDatum

All single-embedding judgments.

Equations

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

def Egressy2026.predictsSimultaneous (d : SOTDatum) : Bool

The grammatical prediction via the Egressy license: is the simultaneous reading available for this datum's clause type (under a past matrix)?

Equations

• Egressy2026.predictsSimultaneous d = decide (SequenceOfTense.Simultaneous (Egressy2026.egressyLicense Egressy2026.pastMatrix (Egressy2026.clauseNode Core.Order.notAfter d.clauseType)))

theorem Egressy2026.all_data_match : (allData.all fun (d : SOTDatum) => d.simultaneousObserved == predictsSimultaneous d) = true

Every datum's observed simultaneous availability matches the prediction.

Fragment grounding: matrix verbs are the past forms of the lexical entries.

theorem Egressy2026.ex4_verb_from_fragment : ex4_lat.matrixVerb = Hungarian.Predicates.lat.formPastDef

theorem Egressy2026.ex5_verb_from_fragment : ex5_hall.matrixVerb = Hungarian.Predicates.hall.formPastDef

theorem Egressy2026.ex7_verb_from_fragment : ex7_gondol.matrixVerb = Hungarian.Predicates.gondol.formPastDef

theorem Egressy2026.ex11_verb_from_fragment : ex11_mond.matrixVerb = Hungarian.Predicates.mond.formPastDef

Pragmatic narrowing: direct perception is simultaneous-only

For the direct-perception examples (4)–(6) the back-shifted reading is excluded for pragmatic reasons — one cannot directly perceive a past event — even though it is grammatically available (nonSpeech_both). This is the layer-2 Narrowing from the foundation: direct perception intersects the grammatical reading set with the overlapping (=) constraint, leaving simultaneous-only (direct_perception_narrows).

def Egressy2026.directPerceptionData : List SOTDatum

The direct-perception data (perception and dreaming).

Equations

• Egressy2026.directPerceptionData = [Egressy2026.ex4_lat, Egressy2026.ex5_hall, Egressy2026.ex6_almodik]

theorem Egressy2026.direct_perception_simultaneous : (directPerceptionData.all fun (d : SOTDatum) => d.simultaneousObserved && toReadings (egressyLicense pastMatrix (clauseNode Core.Order.notAfter d.clauseType)) == [Tense.EmbeddedTenseReading.shifted, Tense.EmbeddedTenseReading.simultaneous]) = true

Direct-perception clauses are observed with the simultaneous reading, while grammatically they are non-speech-reporting (both readings available); the absence of the back-shifted reading is pragmatic.

def Egressy2026.directPerception : SequenceOfTense.Narrowing Unit

Direct perception as a layer-2 Narrowing: it imposes the overlapping (=) constraint — only a simultaneous reading is perceivable.

Equations

• Egressy2026.directPerception x✝ = Core.Order.overlapping

theorem Egressy2026.direct_perception_narrows : directPerception.apply () (egressyLicense pastMatrix (clauseNode Core.Order.notAfter ClauseType.nonSpeechReporting)) = Core.Order.overlapping

The prose fact as a theorem: direct perception narrows the grammatically both-readings non-speech license down to simultaneous-only.

Multiple embedding and locality ([Egr26], §2.3)

Simultaneity is computed locally between structurally adjacent clauses ([Ogi96]): SequenceOfTense.profile folds egressyLicense pairwise down the chain (matrix first). The simultaneity at each level is Simultaneous of the licensed atoms.

def Egressy2026.simProfile (chain : List SequenceOfTense.Node) : List Bool

The per-level simultaneity profile of an embedded chain under a past matrix.

Equations

• Egressy2026.simProfile chain = List.map (fun (s : Finset Ordering) => decide (SequenceOfTense.Simultaneous s)) (SequenceOfTense.profile Egressy2026.egressyLicense Egressy2026.pastMatrix chain)

def Egressy2026.ex16 : List SequenceOfTense.Node

ex. (16): shout > see > be. The intermediate (content of the shout) is speech-reporting → back-shifted; the deepest (Mari's perception) is non-speech-reporting → simultaneous. Only adjacent clauses interact.

Equations

• Egressy2026.ex16 = [Egressy2026.clauseNode Core.Order.notAfter Egressy2026.ClauseType.speechReporting, Egressy2026.clauseNode Core.Order.notAfter Egressy2026.ClauseType.nonSpeechReporting]

theorem Egressy2026.ex16_profile : simProfile ex16 = [false, true]

def Egressy2026.ex17 : List SequenceOfTense.Node

ex. (17): hear > shout > be. Intermediate (perception of the shouting) → simultaneous; deepest (content of the shout) → back-shifted. Opposite of (16).

Equations

• Egressy2026.ex17 = [Egressy2026.clauseNode Core.Order.notAfter Egressy2026.ClauseType.nonSpeechReporting, Egressy2026.clauseNode Core.Order.notAfter Egressy2026.ClauseType.speechReporting]

theorem Egressy2026.ex17_profile : simProfile ex17 = [true, false]

def Egressy2026.ex10 : List SequenceOfTense.Node

ex. (10): dream > see > be, all non-speech-reporting → simultaneous throughout.

Equations

• Egressy2026.ex10 = [Egressy2026.clauseNode Core.Order.notAfter Egressy2026.ClauseType.nonSpeechReporting, Egressy2026.clauseNode Core.Order.notAfter Egressy2026.ClauseType.nonSpeechReporting]

theorem Egressy2026.ex10_profile : simProfile ex10 = [true, true]

def Egressy2026.ex15 : List SequenceOfTense.Node

ex. (15): shout > growl > be, all speech-reporting → back-shifted throughout.

Equations

• Egressy2026.ex15 = [Egressy2026.clauseNode Core.Order.notAfter Egressy2026.ClauseType.speechReporting, Egressy2026.clauseNode Core.Order.notAfter Egressy2026.ClauseType.speechReporting]

theorem Egressy2026.ex15_profile : simProfile ex15 = [false, false]

def Egressy2026.ex18 : List SequenceOfTense.Node

Past-under-will-under-past (English; [Ogi96], discussed by [Egr26]): said > will claim > was. The intervening future will (after) is not an agreeing past, so the deepest was has no simultaneous reading — the agreeingPast gate blocks it, independently of size (English is size-insensitive here).

Equations

• Egressy2026.ex18 = [Egressy2026.clauseNode Core.Order.after Egressy2026.ClauseType.speechReporting, Egressy2026.clauseNode Core.Order.notAfter Egressy2026.ClauseType.speechReporting]

theorem Egressy2026.ex18_no_simultaneous : simProfile ex18 = [false, false]

Williams-Cycle support over an unbounded de re alternative ([Egr26], §3.3)

An unbounded res-movement (de re) derivation would move the embedded PAST to an A-position inside the matrix VP, unstopped by the Say layer — hence size-blind. Egressy argues the Williams Cycle rules this out: a size-blind mechanism would license simultaneity for speech-reporting clauses, contrary to fact. The foil below ([Abu88], [Abu97]) is exactly that size-blind account; the restricted de re of [OS12] (and the Polish account of Mucha, Renans & Romoli) is a different, constrained mechanism this argument does not, on its own, refute.

def Egressy2026.deReUnrestricted : SequenceOfTense.LocalLicense

The unbounded (size-blind) de re foil: it licenses every reading. Local to this study — it is Egressy's reductio against unbounded res-movement, not a neutral SOT mechanism.

Equations

• Egressy2026.deReUnrestricted x✝¹ x✝ = Core.Order.unrestricted

theorem Egressy2026.de_re_overgenerates : SequenceOfTense.Simultaneous (deReUnrestricted pastMatrix (clauseNode Core.Order.notAfter ClauseType.speechReporting)) ∧ ¬SequenceOfTense.Simultaneous (egressyLicense pastMatrix (clauseNode Core.Order.notAfter ClauseType.speechReporting))

The unbounded de re foil overgenerates: size-blind, it licenses simultaneity for a speech-reporting clause, which egressyLicense correctly blocks. This refutes unbounded res-movement, not the restricted de re of [OS12].