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

@cite{dayal-2025} @cite{mccloskey-2006} @cite{zu-2018} @cite{bhatt-dayal-2020}

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:

1. Clause-typing typology (§4.4): forced-CP vs delayed-PerspP variation across English/Italian/Hindi-Urdu (formerly in Phenomena/Questions/Typology.lean §B–C).
2. Hindi-Urdu shiftiness (§3.2): the McCloskey parallel for Hindi-Urdu jaanna: (formerly in Phenomena/Questions/Typology.lean §D).
3. Newari conjunct/disjunct (§5.2): the perspective-shift evidence from Newari person marking (formerly in Phenomena/Questions/Typology.lean §E).
4. Left-Periphery bridge: the verification of the LeftPeriphery SelectionClass apparatus against Phenomena.Questions.Embedding data and the cross-linguistic shiftiness data.

Cross-framework relations

• Rizzi 1997 / Theories/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 Theories/Syntax/Minimalist/Questions.lean.
• Holmberg 2016 / Phenomena/Questions/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 / Theories/Syntax/Minimalist/SpeechActs.lean derives seatOfKnowledge from a 2×2 feature matrix; Dayal places SoK in PerspP with PRO. Both predict the Newari conjunct/disjunct flip; the bridge theorem SpeechActs.SoK ↔ PerspP-PRO over Newari is unformalized.

inductive Phenomena.Questions.Studies.Dayal2025.ClauseTypingStrategy : Type

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).

@[implicit_reducible]

instance Phenomena.Questions.Studies.Dayal2025.instDecidableEqClauseTypingStrategy : DecidableEq ClauseTypingStrategy

Equations

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

def Phenomena.Questions.Studies.Dayal2025.instReprClauseTypingStrategy.repr : ClauseTypingStrategy → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Questions.Studies.Dayal2025.instReprClauseTypingStrategy : Repr ClauseTypingStrategy

Equations

• Phenomena.Questions.Studies.Dayal2025.instReprClauseTypingStrategy = { reprPrec := Phenomena.Questions.Studies.Dayal2025.instReprClauseTypingStrategy.repr }

def Phenomena.Questions.Studies.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

• Phenomena.Questions.Studies.Dayal2025.ClauseTypingStrategy.cpTyped.licensesSimplexSubordination = true
• Phenomena.Questions.Studies.Dayal2025.ClauseTypingStrategy.perspPTyped.licensesSimplexSubordination = false

structure Phenomena.Questions.Studies.Dayal2025.SimplexPolarDatum : Type

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?

def Phenomena.Questions.Studies.Dayal2025.instReprSimplexPolarDatum.repr : SimplexPolarDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Questions.Studies.Dayal2025.instReprSimplexPolarDatum : Repr SimplexPolarDatum

Equations

• Phenomena.Questions.Studies.Dayal2025.instReprSimplexPolarDatum = { reprPrec := Phenomena.Questions.Studies.Dayal2025.instReprSimplexPolarDatum.repr }

def Phenomena.Questions.Studies.Dayal2025.english_simplex : SimplexPolarDatum

Equations

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

def Phenomena.Questions.Studies.Dayal2025.italian_simplex : SimplexPolarDatum

Equations

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

def Phenomena.Questions.Studies.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

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

def Phenomena.Questions.Studies.Dayal2025.allSimplexPolarData : List SimplexPolarDatum

Equations

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

theorem Phenomena.Questions.Studies.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 Phenomena.Questions.Studies.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 Phenomena.Questions.Studies.Dayal2025.DeclarativeQuestionDatum : Type

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

@[implicit_reducible]

instance Phenomena.Questions.Studies.Dayal2025.instReprDeclarativeQuestionDatum : Repr DeclarativeQuestionDatum

Equations

• Phenomena.Questions.Studies.Dayal2025.instReprDeclarativeQuestionDatum = { reprPrec := Phenomena.Questions.Studies.Dayal2025.instReprDeclarativeQuestionDatum.repr }

def Phenomena.Questions.Studies.Dayal2025.instReprDeclarativeQuestionDatum.repr : DeclarativeQuestionDatum → ℕ → Std.Format

Equations

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

def Phenomena.Questions.Studies.Dayal2025.english_decl_q : DeclarativeQuestionDatum

Equations

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

def Phenomena.Questions.Studies.Dayal2025.hindi_urdu_decl_q : DeclarativeQuestionDatum

