Paape & Vasishth (2026) @cite{paape-vasishth-2026}

Context ameliorates but does not eliminate garden-pathing: Novel insights from latent-process modeling. Journal of Memory and Language 148, 104748.

Overview

The paper replicates @cite{altmann-garnham-dennis-1992}'s CC/RC × referential context design (3×2: {amb-CC, amb-RC, unamb-RC} × {unique, non-unique referents}) with N = 319 using masked bidirectional self-paced reading (BSPR). The central contribution is a multinomial processing tree (MPT) model that decomposes reading time distributions into latent cognitive processes: attention, first-pass attachment (garden-pathing), optional triage, covert/overt reanalysis, and success/failure.

Key Findings

The MPT decomposition yields three conclusions (p. 11) unavailable from standard factorial comparison of means:

I. Regardless of context, RC disambiguation results in a higher probability of garden-pathing (choosing an incorrect first-pass parse). II. Contextual match decreases but does not eliminate the first-pass anti-RC bias. III. The cost of in-situ reanalysis is higher for RC than for CC disambiguation, and is lower but still non-zero in cases of context match versus mismatch.

MPT vs. Surprisal

The no-triage MPT outperforms LLM surprisal-based models (GPT-2, LLaMA-2, Mistral, Falcon) and standard factorial models in cross-validated predictive fit (PSIS-LOO elpd). The key architectural difference: the MPT assumes reading times at disambiguation are mixture distributions — bimodal with garden-pathed (slow) and non-garden-pathed (fast) components. Surprisal-based models assume unimodal distributions shifted by surprisal value, which cannot capture this bimodality (@cite{van-schijndel-linzen-2021}, @cite{huang-etal-2024}).

Connections

• Basic.lean: Reuses Disambiguation, ReferentialContext, Condition, disambiguationProfile, rc_pareto_harder
• Core.ProcessingModel: Ordinal profile bridge (§ 7)
• Theories/Semantics/Lexical/Determiner/Definite.lean: Uniqueness presupposition of the_uniq grounds the context manipulation — bare definites fail uniqueness in non-unique contexts, motivating RC modifiers (§ 9)
• Phenomena/Reference/Studies/SedivyEtAl1999.lean: Shared mechanism — modifier informativity given a contrast set drives both contrastive inference (Sedivy) and context-sensitive attachment (§ 9)

MPT Structure (Fig. 1)

The MPT models each trial as a cascade of probabilistic binary decisions. Each path through the tree yields a distinct combination of processing stages and a corresponding reading time distribution.

The full MPT includes a triage path (garden-pathed readers sometimes reject immediately without reanalysis). The best-fitting model variant (no-triage MPT) drops this path, but we include it in the type for completeness.

inductive Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.TrialOutcome : Type

Outcome of a single trial through the processing cascade.

Each constructor corresponds to a leaf node in the MPT (Fig. 1), determining which processing costs accumulate and whether the sentence is ultimately accepted or rejected.

• inattentive : TrialOutcome

  Inattentive trial: biased guess (accept with p_bias ≈ 0.79). Fast reading time, no garden-path processing.

• correctFirstPass : TrialOutcome

  Attentive, correct first-pass parse: no garden-pathing.

• triage : TrialOutcome

  Garden-pathed, triaged: reader rejects immediately without attempting reanalysis. Present in the full MPT but dropped in the best-fitting no-triage variant.

• overtSuccess : TrialOutcome

  Garden-pathed, overt reanalysis (regression to earlier material), reanalysis succeeds.

• overtFail : TrialOutcome

  Garden-pathed, overt reanalysis (regression), fails → reject.

• covertImmediateSuccess : TrialOutcome

  Garden-pathed, covert (in-situ) reanalysis, immediate, succeeds.

• covertImmediateFail : TrialOutcome

  Garden-pathed, covert reanalysis, immediate, fails → reject.

• covertPostponedSuccess : TrialOutcome

  Garden-pathed, covert reanalysis, postponed to spillover, succeeds.

• covertPostponedFail : TrialOutcome

  Garden-pathed, covert reanalysis, postponed to spillover, fails → reject.

