Cross-Linguistic Question Typology

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

Theory-neutral cross-linguistic data on question formation and embedding, following @cite{dayal-2025}. Covers:

1. Clause-typing variation: forced (English, Italian) vs delayed (Hindi-Urdu)
2. Simplex polar questions: subordination restricted by clause-typing strategy
3. Declarative questions: bias conditioned by clause-typing
4. Shiftiness: responsive predicates shift under negation/questioning
5. Conjunct/disjunct marking: Newari person-sensitive verb morphology

Q-particle data classified by left-peripheral layer (which imports from Theories/) lives in Questions.TypologyBridge.

Languages covered

• English, Hindi-Urdu, Japanese, Italian, Newari

inductive Phenomena.Questions.Typology.ClauseTypingStrategy : Type

How a language handles clause-typing for polar questions at CP.

• forced : ClauseTypingStrategy
• delayed : ClauseTypingStrategy

instance Phenomena.Questions.Typology.instDecidableEqClauseTypingStrategy : DecidableEq ClauseTypingStrategy

Equations

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

instance Phenomena.Questions.Typology.instReprClauseTypingStrategy : Repr ClauseTypingStrategy

Equations

• Phenomena.Questions.Typology.instReprClauseTypingStrategy = { reprPrec := Phenomena.Questions.Typology.instReprClauseTypingStrategy.repr }

def Phenomena.Questions.Typology.instReprClauseTypingStrategy.repr : ClauseTypingStrategy → Nat → Std.Format

Equations

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

instance Phenomena.Questions.Typology.instBEqClauseTypingStrategy : BEq ClauseTypingStrategy

Equations

• Phenomena.Questions.Typology.instBEqClauseTypingStrategy = { beq := Phenomena.Questions.Typology.instBEqClauseTypingStrategy.beq }

def Phenomena.Questions.Typology.instBEqClauseTypingStrategy.beq : ClauseTypingStrategy → ClauseTypingStrategy → Bool

Equations

• Phenomena.Questions.Typology.instBEqClauseTypingStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Phenomena.Questions.Typology.SimplexPolarDatum : Type

Data on simplex polar question embedding across languages. A simplex polar question is just the nucleus p (no "or not"). Hindi-Urdu: simplex polars in matrix/quasi-sub but NOT subordination. English/Italian: simplex polars in all three positions (via whether/se).

• language : String
• clauseTyping : ClauseTypingStrategy
• matrixOk : Bool

  Simplex polar in matrix?

• quasiSubOk : Bool

  Simplex polar in quasi-subordination?

• subordinationOk : Bool

  Simplex polar in subordination?

instance Phenomena.Questions.Typology.instReprSimplexPolarDatum : Repr SimplexPolarDatum

Equations

• Phenomena.Questions.Typology.instReprSimplexPolarDatum = { reprPrec := Phenomena.Questions.Typology.instReprSimplexPolarDatum.repr }

def Phenomena.Questions.Typology.instReprSimplexPolarDatum.repr : SimplexPolarDatum → Nat → Std.Format

Equations

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

def Phenomena.Questions.Typology.english_simplex : SimplexPolarDatum

Equations

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

def Phenomena.Questions.Typology.italian_simplex : SimplexPolarDatum

Equations

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

def Phenomena.Questions.Typology.hindi_urdu_simplex : SimplexPolarDatum

Equations

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

def Phenomena.Questions.Typology.allSimplexPolarData : List SimplexPolarDatum

Equations

• Phenomena.Questions.Typology.allSimplexPolarData = [Phenomena.Questions.Typology.english_simplex, Phenomena.Questions.Typology.italian_simplex, Phenomena.Questions.Typology.hindi_urdu_simplex]

theorem Phenomena.Questions.Typology.delayed_blocks_simplex_subordination (d : SimplexPolarDatum) : d ∈ allSimplexPolarData → d.clauseTyping = ClauseTypingStrategy.delayed → d.subordinationOk = false

Delayed clause-typing languages cannot subordinate simplex polars.

structure Phenomena.Questions.Typology.DeclarativeQuestionDatum : Type

Whether declarative questions in a language are obligatorily biased. English: "You drink wine?" is obligatorily biased (speaker expects yes). Hindi-Urdu/Italian: "a:p shara:b pi:te hai?" / "Bevi il vino?" can be neutral. This follows from whether clause-typing is forced at CP.

• language : String
• neutralOk : Bool

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

• obligatorilyBiased : Bool

  Is a rising declarative always biased?

• clauseTyping : ClauseTypingStrategy

