Documentation

Linglib.Studies.Dayal2025

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 cartographic split [SAP [PerspP [CP ...]]] and uses it to account for cross-linguistic clause-typing variation, the responsive/ rogative split, and McCloskey-style quasi-subordination.

This study file is the canonical home for:

Clause-typing typology (§4.4): forced-CP vs delayed-PerspP variation across English/Italian/Hindi-Urdu.
Hindi-Urdu shiftiness (§3.2): the McCloskey parallel for Hindi-Urdu jaanna:.
Newari conjunct/disjunct (§5.2): the perspective-shift evidence from Newari person marking.
Left-Periphery bridge: the verification of the LeftPeriphery SelectionClass apparatus against the English embedding data (§5) and the cross-linguistic shiftiness data.

Cross-framework relations #

Rizzi 1997 / Syntax/Minimalist/Questions.lean places clause-typing at Force⁰[+Q]; Dayal places it at C with a downstream PerspP shift. The disagreement is real and not currently formalized as a bridge theorem. See Syntax/Minimalist/Questions.lean.
Holmberg 2016 / Studies/Holmberg2016.lean places the polar-Q-typing locus at PolP (via the Features/AnsweringSystem.lean typological parameter). Holmberg's analysis competes with Dayal's for the same matrix-polar facts.
Speas-Tenny / Studies/SpeasTenny2003.lean derives SpeasTenny2003.seatOfKnowledge from a 2×2 feature matrix; Dayal places SoK in PerspP with PRO. Both predict the Newari conjunct/disjunct flip; the bridge theorem SpeasTenny2003.seatOfKnowledge ↔ PerspP-PRO over Newari is unformalized.

inductive Dayal2025.ClauseTypingStrategy :

How a language handles clause-typing for polar questions. The contrast is the cartographic locus of [+Q]-typing, not a difference in feature inventory. CP-typed languages license simplex polars in subordination via a wh-complementizer (English whether, Italian se); PerspP-typed languages route polar questions through a higher PerspP layer that does not embed under canonical responsive predicates.

cpTyped : ClauseTypingStrategy
Clause-typing locus is C (English whether, Italian se).
perspPTyped : ClauseTypingStrategy
Clause-typing locus is PerspP (Hindi-Urdu rising intonation).

Instances For

@[implicit_reducible]

instance Dayal2025.instDecidableEqClauseTypingStrategy :

DecidableEq ClauseTypingStrategy

Equations

Dayal2025.instDecidableEqClauseTypingStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Dayal2025.instReprClauseTypingStrategy :

Repr ClauseTypingStrategy

Equations

Dayal2025.instReprClauseTypingStrategy = { reprPrec := Dayal2025.instReprClauseTypingStrategy.repr }

def Dayal2025.instReprClauseTypingStrategy.repr :

ClauseTypingStrategy → ℕ → Std.Format

Equations

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

Instances For

def Dayal2025.ClauseTypingStrategy.licensesSimplexSubordination :

ClauseTypingStrategy → Bool

Structural projection: which clause-typing strategies license simplex polar questions in subordination. CP-typed languages do (the wh- complementizer is the embedding selector); PerspP-typed languages do not (PerspP is too high to be selected by canonical responsive verbs). delayed_blocks_simplex_subordination below derives from this projection together with the Fragment data, rather than holding vacuously over a 1-element sample.

Equations

Instances For

structure Dayal2025.SimplexPolarDatum :

Data on simplex polar question embedding across languages. A simplex polar question is just the nucleus p (no "or not").

language : String
clauseTyping : ClauseTypingStrategy
matrixOk : Bool
Simplex polar in matrix?
quasiSubOk : Bool
Simplex polar in quasi-subordination?
subordinationOk : Bool
Simplex polar in subordination?

Instances For

def Dayal2025.instReprSimplexPolarDatum.repr :

SimplexPolarDatum → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Dayal2025.instReprSimplexPolarDatum :

Repr SimplexPolarDatum

Equations

Dayal2025.instReprSimplexPolarDatum = { reprPrec := Dayal2025.instReprSimplexPolarDatum.repr }

def Dayal2025.english_simplex :

SimplexPolarDatum

Equations

Dayal2025.english_simplex = { language := "English", clauseTyping := Dayal2025.ClauseTypingStrategy.cpTyped, matrixOk := true, quasiSubOk := true, subordinationOk := true }