instance Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instDecidableEqTrialOutcome : DecidableEq TrialOutcome

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instDecidableEqTrialOutcome x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprTrialOutcome : Repr TrialOutcome

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprTrialOutcome = { reprPrec := Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprTrialOutcome.repr }

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprTrialOutcome.repr : TrialOutcome → ℕ → Std.Format

Equations

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

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqTrialOutcome.beq : TrialOutcome → TrialOutcome → Bool

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqTrialOutcome.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqTrialOutcome : BEq TrialOutcome

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqTrialOutcome = { beq := Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqTrialOutcome.beq }

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.TrialOutcome.isGardenPathed : TrialOutcome → Bool

Whether a trial outcome involves garden-pathing.

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.TrialOutcome.inattentive.isGardenPathed = false
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.TrialOutcome.correctFirstPass.isGardenPathed = false
• x✝.isGardenPathed = true

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.TrialOutcome.accepted : TrialOutcome → Bool

Whether a trial outcome results in sentence acceptance.

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.TrialOutcome.inattentive.accepted = true
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.TrialOutcome.correctFirstPass.accepted = true
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.TrialOutcome.covertImmediateSuccess.accepted = true
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.TrialOutcome.covertPostponedSuccess.accepted = true
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.TrialOutcome.overtSuccess.accepted = true
• x✝.accepted = false

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.TrialOutcome.hasRegression : TrialOutcome → Bool

Whether a trial outcome involves a first-pass regression (rereading earlier material). In the MPT, regressions occur only on the overt reanalysis path. Covert reanalysis is signaled by in-situ reading slowdown, not regression.

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.TrialOutcome.overtSuccess.hasRegression = true
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.TrialOutcome.overtFail.hasRegression = true
• x✝.hasRegression = false

Process Probabilities

Each branching node in the MPT has a probability parameter. Some parameters are affected by the experimental manipulation; the predictor structure is:

• p_gp ~ context + disambiguation + context : disambiguation
• p_covert_success ~ disambiguation + match
• p_overt_success ~ disambiguation + match
• covert_reanalysis_cost ~ disambiguation + match

Parameters p_attentive, p_covert, p_postpone can vary between participants but are not assumed to vary by condition.

Estimated via Bayesian inference in Stan (4 MCMC chains × 2000 iterations, 1000 burn-in each).

structure Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.MPTParams : Type

The probability parameters of the MPT model. Values are stored as percentages (0–100).

• pAttentive : ℕ
• pGardenPath : ℕ
• pCovert : ℕ
• pPostpone : ℕ
• pCovertSuccess : ℕ
• pOvertSuccess : ℕ

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprMPTParams.repr : MPTParams → ℕ → Std.Format

Equations

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

instance Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprMPTParams : Repr MPTParams

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprMPTParams = { reprPrec := Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprMPTParams.repr }

Study Design

Replication of @cite{altmann-garnham-dennis-1992} with N = 319 English speakers (Prolific) via masked BSPR with end-of-sentence acceptability judgments. 36 stimulus sentences adapted from the original (replacing told with varied verbs per @cite{staub-etal-2018}), crossed with 2-level context (unique vs. non-unique referents).

inductive Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ExpCondition : Type

Experimental conditions in the 3 × 2 design.

• ambCC_unique : ExpCondition
• ambCC_nonUnique : ExpCondition
• ambRC_unique : ExpCondition
• ambRC_nonUnique : ExpCondition
• unambRC_unique : ExpCondition
• unambRC_nonUnique : ExpCondition

instance Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instDecidableEqExpCondition : DecidableEq ExpCondition

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instDecidableEqExpCondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprExpCondition.repr : ExpCondition → ℕ → Std.Format

Equations

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

instance Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprExpCondition : Repr ExpCondition

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprExpCondition = { reprPrec := Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprExpCondition.repr }

instance Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqExpCondition : BEq ExpCondition

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqExpCondition = { beq := Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqExpCondition.beq }

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqExpCondition.beq : ExpCondition → ExpCondition → Bool

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqExpCondition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ExpCondition.toCondition : ExpCondition → Condition

