Dayal (2025): Three-layer cartography for clause-typing

[Day25] [McC06] [Zu18] [BD20]

Veneeta Dayal (2025), Linguistic Inquiry 56(4):663–712, develops the three-layer split [SAP [PerspP [CP ...]]] of the interrogative left periphery and derives cross-linguistic clause-typing variation, the responsive/rogative split, and McCloskey-style quasi-subordination from it.

Main declarations

• ClauseTyping: the two orthogonal clause-typing parameters (§§4.3–4.4), polar wh-complementizer and delayed typing.
• simplex_subordination_matches_complementizer, neutral_decl_matches_delay: the per-parameter typological projections over the English/Italian/Hindi-Urdu sample.
• cross_linguistic_shiftiness_predicted: Hindi-Urdu kya: shiftiness (§3.2) derived by the same allowsQuasiSub account as McCloskey's English data.
• theory_predicts_embedding: the SelectionClass apparatus checked against the §1.2 English embedding judgments.
• layerOf, layers_derived, particle_layer_predicts_embedding: the CP / PerspP / SAP particle classifier (§1.3), read off embedding distribution.

Implementation notes

Rival analyses of the same facts: Rizzi-style Force⁰[+Q] typing lives in Syntax/Minimalist/Questions.lean, Holmberg's PolP locus in Studies/Holmberg2016.lean, and the Speas–Tenny seat-of-knowledge matrix in Studies/SpeasTenny2003.lean. Both Dayal and Speas–Tenny predict the Newari conjunct/disjunct flip (§5.2, via [Zu18]), which the paper reads as matrix perspective shift only, leaving open whether PerspP is Zu's SentienceP.

Clause-typing typology

Two orthogonal parameters govern polar-question syntax (§§4.3–4.4): a polar wh-complementizer licenses simplex-polar subordination, and delayed clause-typing admits neutral rising declaratives. English and Italian share the first but differ on the second, so the two must not be collapsed.

structure Dayal2025.ClauseTyping : Type

A language's clause-typing profile for polar questions.

• hasPolarComplementizer : Bool

  Has a dedicated polar wh-complementizer (English whether, Italian se; Hindi-Urdu has none).

• delayedTyping : Bool

  Clause-typing may be delayed past C to PerspP (ex. 66); forced-early languages type at C immediately.

def Dayal2025.instDecidableEqClauseTyping.decEq (x✝ x✝¹ : ClauseTyping) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Dayal2025.instDecidableEqClauseTyping : DecidableEq ClauseTyping

Equations

• Dayal2025.instDecidableEqClauseTyping = Dayal2025.instDecidableEqClauseTyping.decEq

@[instance_reducible]

instance Dayal2025.instReprClauseTyping : Repr ClauseTyping

Equations

• Dayal2025.instReprClauseTyping = { reprPrec := Dayal2025.instReprClauseTyping.repr }

def Dayal2025.instReprClauseTyping.repr : ClauseTyping → ℕ → Std.Format

Equations

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

structure Dayal2025.PolarSyntaxDatum : Type

Per-language polar-question syntax: simplex-polar distribution and neutral rising declaratives. A simplex polar is the nucleus alone (p? rather than p or not (p)?).

• language : String
• typing : ClauseTyping
• matrixOk : Bool

  Simplex polar in matrix position?

• quasiSubOk : Bool

  Simplex polar in quasi-subordination?

• subordinationOk : Bool

  Simplex polar in subordination?

• neutralDeclOk : Bool

  Can a rising declarative be a neutral (unbiased) question?

@[instance_reducible]

instance Dayal2025.instDecidableEqPolarSyntaxDatum : DecidableEq PolarSyntaxDatum

Equations

• Dayal2025.instDecidableEqPolarSyntaxDatum = Dayal2025.instDecidableEqPolarSyntaxDatum.decEq

def Dayal2025.instDecidableEqPolarSyntaxDatum.decEq (x✝ x✝¹ : PolarSyntaxDatum) : Decidable (x✝ = x✝¹)

Equations

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

def Dayal2025.instReprPolarSyntaxDatum.repr : PolarSyntaxDatum → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Dayal2025.instReprPolarSyntaxDatum : Repr PolarSyntaxDatum

Equations

