Türk & Hirsch (2026) — Category Match constrains polar question alternatives

[TH26] [Atl23] [FK11] [Roo92]

Connects the empirical judgments in TurkHirsch2026.Examples (modal answers are infelicitous to Turkish polar questions) to the formal explanation [TH26] propose: [FK11] category match over UPOS tags applied to the focus alternatives evoked by the polarity head Σ_F that hosts Turkish mI.

The puzzle

Following [Atl23]'s bidimensional analysis, Turkish mI heads PolP and bears focus (Σ_F). Under [Roo92]-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 (Σ = id, NEG = pnot) 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 TurkHirsch2026.PolarWorld : Type

Four worlds crossing Ali-sleeps with deontic-must.

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

@[implicit_reducible]

instance TurkHirsch2026.instDecidableEqPolarWorld : DecidableEq PolarWorld

Equations

• TurkHirsch2026.instDecidableEqPolarWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def TurkHirsch2026.instReprPolarWorld.repr : PolarWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance TurkHirsch2026.instReprPolarWorld : Repr PolarWorld

Equations

• TurkHirsch2026.instReprPolarWorld = { reprPrec := TurkHirsch2026.instReprPolarWorld.repr }

def TurkHirsch2026.allWorlds : List PolarWorld

Equations

• TurkHirsch2026.allWorlds = [TurkHirsch2026.PolarWorld.sleeps_must, TurkHirsch2026.PolarWorld.sleeps_free, TurkHirsch2026.PolarWorld.nosleep_must, TurkHirsch2026.PolarWorld.nosleep_free]

def TurkHirsch2026.p : Set PolarWorld

p = "Ali sleeps": holds at the worlds where Ali sleeps.

Equations

• TurkHirsch2026.p = {TurkHirsch2026.PolarWorld.sleeps_must, TurkHirsch2026.PolarWorld.sleeps_free}

def TurkHirsch2026.notP : Set PolarWorld

¬p = "Ali doesn't sleep". Set complement of p.

Equations

• TurkHirsch2026.notP = TurkHirsch2026.pᶜ

Deontic must, grounded in [Kra77]'s premise-set semantics.

The deontic source maps each world to the propositions encoding the
deontic obligations in force at that world. In the *_must worlds the
obligation "Ali sleeps" is in force; in the *_free worlds nothing is.
`mustP` is then the Bool reflection of `mustInView deonticBase pProp` —
no longer a stipulated 4-row table. 

def TurkHirsch2026.pProp : PolarWorld → Prop

Prop view of p for use with the polymorphic Kratzer machinery (which lives at type Index → Prop). Just set membership.

Equations

• TurkHirsch2026.pProp w = (w ∈ TurkHirsch2026.p)

def TurkHirsch2026.deonticBase : PolarWorld → List (PolarWorld → Prop)

The deontic premise set: in must-worlds the obligation pProp is in force; in free-worlds the premise set is empty.

Equations

• TurkHirsch2026.deonticBase TurkHirsch2026.PolarWorld.sleeps_must = [TurkHirsch2026.pProp]
• TurkHirsch2026.deonticBase TurkHirsch2026.PolarWorld.nosleep_must = [TurkHirsch2026.pProp]
• TurkHirsch2026.deonticBase TurkHirsch2026.PolarWorld.sleeps_free = []
• TurkHirsch2026.deonticBase TurkHirsch2026.PolarWorld.nosleep_free = []

def TurkHirsch2026.mustGrounded (w : PolarWorld) : Prop

Kratzer-grounded deontic must: □p as [Kra77] Def 5 (mustInView) over the deontic premise set.

Equations

• TurkHirsch2026.mustGrounded w = Intensional.Premise.mustInView TurkHirsch2026.deonticBase TurkHirsch2026.pProp w

def TurkHirsch2026.mustP : Set PolarWorld

□p = "Ali must sleep" (deontic necessity). The Set reflection of mustGrounded; equivalence proved by mustP_iff_mustGrounded.

Equations

• TurkHirsch2026.mustP = {TurkHirsch2026.PolarWorld.sleeps_must, TurkHirsch2026.PolarWorld.nosleep_must}

