Documentation

Linglib.Phenomena.Focus.Studies.TurkHirsch2026

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

@cite{turk-hirsch-2026} @cite{atlamaz-2023} @cite{fox-katzir-2011} @cite{rooth-1992}

Connects the empirical judgments in PolarAnswers.lean (modal answers are infelicitous to Turkish polar questions) to the formal explanation @cite{turk-hirsch-2026} propose: @cite{fox-katzir-2011} category match over UPOS tags applied to the focus alternatives evoked by the polarity head Σ_F that hosts Turkish mI.

The puzzle #

Following @cite{atlamaz-2023}'s bidimensional analysis, Turkish mI heads PolP and bears focus (Σ_F). Under @cite{rooth-1992}-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.

source
inductive Phenomena.Focus.Studies.TurkHirsch2026.PolarWorld :
Type

Four worlds crossing Ali-sleeps with deontic-must.

Instances For
    source
    @[implicit_reducible]
    instance Phenomena.Focus.Studies.TurkHirsch2026.instDecidableEqPolarWorld :
    DecidableEq PolarWorld
    Equations
    source
    @[implicit_reducible]
    instance Phenomena.Focus.Studies.TurkHirsch2026.instReprPolarWorld :
    Repr PolarWorld
    Equations
    source
    def Phenomena.Focus.Studies.TurkHirsch2026.instReprPolarWorld.repr :
    PolarWorld → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Phenomena.Focus.Studies.TurkHirsch2026.allWorlds :
      List PolarWorld
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Phenomena.Focus.Studies.TurkHirsch2026.p :
        Set PolarWorld

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

        Equations
        Instances For
          source
          def Phenomena.Focus.Studies.TurkHirsch2026.notP :
          Set PolarWorld

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

          Equations
          Instances For

            Deontic must, grounded in @cite{kratzer-1977}'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.
            source
            def Phenomena.Focus.Studies.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
            Instances For
              source
              def Phenomena.Focus.Studies.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
              Instances For
                source
                def Phenomena.Focus.Studies.TurkHirsch2026.mustGrounded (w : PolarWorld) :
                Prop

                Kratzer-grounded deontic must: □p as @cite{kratzer-1977} Def 5 (mustInView) over the deontic premise set.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Phenomena.Focus.Studies.TurkHirsch2026.mustP :
                  Set PolarWorld

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

                  Equations
                  Instances For
                    source
                    theorem Phenomena.Focus.Studies.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.

                    source
                    structure Phenomena.Focus.Studies.TurkHirsch2026.TaggedDen (α : Type) :
                    Type

                    A denotation tagged with its UD UPOS category. Study-internal utility used to model @cite{turk-hirsch-2026}'s claim that mI's PART tag licenses only PART-tagged alternatives.

                    Instances For
                      source
                      @[implicit_reducible]
                      instance Phenomena.Focus.Studies.TurkHirsch2026.instReprTaggedDen {α✝ : Type} [Repr α✝] :
                      Repr (TaggedDen α✝)
                      Equations
                      source
                      def Phenomena.Focus.Studies.TurkHirsch2026.instReprTaggedDen.repr {α✝ : Type} [Repr α✝] :
                      TaggedDen α✝ → ℕ → Std.Format
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def Phenomena.Focus.Studies.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
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          def Phenomena.Focus.Studies.TurkHirsch2026.typeTheoAlternatives :
                          List (Set PolarWorld)

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

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            def Phenomena.Focus.Studies.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.
                            Instances For
                              source
                              def Phenomena.Focus.Studies.TurkHirsch2026.typeTheoQ :
                              Semantics.FocusInterpretation.PropFocusValue PolarWorld

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

                              Equations
                              Instances For
                                source
                                def Phenomena.Focus.Studies.TurkHirsch2026.catMatchQ :
                                Semantics.FocusInterpretation.PropFocusValue PolarWorld

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

                                Equations
                                Instances For
                                  source
                                  def Phenomena.Focus.Studies.TurkHirsch2026.polarQ :
                                  Semantics.FocusInterpretation.PropFocusValue PolarWorld

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

                                  Equations
                                  Instances For
                                    source
                                    theorem Phenomena.Focus.Studies.TurkHirsch2026.catMatch_eq_polar :
                                    catMatchQ = polarQ

                                    Category-matched question = standard polar question. @cite{fox-katzir-2011}'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.

                                    source
                                    theorem Phenomena.Focus.Studies.TurkHirsch2026.typeTheo_admits_modal :
                                    mustP ∈ typeTheoQ

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

                                    source
                                    theorem Phenomena.Focus.Studies.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.

                                    source
                                    theorem Phenomena.Focus.Studies.TurkHirsch2026.catMatch_rejects_modal :
                                    mustP ∉ catMatchQ

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

                                    source
                                    theorem Phenomena.Focus.Studies.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 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.

                                    source
                                    theorem Phenomena.Focus.Studies.TurkHirsch2026.data_modal_infelicitous :
                                    Questions.PolarAnswers.turkishPolar_must.felicitous = false

                                    The empirical datum: modal answer is infelicitous.

                                    source
                                    theorem Phenomena.Focus.Studies.TurkHirsch2026.theory_modal_excluded :
                                    mustP ∉ catMatchQ

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

                                    source
                                    theorem Phenomena.Focus.Studies.TurkHirsch2026.theory_overgen_without_catmatch :
                                    mustP ∈ typeTheoQ

                                    The theory would wrongly predict felicity without category match.

                                    Following @cite{rooth-1992}, 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.

                                    @cite{turk-hirsch-2026}'s contribution is showing that this over-generates