• Dayal2025.instReprPolarSyntaxDatum = { reprPrec := Dayal2025.instReprPolarSyntaxDatum.repr }

def Dayal2025.english_polar : PolarSyntaxDatum

Equations

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

def Dayal2025.italian_polar : PolarSyntaxDatum

Equations

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

def Dayal2025.hindi_urdu_polar : PolarSyntaxDatum

Hindi-Urdu: no wh-complementizer, so simplex polars cannot be subordinated (ex. 70–71); typing is delayed, so rising declaratives can be neutral.

Equations

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

def Dayal2025.allPolarSyntaxData : List PolarSyntaxDatum

Equations

• Dayal2025.allPolarSyntaxData = [Dayal2025.english_polar, Dayal2025.italian_polar, Dayal2025.hindi_urdu_polar]

theorem Dayal2025.simplex_subordination_matches_complementizer (d : PolarSyntaxDatum) : d ∈ allPolarSyntaxData → d.subordinationOk = d.typing.hasPolarComplementizer

Simplex-polar subordination tracks the complementizer parameter (§4.4).

theorem Dayal2025.neutral_decl_matches_delay (d : PolarSyntaxDatum) : d ∈ allPolarSyntaxData → d.neutralDeclOk = d.typing.delayedTyping

Neutral rising declaratives track the delayed-typing parameter (§4.3, ex. 63b).

Hindi-Urdu shiftiness (§3.2, ex. 39–41)

Hindi-Urdu kya: under attitude predicates patterns with McCloskey's English embedded inversion: blocked under a bare responsive, licensed under negation or questioning.

structure Dayal2025.CrossLingShiftinessDatum : Type

Cross-linguistic shiftiness data.

• language : String
• verb : String
• sentence : String
• negated : Bool
• questioned : Bool
• quasiSubOk : Bool

@[instance_reducible]

instance Dayal2025.instDecidableEqCrossLingShiftinessDatum : DecidableEq CrossLingShiftinessDatum

Equations

• Dayal2025.instDecidableEqCrossLingShiftinessDatum = Dayal2025.instDecidableEqCrossLingShiftinessDatum.decEq

def Dayal2025.instDecidableEqCrossLingShiftinessDatum.decEq (x✝ x✝¹ : CrossLingShiftinessDatum) : Decidable (x✝ = x✝¹)

Equations

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

def Dayal2025.instReprCrossLingShiftinessDatum.repr : CrossLingShiftinessDatum → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Dayal2025.instReprCrossLingShiftinessDatum : Repr CrossLingShiftinessDatum

Equations

• Dayal2025.instReprCrossLingShiftinessDatum = { reprPrec := Dayal2025.instReprCrossLingShiftinessDatum.repr }

def Dayal2025.hindi_urdu_want_to_know : CrossLingShiftinessDatum

Hindi-Urdu: "want to know" (rogative) freely takes kya: (ex. 39a).

Equations

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

def Dayal2025.hindi_urdu_know_bare : CrossLingShiftinessDatum

Hindi-Urdu: bare "know" (responsive) rejects kya: (ex. 39b).

Equations

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

def Dayal2025.hindi_urdu_know_negated : CrossLingShiftinessDatum

Hindi-Urdu: "nobody knows" + kya: → OK (negation, ex. 41a).

Equations

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

def Dayal2025.hindi_urdu_know_questioned : CrossLingShiftinessDatum

Hindi-Urdu: "does anyone know" + kya: → OK (questioning, ex. 41b).

Equations

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

def Dayal2025.allCrossLingShiftinessData : List CrossLingShiftinessDatum

Equations

• Dayal2025.allCrossLingShiftinessData = [Dayal2025.hindi_urdu_want_to_know, Dayal2025.hindi_urdu_know_bare, Dayal2025.hindi_urdu_know_negated, Dayal2025.hindi_urdu_know_questioned]

def Dayal2025.remember_bare : CrossLingShiftinessDatum

English: bare responsive remember rejects embedded inversion ([McC06]).

Equations

• Dayal2025.remember_bare = { language := "English", verb := "remember", sentence := "*I remember [was Henry a communist↑]", negated := false, questioned := false, quasiSubOk := false }

def Dayal2025.remember_negated : CrossLingShiftinessDatum

English: negated remember licenses embedded inversion — McCloskey's judgment is marginal ("?"), encoded here as licensed.

