@cite{egressy-2026}: Size-Sensitive Sequence of Tense in Hungarian

@cite{egressy-2026}

Empirical data from @cite{egressy-2026}, who shows that Hungarian is a partial SOT language: the simultaneous reading of past-under-past is available in structurally small complements (TP, without hogy 'that') but blocked in full CP complements (with hogy).

Key Empirical Findings

1. CP complements (with hogy): shifted reading only

   • Ági tudta, hogy Mari beteg volt. → only "Mari was sick before Ági knew"

2. Bare TP complements (no hogy): both shifted and simultaneous readings

   • Ági tudta Marit betegnek. → ambiguous: shifted or simultaneous

3. Temporal adverb diagnostics: akkor 'then' forces temporal anchoring and disambiguates complement size effects

4. Williams Cycle: Hungarian is mid-cycle — CP has become opaque to tense Agree while TP remains transparent

Data Organization

Theory-neutral empirical judgments, followed by bridge theorems connecting these to @cite{zeijlstra-2012}'s Agree-based SOT theory: fragment grounding, complement-size mapping, per-datum predictions, Williams Cycle classification, and temporal adverb diagnostics.

inductive Phenomena.TenseAspect.Studies.Egressy2026.HungarianComplementType : Type

Hungarian complement types distinguished by structural size.

The key empirical distinction: complements with the overt complementizer hogy 'that' are full CPs; complements without hogy are structurally smaller (TP-sized).

• hogyCP : HungarianComplementType

  Full CP with hogy 'that' — opaque to SOT

• bareTP : HungarianComplementType

  Bare finite complement without hogy — transparent to SOT

instance Phenomena.TenseAspect.Studies.Egressy2026.instDecidableEqHungarianComplementType : DecidableEq HungarianComplementType

Equations

• Phenomena.TenseAspect.Studies.Egressy2026.instDecidableEqHungarianComplementType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.TenseAspect.Studies.Egressy2026.instReprHungarianComplementType.repr : HungarianComplementType → ℕ → Std.Format

Equations

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

instance Phenomena.TenseAspect.Studies.Egressy2026.instReprHungarianComplementType : Repr HungarianComplementType

Equations

• Phenomena.TenseAspect.Studies.Egressy2026.instReprHungarianComplementType = { reprPrec := Phenomena.TenseAspect.Studies.Egressy2026.instReprHungarianComplementType.repr }

instance Phenomena.TenseAspect.Studies.Egressy2026.instBEqHungarianComplementType : BEq HungarianComplementType

Equations

• Phenomena.TenseAspect.Studies.Egressy2026.instBEqHungarianComplementType = { beq := Phenomena.TenseAspect.Studies.Egressy2026.instBEqHungarianComplementType.beq }

def Phenomena.TenseAspect.Studies.Egressy2026.instBEqHungarianComplementType.beq : HungarianComplementType → HungarianComplementType → Bool

Equations

• Phenomena.TenseAspect.Studies.Egressy2026.instBEqHungarianComplementType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.TenseAspect.Studies.Egressy2026.HungarianComplementType.hasHogy : HungarianComplementType → Bool

Whether the complement type includes the complementizer hogy.

Equations

• Phenomena.TenseAspect.Studies.Egressy2026.HungarianComplementType.hogyCP.hasHogy = true
• Phenomena.TenseAspect.Studies.Egressy2026.HungarianComplementType.bareTP.hasHogy = false

structure Phenomena.TenseAspect.Studies.Egressy2026.SOTJudgment : Type

An empirical SOT judgment: a past-under-past sentence with its complement type and available readings.

Each entry records:

• The matrix verb
• The complement type (CP with hogy vs bare TP)
• Whether the simultaneous reading is available
• Whether the shifted reading is available (always true)

• matrixVerb : String

  Matrix verb (Hungarian)

• matrixGloss : String

  Matrix verb gloss