Equations

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

def Phenomena.Questions.Studies.Dayal2025.italian_decl_q : DeclarativeQuestionDatum

Equations

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

def Phenomena.Questions.Studies.Dayal2025.allDeclQData : List DeclarativeQuestionDatum

Equations

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

structure Phenomena.Questions.Studies.Dayal2025.CrossLingShiftinessDatum : Type

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

def Phenomena.Questions.Studies.Dayal2025.instReprCrossLingShiftinessDatum.repr : CrossLingShiftinessDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Questions.Studies.Dayal2025.instReprCrossLingShiftinessDatum : Repr CrossLingShiftinessDatum

Equations

• Phenomena.Questions.Studies.Dayal2025.instReprCrossLingShiftinessDatum = { reprPrec := Phenomena.Questions.Studies.Dayal2025.instReprCrossLingShiftinessDatum.repr }

def Phenomena.Questions.Studies.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.

def Phenomena.Questions.Studies.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.

def Phenomena.Questions.Studies.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.

def Phenomena.Questions.Studies.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.

def Phenomena.Questions.Studies.Dayal2025.allCrossLingShiftinessData : List CrossLingShiftinessDatum

Equations

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

theorem Phenomena.Questions.Studies.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 Phenomena.Questions.Studies.Dayal2025.ConjunctDisjunctDatum : Type

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

@[implicit_reducible]

instance Phenomena.Questions.Studies.Dayal2025.instReprConjunctDisjunctDatum : Repr ConjunctDisjunctDatum

Equations

• Phenomena.Questions.Studies.Dayal2025.instReprConjunctDisjunctDatum = { reprPrec := Phenomena.Questions.Studies.Dayal2025.instReprConjunctDisjunctDatum.repr }

def Phenomena.Questions.Studies.Dayal2025.instReprConjunctDisjunctDatum.repr : ConjunctDisjunctDatum → ℕ → Std.Format

Equations

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

def Phenomena.Questions.Studies.Dayal2025.newari_declarative : ConjunctDisjunctDatum

Equations

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

def Phenomena.Questions.Studies.Dayal2025.newari_interrogative : ConjunctDisjunctDatum

Equations

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

def Phenomena.Questions.Studies.Dayal2025.allConjunctDisjunctData : List ConjunctDisjunctDatum

Equations

• Phenomena.Questions.Studies.Dayal2025.allConjunctDisjunctData = [Phenomena.Questions.Studies.Dayal2025.newari_declarative, Phenomena.Questions.Studies.Dayal2025.newari_interrogative]

def Phenomena.Questions.Studies.Dayal2025.classifyVerb : String → Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass

Classify each empirical datum from Phenomena.Questions.Embedding.

Equations

• Phenomena.Questions.Studies.Dayal2025.classifyVerb "investigate" = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.rogativeCP
• Phenomena.Questions.Studies.Dayal2025.classifyVerb "depend on" = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.rogativeCP
• Phenomena.Questions.Studies.Dayal2025.classifyVerb "wonder" = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.rogativePerspP
• Phenomena.Questions.Studies.Dayal2025.classifyVerb "ask" = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.rogativeSAP
• Phenomena.Questions.Studies.Dayal2025.classifyVerb "know" = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.responsive
• Phenomena.Questions.Studies.Dayal2025.classifyVerb "care" = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.responsive
• Phenomena.Questions.Studies.Dayal2025.classifyVerb "matter" = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.responsive
• Phenomena.Questions.Studies.Dayal2025.classifyVerb "believe" = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.uninterrogative
• Phenomena.Questions.Studies.Dayal2025.classifyVerb x✝ = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.uninterrogative

theorem Phenomena.Questions.Studies.Dayal2025.theory_predicts_embedding (d : Embedding.EmbeddingDatum) : d ∈ Embedding.allEmbeddingData → Interfaces.SyntaxSemantics.LeftPeriphery.allowsEmbedding (classifyVerb d.verb) Interfaces.SyntaxSemantics.LeftPeriphery.EmbedType.subordination false false = d.subordination ∧ Interfaces.SyntaxSemantics.LeftPeriphery.allowsEmbedding (classifyVerb d.verb) Interfaces.SyntaxSemantics.LeftPeriphery.EmbedType.quasiSubordination false false = d.quasiSubordination ∧ Interfaces.SyntaxSemantics.LeftPeriphery.allowsEmbedding (classifyVerb d.verb) Interfaces.SyntaxSemantics.LeftPeriphery.EmbedType.quotation false false = d.quotation

