Türk and Hirsch (2026): Constraining Alternatives in Turkish Polar Questions

This file formalizes [TH26], an argument from Turkish polar questions that focus alternatives are formed in the syntax under a category constraint. Turkish polar questions carry the focus clitic =mI, which by default attaches to a focused covert polarity head Σ, (4), and [Atl23] derives the Hamblin set of the question from focus alternatives: Σ has the identity as ordinary value and the identity and negation as focus value, the alternatives propagate pointwise, and a question head C_Q sets the ordinary value of the clause to the focus value of its prejacent, hamblinSet. The two alternatives of Σ are assumed rather than derived. Under [Roo85]'s type-theoretic alternatives Σ_F is the F-marked identity, WithAlternatives.focused, whose focus value is every propositional operator, so the Hamblin set is every proposition, hamblinType_eq_univ, and [Day96]'s answerhood operator, which selects the strongest true member, returns total information about the world, isStrongestTrueAnswer_hamblinType; on the sample (31), which adds the deontic modal propositions, it returns the conjunction that Ali had to sleep and did, (35b), rather than the attested complete answer (35a), isStrongestTrueAnswer_sample. Contextual restriction cannot repair this, since any Hamblin set at all is the intersection of the type-theoretic focus value with some context, exists_context_inter_eq, whereas the modalized question (38) is unavailable even in the supporting context (39). Instead alternatives are syntactic objects formed under the Category Match Constraint (42), [FK11], [Kat07]: replacements of the focus share its category, which is the terminal clause of the substrate's syntactic composition Tree.withAlternatives, so Σ_F is that composition interpreted, sigmaCat. With Σ and NEG the only morphemes of category Pol, the Hamblin set is the polar one, withAlternatives_sigma, hamblinCat_eq, hamblinCat_eq_alt_polar, Dayal's operator returns the positive or the negative answer, isStrongestTrueAnswer_hamblinCat, and the modal answer (41) is not a member, mem_hamblinCat_iff. No structural-complexity constraint is involved: the category-match alternatives are substitutions at the focus, hence structural alternatives of [Kat07] without any bound, Tree.alternatives_withAlternatives_subset.

Implementation notes

Propositions are sets of worlds. Σ and NEG are the positive and the negative Polarity, and denote its action on propositions, the identity and complementation. The deontic modal is Modality.necessity over a modal base and an ordering source. The lexicon is a finite set of terminals of PhraseStructure.Tree, so that category match is the terminal clause of Tree.withAlternatives; the denotation of a tree is its terminal's operator and the identity elsewhere. Two-dimensional values are WithAlternatives, whose <*> is pointwise functional application. =mI itself is vacuous and does not enter the composition. The embedding data, (14) and (18), in which =mI below the complementizer diye yields a declarative matrix clause and =mI above it a matrix question, so that =mI tracks the highest focus mark, are recorded as rows and not modelled. The examples are the rows of Data.Examples.TurkHirsch2026.

References

• [TH26]
• [Atl23]
• [FK11]
• [Kat07]
• [Roo85]
• [Roo92]
• [Day96]
• [Ham73]
• [KK20]
• [HS25]

The polar morphemes and the deontic modal

inductive TurkHirsch2026.Cat : Type

The syntactic categories are the polarity category of Σ and NEG and that of the deontic modal.

• pol : Cat
• modal : Cat

@[instance_reducible]

instance TurkHirsch2026.instDecidableEqCat : DecidableEq Cat

Equations

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

def TurkHirsch2026.instReprCat.repr : Cat → ℕ → Std.Format

Equations

• TurkHirsch2026.instReprCat.repr TurkHirsch2026.Cat.pol prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TurkHirsch2026.Cat.pol")).group prec✝
• TurkHirsch2026.instReprCat.repr TurkHirsch2026.Cat.modal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TurkHirsch2026.Cat.modal")).group prec✝

@[instance_reducible]

instance TurkHirsch2026.instReprCat : Repr Cat

Equations

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

inductive TurkHirsch2026.Word : Type

The propositional operators of the lexicon are the polarity heads, Σ the positive and NEG the negative, and the deontic modal.

• polarity (s : Polarity) : Word
• deontic : Word

@[instance_reducible]