• complementType : HungarianComplementType

  Complement type

• example_ : String

  Example sentence

• shiftedGloss : String

  English translation (shifted reading)

• simultaneousGloss : Option String

  English translation (simultaneous reading, if available)

• simultaneousAvailable : Bool

  Is the simultaneous reading available?

• shiftedAvailable : Bool

  Is the shifted reading available? (always true)

instance Phenomena.TenseAspect.Studies.Egressy2026.instReprSOTJudgment : Repr SOTJudgment

Equations

• Phenomena.TenseAspect.Studies.Egressy2026.instReprSOTJudgment = { reprPrec := Phenomena.TenseAspect.Studies.Egressy2026.instReprSOTJudgment.repr }

def Phenomena.TenseAspect.Studies.Egressy2026.instReprSOTJudgment.repr : SOTJudgment → ℕ → Std.Format

Equations

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

instance Phenomena.TenseAspect.Studies.Egressy2026.instBEqSOTJudgment : BEq SOTJudgment

Equations

• Phenomena.TenseAspect.Studies.Egressy2026.instBEqSOTJudgment = { beq := Phenomena.TenseAspect.Studies.Egressy2026.instBEqSOTJudgment.beq }

def Phenomena.TenseAspect.Studies.Egressy2026.instBEqSOTJudgment.beq : SOTJudgment → SOTJudgment → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.TenseAspect.Studies.Egressy2026.instBEqSOTJudgment.beq x✝¹ x✝ = false

CP complements (with hogy): shifted only

def Phenomena.TenseAspect.Studies.Egressy2026.pastUnderPast_hogyCP_tudta : SOTJudgment

@cite{egressy-2026}, ex. (9): Ági tud-t-a, hogy Mari beteg vol-t. 'Ági know-PST-3SG that Mari sick be-PST' → Shifted only: Mari was sick before Ági's knowing

Equations

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

def Phenomena.TenseAspect.Studies.Egressy2026.pastUnderPast_hogyCP_mondta : SOTJudgment

@cite{egressy-2026}, ex. (11a): Ági mond-t-a, hogy Mari beteg vol-t. 'Ági say-PST-3SG that Mari sick be-PST' → Shifted only in full CP

Equations

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

def Phenomena.TenseAspect.Studies.Egressy2026.pastUnderPast_hogyCP_hitte : SOTJudgment

@cite{egressy-2026}, ex. (11b): Ági hit-t-e, hogy Mari beteg vol-t. 'Ági believe-PST-3SG that Mari sick be-PST' → Shifted only in full CP

Equations

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

Bare TP complements (without hogy): both readings

def Phenomena.TenseAspect.Studies.Egressy2026.pastUnderPast_bareTP_tudta : SOTJudgment

@cite{egressy-2026}, ex. (10): Ági tud-t-a Mari-t beteg-nek. 'Ági know-PST-3SG Mari-ACC sick-DAT' → Both readings: shifted and simultaneous

Equations

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

def Phenomena.TenseAspect.Studies.Egressy2026.allJudgments : List SOTJudgment

All SOT judgments from the study.

Equations

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

def Phenomena.TenseAspect.Studies.Egressy2026.cpJudgments : List SOTJudgment

CP complement judgments: shifted only.

Equations

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

def Phenomena.TenseAspect.Studies.Egressy2026.tpJudgments : List SOTJudgment

Bare TP judgments: both readings.

Equations

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

theorem Phenomena.TenseAspect.Studies.Egressy2026.hogyCP_tudta_no_simultaneous : pastUnderPast_hogyCP_tudta.simultaneousAvailable = false

All CP complement judgments block the simultaneous reading.

theorem Phenomena.TenseAspect.Studies.Egressy2026.hogyCP_mondta_no_simultaneous : pastUnderPast_hogyCP_mondta.simultaneousAvailable = false