Map experimental conditions to the abstract Condition type.

Equations

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

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ambRC_nonUnique_matches : ExpCondition.ambRC_nonUnique.toCondition.isMatch = true

Matching conditions verified.

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ambCC_unique_matches : ExpCondition.ambCC_unique.toCondition.isMatch = true

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ambRC_unique_mismatches : ExpCondition.ambRC_unique.toCondition.isMatch = false

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ambCC_nonUnique_mismatches : ExpCondition.ambCC_nonUnique.toCondition.isMatch = false

Bayesian Analysis Results

Standard Bayesian linear mixed-effects analysis using brms, with sum contrasts for CONTEXT (unique = −1, non-unique = +1) and treatment contrasts for DISAMBIGUATION (amb-RC = baseline). Lognormal likelihood for first-pass reading times (FPRT), Bernoulli for first-pass regressions.

BF10 values > 3 indicate evidence for the alternative hypothesis. We record the critical region effects, which are the earliest measures potentially affected by garden-pathing.

structure Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.CriticalRegionBF : Type

Bayes factor (BF10) for key effects at the critical disambiguating region. BF10 > 3 indicates evidence; values >1000 are decisive.

• label : String
• bf10 : ℕ

instance Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprCriticalRegionBF : Repr CriticalRegionBF

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprCriticalRegionBF = { reprPrec := Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprCriticalRegionBF.repr }

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprCriticalRegionBF.repr : CriticalRegionBF → ℕ → Std.Format

Equations

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

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.bayesianResults : List CriticalRegionBF

Key Bayesian analysis results from Table 2 (critical region).

Equations

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

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.all_effects_evidenced : (bayesianResults.all fun (x : CriticalRegionBF) => decide (x.bf10 > 3)) = true

All recorded Bayes factors exceed the evidence threshold of 3.

Parameter Estimates

The no-triage MPT model achieves the best cross-validated predictive fit (Fig. 6). The following estimates are approximate posterior medians from Fig. 8–10. The intercept corresponds to the mean probability in the ambiguous RC condition across matching and mismatching contexts.

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.baselineParams : MPTParams

Baseline MPT parameters (ambiguous RC, averaged over contexts). Approximate posterior medians from the no-triage model.

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.baselineParams = { pAttentive := 75, pGardenPath := 75, pCovert := 60, pPostpone := 25, pCovertSuccess := 85, pOvertSuccess := 60 }

Garden-Path Probability by Condition

Approximate cell estimates derived from the intercept + slope posteriors (Figs. 8–9). The slopes are on the logit scale; back-transformed estimates are approximate.

Key constraints from the paper (p. 8):

• Amb-RC average across contexts ≈ 75%
• Non-unique referents decrease RC GP by ~15 pp
• Non-unique referents increase CC GP by ~40 pp
• Unamb-RC is reduced by ~35 pp relative to amb-RC

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.gardenPathRate : ExpCondition → ℕ

Garden-path probability estimates (percent) by condition.

These are approximate back-transformed posterior medians for p_gp from the no-triage MPT model, constructed to satisfy the paper's stated constraints.

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.gardenPathRate Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ExpCondition.ambRC_unique = 82
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.gardenPathRate Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ExpCondition.ambRC_nonUnique = 67
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.gardenPathRate Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ExpCondition.ambCC_unique = 10
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.gardenPathRate Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ExpCondition.ambCC_nonUnique = 50
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.gardenPathRate Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ExpCondition.unambRC_unique = 45
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.gardenPathRate Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ExpCondition.unambRC_nonUnique = 35

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ambRC_averages_near_75 : (gardenPathRate ExpCondition.ambRC_unique + gardenPathRate ExpCondition.ambRC_nonUnique) / 2 = 74

Amb-RC cell estimates average to approximately 75%.

Finding I: RC always harder (p. 11)

"Regardless of context, RC disambiguation results in a higher probability of garden-pathing, that is, choosing an incorrect first-pass attachment."

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.finding_I_rc_harder_than_cc : gardenPathRate ExpCondition.ambRC_unique > gardenPathRate ExpCondition.ambCC_unique ∧ gardenPathRate ExpCondition.ambRC_nonUnique > gardenPathRate ExpCondition.ambCC_nonUnique

