Turk, Hirsch & İnce (2026) — Category Match Bridge

@cite{fox-katzir-2011} @cite{kratzer-selkirk-2020} @cite{rooth-1992} @cite{turk-hirsch-2026}

Connects the empirical judgments in PolarAnswers.lean (modal answers are infelicitous to Turkish polar questions) to the formal explanation: @cite{fox-katzir-2011} category match over UPOS tags.

The Problem

Turkish mI heads PolP and bears focus (Σ_F). Under Rooth-style type-theoretic alternative computation, any operator of the same semantic type counts as an alternative — including deontic modals. This yields {p, ¬p, □p}, wrongly predicting □p is a felicitous answer.

The Fix

Category match restricts alternatives to items sharing mI's UPOS tag PART. Polarity operators (Σ, NEG) are PART; "must" is AUX. Category match yields {p, ¬p} — the correct polar question.

Scenario

Four worlds: Ali sleeps/doesn't × deontic must/free.

inductive Phenomena.Questions.Studies.TurkHirschInce2026.PolarWorld : Type

Four worlds crossing Ali-sleeps with deontic-must.

• sleeps_must : PolarWorld
• sleeps_free : PolarWorld
• nosleep_must : PolarWorld
• nosleep_free : PolarWorld

instance Phenomena.Questions.Studies.TurkHirschInce2026.instDecidableEqPolarWorld : DecidableEq PolarWorld

Equations

• Phenomena.Questions.Studies.TurkHirschInce2026.instDecidableEqPolarWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Questions.Studies.TurkHirschInce2026.instBEqPolarWorld.beq : PolarWorld → PolarWorld → Bool

Equations

• Phenomena.Questions.Studies.TurkHirschInce2026.instBEqPolarWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Questions.Studies.TurkHirschInce2026.instBEqPolarWorld : BEq PolarWorld

Equations

• Phenomena.Questions.Studies.TurkHirschInce2026.instBEqPolarWorld = { beq := Phenomena.Questions.Studies.TurkHirschInce2026.instBEqPolarWorld.beq }

def Phenomena.Questions.Studies.TurkHirschInce2026.instReprPolarWorld.repr : PolarWorld → ℕ → Std.Format

Equations

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

instance Phenomena.Questions.Studies.TurkHirschInce2026.instReprPolarWorld : Repr PolarWorld

Equations

• Phenomena.Questions.Studies.TurkHirschInce2026.instReprPolarWorld = { reprPrec := Phenomena.Questions.Studies.TurkHirschInce2026.instReprPolarWorld.repr }

def Phenomena.Questions.Studies.TurkHirschInce2026.allWorlds : List PolarWorld

Equations

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

def Phenomena.Questions.Studies.TurkHirschInce2026.p : PolarWorld → Bool

p = "Ali sleeps": true when Ali sleeps regardless of modality.

Equations

• Phenomena.Questions.Studies.TurkHirschInce2026.p Phenomena.Questions.Studies.TurkHirschInce2026.PolarWorld.sleeps_must = true
• Phenomena.Questions.Studies.TurkHirschInce2026.p Phenomena.Questions.Studies.TurkHirschInce2026.PolarWorld.sleeps_free = true
• Phenomena.Questions.Studies.TurkHirschInce2026.p Phenomena.Questions.Studies.TurkHirschInce2026.PolarWorld.nosleep_must = false
• Phenomena.Questions.Studies.TurkHirschInce2026.p Phenomena.Questions.Studies.TurkHirschInce2026.PolarWorld.nosleep_free = false

def Phenomena.Questions.Studies.TurkHirschInce2026.notP : PolarWorld → Bool

¬p = "Ali doesn't sleep".

Equations

• Phenomena.Questions.Studies.TurkHirschInce2026.notP Phenomena.Questions.Studies.TurkHirschInce2026.PolarWorld.sleeps_must = false
• Phenomena.Questions.Studies.TurkHirschInce2026.notP Phenomena.Questions.Studies.TurkHirschInce2026.PolarWorld.sleeps_free = false
• Phenomena.Questions.Studies.TurkHirschInce2026.notP Phenomena.Questions.Studies.TurkHirschInce2026.PolarWorld.nosleep_must = true
• Phenomena.Questions.Studies.TurkHirschInce2026.notP Phenomena.Questions.Studies.TurkHirschInce2026.PolarWorld.nosleep_free = true

def Phenomena.Questions.Studies.TurkHirschInce2026.mustP : PolarWorld → Bool

□p = "Ali must sleep" (deontic necessity).

Equations

• Phenomena.Questions.Studies.TurkHirschInce2026.mustP Phenomena.Questions.Studies.TurkHirschInce2026.PolarWorld.sleeps_must = true
• Phenomena.Questions.Studies.TurkHirschInce2026.mustP Phenomena.Questions.Studies.TurkHirschInce2026.PolarWorld.sleeps_free = false
• Phenomena.Questions.Studies.TurkHirschInce2026.mustP Phenomena.Questions.Studies.TurkHirschInce2026.PolarWorld.nosleep_must = true
• Phenomena.Questions.Studies.TurkHirschInce2026.mustP Phenomena.Questions.Studies.TurkHirschInce2026.PolarWorld.nosleep_free = false

def Phenomena.Questions.Studies.TurkHirschInce2026.opLexicon : List (Core.InformationStructure.CatItem (PolarWorld → Bool))

The lexicon of propositional operators at type ⟨⟨s,t⟩,t⟩. Polarity heads (Σ, NEG) are tagged PART; the deontic modal is AUX. This UPOS distinction is what category match exploits.

Equations

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