theorem TurkHirsch2026.mustP_iff_mustGrounded (w : PolarWorld) : w ∈ mustP ↔ mustGrounded w

The stipulated table matches the Kratzer-grounded derivation. The over-generation argument below is therefore about a genuine modal proposition, not a hand-tuned function.

structure TurkHirsch2026.TaggedDen (α : Type) : Type

A denotation tagged with its UD UPOS category. Study-internal utility used to model [TH26]'s claim that mI's PART tag licenses only PART-tagged alternatives.

• cat : UD.UPOS
• den : α

@[implicit_reducible]

instance TurkHirsch2026.instReprTaggedDen {α✝ : Type} [Repr α✝] : Repr (TaggedDen α✝)

Equations

• TurkHirsch2026.instReprTaggedDen = { reprPrec := TurkHirsch2026.instReprTaggedDen.repr }

def TurkHirsch2026.instReprTaggedDen.repr {α✝ : Type} [Repr α✝] : TaggedDen α✝ → ℕ → Std.Format

Equations

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

def TurkHirsch2026.opLexicon : List (TaggedDen (Set PolarWorld))

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

• TurkHirsch2026.opLexicon = [{ cat := UD.UPOS.PART, den := TurkHirsch2026.p }, { cat := UD.UPOS.PART, den := TurkHirsch2026.notP }, { cat := UD.UPOS.AUX, den := TurkHirsch2026.mustP }]

def TurkHirsch2026.typeTheoAlternatives : List (Set PolarWorld)

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

Equations

• TurkHirsch2026.typeTheoAlternatives = List.map (fun (x : TurkHirsch2026.TaggedDen (Set TurkHirsch2026.PolarWorld)) => x.den) TurkHirsch2026.opLexicon

def TurkHirsch2026.catMatchAlternatives : List (Set PolarWorld)

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

Equations

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

def TurkHirsch2026.typeTheoQ : Semantics.Focus.Interpretation.PropFocusValue PolarWorld

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

Equations

• TurkHirsch2026.typeTheoQ = {q : Set TurkHirsch2026.PolarWorld | q ∈ TurkHirsch2026.typeTheoAlternatives}

def TurkHirsch2026.catMatchQ : Semantics.Focus.Interpretation.PropFocusValue PolarWorld

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

Equations

• TurkHirsch2026.catMatchQ = {q : Set TurkHirsch2026.PolarWorld | q ∈ TurkHirsch2026.catMatchAlternatives}

def TurkHirsch2026.polarQ : Semantics.Focus.Interpretation.PropFocusValue PolarWorld

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

Equations

• TurkHirsch2026.polarQ = {TurkHirsch2026.p, TurkHirsch2026.notP}

theorem TurkHirsch2026.catMatch_eq_polar : catMatchQ = polarQ

Category-matched question = standard polar question. [FK11]'s category match yields the correct {p, ¬p} partition. catMatchAlternatives filters opLexicon to [p, notP], and the resulting set-of-alternatives equals the polar {p, notP} literal.

theorem TurkHirsch2026.typeTheo_admits_modal : mustP ∈ typeTheoQ

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

theorem TurkHirsch2026.polar_rejects_modal : mustP ∉ polarQ

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 TurkHirsch2026.catMatch_rejects_modal : mustP ∉ catMatchQ

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

theorem TurkHirsch2026.typeTheo_ne_polar : typeTheoQ ≠ polarQ

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

Connect the empirical judgments from TurkHirsch2026.Examples 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 TurkHirsch2026.data_modal_infelicitous : Examples.polar_must.judgment = Features.Judgment.unacceptable

The empirical datum: the deontic modal answer ("Ali uyumalı" to "Ali uyuyor mu?") is unacceptable.

theorem TurkHirsch2026.theory_modal_excluded : mustP ∉ catMatchQ

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

theorem TurkHirsch2026.theory_overgen_without_catmatch : mustP ∈ typeTheoQ

The theory would wrongly predict felicity without category match.

Following [Roo92], 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-hirsch-2026]'s contribution is showing that this over-generates
for Turkish polar questions, and that category match ([fox-katzir-2011])
is the correct constraint on alternative computation when the focus host
is Σ_F. 