Finding II: Context reduces but does not eliminate (p. 11)

"Contextual match decreases but does not eliminate the first-pass anti-RC bias."

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.finding_II_context_reduces_rc : gardenPathRate ExpCondition.ambRC_nonUnique < gardenPathRate ExpCondition.ambRC_unique

Context reduces RC garden-pathing.

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.finding_II_not_eliminated : gardenPathRate ExpCondition.ambRC_nonUnique > gardenPathRate ExpCondition.ambCC_unique

Context does not eliminate RC garden-pathing — the rate with supporting context still far exceeds the CC baseline.

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.context_crossover : gardenPathRate ExpCondition.ambRC_nonUnique < gardenPathRate ExpCondition.ambRC_unique ∧ gardenPathRate ExpCondition.ambCC_nonUnique > gardenPathRate ExpCondition.ambCC_unique

Context × disambiguation crossover: non-unique referents help RC but hurt CC. This is the interaction predicted by the context-sensitive attachment hypothesis.

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.graded_context_sensitivity : gardenPathRate ExpCondition.ambRC_nonUnique < gardenPathRate ExpCondition.ambRC_unique ∧ gardenPathRate ExpCondition.ambRC_nonUnique > gardenPathRate ExpCondition.ambCC_nonUnique

The results support a graded version of context-sensitive attachment: context affects first-pass parsing (there IS an interaction), but the bias is not fully overridden (there IS a main effect of disambiguation). Neither hypothesis alone suffices.

Finding III: Reanalysis cost is separable (p. 11)

"The cost of in-situ reanalysis is higher for RC than for CC disambiguation, and is lower but still non-zero in cases of context–disambiguation match versus mismatch."

structure Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ProcessingCosts : Type

Processing cost structure from posterior estimates (Fig. 10). All values in milliseconds.

• gardenPathCost : ℕ
• attentionCost : ℕ
• regressionCost : ℕ
• covertReanalysisCost : ℕ

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprProcessingCosts.repr : ProcessingCosts → ℕ → Std.Format

Equations

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

instance Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprProcessingCosts : Repr ProcessingCosts

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprProcessingCosts = { reprPrec := Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprProcessingCosts.repr }

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.rcCosts : ProcessingCosts

Baseline costs for RC disambiguation (intercept posteriors, Fig. 10).

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.rcCosts = { gardenPathCost := 15, attentionCost := 5, regressionCost := 275, covertReanalysisCost := 400 }

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ccCosts : ProcessingCosts

CC disambiguation costs: covert reanalysis is ~150–200ms cheaper than RC (Fig. 10 CC vs RC slope centered around -150 to -200ms).

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ccCosts = { gardenPathCost := 15, attentionCost := 5, regressionCost := 275, covertReanalysisCost := 225 }

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.finding_III_rc_costlier : rcCosts.covertReanalysisCost > ccCosts.covertReanalysisCost

Finding III: RC covert reanalysis is costlier than CC.

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.finding_III_cc_still_costly : ccCosts.covertReanalysisCost > 0

Finding III (second part): covert reanalysis cost is non-trivial even for CC disambiguation (i.e., still non-zero).

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.gp_cost_small_relative_to_reanalysis : rcCosts.gardenPathCost * 10 < rcCosts.covertReanalysisCost

Pure garden-pathing cost is small relative to reanalysis cost. This is a key MPT insight: the cost of being garden-pathed is tiny; the cost comes from reanalysis.

Why the MPT outperforms surprisal

Surprisal theory (@cite{hale-2001}, @cite{levy-2008}) predicts that processing difficulty is proportional to the negative log probability of a word in context. For garden-path sentences, surprisal at the disambiguating region should be higher for less expected continuations.

The MPT outperforms all four LLM surprisal models and the standard factorial model in cross-validated predictive fit. The key architectural difference is the mixture assumption: reading times at disambiguation are generated by a mixture of latent populations (garden-pathed vs. not), each with distinct cost distributions. Single-stage surprisal models predict a unimodal distribution shifted by the surprisal value.