theorem Phenomena.TenseAspect.Studies.Egressy2026.hogyCP_hitte_no_simultaneous : pastUnderPast_hogyCP_hitte.simultaneousAvailable = false

theorem Phenomena.TenseAspect.Studies.Egressy2026.bareTP_tudta_simultaneous : pastUnderPast_bareTP_tudta.simultaneousAvailable = true

Bare TP judgments allow the simultaneous reading.

theorem Phenomena.TenseAspect.Studies.Egressy2026.all_shifted_available : (allJudgments.all fun (x : SOTJudgment) => x.shiftedAvailable) = true

All judgments have the shifted reading available.

theorem Phenomena.TenseAspect.Studies.Egressy2026.no_cp_simultaneous : (cpJudgments.all fun (j : SOTJudgment) => !j.simultaneousAvailable) = true

No CP judgment has the simultaneous reading.

theorem Phenomena.TenseAspect.Studies.Egressy2026.all_tp_simultaneous : (tpJudgments.all fun (x : SOTJudgment) => x.simultaneousAvailable) = true

All bare TP judgments have the simultaneous reading.

Prove that the string literals in Data.lean match the Fragment entries. This ensures the data is derived from fragments, not independently stipulated.

theorem Phenomena.TenseAspect.Studies.Egressy2026.tudta_from_fragment : pastUnderPast_hogyCP_tudta.matrixVerb = Fragments.Hungarian.Predicates.tud.formPastDef

tudta in Data.lean is the past definite form of tud.

theorem Phenomena.TenseAspect.Studies.Egressy2026.mondta_from_fragment : pastUnderPast_hogyCP_mondta.matrixVerb = Fragments.Hungarian.Predicates.mond.formPastDef

mondta in Data.lean is the past definite form of mond.

theorem Phenomena.TenseAspect.Studies.Egressy2026.hitte_from_fragment : pastUnderPast_hogyCP_hitte.matrixVerb = Fragments.Hungarian.Predicates.hisz.formPastDef

hitte in Data.lean is the past definite form of hisz.

theorem Phenomena.TenseAspect.Studies.Egressy2026.bareTP_tudta_from_fragment : pastUnderPast_bareTP_tudta.matrixVerb = Fragments.Hungarian.Predicates.tud.formPastDef

The bare TP tudta also matches the past definite form. (Both CP and bare TP examples use definite conjugation with tud.)

theorem Phenomena.TenseAspect.Studies.Egressy2026.glosses_from_fragments : pastUnderPast_hogyCP_tudta.matrixGloss = "knew" ∧ pastUnderPast_hogyCP_mondta.matrixGloss = "said" ∧ pastUnderPast_hogyCP_hitte.matrixGloss = "believed"

Glosses match fragment glosses.

def Phenomena.TenseAspect.Studies.Egressy2026.complementTypeToSize : HungarianComplementType → Minimalism.ComplementSize

Map Hungarian complement types to structural complement sizes.

• hogy-CP → full CP (fValue 6, phase-sized, opaque)
• bare TP → TP (fValue 2, sub-phase, transparent)

Equations

• Phenomena.TenseAspect.Studies.Egressy2026.complementTypeToSize Phenomena.TenseAspect.Studies.Egressy2026.HungarianComplementType.hogyCP = Minimalism.ComplementSize.cP
• Phenomena.TenseAspect.Studies.Egressy2026.complementTypeToSize Phenomena.TenseAspect.Studies.Egressy2026.HungarianComplementType.bareTP = Minimalism.ComplementSize.tP

theorem Phenomena.TenseAspect.Studies.Egressy2026.hogyCP_is_cP : complementTypeToSize HungarianComplementType.hogyCP = Minimalism.ComplementSize.cP

hogy-CP maps to CP.

theorem Phenomena.TenseAspect.Studies.Egressy2026.bareTP_is_tP : complementTypeToSize HungarianComplementType.bareTP = Minimalism.ComplementSize.tP

Bare TP maps to TP.