def TurkHirsch2026.applyFoC_typeTheo : Alternatives.AltMeaning (Set PolarWorld)

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

Equations

• TurkHirsch2026.applyFoC_typeTheo = { oValue := TurkHirsch2026.p, aValue := TurkHirsch2026.typeTheoAlternatives }

theorem TurkHirsch2026.applyFoC_typeTheo_aSet : applyFoC_typeTheo.aSet = typeTheoQ

The two carriers agree definitionally: the type-theoretic [FoC] A-value as a set is the type-theoretic question.

theorem TurkHirsch2026.applyFoC_is_typeTheo : mustP ∈ applyFoC_typeTheo.aSet

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

def TurkHirsch2026.applyFoC_catMatch : Alternatives.AltMeaning (Set PolarWorld)

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

Equations

• TurkHirsch2026.applyFoC_catMatch = { oValue := TurkHirsch2026.p, aValue := TurkHirsch2026.catMatchAlternatives }

theorem TurkHirsch2026.applyFoC_catMatch_aSet : applyFoC_catMatch.aSet = catMatchQ

The two carriers agree definitionally on the category-matched side as well.

theorem TurkHirsch2026.categoryMatch_fixes_applyFoC : mustP ∉ applyFoC_catMatch.aSet

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

The fragment exposes only theory-neutral lexical primitives. Here we add the theory-specific tagging that [TH26]'s analysis requires: a UPOS label (for [FK11] category match) and a Head label (for [Lak90]-style PolP). These commitments live in the study file, not the fragment, so the fragment stays reusable across syntactic theories.

inductive TurkHirsch2026.Head : Type

Polarity-head labels assumed by this study (Laka-style ΣP/NEGP). Lean reserves Σ for sigma types, so the affirmative head's Lean-side identifier is affirm (the linguistic name "Σ" is preserved in docstrings).

• affirm : Head

  Affirmative polarity head (Laka's Σ).

• neg : Head

  Negation polarity head.

@[implicit_reducible]

instance TurkHirsch2026.instDecidableEqHead : DecidableEq Head

Equations

• TurkHirsch2026.instDecidableEqHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance TurkHirsch2026.instReprHead : Repr Head

Equations

• TurkHirsch2026.instReprHead = { reprPrec := TurkHirsch2026.instReprHead.repr }

def TurkHirsch2026.instReprHead.repr : Head → ℕ → Std.Format

Equations

• TurkHirsch2026.instReprHead.repr TurkHirsch2026.Head.affirm prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TurkHirsch2026.Head.affirm")).group prec✝
• TurkHirsch2026.instReprHead.repr TurkHirsch2026.Head.neg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TurkHirsch2026.Head.neg")).group prec✝

def TurkHirsch2026.Head.toOp : Head → (PolarWorld → Prop) → PolarWorld → Prop

The bare semantic operator each head spells out.

Equations

• TurkHirsch2026.Head.affirm.toOp = Semantics.Polarity.affirm TurkHirsch2026.PolarWorld
• TurkHirsch2026.Head.neg.toOp = Semantics.Polarity.neg TurkHirsch2026.PolarWorld

structure TurkHirsch2026.MiAnalysis : Type

This study's commitments about Turkish mI.

• head : Head

  Which polarity head mI spells out (Σ in [Atl23]).

• upos : UD.UPOS

  UPOS tag used by [FK11] category match.

def TurkHirsch2026.miAnalysis : MiAnalysis

The [TH26] / [Atl23] analysis: mI is Σ and tagged PART.

Equations

• TurkHirsch2026.miAnalysis = { head := TurkHirsch2026.Head.affirm, upos := UD.UPOS.PART }

theorem TurkHirsch2026.mi_denotation_matches_head : Turkish.QuestionParticles.mi.denotation = miAnalysis.head.toOp

mI's lexical denotation matches the operator its analyzed head spells out — a definitional consistency check between the fragment entry and the head analysis adopted here.

theorem TurkHirsch2026.mi_category_matches : miAnalysis.upos = UD.UPOS.PART

The UPOS tag this study assigns to mI matches the category used in the alternative-restriction computation.