instance TurkHirsch2026.instDecidableEqWord : DecidableEq Word

Equations

• TurkHirsch2026.instDecidableEqWord = TurkHirsch2026.instDecidableEqWord.decEq

def TurkHirsch2026.instDecidableEqWord.decEq (x✝ x✝¹ : Word) : Decidable (x✝ = x✝¹)

Equations

• TurkHirsch2026.instDecidableEqWord.decEq (TurkHirsch2026.Word.polarity a) (TurkHirsch2026.Word.polarity b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• TurkHirsch2026.instDecidableEqWord.decEq (TurkHirsch2026.Word.polarity s) TurkHirsch2026.Word.deontic = isFalse ⋯
• TurkHirsch2026.instDecidableEqWord.decEq TurkHirsch2026.Word.deontic (TurkHirsch2026.Word.polarity s) = isFalse ⋯
• TurkHirsch2026.instDecidableEqWord.decEq TurkHirsch2026.Word.deontic TurkHirsch2026.Word.deontic = isTrue ⋯

def TurkHirsch2026.instReprWord.repr : Word → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance TurkHirsch2026.instReprWord : Repr Word

Equations

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

def TurkHirsch2026.Word.den {W : Type} (f g : Modality.Background W) : Word → Set W → Set W

The operator a word denotes. A polarity head acts on propositions, so that Σ is the identity and NEG complementation, and the deontic modal is necessity over the modal base and ordering source.

Equations

• TurkHirsch2026.Word.den f g (TurkHirsch2026.Word.polarity s) = fun (x : Set W) => s • x
• TurkHirsch2026.Word.den f g TurkHirsch2026.Word.deontic = fun (p : Set W) => {w : W | Modality.necessity f g (fun (x : W) => x ∈ p) w}

def TurkHirsch2026.den {W : Type} (f g : Modality.Background W) : PhraseStructure.Tree Cat Word → Set W → Set W

A tree denotes its terminal's operator, and the identity elsewhere.

Equations

• TurkHirsch2026.den f g (RoseTree.node (PhraseStructure.Tree.Label.terminal a w) []) = TurkHirsch2026.Word.den f g w
• TurkHirsch2026.den f g x✝ = id

def TurkHirsch2026.lexicon : Finset (PhraseStructure.Tree Cat Word)

The lexicon of propositional operators (44) has Σ and NEG of category Pol and the deontic modal of its own category.

Equations

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

def TurkHirsch2026.sigma : PhraseStructure.Tree Cat Word

The focused polarity head Σ_F.

Equations

• TurkHirsch2026.sigma = PhraseStructure.Tree.terminal TurkHirsch2026.Cat.pol (TurkHirsch2026.Word.polarity Polarity.positive)

Composing the question

Σ_F with focus value A is the two-dimensional value ⟨id, A⟩, (8a); the TP applies it pointwise to the unfocused prejacent, (9), and C_Q returns the focus value of its prejacent as the Hamblin set, (10). Type-theoretic alternatives make Σ_F the F-marked identity, WithAlternatives.focused id; category match makes it the interpretation of the syntactic composition Tree.withAlternatives over the lexicon.

def TurkHirsch2026.hamblinSet {W : Type} (m : WithAlternatives (Set W → Set W)) (p : Set W) : Set (Set W)

The Hamblin set of the question formed on Σ_F with two-dimensional value m is the focus value of the TP m <*> pure p, (9) and (10).

Equations

• TurkHirsch2026.hamblinSet m p = (m <*> pure p).alternatives

theorem TurkHirsch2026.mem_hamblinSet {W : Type} {m : WithAlternatives (Set W → Set W)} {p q : Set W} : q ∈ hamblinSet m p ↔ ∃ g ∈ m.alternatives, g p = q

Type-theoretic alternatives over-generate

def TurkHirsch2026.hamblinType {W : Type} (p : Set W) : Set (Set W)

The Hamblin set under [Roo85]'s type-theoretic focus value, every operator of Σ's type (26), where Σ_F is the F-marked identity.

Equations

• TurkHirsch2026.hamblinType p = TurkHirsch2026.hamblinSet (WithAlternatives.focused id) p

theorem TurkHirsch2026.hamblinType_eq_univ {W : Type} (p : Set W) : hamblinType p = Set.univ

The type-theoretic Hamblin set is every proposition (28).

theorem TurkHirsch2026.isStrongestTrueAnswer_hamblinType {W : Type} (p : Set W) (w : W) : Question.IsStrongestTrueAnswer (hamblinType p) w {w}

Under type-theoretic alternatives the complete answer at w is total information about w, so the responder must supply every true proposition.

def TurkHirsch2026.sample {W : Type} (f g : Modality.Background W) (p : Set W) : Set (Set W)

The sample of the Hamblin set with the deontic propositions (31).

Equations

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

theorem TurkHirsch2026.sample_subset_hamblinType {W : Type} (f g : Modality.Background W) (p : Set W) : sample f g p ⊆ hamblinType p

theorem TurkHirsch2026.isStrongestTrueAnswer_sample {W : Type} (f g : Modality.Background W) {p : Set W} {w : W} (hw : w ∈ p) (hbox : w ∈ Word.den f g Word.deontic p) : Question.IsStrongestTrueAnswer (sample f g p) w (Word.den f g Word.deontic p ∩ p)

At a world where Ali had to sleep and slept (34), the strongest true member of the sample is the conjunction that he had to sleep and did, the over-informative answer (35b).

theorem TurkHirsch2026.exists_context_inter_eq {W : Type} (p : Set W) (H : Set (Set W)) : ∃ (c : Set (Set W)), hamblinType p ∩ c = H

Any Hamblin set whatever is the type-theoretic focus value restricted by some context (36), so restriction by context alone cannot exclude the modalized question (38).

Category match

def TurkHirsch2026.sigmaCat {W : Type} (f g : Modality.Background W) : WithAlternatives (Set W → Set W)

Under the Category Match Constraint (42), Σ_F evokes its same-category replacements from the lexicon, the terminal clause of the substrate's syntactic composition, so its two-dimensional value is the interpretation of Tree.withAlternatives.

Equations

• TurkHirsch2026.sigmaCat f g = TurkHirsch2026.den f g <$> PhraseStructure.Tree.withAlternatives TurkHirsch2026.lexicon TurkHirsch2026.sigma

theorem TurkHirsch2026.withAlternatives_sigma : (PhraseStructure.Tree.withAlternatives lexicon sigma).alternatives = {sigma, PhraseStructure.Tree.terminal Cat.pol (Word.polarity Polarity.negative)}

The category-match alternatives of Σ_F are Σ and NEG (45).

def TurkHirsch2026.hamblinCat {W : Type} (f g : Modality.Background W) (p : Set W) : Set (Set W)

The Hamblin set under category match.

Equations

• TurkHirsch2026.hamblinCat f g p = TurkHirsch2026.hamblinSet (TurkHirsch2026.sigmaCat f g) p

theorem TurkHirsch2026.hamblinCat_eq {W : Type} (f g : Modality.Background W) (p : Set W) : hamblinCat f g p = {p, pᶜ}

Under category match the Hamblin set is the polar one, (23).

theorem TurkHirsch2026.hamblinCat_eq_alt_polar {W : Type} (f g : Modality.Background W) {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : hamblinCat f g p = (Question.polar p).alt

The category-match Hamblin set is the alternative set of the polar interrogative.

theorem TurkHirsch2026.mem_hamblinCat_iff {W : Type} (f g : Modality.Background W) (p q : Set W) : q ∈ hamblinCat f g p ↔ q = p ∨ q = pᶜ

A proposition is a member of the category-match Hamblin set only as the positive or the negative answer (41); the modal answer is excluded as soon as it differs from both.

theorem TurkHirsch2026.isStrongestTrueAnswer_hamblinCat {W : Type} (f g : Modality.Background W) {p : Set W} {w : W} (hw : w ∈ p) : Question.IsStrongestTrueAnswer (hamblinCat f g p) w p

Under category match the complete answer is the positive answer when it is true (35a).

theorem TurkHirsch2026.isStrongestTrueAnswer_hamblinCat_compl {W : Type} (f g : Modality.Background W) {p : Set W} {w : W} (hw : w ∉ p) : Question.IsStrongestTrueAnswer (hamblinCat f g p) w pᶜ

And the negative answer when the positive one is false.