The theory correctly predicts all embedding judgments from the data.

theorem Phenomena.Questions.Studies.Dayal2025.shiftiness_predicted : Interfaces.SyntaxSemantics.LeftPeriphery.allowsQuasiSub Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.responsive Embedding.remember_bare.negated Embedding.remember_bare.questioned = Embedding.remember_bare.quasiSubOk ∧ Interfaces.SyntaxSemantics.LeftPeriphery.allowsQuasiSub Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.responsive Embedding.remember_negated.negated Embedding.remember_negated.questioned = Embedding.remember_negated.quasiSubOk ∧ Interfaces.SyntaxSemantics.LeftPeriphery.allowsQuasiSub Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.responsive Embedding.remember_questioned.negated Embedding.remember_questioned.questioned = Embedding.remember_questioned.quasiSubOk

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

def Phenomena.Questions.Studies.Dayal2025.classifyCrossLingVerb : String → Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass

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

Equations

• Phenomena.Questions.Studies.Dayal2025.classifyCrossLingVerb "ja:n-na: ca:h-na: (want to know)" = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.rogativePerspP
• Phenomena.Questions.Studies.Dayal2025.classifyCrossLingVerb "ja:n-na: (know)" = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.responsive
• Phenomena.Questions.Studies.Dayal2025.classifyCrossLingVerb x✝ = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.responsive

theorem Phenomena.Questions.Studies.Dayal2025.cross_linguistic_shiftiness_predicted (d : CrossLingShiftinessDatum) : d ∈ allCrossLingShiftinessData → Interfaces.SyntaxSemantics.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 Phenomena.Questions.Studies.Dayal2025.particle_layer_predicts_embedding (d : BhattDayal2020.QParticleDatum) : d ∈ BhattDayal2020.allQParticleData → (d.layer = Features.QParticleLayer.cp → d.inSubordinated = true) ∧ (d.layer = Features.QParticleLayer.perspP → d.inSubordinated = false) ∧ (d.layer = Features.QParticleLayer.sap → d.inQuasiSub = false)

Q-particle embedding follows from which left-peripheral layer they occupy. CP-layer particles appear in subordination; PerspP and SAP particles do not.

theorem Phenomena.Questions.Studies.Dayal2025.derived_class_matches_manual : Interfaces.SyntaxSemantics.LeftPeriphery.deriveSelectionClass Fragments.English.Predicates.Verbal.know = classifyVerb "know" ∧ Interfaces.SyntaxSemantics.LeftPeriphery.deriveSelectionClass Fragments.English.Predicates.Verbal.wonder = classifyVerb "wonder" ∧ Interfaces.SyntaxSemantics.LeftPeriphery.deriveSelectionClass Fragments.English.Predicates.Verbal.ask = classifyVerb "ask" ∧ Interfaces.SyntaxSemantics.LeftPeriphery.deriveSelectionClass Fragments.English.Predicates.Verbal.investigate = classifyVerb "investigate" ∧ Interfaces.SyntaxSemantics.LeftPeriphery.deriveSelectionClass Fragments.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 Phenomena.Questions.Studies.Dayal2025.classifyVerb_agrees_with_selectionClass : classifyVerb "know" = Interfaces.SyntaxSemantics.LeftPeriphery.fieldSelectionClass Fragments.English.Predicates.Verbal.know ∧ classifyVerb "wonder" = Interfaces.SyntaxSemantics.LeftPeriphery.fieldSelectionClass Fragments.English.Predicates.Verbal.wonder ∧ classifyVerb "ask" = Interfaces.SyntaxSemantics.LeftPeriphery.fieldSelectionClass Fragments.English.Predicates.Verbal.ask ∧ classifyVerb "investigate" = Interfaces.SyntaxSemantics.LeftPeriphery.fieldSelectionClass Fragments.English.Predicates.Verbal.investigate ∧ classifyVerb "depend on" = Interfaces.SyntaxSemantics.LeftPeriphery.fieldSelectionClass Fragments.English.Predicates.Verbal.depend_on ∧ classifyVerb "believe" = Interfaces.SyntaxSemantics.LeftPeriphery.fieldSelectionClass Fragments.English.Predicates.Verbal.believe

String-based classification matches field-based derivation.