Bhatt & Dayal (2020): PQP analysis of Hindi-Urdu kya: [BD20]

Polar Question Particle analysis: Hindi-Urdu kya: sits at PerspP, not CP. Combined with [Day25]'s three-layer cartography [SAP [PerspP [CP ...]]] and [SY17]'s analysis of Japanese kke as a meta question particle (MQP).

This study file is the canonical home for the layer assignments of the four typologically representative particles that motivate the three-way cp / perspP / sap split:

Layer	Language	Particle	Distribution
CP	Japanese	ka	matrix + subord + QS
PerspP	Hindi-Urdu	kya:	matrix + QS, no sub
SAP	Japanese	kke	matrix + quotation
SAP	English	quick(ly)	matrix only

The layer of each particle is DERIVED from its fragment's embedding-distribution facet by layerOf — the cartography's defining correlation (layer ↔ embedding distribution), stated once as a classifier rather than stipulated per particle.

def BhattDayal2020.layerOf (p : Particle) : Option Features.QParticleLayer

The [Day25] cartography's defining correlation, as a classifier: a question particle's left-peripheral layer is read off its embedding distribution — subordinated-licensed → CP (clause-typing); subordinated-excluded but quasi-subordinated- licensed → PerspP; quasi-subordinated-excluded but matrix-licensed → SAP. Defined for question particles only — Japanese koto (a declarative complementizer, kept in the fragment for the ka contrast at [Day25] (15)) is outside its intended domain.

Equations

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

def BhattDayal2020.qParticles : List Particle

layerOf's intended domain: the question particles this study classifies. Membership is a claim about what the particle does (question-forming), not about its distribution — Japanese koto (declarative complementizer) has an embedding facet but is deliberately outside.

Equations

• BhattDayal2020.qParticles = [Japanese.Particles.ka, HindiUrdu.Particles.kya, Japanese.Particles.kke, English.QuestionParticles.quick]

theorem BhattDayal2020.layers_derived : layerOf Japanese.Particles.ka = some Features.QParticleLayer.cp ∧ layerOf HindiUrdu.Particles.kya = some Features.QParticleLayer.perspP ∧ layerOf Japanese.Particles.kke = some Features.QParticleLayer.sap ∧ layerOf English.QuestionParticles.quick = some Features.QParticleLayer.sap

The four representative layer assignments, DERIVED from the fragments' embedding facets: ka CP ([Day25]), kya: PerspP ([BD20]), kke SAP ([SY17]), quick SAP ([Day25] ex. (19)). Formerly four stipulated constants; now one classifier plus kernel-checked facts.

theorem BhattDayal2020.qParticles_layered (p : Particle) : p ∈ qParticles → (layerOf p).isSome = true

Every particle in the classifier's domain receives a layer.

[BD20] eq. 23: ⟦kya:⟧ = λp[∃q ∈ Q[∀q′[q′ ∈ Q → q′ = q]].Q i.e. kya: is interpreted only when its sister question Q has a singleton alternative set, in which case the particle is the identity on Q. The presupposition is exactly Question.IsSingleton; the well-typed analogue of "felicitous sister content" is the subtype SingletonQuestion W (a question paired with a proof that its alternative set is a singleton). The "highlighted" terminology of [RF15] corresponds to declarative p in this setting (one-cell denotation, in contrast to the two-cell polar p).

[BD20] fn. 11 cites the parallel Mandarin nandao analysis as the model for kya:; the shared IsSingleton predicate captures that convergence by construction. See Zheng2025 for the nandao binding.

theorem BhattDayal2020.kya_felicitous_declarative {W : Type u} (p : Set W) : (Question.declarative p).IsSingleton

Empirical prediction (felicitous case): kya: composes felicitously with a one-cell "highlighted" polar — i.e. with the declarative content declarative p, the singleton-alternative analogue of the standard two-cell polar. The canonical good input.

theorem BhattDayal2020.kya_interp_declarative {W : Type u} (p : Set W) : (Question.SingletonQuestion.ofDeclarative p).issue = Question.declarative p

Empirical prediction (defined case): kya: on a felicitous sister returns the question unchanged — packaged as a SingletonQuestion whose underlying issue is the input declarative. Mathlib pattern: subtype + .val rather than Option.

theorem BhattDayal2020.kya_infelicitous_two_cell_polar {W : Type u} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : ¬(Question.polar p).IsSingleton

Empirical prediction (infelicitous case): kya: cannot license a two-cell Hamblin polar with a non-trivial proposition — the presupposition fails because such a polar has two alternatives.

theorem BhattDayal2020.kya_perspP_signals_singletonPresup : layerOf HindiUrdu.Particles.kya = some Features.QParticleLayer.perspP

Bridge to fragment: the PerspP layer derived from kya:'s embedding facet (layers_derived) is the surface signal of the singleton-presupposition analysis — the PerspP-layer particle is the one whose interpretation is given by the IsSingleton presupposition + identity on SingletonQuestion.