instance Phenomena.Questions.Typology.instReprDeclarativeQuestionDatum : Repr DeclarativeQuestionDatum

Equations

• Phenomena.Questions.Typology.instReprDeclarativeQuestionDatum = { reprPrec := Phenomena.Questions.Typology.instReprDeclarativeQuestionDatum.repr }

def Phenomena.Questions.Typology.instReprDeclarativeQuestionDatum.repr : DeclarativeQuestionDatum → Nat → Std.Format

Equations

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

def Phenomena.Questions.Typology.english_decl_q : DeclarativeQuestionDatum

Equations

• Phenomena.Questions.Typology.english_decl_q = { language := "English", neutralOk := false, obligatorilyBiased := true, clauseTyping := Phenomena.Questions.Typology.ClauseTypingStrategy.forced }

def Phenomena.Questions.Typology.hindi_urdu_decl_q : DeclarativeQuestionDatum

Equations

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

def Phenomena.Questions.Typology.italian_decl_q : DeclarativeQuestionDatum

Equations

• Phenomena.Questions.Typology.italian_decl_q = { language := "Italian", neutralOk := true, obligatorilyBiased := false, clauseTyping := Phenomena.Questions.Typology.ClauseTypingStrategy.forced }

def Phenomena.Questions.Typology.allDeclQData : List DeclarativeQuestionDatum

Equations

• Phenomena.Questions.Typology.allDeclQData = [Phenomena.Questions.Typology.english_decl_q, Phenomena.Questions.Typology.hindi_urdu_decl_q, Phenomena.Questions.Typology.italian_decl_q]

structure Phenomena.Questions.Typology.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.Typology.instReprCrossLingShiftinessDatum.repr : CrossLingShiftinessDatum → Nat → Std.Format

Equations

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

instance Phenomena.Questions.Typology.instReprCrossLingShiftinessDatum : Repr CrossLingShiftinessDatum

Equations

• Phenomena.Questions.Typology.instReprCrossLingShiftinessDatum = { reprPrec := Phenomena.Questions.Typology.instReprCrossLingShiftinessDatum.repr }

def Phenomena.Questions.Typology.hindi_urdu_want_to_know : CrossLingShiftinessDatum

Equations

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

def Phenomena.Questions.Typology.hindi_urdu_know_bare : CrossLingShiftinessDatum

Equations

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

def Phenomena.Questions.Typology.hindi_urdu_know_negated : CrossLingShiftinessDatum

Equations

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

def Phenomena.Questions.Typology.hindi_urdu_know_questioned : CrossLingShiftinessDatum

Equations

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

def Phenomena.Questions.Typology.allCrossLingShiftinessData : List CrossLingShiftinessDatum

Equations

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

theorem Phenomena.Questions.Typology.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.Typology.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.

• language : String
• clauseType : String
• conjunctPerson : String

def Phenomena.Questions.Typology.instReprConjunctDisjunctDatum.repr : ConjunctDisjunctDatum → Nat → Std.Format

Equations

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

instance Phenomena.Questions.Typology.instReprConjunctDisjunctDatum : Repr ConjunctDisjunctDatum

Equations

• Phenomena.Questions.Typology.instReprConjunctDisjunctDatum = { reprPrec := Phenomena.Questions.Typology.instReprConjunctDisjunctDatum.repr }

def Phenomena.Questions.Typology.newari_declarative : ConjunctDisjunctDatum

Equations

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

def Phenomena.Questions.Typology.newari_interrogative : ConjunctDisjunctDatum

Equations

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

def Phenomena.Questions.Typology.allConjunctDisjunctData : List ConjunctDisjunctDatum

Equations

• Phenomena.Questions.Typology.allConjunctDisjunctData = [Phenomena.Questions.Typology.newari_declarative, Phenomena.Questions.Typology.newari_interrogative]

inductive Phenomena.Questions.Typology.QParticlePosition : Type

WALS Ch 92A: Position of polar question particles.

• initial : QParticlePosition
• final : QParticlePosition
• secondPosition : QParticlePosition
• otherPosition : QParticlePosition
• eitherOfTwo : QParticlePosition
• noParticle : QParticlePosition

instance Phenomena.Questions.Typology.instDecidableEqQParticlePosition : DecidableEq QParticlePosition

Equations

• Phenomena.Questions.Typology.instDecidableEqQParticlePosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Questions.Typology.instBEqQParticlePosition.beq : QParticlePosition → QParticlePosition → Bool

Equations

• Phenomena.Questions.Typology.instBEqQParticlePosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Questions.Typology.instBEqQParticlePosition : BEq QParticlePosition

Equations

