Egressy (2026): Size-Sensitive Sequence of Tense in Hungarian

This file formalizes [Egr26]'s account of a split among Hungarian past-under-past clauses: a non-speech-reporting clause (perception, dreaming, thought, belief, a reason adjunct) has the simultaneous reading, like an English complement, while a speech-reporting clause, one encoding the content of a verbal or other sign, is backshifted only, like a Japanese one. The split is clause-internal, since one verb embeds either type. Non-speech-reporting clauses are bare TPs and speech-reporting clauses SayPs with Say > Foc > T, Hungarian having no CP; the Sequence of Tense Rule of [Ogi96] deletes an embedded PAST under Agree with a matrix PAST, and that Agree obeys the Williams Cycle of [Wil03a]: a dependency headed at T cannot search a projection above T in the functional sequence. It therefore crosses a TP and is blocked by a SayP, just as focus movement to Spec,FocP escapes a TP but not a SayP and raising to Spec,TP crosses a TP but not a CP. The Williams Cycle in Agree is derived from size-dependent adjunction: an embedded clause adjoins to the matrix projection of its own size, so only a clause no larger than TP lies inside a projection of the matrix PAST. The same derivation gives the multiple-embedding data, where only structurally adjacent clauses interact, and locates the size-insensitive Sequence of Tense of English in its CP complements sitting inside the VP.

Implementation notes

• Clause size is Minimalist.ComplementSize on the shared functional sequence Cat.fValue, where Cat.Say sits at Say > Foc > T. The Williams Cycle (26) and its version for Agree (35) are one relation, WilliamsCycle x y, between the head of a dependency and the crossed projection.
• Readings are positions of the embedded reference time against the attitude's now, an Ordering: backshifted .lt, simultaneous .eq. The clause-internal value of [OS12]'s Sequence of Tense parameter is SOTRule.Applicable itself, so readings is Tense.pastUnderPast at it, and a chain of embeddings is read pairwise by profile.
• The examples are Data.Examples.Egressy2026. A row's clause type is its clauseType feature, its matrix verb the Hungarian.Verbs entry named by its matrixVerb feature, and direct perception, which the paper says removes the backshifted reading pragmatically, its directPerception feature.
• Footnote 9 allows the complement of mond to be an XP with Say > Foc > X > T, which movement to Spec,FocP escapes but Agree from T does not; the shared sequence has no such head, so those complements are SayPs here.

References

• [Egr26]
• [Egr25]
• [Wil03a]
• [Kei19]
• [Kei20]
• [Ogi96]
• [OS12]
• [Sha20]
• [EK23]
• [Abu88]
• [Hei94a]

The two clause types and their size (§2, §3.1)

inductive Egressy2026.ClauseType : Type

An embedded clause either encodes the content of a verbal or other sign or does not (§2.2), a property of the clause, not of the matrix predicate, which may embed either type.

• nonSpeechReporting : ClauseType
• speechReporting : ClauseType

@[instance_reducible]

instance Egressy2026.instDecidableEqClauseType : DecidableEq ClauseType

Equations

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