for Turkish polar questions, and that category match (@cite{fox-katzir-2011})
is the correct constraint on alternative computation when the focus host
is Σ_F.
                                    source
                                    def Phenomena.Focus.Studies.TurkHirsch2026.applyFoC_typeTheo :
                                    Semantics.Alternatives.AltMeaning (Set PolarWorld)

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

                                    Equations
                                    Instances For
                                      source
                                      theorem Phenomena.Focus.Studies.TurkHirsch2026.applyFoC_is_typeTheo :
                                      mustP ∈ {q : Set PolarWorld | q ∈ applyFoC_typeTheo.aValue}

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

                                      source
                                      def Phenomena.Focus.Studies.TurkHirsch2026.applyFoC_catMatch :
                                      Semantics.Alternatives.AltMeaning (Set PolarWorld)

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

                                      Equations
                                      Instances For
                                        source
                                        theorem Phenomena.Focus.Studies.TurkHirsch2026.categoryMatch_fixes_applyFoC :
                                        mustP ∉ {q : Set PolarWorld | q ∈ applyFoC_catMatch.aValue}

                                        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 @cite{turk-hirsch-2026}'s analysis requires: a UPOS label (for @cite{fox-katzir-2011} category match) and a Head label (for @cite{laka-1990}-style PolP). These commitments live in the study file, not the fragment, so the fragment stays reusable across syntactic theories.

                                        source
                                        inductive Phenomena.Focus.Studies.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.

                                        Instances For
                                          source
                                          @[implicit_reducible]
                                          instance Phenomena.Focus.Studies.TurkHirsch2026.instDecidableEqHead :
                                          DecidableEq Head
                                          Equations
                                          source
                                          def Phenomena.Focus.Studies.TurkHirsch2026.instReprHead.repr :
                                          Head → ℕ → Std.Format
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            source
                                            @[implicit_reducible]
                                            instance Phenomena.Focus.Studies.TurkHirsch2026.instReprHead :
                                            Repr Head
                                            Equations
                                            source
                                            def Phenomena.Focus.Studies.TurkHirsch2026.Head.toOp :
                                            Head → (PolarWorld → Prop) → PolarWorld → Prop

                                            The bare semantic operator each head spells out.

                                            Equations
                                            Instances For
                                              source
                                              structure Phenomena.Focus.Studies.TurkHirsch2026.MiAnalysis :
                                              Type

                                              This study's commitments about Turkish mI.

                                              • head : Head

                                                Which polarity head mI spells out (Σ in @cite{atlamaz-2023}).

                                              • upos : UD.UPOS

                                                UPOS tag used by @cite{fox-katzir-2011} category match.

                                              Instances For
                                                source
                                                def Phenomena.Focus.Studies.TurkHirsch2026.miAnalysis :
                                                MiAnalysis

                                                The @cite{turk-hirsch-2026} / @cite{atlamaz-2023} analysis: mI is Σ and tagged PART.

                                                Equations
                                                Instances For
                                                  source
                                                  theorem Phenomena.Focus.Studies.TurkHirsch2026.mi_denotation_matches_head :
                                                  Fragments.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.

                                                  source
                                                  theorem Phenomena.Focus.Studies.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.