Equations

• Dayal2025.remember_negated = { language := "English", verb := "remember", sentence := "?I don't remember [was Henry a communist↑]", negated := true, questioned := false, quasiSubOk := true }

def Dayal2025.remember_questioned : CrossLingShiftinessDatum

English: questioned remember licenses embedded inversion ([McC06]).

Equations

• Dayal2025.remember_questioned = { language := "English", verb := "remember", sentence := "Does Sue remember [was Henry a communist↑]", negated := false, questioned := true, quasiSubOk := true }

Verification against empirical embedding data

The SelectionClass apparatus checked against the paper's §1.2 classification of English attitude predicates: rogatives split three ways by the largest structure they take (CP / PerspP / SAP); responsives and uninterrogatives take none of the larger structures.

structure Dayal2025.EmbeddingDatum : Type

Embedding judgment for an English attitude predicate (§1.2).

• verb : String
• subordination : Bool

  "V whether/who..."

• quasiSubordination : Bool

  "V [did S leave↑]" (embedded inversion + matrix intonation)

• quotation : Bool

  'V, "Did S leave?"'

def Dayal2025.instDecidableEqEmbeddingDatum.decEq (x✝ x✝¹ : EmbeddingDatum) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Dayal2025.instDecidableEqEmbeddingDatum : DecidableEq EmbeddingDatum

Equations

• Dayal2025.instDecidableEqEmbeddingDatum = Dayal2025.instDecidableEqEmbeddingDatum.decEq

def Dayal2025.instReprEmbeddingDatum.repr : EmbeddingDatum → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Dayal2025.instReprEmbeddingDatum : Repr EmbeddingDatum

Equations

• Dayal2025.instReprEmbeddingDatum = { reprPrec := Dayal2025.instReprEmbeddingDatum.repr }

def Dayal2025.investigate_d : EmbeddingDatum

Equations

• Dayal2025.investigate_d = { verb := "investigate", subordination := true, quasiSubordination := false, quotation := false }

def Dayal2025.depend_on_d : EmbeddingDatum

Equations

• Dayal2025.depend_on_d = { verb := "depend on", subordination := true, quasiSubordination := false, quotation := false }

def Dayal2025.wonder_d : EmbeddingDatum

Equations

• Dayal2025.wonder_d = { verb := "wonder", subordination := true, quasiSubordination := true, quotation := false }

def Dayal2025.ask_d : EmbeddingDatum

Equations

• Dayal2025.ask_d = { verb := "ask", subordination := true, quasiSubordination := true, quotation := true }

def Dayal2025.know_d : EmbeddingDatum

Equations

• Dayal2025.know_d = { verb := "know", subordination := true, quasiSubordination := false, quotation := false }

def Dayal2025.care_d : EmbeddingDatum

Predicate of Relevance: responsive but resists question-to-proposition reduction ([EKSU17]). The reduction-resistance is a separate property — see Elliott2017.

Equations

• Dayal2025.care_d = { verb := "care", subordination := true, quasiSubordination := false, quotation := false }

def Dayal2025.matter_d : EmbeddingDatum

Predicate of Relevance ([EKSU17]).

Equations

• Dayal2025.matter_d = { verb := "matter", subordination := true, quasiSubordination := false, quotation := false }

def Dayal2025.believe_d : EmbeddingDatum

Equations

• Dayal2025.believe_d = { verb := "believe", subordination := false, quasiSubordination := false, quotation := false }

def Dayal2025.allEmbeddingData : List EmbeddingDatum

Equations

• Dayal2025.allEmbeddingData = [Dayal2025.investigate_d, Dayal2025.depend_on_d, Dayal2025.wonder_d, Dayal2025.ask_d, Dayal2025.know_d, Dayal2025.care_d, Dayal2025.matter_d, Dayal2025.believe_d]

theorem Dayal2025.quasi_sub_implies_sub (d : EmbeddingDatum) : d ∈ allEmbeddingData → d.quasiSubordination = true → d.subordination = true

Quasi-subordination implies subordination: the §1.2 classification is cumulative — each larger-structure class also takes the smaller ones.

theorem Dayal2025.quotation_implies_quasi_sub (d : EmbeddingDatum) : d ∈ allEmbeddingData → d.quotation = true → d.quasiSubordination = true