• Phenomena.Questions.Typology.instBEqQParticlePosition = { beq := Phenomena.Questions.Typology.instBEqQParticlePosition.beq }

instance Phenomena.Questions.Typology.instReprQParticlePosition : Repr QParticlePosition

Equations

• Phenomena.Questions.Typology.instReprQParticlePosition = { reprPrec := Phenomena.Questions.Typology.instReprQParticlePosition.repr }

def Phenomena.Questions.Typology.instReprQParticlePosition.repr : QParticlePosition → Nat → Std.Format

Equations

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

inductive Phenomena.Questions.Typology.WhMovementStrategy : Type

WALS Ch 93A: Position of interrogative phrases (wh-words).

• initial : WhMovementStrategy
• inSitu : WhMovementStrategy
• mixed : WhMovementStrategy

instance Phenomena.Questions.Typology.instDecidableEqWhMovementStrategy : DecidableEq WhMovementStrategy

Equations

• Phenomena.Questions.Typology.instDecidableEqWhMovementStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Questions.Typology.instBEqWhMovementStrategy.beq : WhMovementStrategy → WhMovementStrategy → Bool

Equations

• Phenomena.Questions.Typology.instBEqWhMovementStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Questions.Typology.instBEqWhMovementStrategy : BEq WhMovementStrategy

Equations

• Phenomena.Questions.Typology.instBEqWhMovementStrategy = { beq := Phenomena.Questions.Typology.instBEqWhMovementStrategy.beq }

def Phenomena.Questions.Typology.instReprWhMovementStrategy.repr : WhMovementStrategy → Nat → Std.Format

Equations

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

instance Phenomena.Questions.Typology.instReprWhMovementStrategy : Repr WhMovementStrategy

Equations

• Phenomena.Questions.Typology.instReprWhMovementStrategy = { reprPrec := Phenomena.Questions.Typology.instReprWhMovementStrategy.repr }

inductive Phenomena.Questions.Typology.PolarQuestionStrategy : Type

WALS Ch 116A: How polar questions are formed.

• particle : PolarQuestionStrategy
• verbMorphology : PolarQuestionStrategy
• particleOrMorphology : PolarQuestionStrategy
• wordOrder : PolarQuestionStrategy
• absenceOfDeclarative : PolarQuestionStrategy
• intonationOnly : PolarQuestionStrategy
• noDistinction : PolarQuestionStrategy

instance Phenomena.Questions.Typology.instDecidableEqPolarQuestionStrategy : DecidableEq PolarQuestionStrategy

Equations

• Phenomena.Questions.Typology.instDecidableEqPolarQuestionStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Questions.Typology.instBEqPolarQuestionStrategy.beq : PolarQuestionStrategy → PolarQuestionStrategy → Bool

Equations

• Phenomena.Questions.Typology.instBEqPolarQuestionStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Questions.Typology.instBEqPolarQuestionStrategy : BEq PolarQuestionStrategy

Equations

• Phenomena.Questions.Typology.instBEqPolarQuestionStrategy = { beq := Phenomena.Questions.Typology.instBEqPolarQuestionStrategy.beq }

def Phenomena.Questions.Typology.instReprPolarQuestionStrategy.repr : PolarQuestionStrategy → Nat → Std.Format

Equations

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

instance Phenomena.Questions.Typology.instReprPolarQuestionStrategy : Repr PolarQuestionStrategy

Equations

• Phenomena.Questions.Typology.instReprPolarQuestionStrategy = { reprPrec := Phenomena.Questions.Typology.instReprPolarQuestionStrategy.repr }

theorem Phenomena.Questions.Typology.ch92_total : Phenomena.Questions.Typology.ch92✝.length = 884

theorem Phenomena.Questions.Typology.ch93_total : Phenomena.Questions.Typology.ch93✝.length = 902

theorem Phenomena.Questions.Typology.ch116_total : Phenomena.Questions.Typology.ch116✝.length = 955

structure Phenomena.Questions.Typology.QuestionProfile : Type

A language's question-formation profile across WALS Chapters 92A, 93A, 116A.

• language : String

  Language name.

• walsCode : String

  WALS language code.

• qParticlePos : Option QParticlePosition

  Ch 92A: Position of polar question particles.

• whMovement : Option WhMovementStrategy

  Ch 93A: Wh-phrase position in content questions.

• polarStrategy : Option PolarQuestionStrategy

  Ch 116A: Strategy for forming polar questions.

instance Phenomena.Questions.Typology.instReprQuestionProfile : Repr QuestionProfile

Equations

• Phenomena.Questions.Typology.instReprQuestionProfile = { reprPrec := Phenomena.Questions.Typology.instReprQuestionProfile.repr }