Instances For

def Dayal2025.italian_simplex :

SimplexPolarDatum

Equations

Dayal2025.italian_simplex = { language := "Italian", clauseTyping := Dayal2025.ClauseTypingStrategy.cpTyped, matrixOk := true, quasiSubOk := true, subordinationOk := true }

Instances For

def Dayal2025.hindi_urdu_simplex :

SimplexPolarDatum

Hindi-Urdu: simplex polar questions require PerspP (rising intonation activates [+WH] at PerspP level). No wh-complementizer → cannot clause-type at C. (Dayal 2025: ex (70)–(71); UNVERIFIED page numbers.)

Equations

Dayal2025.hindi_urdu_simplex = { language := "Hindi-Urdu", clauseTyping := Dayal2025.ClauseTypingStrategy.perspPTyped, matrixOk := true, quasiSubOk := true, subordinationOk := false }

Instances For

def Dayal2025.allSimplexPolarData :

List SimplexPolarDatum

Equations

Dayal2025.allSimplexPolarData = [Dayal2025.english_simplex, Dayal2025.italian_simplex, Dayal2025.hindi_urdu_simplex]

Instances For

theorem Dayal2025.simplex_subordination_matches_projection (d : SimplexPolarDatum) :

d ∈ allSimplexPolarData → d.subordinationOk = d.clauseTyping.licensesSimplexSubordination

The Fragment data is consistent with the structural projection: every PerspP-typed language in the sample lacks simplex-polar subordination. Unlike a 1-direction stipulation, this connects per-language data to a typed projection on ClauseTypingStrategy.

theorem Dayal2025.perspPTyped_blocks_simplex_subordination (d : SimplexPolarDatum) :

d ∈ allSimplexPolarData → d.clauseTyping = ClauseTypingStrategy.perspPTyped → d.subordinationOk = false

Corollary: PerspP-typed languages cannot subordinate simplex polars. Now derived from the structural projection, not from the data alone.

structure Dayal2025.DeclarativeQuestionDatum :

Whether declarative questions in a language are obligatorily biased. English: "You drink wine?" is obligatorily biased (speaker expects yes). Hindi-Urdu/Italian: rising declaratives can be neutral. This follows from whether clause-typing is forced at C (CP-typed) or routed through PerspP. (Italian neutralOk := true is contested in the rising-declarative literature, e.g. Gunlogson 2003 vs Bartels 1999; Dayal 2025 makes the specific claim — UNVERIFIED page numbers.)

language : String
neutralOk : Bool
Can a rising declarative be a neutral (unbiased) question?
obligatorilyBiased : Bool
Is a rising declarative always biased?
clauseTyping : ClauseTypingStrategy

Instances For

def Dayal2025.instReprDeclarativeQuestionDatum.repr :

DeclarativeQuestionDatum → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Dayal2025.instReprDeclarativeQuestionDatum :

Repr DeclarativeQuestionDatum

Equations

Dayal2025.instReprDeclarativeQuestionDatum = { reprPrec := Dayal2025.instReprDeclarativeQuestionDatum.repr }

def Dayal2025.english_decl_q :

DeclarativeQuestionDatum

Equations

Dayal2025.english_decl_q = { language := "English", neutralOk := false, obligatorilyBiased := true, clauseTyping := Dayal2025.ClauseTypingStrategy.cpTyped }

Instances For

def Dayal2025.hindi_urdu_decl_q :

DeclarativeQuestionDatum

Equations

Dayal2025.hindi_urdu_decl_q = { language := "Hindi-Urdu", neutralOk := true, obligatorilyBiased := false, clauseTyping := Dayal2025.ClauseTypingStrategy.perspPTyped }

Instances For

def Dayal2025.italian_decl_q :

DeclarativeQuestionDatum

Equations

Dayal2025.italian_decl_q = { language := "Italian", neutralOk := true, obligatorilyBiased := false, clauseTyping := Dayal2025.ClauseTypingStrategy.cpTyped }

Instances For

def Dayal2025.allDeclQData :

List DeclarativeQuestionDatum

Equations

Dayal2025.allDeclQData = [Dayal2025.english_decl_q, Dayal2025.hindi_urdu_decl_q, Dayal2025.italian_decl_q]

Instances For

structure Dayal2025.CrossLingShiftinessDatum :