This is structurally analogous to the limitation identified by @cite{van-schijndel-linzen-2021} and @cite{huang-etal-2024}: single-stage surprisal models underestimate the magnitude of garden-path effects because they lack a distinct, costly reanalysis mechanism.

inductive Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ModelVariant : Type

Model rankings from cross-validated predictive fit (PSIS-LOO elpd, Fig. 6). Higher rank = better fit. Rank 1 = best.

The ranking shows that even the simplest MPT model (mpt-simple) outperforms the best surprisal model, and adding an inattention component to a factorial model (factorial-inattention) only barely exceeds mpt-simple.

• factorial : ModelVariant
• factorialInattention : ModelVariant
• gpt2Surprisal : ModelVariant
• llamaSurprisal : ModelVariant
• mistralSurprisal : ModelVariant
• falconSurprisal : ModelVariant
• gpt2Inattention : ModelVariant
• mptSimple : ModelVariant
• mptNoTriage : ModelVariant
• mptFull : ModelVariant

instance Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instDecidableEqModelVariant : DecidableEq ModelVariant

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instDecidableEqModelVariant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprModelVariant.repr : ModelVariant → ℕ → Std.Format

Equations

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

instance Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprModelVariant : Repr ModelVariant

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprModelVariant = { reprPrec := Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprModelVariant.repr }

instance Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqModelVariant : BEq ModelVariant

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqModelVariant = { beq := Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqModelVariant.beq }

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqModelVariant.beq : ModelVariant → ModelVariant → Bool

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqModelVariant.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.modelRank : ModelVariant → ℕ

Cross-validated predictive fit ranking (1 = best).

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.modelRank Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ModelVariant.mptNoTriage = 1
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.modelRank Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ModelVariant.mptFull = 2
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.modelRank Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ModelVariant.mptSimple = 3
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.modelRank Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ModelVariant.gpt2Inattention = 4
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.modelRank Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ModelVariant.factorialInattention = 5
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.modelRank Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ModelVariant.falconSurprisal = 6
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.modelRank Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ModelVariant.mistralSurprisal = 7
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.modelRank Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ModelVariant.llamaSurprisal = 8
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.modelRank Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ModelVariant.gpt2Surprisal = 9
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.modelRank Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.ModelVariant.factorial = 10

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.mpt_beats_surprisal : modelRank ModelVariant.mptSimple < modelRank ModelVariant.gpt2Surprisal ∧ modelRank ModelVariant.mptSimple < modelRank ModelVariant.llamaSurprisal ∧ modelRank ModelVariant.mptSimple < modelRank ModelVariant.mistralSurprisal ∧ modelRank ModelVariant.mptSimple < modelRank ModelVariant.falconSurprisal

All MPT variants outperform all surprisal models.

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.noTriage_beats_full : modelRank ModelVariant.mptNoTriage < modelRank ModelVariant.mptFull

The no-triage variant beats the full MPT — triage is not needed.

From ordinal to quantitative

The ProcessingProfile from Core.ProcessingModel captures the ordinal claim that RC is harder than CC (see rc_pareto_harder in Basic.lean). The MPT explains this ordering by decomposing it into quantitative components: RC has higher garden-path probability, higher reanalysis cost, and lower reanalysis success rate. The ordinal profile is the observable consequence; the MPT is the latent mechanism.

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.mpt_consistent_with_pareto : gardenPathRate ExpCondition.ambRC_unique > gardenPathRate ExpCondition.ambCC_unique ∧ rcCosts.covertReanalysisCost > ccCosts.covertReanalysisCost

The MPT decomposition is consistent with the Pareto ordering: every quantitative measure points in the same direction.

Uniqueness presupposition grounds referential context

The experimental manipulation of referential context (unique vs. non-unique referents) is grounded in the uniqueness presupposition of definite descriptions (the_uniq in Theories/Semantics/Lexical/Determiner/Definite.lean).