@[instance_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.

@[instance_reducible]

instance Egressy2026.instFintypeClauseType : Fintype ClauseType

Equations

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

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

(21)–(22): a non-speech-reporting clause is a bare TP, a speech-reporting clause a SayP.

Equations

• Egressy2026.ClauseType.nonSpeechReporting.size = Minimalist.ComplementSize.tP
• Egressy2026.ClauseType.speechReporting.size = { highestHead := Minimalist.Cat.Say }

theorem Egressy2026.size_nonSpeech_lt_speech : ClauseType.nonSpeechReporting.size.fLevel < ClauseType.speechReporting.size.fLevel

Speech-reporting clauses are the larger ones (§3.1).

The Williams Cycle (26) and the Williams Cycle in Agree (35)

def Egressy2026.WilliamsCycle (x y : Minimalist.Cat) : Prop

A dependency headed at x, movement to Spec,XP or Agree from X or XP, may cross or search a projection of y unless Y is above X in the functional sequence.

Equations

• Egressy2026.WilliamsCycle x y = (y.fValue ≤ x.fValue)

@[instance_reducible]

instance Egressy2026.instDecidableWilliamsCycle (x y : Minimalist.Cat) : Decidable (WilliamsCycle x y)

Equations

• Egressy2026.instDecidableWilliamsCycle x y = { decide := y.fValue.ble x.fValue, reflects_decide := ⋯ }

theorem Egressy2026.WilliamsCycle.refl (x : Minimalist.Cat) : WilliamsCycle x x

A projection of the dependency's own category is crossed.

theorem Egressy2026.WilliamsCycle.of_le {x y y' : Minimalist.Cat} (h : y'.fValue ≤ y.fValue) (hxy : WilliamsCycle x y) : WilliamsCycle x y'

Upward entailment says that whatever a projection blocks, every higher projection blocks.

theorem Egressy2026.focus_crosses_TP : WilliamsCycle Minimalist.Cat.Foc Minimalist.Cat.T

(24)–(25), [Egr25]: focus and wh-movement to Spec,FocP escape a TP.

theorem Egressy2026.focus_blocked_by_SayP : ¬WilliamsCycle Minimalist.Cat.Foc Minimalist.Cat.Say

(24)–(25): movement to Spec,FocP cannot leave a SayP, whose Say is above Foc.

theorem Egressy2026.raising_crosses_TP : WilliamsCycle Minimalist.Cat.T Minimalist.Cat.T

(27): raising to Spec,TP crosses a TP.

theorem Egressy2026.raising_blocked_by_CP : ¬WilliamsCycle Minimalist.Cat.T Minimalist.Cat.C

(28), the ban on hyperraising: raising to Spec,TP cannot cross a CP.

def Egressy2026.crossed? (e : Datum) : Option Minimalist.ComplementSize

The complement size crossed in a raising row.

Equations

• Egressy2026.crossed? e = e.parse? "crossed" [("tP", Minimalist.ComplementSize.tP), ("cP", Minimalist.ComplementSize.cP)]

theorem Egressy2026.raising_rows (e : Datum) : e ∈ [Examples.ex_27, Examples.ex_28] → ∀ cs ∈ crossed? e, e.judgment = Judgment.acceptable ↔ WilliamsCycle Minimalist.Cat.T cs.highestHead

The raising rows are judged exactly as the Williams Cycle predicts.

def Egressy2026.HostsEvaluativeAdverb (cs : Minimalist.ComplementSize) : Prop

(23): evaluative adverbs such as sajnos sit in the Say layer above foci, so a clause hosts one iff it is at least a SayP.

Equations

• Egressy2026.HostsEvaluativeAdverb cs = (Minimalist.Cat.Say.fValue ≤ cs.fLevel)

@[instance_reducible]

instance Egressy2026.instDecidableHostsEvaluativeAdverb (cs : Minimalist.ComplementSize) : Decidable (HostsEvaluativeAdverb cs)

Equations

• Egressy2026.instDecidableHostsEvaluativeAdverb cs = { decide := Minimalist.Cat.Say.fValue.ble cs.fLevel, reflects_decide := ⋯ }

theorem Egressy2026.hostsEvaluativeAdverb_iff (ct : ClauseType) : HostsEvaluativeAdverb ct.size ↔ ct = ClauseType.speechReporting

The complements of mond, hall and gondol in (23) host sajnos; the TP complement of álmodik cannot.

The Sequence of Tense Rule (31) and size-dependent adjunction (41)

inductive Egressy2026.Attachment : Type

An embedded clause attaches (§4) by (41) to the matrix projection of its own size, as in Hungarian, or inside the matrix VP as the sister of V, as in English, where (41) does not hold.

• sizeDependent : Attachment
• vpInternal : Attachment

@[instance_reducible]

instance Egressy2026.instDecidableEqAttachment : DecidableEq Attachment

Equations

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

def Egressy2026.Attachment.level : Attachment → Minimalist.ComplementSize → ℕ

The functional-sequence level of the matrix projection an embedded clause attaches to.

Equations

• Egressy2026.Attachment.sizeDependent.level x✝ = x✝.fLevel
• Egressy2026.Attachment.vpInternal.level x✝ = Minimalist.Cat.V.fValue

def Egressy2026.SOTRule.Applicable (a : Attachment) (cs : Minimalist.ComplementSize) : Prop

The Sequence of Tense Rule (31) can delete an embedded PAST iff the embedded T is contained in a projection of the matrix PAST T, that is, iff the clause attaches no higher than TP.

Equations

• Egressy2026.SOTRule.Applicable a cs = (a.level cs ≤ Minimalist.Cat.T.fValue)

@[instance_reducible]

instance Egressy2026.instDecidableApplicable (a : Attachment) (cs : Minimalist.ComplementSize) : Decidable (SOTRule.Applicable a cs)

Equations

• Egressy2026.instDecidableApplicable a cs = { decide := (a.level cs).ble Minimalist.Cat.T.fValue, reflects_decide := ⋯ }

theorem Egressy2026.applicable_sizeDependent_iff (cs : Minimalist.ComplementSize) : SOTRule.Applicable Attachment.sizeDependent cs ↔ WilliamsCycle Minimalist.Cat.T cs.highestHead

§3.3 and §4: under size-dependent adjunction the Sequence of Tense Rule obeys the Williams Cycle in Agree, reaching the embedded PAST exactly where the cycle lets T search the clause.

theorem Egressy2026.applicable_vpInternal_cP : SOTRule.Applicable Attachment.vpInternal Minimalist.ComplementSize.cP ∧ ¬WilliamsCycle Minimalist.Cat.T Minimalist.Cat.C

§4: with the embedded clause inside the VP the rule ignores size. English CP complements are deleted under Agree although the Williams Cycle would keep T out of a CP, which is why English Sequence of Tense is size-insensitive.

Readings: the language-wide parameter realized clause-internally (§1, §2.4)

def Egressy2026.readings (a : Attachment) (cs : Minimalist.ComplementSize) : Finset Ordering

The readings of a past clause under a past matrix, where backshift is the default and the simultaneous reading arises only through the rule.

Equations

• Egressy2026.readings a cs = Tense.pastUnderPast (Egressy2026.SOTRule.Applicable a cs)

theorem Egressy2026.applicable_nonSpeech : SOTRule.Applicable Attachment.sizeDependent ClauseType.nonSpeechReporting.size

The rule reaches a non-speech-reporting clause, as it reaches an English complement.

theorem Egressy2026.not_applicable_speech : ¬SOTRule.Applicable Attachment.sizeDependent ClauseType.speechReporting.size

The rule does not reach a speech-reporting clause, as it reaches no Japanese complement.

theorem Egressy2026.simultaneous_iff (ct : ClauseType) : Ordering.eq ∈ readings Attachment.sizeDependent ct.size ↔ ct = ClauseType.nonSpeechReporting

The core asymmetry (§2.4) is that the simultaneous reading is available exactly in non-speech-reporting clauses.

theorem Egressy2026.shifted_mem (a : Attachment) (cs : Minimalist.ComplementSize) : Ordering.lt ∈ readings a cs

The grammar always leaves the backshifted reading; only pragmatics removes it.

theorem Egressy2026.english_simultaneous : Ordering.eq ∈ readings Attachment.vpInternal Minimalist.ComplementSize.cP

(19): an English past-under-past complement has the simultaneous reading.

Direct perception (§2.1)

def Egressy2026.observed (direct : Prop) [Decidable direct] (rs : Finset Ordering) : Finset Ordering

One can only perceive directly what happens now: the readings the paper reports are the grammatical ones, narrowed to the simultaneous reading under direct perception.

Equations

• Egressy2026.observed direct rs = if direct then rs ⊓ Semantics.Denotes.denote Tense.present else rs

theorem Egressy2026.observed_le (direct : Prop) [Decidable direct] (rs : Finset Ordering) : observed direct rs ⊆ rs

Pragmatics only removes readings.

The data (§2)

def Egressy2026.clauseTypeTable : List (String × ClauseType)

The clause types as recorded in the rows.

Equations

• Egressy2026.clauseTypeTable = [("nonSpeechReporting", Egressy2026.ClauseType.nonSpeechReporting), ("speechReporting", Egressy2026.ClauseType.speechReporting)]

def Egressy2026.clauseType? (e : Datum) : Option ClauseType

The clause type of a single-embedding row.

Equations

• Egressy2026.clauseType? e = e.parse? "clauseType" Egressy2026.clauseTypeTable

def Egressy2026.DirectPerceptionAt (e : Datum) (key : String) : Prop

Whether a row's feature key records direct perception.

Equations

• Egressy2026.DirectPerceptionAt e key = (e.feature? key = some "yes")

@[instance_reducible]

instance Egressy2026.instDecidableDirectPerceptionAt (e : Datum) (key : String) : Decidable (DirectPerceptionAt e key)

Equations

• Egressy2026.instDecidableDirectPerceptionAt e key = Egressy2026.instDecidableDirectPerceptionAt._aux_1 e key

def Egressy2026.readingTable : List (String × Ordering)

The readings as named in the rows.

Equations

• Egressy2026.readingTable = [("simultaneous", Ordering.eq), ("backshifted", Ordering.lt)]

def Egressy2026.Agrees (e : Datum) (lvl : String) (rs : Finset Ordering) : Prop

A row's reported readings at embedding level lvl agree with a predicted reading set when each named reading is judged acceptable exactly if predicted.

Equations

• Egressy2026.Agrees e lvl rs = ∀ r ∈ e.readings, ∀ x ∈ Egressy2026.readingTable, r.1 = lvl ++ x.1 → (r.2 = Judgment.acceptable ↔ x.2 ∈ rs)

@[instance_reducible]

instance Egressy2026.instDecidableAgrees (e : Datum) (lvl : String) (rs : Finset Ordering) : Decidable (Agrees e lvl rs)

Equations

• Egressy2026.instDecidableAgrees e lvl rs = Egressy2026.instDecidableAgrees._aux_1 e lvl rs

def Egressy2026.predicted (e : Datum) (ct : ClauseType) : Finset Ordering

The predicted readings of a single-embedding Hungarian row: the grammar at its clause type, narrowed by direct perception.

Equations

• Egressy2026.predicted e ct = Egressy2026.observed (Egressy2026.DirectPerceptionAt e "directPerception") (Egressy2026.readings Egressy2026.Attachment.sizeDependent ct.size)

def Egressy2026.singleRows : List Datum

The single-embedding rows of §2.1–2.2: object, subject and adjunct clauses of both types.

Equations

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

theorem Egressy2026.singleRows_predicted (e : Datum) : e ∈ singleRows → ∀ (ct : ClauseType), clauseType? e = some ct → Agrees e "" (predicted e ct)

Every single-embedding row is predicted: the simultaneous reading exactly in non-speech-reporting clauses, and backshift wherever direct perception does not exclude it.

def Egressy2026.matrixVerb? (e : Datum) : Option Verb

The fragment entry named by a row's matrixVerb feature.

Equations

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

theorem Egressy2026.clauseType_not_of_verb : ¬∃ (f : Verb → ClauseType), ∀ e ∈ [Examples.ex_5, Examples.ex_13, Examples.ex_9, Examples.ex_11c], ∀ (v : Verb) (ct : ClauseType), matrixVerb? e = some v → clauseType? e = some ct → f v = ct

§2.2: the clause type is a property of the clause, not of the matrix verb. hall 'hear' embeds a non-speech-reporting clause in (5) and the speech-reporting content of a report in (13), and morog 'growl' a non-speech-reporting reason adjunct in (9) and the speech-reporting content of the growl in (11): no assignment of clause types to verbs fits the rows.

Multiple embedding (§2.3, §4)

structure Egressy2026.Clause : Type

An embedded clause carries its morphological tense and its size.

• tense : Finset Ordering

  The clause's tense as a comparison cell, ⟦Tense.past⟧ or ⟦Tense.future⟧.

• size : Minimalist.ComplementSize

  The clause's size.

def Egressy2026.linkReadings (a : Attachment) (matrix : Finset Ordering) (c : Clause) : Finset Ordering

The readings of an embedded clause against the clause immediately containing it. A past clause under a past clause is read by the rule; a past clause under any other tense is backshifted only, since the rule needs an agreeing PAST above; a non-past clause has no past-under-past reading.

Equations

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

def Egressy2026.profile (a : Attachment) : Finset Ordering → List Clause → List (Finset Ordering)

The readings at each level of a chain of embedded clauses under a matrix tense, matrix first. Each clause is read against the clause immediately containing it: by (41) every clause attaches at its own size, so a SayP is never inside a TP of any higher clause while a TP is inside the TP of the clause containing it, and only structurally adjacent clauses interact (§2.3, §4).

Equations

• Egressy2026.profile a x✝ [] = []
• Egressy2026.profile a x✝ (c :: rest) = Egressy2026.linkReadings a x✝ c :: Egressy2026.profile a c.tense rest

def Egressy2026.chain (ct₁ ct₂ : ClauseType) : List Clause

The chain of a two-level Hungarian row, from its two clause-type features.

Equations

• Egressy2026.chain ct₁ ct₂ = [{ tense := Semantics.Denotes.denote Tense.past, size := ct₁.size }, { tense := Semantics.Denotes.denote Tense.past, size := ct₂.size }]

theorem Egressy2026.ex16_profile : profile Attachment.sizeDependent (Semantics.Denotes.denote Tense.past) (chain ClauseType.speechReporting ClauseType.nonSpeechReporting) = [Semantics.Denotes.denote Tense.past, Semantics.Denotes.denote Tense.past ⊔ Semantics.Denotes.denote Tense.present]

(16): shout > see > be. The speech-reporting intermediate clause is backshifted; the non-speech-reporting deepest clause is simultaneous with it.

theorem Egressy2026.ex17_profile : profile Attachment.sizeDependent (Semantics.Denotes.denote Tense.past) (chain ClauseType.nonSpeechReporting ClauseType.speechReporting) = [Semantics.Denotes.denote Tense.past ⊔ Semantics.Denotes.denote Tense.present, Semantics.Denotes.denote Tense.past]

(17): hear > shout > be, the mirror image of (16): only adjacent clauses interact, and a speech-reporting clause is backshifted whatever contains it.

theorem Egressy2026.doubleRows_predicted (e : Datum) : e ∈ [Examples.ex_10, Examples.ex_15, Examples.ex_16, Examples.ex_17] → ∀ (ct₁ ct₂ : ClauseType), e.parse? "intermediateClauseType" clauseTypeTable = some ct₁ → e.parse? "deepestClauseType" clauseTypeTable = some ct₂ → Agrees e "intermediate " (observed (DirectPerceptionAt e "intermediateDirectPerception") ((profile Attachment.sizeDependent (Semantics.Denotes.denote Tense.past) (chain ct₁ ct₂)).getD 0 ⊥)) ∧ Agrees e "deepest " (observed (DirectPerceptionAt e "deepestDirectPerception") ((profile Attachment.sizeDependent (Semantics.Denotes.denote Tense.past) (chain ct₁ ct₂)).getD 1 ⊥))

The two-level rows (10), (15), (16) and (17) are predicted level by level, direct perception narrowing the level of the perceiving clause.

theorem Egressy2026.ex18_profile : profile Attachment.vpInternal (Semantics.Denotes.denote Tense.past) [{ tense := Semantics.Denotes.denote Tense.future, size := Minimalist.ComplementSize.cP }, { tense := Semantics.Denotes.denote Tense.past, size := Minimalist.ComplementSize.cP }] = [⊥, Semantics.Denotes.denote Tense.past]

(18), [Ogi96]: English past under will under past. The deepest past has no simultaneous reading, the tense immediately above it being a future rather than an agreeing past, although English complements attach inside the VP and are otherwise deleted freely.

theorem Egressy2026.ex18_predicted : Agrees Examples.ex_18 "deepest " (Semantics.Denotes.denote Tense.past)

Rival mechanisms (§3.3, §4)

theorem Egressy2026.resMovement_blocked_by_TP : ¬WilliamsCycle Minimalist.Cat.V Minimalist.Cat.T

De re res-movement of the embedded PAST ([Abu88], [Hei94a]) targets an A-position inside the matrix VP. A res-movement obeying the Williams Cycle could not leave even a TP, since T is above V, so it could not derive the simultaneous reading of non-speech-reporting clauses; deriving them requires a movement free of the locality every other Hungarian dependency obeys, whereas Agree from T (raising_crosses_TP) derives them within it.

def Egressy2026.sotProbe : Minimalist.Probe.Profile

Sequence of Tense as a probe of [Kei20]: a probe on T whose horizon is Say.

Equations

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

theorem Egressy2026.sotProbe_clauseTypes : sotProbe.TransparentTo Minimalist.ClauseSpine.tP.label ∧ ¬sotProbe.TransparentTo (Minimalist.ClauseSpine.tP.append [Minimalist.Cat.Foc, Minimalist.Cat.Say]).label

The horizon account agrees with the Williams Cycle on the two Hungarian clause types.

theorem Egressy2026.horizon_admits_FocP : sotProbe.TransparentTo (Minimalist.ClauseSpine.tP.append [Minimalist.Cat.Foc]).label ∧ ¬WilliamsCycle Minimalist.Cat.T Minimalist.Cat.Foc

§4: the horizon account is the less restrictive of the two. A clause whose highest head lies strictly between T and Say, such as a FocP, is transparent to the probe yet beyond the reach of T under the Williams Cycle, the pattern footnote 9 needs for the complements of mond.