theorem Phenomena.TenseAspect.Studies.Egressy2026.hogy_fragment_matches_mapping : complementTypeToSize HungarianComplementType.hogyCP = Fragments.Hungarian.FunctionWords.hogy.complementSize

The hogy fragment entry and the complementTypeToSize function agree.

theorem Phenomena.TenseAspect.Studies.Egressy2026.hogyCP_opaque : (complementTypeToSize HungarianComplementType.hogyCP).transparentToTenseAgree = false

hogy-CP is opaque to tense Agree.

theorem Phenomena.TenseAspect.Studies.Egressy2026.bareTP_transparent : (complementTypeToSize HungarianComplementType.bareTP).transparentToTenseAgree = true

Bare TP is transparent to tense Agree.

theorem Phenomena.TenseAspect.Studies.Egressy2026.hogyCP_predicted_readings : Minimalism.Tense.AgreeSOT.availableReadingsBySize (complementTypeToSize HungarianComplementType.hogyCP) = [Semantics.Tense.EmbeddedTenseReading.shifted]

Predicted readings for hogy-CP: shifted only.

theorem Phenomena.TenseAspect.Studies.Egressy2026.bareTP_predicted_readings : Minimalism.Tense.AgreeSOT.availableReadingsBySize (complementTypeToSize HungarianComplementType.bareTP) = [Semantics.Tense.EmbeddedTenseReading.shifted, Semantics.Tense.EmbeddedTenseReading.simultaneous]

Predicted readings for bare TP: both shifted and simultaneous.

For each empirical judgment, prove that the observed availability of the simultaneous reading matches what availableReadingsBySize predicts for the complement type.

def Phenomena.TenseAspect.Studies.Egressy2026.judgmentMatchesPrediction (j : SOTJudgment) : Bool

Helper: check if a judgment's simultaneous availability matches the theoretical prediction. The prediction is: simultaneous is available iff the complement is transparent to tense Agree.

Equations

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

theorem Phenomena.TenseAspect.Studies.Egressy2026.tudta_hogyCP_matches : judgmentMatchesPrediction pastUnderPast_hogyCP_tudta = true

tudta + hogy-CP: no simultaneous reading, as predicted.

theorem Phenomena.TenseAspect.Studies.Egressy2026.mondta_hogyCP_matches : judgmentMatchesPrediction pastUnderPast_hogyCP_mondta = true

mondta + hogy-CP: no simultaneous reading, as predicted.

theorem Phenomena.TenseAspect.Studies.Egressy2026.hitte_hogyCP_matches : judgmentMatchesPrediction pastUnderPast_hogyCP_hitte = true

hitte + hogy-CP: no simultaneous reading, as predicted.

theorem Phenomena.TenseAspect.Studies.Egressy2026.tudta_bareTP_matches : judgmentMatchesPrediction pastUnderPast_bareTP_tudta = true

tudta + bare TP: simultaneous reading available, as predicted.

theorem Phenomena.TenseAspect.Studies.Egressy2026.all_judgments_match : allJudgments.all judgmentMatchesPrediction = true

All judgments match predictions.

def Phenomena.TenseAspect.Studies.Egressy2026.hungarianStage : Minimalism.Tense.AgreeSOT.WilliamsCycleStage

Hungarian's Williams Cycle stage.

Equations

• Phenomena.TenseAspect.Studies.Egressy2026.hungarianStage = Minimalism.Tense.AgreeSOT.WilliamsCycleStage.partialSOT

theorem Phenomena.TenseAspect.Studies.Egressy2026.hungarian_partial_sot : Minimalism.Tense.AgreeSOT.readingsByStage hungarianStage (complementTypeToSize HungarianComplementType.bareTP) = [Semantics.Tense.EmbeddedTenseReading.shifted, Semantics.Tense.EmbeddedTenseReading.simultaneous] ∧ Minimalism.Tense.AgreeSOT.readingsByStage hungarianStage (complementTypeToSize HungarianComplementType.hogyCP) = [Semantics.Tense.EmbeddedTenseReading.shifted]