def Phenomena.Questions.Studies.TurkHirschInce2026.typeTheoAlternatives : List (PolarWorld → Bool)

Type-theoretic alternatives (Rooth D_τ): all operators regardless of UPOS → {p, ¬p, □p}. Over-generates.

Equations

• Phenomena.Questions.Studies.TurkHirschInce2026.typeTheoAlternatives = Core.InformationStructure.typeTheoAlts Phenomena.Questions.Studies.TurkHirschInce2026.opLexicon

def Phenomena.Questions.Studies.TurkHirschInce2026.catMatchAlternatives : List (PolarWorld → Bool)

Category-match alternatives: only PART-tagged operators → {p, ¬p}. Correct.

Equations

• Phenomena.Questions.Studies.TurkHirschInce2026.catMatchAlternatives = Core.InformationStructure.categoryMatchAlts UD.UPOS.PART Phenomena.Questions.Studies.TurkHirschInce2026.opLexicon

def Phenomena.Questions.Studies.TurkHirschInce2026.typeTheoQ : Semantics.Questions.Hamblin.QuestionDen PolarWorld

Type-theoretic question: {p, ¬p, □p} — over-generated.

Equations

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

def Phenomena.Questions.Studies.TurkHirschInce2026.catMatchQ : Semantics.Questions.Hamblin.QuestionDen PolarWorld

Category-match question: {p, ¬p} — correct.

Equations

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

def Phenomena.Questions.Studies.TurkHirschInce2026.polarQ : Semantics.Questions.Hamblin.QuestionDen PolarWorld

The expected polar question: {p, ¬p}.

Equations

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

theorem Phenomena.Questions.Studies.TurkHirschInce2026.catMatch_eq_polar : catMatchQ mustP = polarQ mustP ∧ catMatchQ p = polarQ p ∧ catMatchQ notP = polarQ notP

Category-matched question = standard polar question. Fox & Katzir's category match yields the correct {p, ¬p} partition.

theorem Phenomena.Questions.Studies.TurkHirschInce2026.typeTheo_ne_polar : typeTheoQ mustP ≠ polarQ mustP

Type-theoretic question ≠ polar question. The D_τ computation admits □p as an answer, which the polar question rejects.

theorem Phenomena.Questions.Studies.TurkHirschInce2026.typeTheo_admits_modal : Semantics.Questions.Hamblin.isAnswer typeTheoQ mustP = true

The spurious prediction: □p is an answer to the type-theoretic question. Under Rooth-style D_τ, "Ali must sleep" is predicted to be a felicitous answer to "Does Ali sleep?" — which is empirically wrong.

theorem Phenomena.Questions.Studies.TurkHirschInce2026.polar_rejects_modal : Semantics.Questions.Hamblin.isAnswer polarQ mustP = false

The correct prediction: □p is NOT an answer to the polar question. "Ali must sleep" is not a felicitous answer to a yes/no question about whether Ali sleeps.

theorem Phenomena.Questions.Studies.TurkHirschInce2026.catMatch_rejects_modal : Semantics.Questions.Hamblin.isAnswer catMatchQ mustP = false

Category match fixes the over-generation: □p is NOT an answer to the category-matched question.

Connect the empirical judgments from PolarAnswers.lean to the formal model. The data says modal answers are infelicitous; the theory (category match) explains why: □p is excluded from the Hamblin alternative set.

theorem Phenomena.Questions.Studies.TurkHirschInce2026.data_modal_infelicitous : PolarAnswers.turkishPolar_must.felicitous = false

The empirical datum: modal answer is infelicitous.

theorem Phenomena.Questions.Studies.TurkHirschInce2026.theory_modal_excluded : Semantics.Questions.Hamblin.isAnswer catMatchQ mustP = false

The theory predicts it: □p is not an answer under category match.

theorem Phenomena.Questions.Studies.TurkHirschInce2026.theory_overgen_without_catmatch : Semantics.Questions.Hamblin.isAnswer typeTheoQ mustP = true

The theory would wrongly predict felicity without category match.

The connection to @cite{kratzer-selkirk-2020} is via the A-value of a [FoC]-marked expression. In Rooth/K&S's framework, the A-value of a [FoC]-marked constituent is the set of alternatives of the same semantic type — i.e., exactly the type-theoretic D_τ computation.

Turk et al.'s contribution is showing that this over-generates for
Turkish polar questions, and that category match
is the correct constraint on alternative computation. 

def Phenomena.Questions.Studies.TurkHirschInce2026.applyFoC_typeTheo : Core.InformationStructure.AltMeaning (PolarWorld → Bool)

Applying [FoC] with type-theoretic A-value yields the over-generating set.

Equations

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

theorem Phenomena.Questions.Studies.TurkHirschInce2026.applyFoC_is_typeTheo : Semantics.Questions.Hamblin.fromAlternatives applyFoC_typeTheo.aValue allWorlds mustP = true

The type-theoretic A-value produces the wrong question denotation.

def Phenomena.Questions.Studies.TurkHirschInce2026.applyFoC_catMatch : Core.InformationStructure.AltMeaning (PolarWorld → Bool)

Restricting the A-value by category match corrects the prediction.

Equations

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

theorem Phenomena.Questions.Studies.TurkHirschInce2026.categoryMatch_fixes_applyFoC : Semantics.Questions.Hamblin.fromAlternatives applyFoC_catMatch.aValue allWorlds mustP = false

The category-matched A-value produces the correct question denotation.

theorem Phenomena.Questions.Studies.TurkHirschInce2026.mi_category_matches : Fragments.Turkish.QuestionParticles.mi.cat = UD.UPOS.PART

The Turkish mI particle's UPOS tag matches the category used in the category-match computation.