Quotation implies quasi-subordination among the interrogative-selecting predicates sampled here (per §1.2; say takes interrogative quotations without quasi-subordinating, but is not interrogative-selecting).

def Dayal2025.classify : String → Minimalist.LeftPeriphery.SelectionClass

The substrate classifier extended with [EKSU17]'s predicates of relevance (care, matter), which classify as responsive.

Equations

• Dayal2025.classify "care" = Minimalist.LeftPeriphery.SelectionClass.responsive
• Dayal2025.classify "matter" = Minimalist.LeftPeriphery.SelectionClass.responsive
• Dayal2025.classify x✝ = Minimalist.LeftPeriphery.classifyVerb x✝

theorem Dayal2025.theory_predicts_embedding (d : EmbeddingDatum) : d ∈ allEmbeddingData → Minimalist.LeftPeriphery.allowsEmbedding (classify d.verb) Minimalist.LeftPeriphery.EmbedType.subordination false false = d.subordination ∧ Minimalist.LeftPeriphery.allowsEmbedding (classify d.verb) Minimalist.LeftPeriphery.EmbedType.quasiSubordination false false = d.quasiSubordination ∧ Minimalist.LeftPeriphery.allowsEmbedding (classify d.verb) Minimalist.LeftPeriphery.EmbedType.quotation false false = d.quotation

The theory correctly predicts all embedding judgments from the data.

theorem Dayal2025.shiftiness_predicted : Minimalist.LeftPeriphery.allowsQuasiSub Minimalist.LeftPeriphery.SelectionClass.responsive remember_bare.negated remember_bare.questioned = remember_bare.quasiSubOk ∧ Minimalist.LeftPeriphery.allowsQuasiSub Minimalist.LeftPeriphery.SelectionClass.responsive remember_negated.negated remember_negated.questioned = remember_negated.quasiSubOk ∧ Minimalist.LeftPeriphery.allowsQuasiSub Minimalist.LeftPeriphery.SelectionClass.responsive remember_questioned.negated remember_questioned.questioned = remember_questioned.quasiSubOk

Shiftiness predictions match McCloskey's data for remember (responsive).

Cross-linguistic predictions

theorem Dayal2025.cross_linguistic_shiftiness_predicted (d : CrossLingShiftinessDatum) : d ∈ allCrossLingShiftinessData → Minimalist.LeftPeriphery.allowsQuasiSub (Minimalist.LeftPeriphery.classifyCrossLingVerb d.verb) d.negated d.questioned = d.quasiSubOk

Hindi-Urdu shiftiness follows the same derivation as English: responsive predicates reject quasi-sub in bare form, allow it under negation/questioning.

The three-layer classifier for question particles

A question particle's left-peripheral layer is read off its embedding distribution (§1.3); the four representative assignments:

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 + quotation

[BD20]'s ForceP location for kya: is recast here as PerspP (a terminological change by the paper's own fn. 3).

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

A question particle's layer, read off its embedding distribution. Defined for question particles only — Japanese koto (a declarative complementizer, the ka contrast of ex. 15) is outside the intended domain.

Equations

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

def Dayal2025.qParticles : List Particle

The classifier's intended domain: the question particles this study classifies. Membership is a claim about what the particle does (question-forming), not about its distribution.

Equations

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

theorem Dayal2025.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, kya: PerspP (recasting [BD20]'s ForceP), kke SAP ([SY17]), quick SAP (ex. 18–19).

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

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

theorem Dayal2025.particle_layer_predicts_embedding (p : Particle) : p ∈ qParticles → (layerOf p = some Features.QParticleLayer.cp → p.LicensedInEmbed Clause.EmbeddingContext.subordinated) ∧ (layerOf p = some Features.QParticleLayer.perspP → ¬p.LicensedInEmbed Clause.EmbeddingContext.subordinated) ∧ (layerOf p = some Features.QParticleLayer.sap → ¬p.LicensedInEmbed Clause.EmbeddingContext.quasiSubordinated)

Q-particle embedding follows from which left-peripheral layer they occupy: CP-layer particles are licensed in subordination, PerspP- and SAP-layer particles are not, and SAP-layer particles are excluded even from quasi-subordination. Stated over layerOf, which derives the layer from the embedding facet, so this is the kernel-checked converse guarantee for the study's particle sample.