Cross-linguistic shiftiness data. Parallels McCloskey's English data. Hindi-Urdu kya: shows the same pattern as English embedded inversion: blocked under bare responsive, licensed under negation/questioning.

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

Instances For

def Dayal2025.instReprCrossLingShiftinessDatum.repr :

CrossLingShiftinessDatum → ℕ → Std.Format

Equations

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

Instances For

@[implicit_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: (Dayal 2025: ex (39a)).

Equations

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

Instances For

def Dayal2025.hindi_urdu_know_bare :

CrossLingShiftinessDatum

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

Equations

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

Instances For

def Dayal2025.hindi_urdu_know_negated :

CrossLingShiftinessDatum

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

Equations

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

Instances For

def Dayal2025.hindi_urdu_know_questioned :

CrossLingShiftinessDatum

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

Equations

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

Instances For

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]

Instances For

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 }

Instances For

def Dayal2025.remember_negated :

CrossLingShiftinessDatum

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

Equations

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

Instances For

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 }

Instances For

theorem Dayal2025.hindi_urdu_shiftiness_parallels_english :

hindi_urdu_know_bare.quasiSubOk = false ∧ hindi_urdu_know_negated.quasiSubOk = true ∧ hindi_urdu_know_questioned.quasiSubOk = true

Hindi-Urdu shiftiness parallels English: bare responsive blocks quasi-sub, negation and questioning license it.

structure Dayal2025.ConjunctDisjunctDatum :

Newari uses conjunct vs disjunct verb forms sensitive to whether the subject is coindexed with the perspectival center (Seat of Knowledge).

Declaratives: conjunct = 1st person subject (SoK = speaker)
Interrogatives: conjunct = 2nd person subject (SoK = addressee) This provides independent evidence for perspective shift in questions (canonical Newari conjunct/disjunct pattern; Zu 2018 reanalyses as perspective shift).

language : String
clauseType : String
conjunctPerson : String

Instances For

@[implicit_reducible]

instance Dayal2025.instReprConjunctDisjunctDatum :

Repr ConjunctDisjunctDatum

Equations

Dayal2025.instReprConjunctDisjunctDatum = { reprPrec := Dayal2025.instReprConjunctDisjunctDatum.repr }

def Dayal2025.instReprConjunctDisjunctDatum.repr :

ConjunctDisjunctDatum → ℕ → Std.Format

Equations

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

Instances For

def Dayal2025.newari_declarative :

ConjunctDisjunctDatum

Equations

Dayal2025.newari_declarative = { language := "Newari", clauseType := "declarative", conjunctPerson := "1st" }

Instances For

def Dayal2025.newari_interrogative :

ConjunctDisjunctDatum

Equations

Dayal2025.newari_interrogative = { language := "Newari", clauseType := "interrogative", conjunctPerson := "2nd" }

Instances For

def Dayal2025.allConjunctDisjunctData :

List ConjunctDisjunctDatum

Equations

Dayal2025.allConjunctDisjunctData = [Dayal2025.newari_declarative, Dayal2025.newari_interrogative]

Instances For

structure Dayal2025.EmbeddingDatum :

Embedding judgment for an English attitude predicate ([Day25]: §§1–3).

verb : String
subordination : Bool
"V whether/who..."
quasiSubordination : Bool
"V [did S leave↑]" (embedded inversion + matrix intonation)
quotation : Bool
'V, "Did S leave?"'

Instances For

def Dayal2025.instReprEmbeddingDatum.repr :

EmbeddingDatum → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Dayal2025.instReprEmbeddingDatum :

Repr EmbeddingDatum

Equations

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

def Dayal2025.investigate_d :

Equations

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

Instances For

def Dayal2025.depend_on_d :

Equations

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

Instances For

def Dayal2025.wonder_d :

Equations

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

Instances For

def Dayal2025.ask_d :

Equations

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

Instances For

def Dayal2025.know_d :

Equations

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

Instances For

def Dayal2025.care_d :

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 }

Instances For

def Dayal2025.matter_d :

Predicate of Relevance ([EKSU17]).

Equations

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

Instances For

def Dayal2025.believe_d :

Equations

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

Instances For

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]

Instances For

theorem Dayal2025.quasi_sub_implies_sub (d : EmbeddingDatum) :

d ∈ allEmbeddingData → d.quasiSubordination = true → d.subordination = true

Quasi-subordination implies subordination ([Day25]).