In the non-unique condition (He was introduced to two women. He told the woman that...), a bare definite "the woman" fails uniqueness because two entities satisfy the restrictor. An RC modifier ("the woman that he'd risked his life for") intersects the restrictor with the RC predicate, narrowing to a single entity and rescuing uniqueness.

This makes the RC pragmatically necessary in non-unique contexts — the same mechanism underlying @cite{sedivy-etal-1999}'s contrastive inference: a modifier is informative when a contrast set is available. In Sedivy et al.'s visual-world paradigm, the contrast set is perceptual (tall glass vs. short glass); here, it is discourse-referential (woman₁ vs. woman₂). Both are instances of modifier informativity increasing with the availability of alternatives.

The argument chain:

1. the_uniq presupposes exactly one restrictor-satisfier
2. Non-unique context → presupposition fails for bare NP
3. RC modifier narrows restrictor → presupposition can succeed
4. Therefore RC is pragmatically licensed in non-unique contexts
5. This matches contextSupports .nonUniqueReferents .relativeClause = true
6. Parser is biased toward RC → less garden-pathing (Finding II)

inductive Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.DiscEntity : Type

Toy discourse entity for the uniqueness worked example.

• woman1 : DiscEntity
• woman2 : DiscEntity
• man : DiscEntity

instance Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instDecidableEqDiscEntity : DecidableEq DiscEntity

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instDecidableEqDiscEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqDiscEntity.beq : DiscEntity → DiscEntity → Bool

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqDiscEntity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqDiscEntity : BEq DiscEntity

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqDiscEntity = { beq := Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqDiscEntity.beq }

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprDiscEntity.repr : DiscEntity → ℕ → Std.Format

Equations

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

instance Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprDiscEntity : Repr DiscEntity

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprDiscEntity = { reprPrec := Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprDiscEntity.repr }

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.nonUniqueDomain : List DiscEntity

Non-unique context domain: a man and two women.

Equations

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

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.uniqueDomain : List DiscEntity

Unique context domain: a man and one woman.

Equations

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

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.isWoman : DiscEntity → Bool

Restrictor predicate: "woman".

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.isWoman Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.DiscEntity.woman1 = true
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.isWoman Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.DiscEntity.woman2 = true
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.isWoman Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.DiscEntity.man = false

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.rcModifier : DiscEntity → Bool

RC modifier predicate: "that he'd risked his life for".

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.rcModifier Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.DiscEntity.woman1 = true
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.rcModifier x✝ = false

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.toldScope : DiscEntity → Bool

Trivial scope for the worked example.

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.toldScope x✝ = true

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.bare_fails_nonunique : (Semantics.Lexical.Determiner.Definite.the_uniq nonUniqueDomain isWoman toldScope).presup () = false

In non-unique context, bare "the woman" FAILS uniqueness: two entities satisfy the restrictor, so the presupposition of the_uniq is not met.

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.modified_succeeds_nonunique : (Semantics.Lexical.Determiner.Definite.the_uniq nonUniqueDomain (fun (e : DiscEntity) => isWoman e && rcModifier e) toldScope).presup () = true

In non-unique context, modified "the woman that he'd risked his life for" SUCCEEDS: the RC modifier narrows to one entity.

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.bare_succeeds_unique : (Semantics.Lexical.Determiner.Definite.the_uniq uniqueDomain isWoman toldScope).presup () = true

In unique context, bare "the woman" already SUCCEEDS: only one entity satisfies the restrictor, so no modifier needed.

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.uniqueness_grounds_context_supports : (Semantics.Lexical.Determiner.Definite.the_uniq nonUniqueDomain isWoman toldScope).presup () = false ∧ (Semantics.Lexical.Determiner.Definite.the_uniq nonUniqueDomain (fun (e : DiscEntity) => isWoman e && rcModifier e) toldScope).presup () = true ∧ contextSupports ReferentialContext.nonUniqueReferents Disambiguation.relativeClause = true ∧ (Semantics.Lexical.Determiner.Definite.the_uniq uniqueDomain isWoman toldScope).presup () = true ∧ contextSupports ReferentialContext.uniqueReferent Disambiguation.complementClause = true

The full argument chain: uniqueness presupposition grounds contextSupports from Basic.lean.

