Bhatt and Dayal 2020: the polar question particle kya:

This file formalizes Bhatt and Dayal's analysis of Hindi-Urdu polar kya:. The particle is not a clause-typing Q-morpheme of the Japanese -ka kind: it occurs in polar and alternative questions but not in constituent questions, and it embeds under rogative predicates and modified responsives but not under plain responsives — the quasi-subordinated configuration, which the authors place in a projection above CP, ForceP, that only some predicates select. Semantically kya: is the identity on its sister question, defined only when that question's alternative set is a singleton; a polar question denotes the singleton of its nucleus proposition, a constituent question a plural set. An alternative question is the disjunction of two polar questions and so has two alternatives; kya: is licensed in it by applying inside a disjunct, and fails when it scopes over the disjunction. That failure rules out one parse of clause-final kya: with a disjunction (51); the paper leaves open why the other parse, with kya: on the second disjunct (52), is unavailable.

Main definitions

• KyaDefined: the domain of kya:, a sister with a single alternative (23).
• altQ: the alternative question p or q as the disjunction of two polar questions.
• selectsForceP: the embedding contexts whose selecting predicate takes a ForceP complement.

Main results

• kya_polar, kya_not_wh: the presupposition holds of a polar question and fails on a constituent question with two answer cells.
• altQ_not_kyaDefined: kya: over an alternative question fails.
• kyaDefined_iff_not_isInquisitive: in the type-uniform setting the presupposition picks out exactly the non-inquisitive contents, declaratives included.
• kya_licensed_iff_selectsForceP, kya_clause_types: the fragment's embedding and clause-type distributions.

Implementation notes

Questions are inquisitive contents, and the paper's Hamblin set is a content's set of alternatives alt: the polar question {p} of (22b) is ofSet p and the constituent question of (22a) is which. Inquisitive contents do not separate declaratives from interrogatives, so the declarative p is ofSet p as well and meets the presupposition. The paper keeps kya: off declaratives by a type distinction instead, and names highlighting in the sense of [RF15] as the replacement in theories without one; [Xu17] analyses nandao that way. kyaDefined_iff_not_isInquisitive states the collapse. The paper's alternative question is the union {p, q} of the two disjuncts; the inquisitive disjunction altQ p q has both as alternatives only when neither entails the other, which the theorems about it assume.

References

• [BD20]
• [RF15]: highlighting, the alternative to the singleton requirement.
• [Xu12a], [Xu17]: the Mandarin nandao analysis the account draws on.

The singleton presupposition

def BhattDayal2020.KyaDefined {W : Type u_1} (Q : Question W) : Prop

kya: is defined (23) when its sister has a single alternative, the paper's ∃p ∈ Q[∀q[q ∈ Q → q = p]] read on the sister's alternatives. On that domain kya: is the identity.

Equations

• BhattDayal2020.KyaDefined Q = ∃ (p : Set W), Q.alt = {p}

theorem BhattDayal2020.not_kyaDefined_of_mem_alt {W : Type u_1} {Q : Question W} {p₁ p₂ : Set W} (h₁ : p₁ ∈ Q.alt) (h₂ : p₂ ∈ Q.alt) (hne : p₁ ≠ p₂) : ¬KyaDefined Q

Two distinct alternatives break the presupposition.

theorem BhattDayal2020.kya_polar {W : Type u_1} (p : Set W) : KyaDefined (Question.ofSet p)

A polar question denotes the singleton of its nucleus proposition (22b), so kya: is defined on it and returns it (23).

theorem BhattDayal2020.kya_not_wh {W : Type u_1} {E : Type u_2} {D : Set E} {P : E → Set W} (hD : D.Nonempty) (hA : IsAntichain (fun (x1 x2 : Set W) => x1 ⊆ x2) (P '' D)) {e₁ e₂ : E} (h₁ : e₁ ∈ D) (h₂ : e₂ ∈ D) (hPne : P e₁ ≠ P e₂) : ¬KyaDefined (Question.which D P)

A constituent question with two distinct answer cells is not a singleton (22a), so kya: is undefined on it (4).

theorem BhattDayal2020.kya_not_two_cell {W : Type u_1} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : ¬KyaDefined (Question.polar p)

The two-cell Hamblin polar question fails the presupposition as well; the paper's polar question is the one-cell ofSet p.

theorem BhattDayal2020.kyaDefined_iff_not_isInquisitive {W : Type u_1} {Q : Question W} (hQ : Q.IsNormal) : KyaDefined Q ↔ ¬Q.IsInquisitive

The presupposition picks out exactly the non-inquisitive contents among the normal ones. The declarative p meets it as well as the polar question, since both are ofSet p.

Alternative questions

def BhattDayal2020.altQ {W : Type u_1} (p q : Set W) : Question W

The alternative question p or q is the disjunction of the two polar questions, (44) and (52).

Equations

• BhattDayal2020.altQ p q = Question.ofSet p ⊔ Question.ofSet q

theorem BhattDayal2020.mem_alt_altQ_left {W : Type u_1} {p q : Set W} (h : ¬p ⊆ q) : p ∈ (altQ p q).alt

theorem BhattDayal2020.mem_alt_altQ_right {W : Type u_1} {p q : Set W} (h : ¬q ⊆ p) : q ∈ (altQ p q).alt

theorem BhattDayal2020.altQ_not_kyaDefined {W : Type u_1} {p q : Set W} (hpq : ¬p ⊆ q) (hqp : ¬q ⊆ p) : ¬KyaDefined (altQ p q)

An alternative question has two alternatives, so kya: scoping over it fails the presupposition ((43), (51)), while each disjunct meets it by kya_polar ((44), (47), (52)).

theorem BhattDayal2020.kya_polar_disjunction {W : Type u_1} (p q : Set W) : KyaDefined (Question.ofSet (p ∪ q))

Disjunction inside a polar question keeps a singleton, the yes/no reading of p or q, (45).

Distribution

def BhattDayal2020.selectsForceP (e : Clause.EmbeddingContext) : Prop

The embedding contexts whose selecting predicate takes a ForceP complement, (21), are the matrix clause and quasi-subordination, not ordinary subordination.

Equations

• BhattDayal2020.selectsForceP e = (e = Clause.EmbeddingContext.matrix ∨ e = Clause.EmbeddingContext.quasiSubordinated)

@[instance_reducible]

instance BhattDayal2020.instDecidableSelectsForceP (e : Clause.EmbeddingContext) : Decidable (selectsForceP e)

Equations

• BhattDayal2020.instDecidableSelectsForceP e = { decide := decide (e = Clause.EmbeddingContext.matrix) || decide (e = Clause.EmbeddingContext.quasiSubordinated), reflects_decide := ⋯ }

theorem BhattDayal2020.kya_licensed_iff_selectsForceP (e : Clause.EmbeddingContext) : e ≠ Clause.EmbeddingContext.quotation → (HindiUrdu.Particles.kya.LicensedInEmbed e ↔ selectsForceP e)

Over the contexts the paper records, kya: is licensed exactly where ForceP is selected ((8), (9), (21)).

theorem BhattDayal2020.kya_clause_types (c : Clause.SentenceType) : HindiUrdu.Particles.kya.LicensedIn c ↔ c = Clause.SentenceType.polar ∨ c = Clause.SentenceType.alternative

kya: is licensed in polar and alternative questions and not in constituent questions, (4) and (5).