theorem Dayal2025.quotation_implies_quasi_sub (d : EmbeddingDatum) :

d ∈ allEmbeddingData → d.quotation = true → d.quasiSubordination = true

Quotation implies quasi-subordination ([Day25]).

def Dayal2025.classifyVerb :

String → Minimalist.LeftPeriphery.SelectionClass

Classify each empirical embedding datum.

Equations

Instances For

theorem Dayal2025.theory_predicts_embedding (d : EmbeddingDatum) :

d ∈ allEmbeddingData → Minimalist.LeftPeriphery.allowsEmbedding (classifyVerb d.verb) Minimalist.LeftPeriphery.EmbedType.subordination false false = d.subordination ∧ Minimalist.LeftPeriphery.allowsEmbedding (classifyVerb d.verb) Minimalist.LeftPeriphery.EmbedType.quasiSubordination false false = d.quasiSubordination ∧ Minimalist.LeftPeriphery.allowsEmbedding (classifyVerb d.verb) Minimalist.LeftPeriphery.EmbedType.quotation false false = d.quotation

The theory correctly predicts all embedding judgments from the data.

def Dayal2025.classifyCrossLingVerb :

String → Minimalist.LeftPeriphery.SelectionClass

Classify Hindi-Urdu verbs from the cross-linguistic shiftiness data.

Equations

Dayal2025.classifyCrossLingVerb "ja:n-na: ca:h-na: (want to know)" = Minimalist.LeftPeriphery.SelectionClass.rogativePerspP
Dayal2025.classifyCrossLingVerb "ja:n-na: (know)" = Minimalist.LeftPeriphery.SelectionClass.responsive
Dayal2025.classifyCrossLingVerb x✝ = Minimalist.LeftPeriphery.SelectionClass.responsive

Instances For

theorem Dayal2025.cross_linguistic_shiftiness_predicted (d : CrossLingShiftinessDatum) :

d ∈ allCrossLingShiftinessData → Minimalist.LeftPeriphery.allowsQuasiSub (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 under negation/questioning. The theory predicts ALL cross-linguistic data.

theorem Dayal2025.particle_layer_predicts_embedding (p : Particle) :

p ∈ BhattDayal2020.qParticles → (BhattDayal2020.layerOf p = some Features.QParticleLayer.cp → p.LicensedInEmbed Clause.Embedding.subordinated) ∧ (BhattDayal2020.layerOf p = some Features.QParticleLayer.perspP → ¬p.LicensedInEmbed Clause.Embedding.subordinated) ∧ (BhattDayal2020.layerOf p = some Features.QParticleLayer.sap → ¬p.LicensedInEmbed Clause.Embedding.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.

theorem Dayal2025.derived_class_matches_manual :

Minimalist.LeftPeriphery.deriveSelectionClass English.Predicates.Verbal.know = classifyVerb "know" ∧ Minimalist.LeftPeriphery.deriveSelectionClass English.Predicates.Verbal.wonder = classifyVerb "wonder" ∧ Minimalist.LeftPeriphery.deriveSelectionClass English.Predicates.Verbal.ask = classifyVerb "ask" ∧ Minimalist.LeftPeriphery.deriveSelectionClass English.Predicates.Verbal.investigate = classifyVerb "investigate" ∧ Minimalist.LeftPeriphery.deriveSelectionClass English.Predicates.Verbal.believe = classifyVerb "believe"

The structurally derived classification matches the manually-assigned string-based classification for all verbs in the embedding data.

theorem Dayal2025.classifyVerb_agrees_with_selectionClass :

classifyVerb "know" = Minimalist.LeftPeriphery.fieldSelectionClass English.Predicates.Verbal.know ∧ classifyVerb "wonder" = Minimalist.LeftPeriphery.fieldSelectionClass English.Predicates.Verbal.wonder ∧ classifyVerb "ask" = Minimalist.LeftPeriphery.fieldSelectionClass English.Predicates.Verbal.ask ∧ classifyVerb "investigate" = Minimalist.LeftPeriphery.fieldSelectionClass English.Predicates.Verbal.investigate ∧ classifyVerb "depend on" = Minimalist.LeftPeriphery.fieldSelectionClass English.Predicates.Verbal.depend_on ∧ classifyVerb "believe" = Minimalist.LeftPeriphery.fieldSelectionClass English.Predicates.Verbal.believe

String-based classification matches field-based derivation.