1. Non-unique context → bare definite fails → RC modifier needed
2. This is exactly contextSupports .nonUniqueReferents .relativeClause
3. Unique context → bare definite succeeds → no modifier needed
4. This is exactly contextSupports .uniqueReferent .complementClause

Shared mechanism with contrastive inference

modifierNecessary (defined in Definite.lean) captures the abstract predicate: a modifier rescues a failed uniqueness presupposition. Both Paape & Vasishth's context-sensitive attachment and @cite{sedivy-etal-1999}'s contrastive inference are instances of the same predicate — the modifier type differs (RC vs. scalar adjective) but the referential mechanism is identical.

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.pv_modifier_necessary : Semantics.Lexical.Determiner.Definite.modifierNecessary nonUniqueDomain isWoman rcModifier = true

In non-unique context, the RC modifier is referentially necessary: bare "the woman" is ambiguous, modified "the woman that P" is unique.

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.pv_modifier_unnecessary : Semantics.Lexical.Determiner.Definite.modifierNecessary uniqueDomain isWoman rcModifier = false

In unique context, the RC modifier is unnecessary: bare "the woman" already uniquely identifies.

inductive Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.SedivyEntity : Type

Toy visual-world entity for the @cite{sedivy-etal-1999} scenario.

• tallGlass : SedivyEntity
• shortGlass : SedivyEntity
• ball : SedivyEntity
• key : SedivyEntity

instance Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instDecidableEqSedivyEntity : DecidableEq SedivyEntity

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instDecidableEqSedivyEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqSedivyEntity.beq : SedivyEntity → SedivyEntity → Bool

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqSedivyEntity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqSedivyEntity : BEq SedivyEntity

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqSedivyEntity = { beq := Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instBEqSedivyEntity.beq }

instance Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprSedivyEntity : Repr SedivyEntity

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprSedivyEntity = { reprPrec := Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprSedivyEntity.repr }

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.instReprSedivyEntity.repr : SedivyEntity → ℕ → Std.Format

Equations

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

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.contrastDisplay : List SedivyEntity

Contrast display: two glasses (tall and short) plus distractors.

Equations

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

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.noContrastDisplay : List SedivyEntity

No-contrast display: one glass plus distractors.

Equations

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

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.isGlass : SedivyEntity → Bool

Restrictor predicate: "glass".

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.isGlass Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.SedivyEntity.tallGlass = true
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.isGlass Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.SedivyEntity.shortGlass = true
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.isGlass x✝ = false

def Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.isTall : SedivyEntity → Bool

Modifier predicate: "tall".

Equations

• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.isTall Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.SedivyEntity.tallGlass = true
• Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.isTall x✝ = false

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.sedivy_modifier_necessary : Semantics.Lexical.Determiner.Definite.modifierNecessary contrastDisplay isGlass isTall = true

With a contrast set (two glasses), "tall" is referentially necessary: bare "the glass" is ambiguous, "the tall glass" is unique.

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.sedivy_modifier_unnecessary : Semantics.Lexical.Determiner.Definite.modifierNecessary noContrastDisplay isGlass isTall = false

Without a contrast set (one glass), "tall" is unnecessary: bare "the glass" already uniquely identifies.

theorem Phenomena.SyntacticAmbiguity.Studies.PaapeVasishth2026.shared_mechanism : Semantics.Lexical.Determiner.Definite.modifierNecessary nonUniqueDomain isWoman rcModifier = true ∧ Semantics.Lexical.Determiner.Definite.modifierNecessary contrastDisplay isGlass isTall = true ∧ Semantics.Lexical.Determiner.Definite.modifierNecessary uniqueDomain isWoman rcModifier = false ∧ Semantics.Lexical.Determiner.Definite.modifierNecessary noContrastDisplay isGlass isTall = false

Structural identity: the same modifierNecessary predicate governs both phenomena. When alternatives are available, the modifier is necessary; when the referent is already unique, the modifier is redundant. The modifier type is irrelevant — RC (Paape & Vasishth) and scalar adjective (Sedivy et al.) behave identically at this level of abstraction.