def Phenomena.Questions.Typology.instReprQuestionProfile.repr : QuestionProfile → Nat → Std.Format

Equations

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

def Phenomena.Questions.Typology.english_qProfile : QuestionProfile

Equations

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

def Phenomena.Questions.Typology.hindi_qProfile : QuestionProfile

Equations

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

def Phenomena.Questions.Typology.japanese_qProfile : QuestionProfile

Equations

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

def Phenomena.Questions.Typology.italian_qProfile : QuestionProfile

Equations

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

def Phenomena.Questions.Typology.newari_qProfile : QuestionProfile

Equations

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

def Phenomena.Questions.Typology.allQuestionProfiles : List QuestionProfile

Equations

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

theorem Phenomena.Questions.Typology.english_ch92 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F92A.PositionOfPolarQuestionParticles) => Phenomena.Questions.Typology.fromWALS92A✝ x.value) (Core.WALS.F92A.lookup "eng") = english_qProfile.qParticlePos

theorem Phenomena.Questions.Typology.hindi_ch92 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F92A.PositionOfPolarQuestionParticles) => Phenomena.Questions.Typology.fromWALS92A✝ x.value) (Core.WALS.F92A.lookup "hin") = hindi_qProfile.qParticlePos

theorem Phenomena.Questions.Typology.japanese_ch92 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F92A.PositionOfPolarQuestionParticles) => Phenomena.Questions.Typology.fromWALS92A✝ x.value) (Core.WALS.F92A.lookup "jpn") = japanese_qProfile.qParticlePos

theorem Phenomena.Questions.Typology.italian_ch92 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F92A.PositionOfPolarQuestionParticles) => Phenomena.Questions.Typology.fromWALS92A✝ x.value) (Core.WALS.F92A.lookup "ita") = italian_qProfile.qParticlePos

theorem Phenomena.Questions.Typology.newari_ch92 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F92A.PositionOfPolarQuestionParticles) => Phenomena.Questions.Typology.fromWALS92A✝ x.value) (Core.WALS.F92A.lookup "new") = newari_qProfile.qParticlePos

theorem Phenomena.Questions.Typology.english_ch93 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F93A.PositionOfInterrogativePhrasesInContentQuestions) => Phenomena.Questions.Typology.fromWALS93A✝ x.value) (Core.WALS.F93A.lookup "eng") = english_qProfile.whMovement

theorem Phenomena.Questions.Typology.hindi_ch93 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F93A.PositionOfInterrogativePhrasesInContentQuestions) => Phenomena.Questions.Typology.fromWALS93A✝ x.value) (Core.WALS.F93A.lookup "hin") = hindi_qProfile.whMovement

theorem Phenomena.Questions.Typology.japanese_ch93 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F93A.PositionOfInterrogativePhrasesInContentQuestions) => Phenomena.Questions.Typology.fromWALS93A✝ x.value) (Core.WALS.F93A.lookup "jpn") = japanese_qProfile.whMovement

theorem Phenomena.Questions.Typology.newari_ch93 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F93A.PositionOfInterrogativePhrasesInContentQuestions) => Phenomena.Questions.Typology.fromWALS93A✝ x.value) (Core.WALS.F93A.lookup "new") = newari_qProfile.whMovement

theorem Phenomena.Questions.Typology.english_ch116 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F116A.PolarQuestionType) => Phenomena.Questions.Typology.fromWALS116A✝ x.value) (Core.WALS.F116A.lookup "eng") = english_qProfile.polarStrategy

theorem Phenomena.Questions.Typology.hindi_ch116 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F116A.PolarQuestionType) => Phenomena.Questions.Typology.fromWALS116A✝ x.value) (Core.WALS.F116A.lookup "hin") = hindi_qProfile.polarStrategy

theorem Phenomena.Questions.Typology.japanese_ch116 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F116A.PolarQuestionType) => Phenomena.Questions.Typology.fromWALS116A✝ x.value) (Core.WALS.F116A.lookup "jpn") = japanese_qProfile.polarStrategy

theorem Phenomena.Questions.Typology.italian_ch116 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F116A.PolarQuestionType) => Phenomena.Questions.Typology.fromWALS116A✝ x.value) (Core.WALS.F116A.lookup "ita") = italian_qProfile.polarStrategy

theorem Phenomena.Questions.Typology.newari_ch116 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F116A.PolarQuestionType) => Phenomena.Questions.Typology.fromWALS116A✝ x.value) (Core.WALS.F116A.lookup "new") = newari_qProfile.polarStrategy