Hungarian's partial SOT matches the empirical pattern: both readings in TP, shifted only in CP.

def Phenomena.TenseAspect.Studies.Egressy2026.englishStage : Minimalism.Tense.AgreeSOT.WilliamsCycleStage

English, by contrast, is full SOT — both readings in all complement types.

Equations

• Phenomena.TenseAspect.Studies.Egressy2026.englishStage = Minimalism.Tense.AgreeSOT.WilliamsCycleStage.fullSOT

theorem Phenomena.TenseAspect.Studies.Egressy2026.english_full_sot (ct : HungarianComplementType) : Minimalism.Tense.AgreeSOT.readingsByStage englishStage (complementTypeToSize ct) = [Semantics.Tense.EmbeddedTenseReading.shifted, Semantics.Tense.EmbeddedTenseReading.simultaneous]

def Phenomena.TenseAspect.Studies.Egressy2026.japaneseStage : Minimalism.Tense.AgreeSOT.WilliamsCycleStage

Japanese is non-SOT — shifted only in all complement types.

Equations

• Phenomena.TenseAspect.Studies.Egressy2026.japaneseStage = Minimalism.Tense.AgreeSOT.WilliamsCycleStage.noSOT

theorem Phenomena.TenseAspect.Studies.Egressy2026.japanese_no_sot (ct : HungarianComplementType) : Minimalism.Tense.AgreeSOT.readingsByStage japaneseStage (complementTypeToSize ct) = [Semantics.Tense.EmbeddedTenseReading.shifted]

The temporal adverb előző nap 'the day before' forces the shifted reading. In hogy-CP complements (where only shifted is available), this is compatible. In bare TP complements (where both readings are available), it selects the shifted reading. This provides independent evidence that the CP complement really does lack the simultaneous reading, rather than there being some other blocking effect.

theorem Phenomena.TenseAspect.Studies.Egressy2026.elozo_nap_compat_hogyCP : Fragments.Hungarian.TemporalDeictic.elozo_nap.forcesShifted = true ∧ (complementTypeToSize HungarianComplementType.hogyCP).transparentToTenseAgree = false

előző nap is compatible with hogy-CP (shifted-only) complements, because it itself forces the shifted reading.

theorem Phenomena.TenseAspect.Studies.Egressy2026.aznap_diagnoses_bareTP : Fragments.Hungarian.TemporalDeictic.aznap.compatSimultaneous = true ∧ (complementTypeToSize HungarianComplementType.bareTP).transparentToTenseAgree = true

aznap 'that day' can diagnose the simultaneous reading in bare TP, because it is compatible with both readings.

theorem Phenomena.TenseAspect.Studies.Egressy2026.akkor_shifts : Fragments.Hungarian.TemporalDeictic.akkor.shiftsPerspective = true

Hungarian akkor 'then' shifts perspective, like all cross-linguistic "then" adverbs.

@cite{egressy-2026} uses the definite/indefinite conjugation split as independent evidence for complement size. hogy-CP triggers definite conjugation; bare complements may allow indefinite.

The fragment entries record both conjugation forms, so we can verify
that the matrix verb forms in the data entries are the expected
conjugation type. 

theorem Phenomena.TenseAspect.Studies.Egressy2026.hogyCP_uses_definite_conjugation : pastUnderPast_hogyCP_tudta.matrixVerb = Fragments.Hungarian.Predicates.tud.formPastDef ∧ pastUnderPast_hogyCP_mondta.matrixVerb = Fragments.Hungarian.Predicates.mond.formPastDef ∧ pastUnderPast_hogyCP_hitte.matrixVerb = Fragments.Hungarian.Predicates.hisz.formPastDef

All hogy-CP judgments use the definite conjugation past form.