Dayal (2025): The interrogative left periphery

Question meaning is built at three points of the left periphery. At C a proposition becomes a set of propositions; at PerspP a perspectival center is introduced for whom the question is potentially active, which presupposes that the center may not know the answer; at SAP the speaker puts the addressee under an obligation to answer. Embedding predicates select up to one of the layers, and the middle one, quasi-subordination with matrix syntax and intonation, carries a semantic filter: know and remember assert knowledge of the answer and so cannot host it, negation or questioning of them and forget leave the center's ignorance open and can, which is McCloskey's shiftiness. Boundary tones realize the features of the two upper layers, so a declarative question is biased in English, where C is typed early, and can be neutral in Hindi-Urdu and Italian, where typing is delayed; and a bare polar clause can only be subordinated where a complementizer or Q-morpheme types it, which Hindi-Urdu lacks. Question particles sit at the layer their embedding distribution shows.

Implementation notes

• Predicates enter through their at-issue content as a set of worlds: know and remember are the center's knowledge of the answer at the evaluation time and forget its negation (43b), the past presuppositions set aside as the paper does.
• Boundary tones stand in for the features they realize: Persp_CQ and SA_ASK rise, Persp_CP and SA_ASSERT fall, the combined act of a biased question licenses both (§4.3).

TODO

• The de se requirement of §3.3, disjoined questions (§4.2), imperatives, sentience and rhetorical questions (§5), and selection (§6) are not formalized. The centering condition alone licenses Have you forgotten [was Henry a communist], which the paper marks unacceptable and attributes to who is invested in the answer (possiblyIgnorant_forgets_question_iff).

References

• V. Dayal, The interrogative left periphery (2025)
• J. McCloskey, Questions and questioning in a local English (2006)
• R. Bhatt and V. Dayal, Polar question particles (2020)
• U. Sauerland and K. Yatsushiro, Remind-me presuppositions and speech-act decomposition (2017)
• C. Gunlogson, True to form (2004)
• D. Büring and C. Gunlogson, Aren't positive and negative polar questions the same? (2000)
• D. Büring, Intonation and meaning (2016)
• L. Cheng, On the typology of wh-questions (1991)
• M. Speas and C. Tenny, Configurational properties of point of view roles (2003)
• M. Krifka, Embedding illocutionary acts (2014)
• V. Dayal, Locality in WH quantification (1996)
• X. V. Zu, Discourse participants and the structural representation of the context (2018)

The left periphery

The WH-feature on C, the three layers ordered by height, and the classes of embedding predicates by the largest layer they select.

inductive Dayal2025.WHFeature : Type

The WH-feature on C is interrogative, declarative, or unspecified with typing delayed to a higher layer (Hindi-Urdu polar clauses, [Day25] §4.4).

• plusWH : WHFeature
• minusWH : WHFeature
• alphaWH : WHFeature

@[instance_reducible]

instance Dayal2025.instDecidableEqWHFeature : DecidableEq WHFeature

Equations

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

def Dayal2025.instReprWHFeature.repr : WHFeature → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Dayal2025.instReprWHFeature.repr Dayal2025.WHFeature.plusWH prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dayal2025.WHFeature.plusWH")).group prec✝

@[instance_reducible]

instance Dayal2025.instReprWHFeature : Repr WHFeature

Equations

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

@[instance_reducible]

instance Dayal2025.instFintypeWHFeature : Fintype WHFeature

Equations

• Dayal2025.instFintypeWHFeature = { elems := { val := ↑Dayal2025.WHFeature.enumList, nodup := Dayal2025.WHFeature.enumList_nodup }, complete := Dayal2025.instFintypeWHFeature._proof_1 }

inductive Dayal2025.PeripheryLayer : Type

The interrogative left periphery has three layers, clause typing at C, centering at PerspP, and the speech act at SAP.

• cp : PeripheryLayer
• perspP : PeripheryLayer
• sap : PeripheryLayer

@[instance_reducible]

instance Dayal2025.instDecidableEqPeripheryLayer : DecidableEq PeripheryLayer

Equations

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

def Dayal2025.instReprPeripheryLayer.repr : PeripheryLayer → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Dayal2025.instReprPeripheryLayer : Repr PeripheryLayer

Equations

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

@[instance_reducible]

instance Dayal2025.instFintypePeripheryLayer : Fintype PeripheryLayer

Equations

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

def Dayal2025.PeripheryLayer.height : PeripheryLayer → ℕ

The height of a layer in the periphery.

Equations

• Dayal2025.PeripheryLayer.cp.height = 0
• Dayal2025.PeripheryLayer.perspP.height = 1
• Dayal2025.PeripheryLayer.sap.height = 2

@[instance_reducible]

instance Dayal2025.instLinearOrderPeripheryLayer : LinearOrder PeripheryLayer

Layers ordered by height.

Equations

• Dayal2025.instLinearOrderPeripheryLayer = LinearOrder.lift' Dayal2025.PeripheryLayer.height Dayal2025.instLinearOrderPeripheryLayer._proof_1

inductive Dayal2025.SelectionClass : Type

Embedding predicates are classed by the largest left-peripheral structure they select ([Day25] §1.2). Uninterrogatives take no interrogative; rogatives take CP only (depend on, investigate), PerspP (wonder, want to know) or SAP (ask); responsives (know, remember, forget) take CP and, where their meaning leaves the center's ignorance open, PerspP.

• uninterrogative : SelectionClass
• rogativeCP : SelectionClass
• rogativePerspP : SelectionClass
• rogativeSAP : SelectionClass
• responsive : SelectionClass

@[instance_reducible]

instance Dayal2025.instDecidableEqSelectionClass : DecidableEq SelectionClass

Equations

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

def Dayal2025.instReprSelectionClass.repr : SelectionClass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Dayal2025.instReprSelectionClass : Repr SelectionClass

Equations

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

@[instance_reducible]

instance Dayal2025.instFintypeSelectionClass : Fintype SelectionClass

Equations

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

def Dayal2025.SelectionClass.layer : SelectionClass → Option PeripheryLayer

The largest layer a class selects.

Equations

• Dayal2025.SelectionClass.uninterrogative.layer = none
• Dayal2025.SelectionClass.rogativeCP.layer = some Dayal2025.PeripheryLayer.cp
• Dayal2025.SelectionClass.rogativePerspP.layer = some Dayal2025.PeripheryLayer.perspP
• Dayal2025.SelectionClass.rogativeSAP.layer = some Dayal2025.PeripheryLayer.sap
• Dayal2025.SelectionClass.responsive.layer = some Dayal2025.PeripheryLayer.perspP

def Dayal2025.deriveSelectionClass (v : Verb) : SelectionClass

The selection class of a lexical entry. Question-taking factives are responsive, non-veridical doxastic attitudes uninterrogative, question-taking speech-act verbs select SAP, opaque question-taking verbs PerspP, and other question-taking verbs CP.

Equations

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

def Dayal2025.deriveSelectionClass.citationQuestion (v : Verb) : Bool

The basic frame is an embedded question.

Equations

• Dayal2025.deriveSelectionClass.citationQuestion v = decide (∃ fr ∈ v.valency.frames.head?, ∃ (t : Clause.SentenceType), t.IsInterrogative ∧ fr.hasType t)

The three layers (7), (20)

def Dayal2025.layerOfContext : Clause.EmbeddingContext → PeripheryLayer

The layer an embedding context reaches is CP under subordination, PerspP under quasi-subordination, and SAP for a matrix clause, a quotation or an insubordinated root utterance.

Equations

• Dayal2025.layerOfContext Clause.EmbeddingContext.subordinated = Dayal2025.PeripheryLayer.cp
• Dayal2025.layerOfContext Clause.EmbeddingContext.quasiSubordinated = Dayal2025.PeripheryLayer.perspP
• Dayal2025.layerOfContext Clause.EmbeddingContext.matrix = Dayal2025.PeripheryLayer.sap
• Dayal2025.layerOfContext Clause.EmbeddingContext.quotation = Dayal2025.PeripheryLayer.sap
• Dayal2025.layerOfContext Clause.EmbeddingContext.insubordinated = Dayal2025.PeripheryLayer.sap

def Dayal2025.Selects (cls : SelectionClass) (e : Clause.EmbeddingContext) : Prop

A class takes an embedding context when the context's layer is within what it selects.

Equations

• Dayal2025.Selects cls e = match cls.layer with | none => False | some l => Dayal2025.layerOfContext e ≤ l

@[instance_reducible]

instance Dayal2025.instDecidableSelects (cls : SelectionClass) (e : Clause.EmbeddingContext) : Decidable (Selects cls e)

Equations

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

Question particles (§1.3)

def Dayal2025.layerOf (p : Particle) : Option PeripheryLayer

A particle's layer is read off its embedding distribution (20): CP if it is licensed in subordination, otherwise PerspP if it is licensed in quasi-subordination, otherwise SAP if it is licensed in matrix clauses.

Equations

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

theorem Dayal2025.layers_derived : layerOf Japanese.Particles.ka = some PeripheryLayer.cp ∧ layerOf HindiUrdu.Particles.kya = some PeripheryLayer.perspP ∧ layerOf Japanese.Particles.kke = some PeripheryLayer.sap ∧ layerOf English.Particles.quick = some PeripheryLayer.sap

Japanese ka types the clause at CP, Hindi-Urdu kya: sits at PerspP, and the meta question particles kke and quick sit at SAP, as in (15)–(19).

Centering (25)–(26), (42)–(43)

def Dayal2025.knows {W : Type u_1} (H : Set (Set W)) (Dox : SetRel W W) : Set W

The at-issue content of x knows Q and of x remembers Q is knowledge of the answer at the evaluation time, through the center's doxastic alternatives Dox.

Equations

• Dayal2025.knows H Dox = {w : W | Question.KnowsAnswer H w Dox}

def Dayal2025.forgets {W : Type u_1} (H : Set (Set W)) (Dox : SetRel W W) : Set W

In (43b), x forgets Q is ignorance of the answer, its past-knowledge presupposition set aside.

Equations

• Dayal2025.forgets H Dox = (Dayal2025.knows H Dox)ᶜ

theorem Dayal2025.not_possiblyIgnorant_knows {W : Type u_1} {c : Set W} (H : Set (Set W)) (Dox : SetRel W W) : ¬Question.PossiblyIgnorant H (c ∩ knows H Dox) Dox

Bare know and remember reject quasi-subordination in every context, as in (26d) and (42a), because the requirement of Persp_CQ fails on the context updated with the assertion.

theorem Dayal2025.possiblyIgnorant_forgets_iff {W : Type u_1} {c : Set W} (H : Set (Set W)) (Dox : SetRel W W) : Question.PossiblyIgnorant H (c ∩ forgets H Dox) Dox ↔ Question.PossiblyIgnorant H c Dox

Negated remember and bare forget quasi-subordinate exactly in the contexts where the center may be ignorant, as in (42b) and (43).

theorem Dayal2025.possiblyIgnorant_knows_question_iff {W : Type u_1} {c : Set W} (H : Set (Set W)) (Dox : SetRel W W) : Question.PossiblyIgnorant H (c ∩ (knows H Dox ∪ (knows H Dox)ᶜ)) Dox ↔ Question.PossiblyIgnorant H c Dox

Under a polar question either answer is at issue, so the same holds of Does Sue remember? (42c).

theorem Dayal2025.possiblyIgnorant_forgets_question_iff {W : Type u_1} {c : Set W} (H : Set (Set W)) (Dox : SetRel W W) : Question.PossiblyIgnorant H (c ∩ (forgets H Dox ∪ (forgets H Dox)ᶜ)) Dox ↔ Question.PossiblyIgnorant H c Dox

The same computation licenses Have you forgotten [was Henry a communist] (46b), which the paper marks unacceptable; §3.3 attributes the difference to who is invested in the answer, not formalized here.

Boundary tones and the features they realize (§4.3–4.4)

inductive Dayal2025.Tone : Type

• rise : Tone
• fall : Tone

@[instance_reducible]

instance Dayal2025.instDecidableEqTone : DecidableEq Tone

Equations

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

def Dayal2025.instReprTone.repr : Tone → ℕ → Std.Format

Equations

• Dayal2025.instReprTone.repr Dayal2025.Tone.rise prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dayal2025.Tone.rise")).group prec✝
• Dayal2025.instReprTone.repr Dayal2025.Tone.fall prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dayal2025.Tone.fall")).group prec✝

@[instance_reducible]

instance Dayal2025.instReprTone : Repr Tone

Equations

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

inductive Dayal2025.PerspFeature : Type

The feature on Persp marks a centered question or a centered proposition.

• cq : PerspFeature
• cp : PerspFeature

@[instance_reducible]

instance Dayal2025.instDecidableEqPerspFeature : DecidableEq PerspFeature

Equations

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

@[instance_reducible]

instance Dayal2025.instReprPerspFeature : Repr PerspFeature

Equations

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

def Dayal2025.instReprPerspFeature.repr : PerspFeature → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Dayal2025.instFintypePerspFeature : Fintype PerspFeature

Equations

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

def Dayal2025.PerspFeature.tone : PerspFeature → Tone

The tone a Persp feature is realized as.

Equations

• Dayal2025.PerspFeature.cq.tone = Dayal2025.Tone.rise
• Dayal2025.PerspFeature.cp.tone = Dayal2025.Tone.fall

inductive Dayal2025.Illocution : Type

The illocutionary head is asking, asserting, or the combined act of a biased question (64b).

• ask : Illocution
• assert : Illocution
• assertAsk : Illocution

@[instance_reducible]

instance Dayal2025.instDecidableEqIllocution : DecidableEq Illocution

Equations

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

def Dayal2025.instReprIllocution.repr : Illocution → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Dayal2025.instReprIllocution.repr Dayal2025.Illocution.ask prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dayal2025.Illocution.ask")).group prec✝

@[instance_reducible]

instance Dayal2025.instReprIllocution : Repr Illocution

Equations

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

def Dayal2025.Illocution.licenses : Illocution → Tone → Prop

The tones an illocution licenses.

Equations

• Dayal2025.Illocution.ask.licenses Dayal2025.Tone.rise = True
• Dayal2025.Illocution.assert.licenses Dayal2025.Tone.fall = True
• Dayal2025.Illocution.assertAsk.licenses x✝ = True
• x✝¹.licenses x✝ = False

@[instance_reducible]

instance Dayal2025.instDecidableLicenses (sa : Illocution) (t : Tone) : Decidable (sa.licenses t)

Equations

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

def Dayal2025.demand : WHFeature → Option Tone

The tone C demands of Persp, if C is typed.

Equations

• Dayal2025.demand Dayal2025.WHFeature.plusWH = some Dayal2025.Tone.rise
• Dayal2025.demand Dayal2025.WHFeature.minusWH = some Dayal2025.Tone.fall
• Dayal2025.demand Dayal2025.WHFeature.alphaWH = none

def Dayal2025.AgreesC (f : WHFeature) (p : PerspFeature) : Prop

Persp agrees with C when C, if typed, demands Persp's tone (75).

Equations

• Dayal2025.AgreesC f p = (Dayal2025.demand f = none ∨ Dayal2025.demand f = some p.tone)

@[instance_reducible]

instance Dayal2025.instDecidableAgreesC (f : WHFeature) (p : PerspFeature) : Decidable (AgreesC f p)

Equations

• Dayal2025.instDecidableAgreesC f p = { decide := decide (Dayal2025.demand f = none) || decide (Dayal2025.demand f = some p.tone), reflects_decide := ⋯ }

def Dayal2025.Derivable (f : WHFeature) (p : PerspFeature) (sa : Illocution) : Prop

A full left periphery is derivable when Persp agrees with C and SAP licenses Persp's tone (75).

Equations

• Dayal2025.Derivable f p sa = (Dayal2025.AgreesC f p ∧ sa.licenses p.tone)

@[instance_reducible]

instance Dayal2025.instDecidableDerivable (f : WHFeature) (p : PerspFeature) (sa : Illocution) : Decidable (Derivable f p sa)

Equations

• Dayal2025.instDecidableDerivable f p sa = { decide := decide (Dayal2025.AgreesC f p) && decide (sa.licenses p.tone), reflects_decide := ⋯ }

theorem Dayal2025.english_declarative_biased : Derivable WHFeature.plusWH PerspFeature.cq Illocution.ask ∧ Derivable WHFeature.minusWH PerspFeature.cp Illocution.assertAsk ∧ ∀ (p : PerspFeature), ¬Derivable WHFeature.minusWH p Illocution.ask

With interrogative syntax a neutral question is derivable, and with declarative syntax only the combined act of a biased question is (64).

theorem Dayal2025.delayed_typing_neutral : Derivable WHFeature.alphaWH PerspFeature.cq Illocution.ask ∧ Derivable WHFeature.alphaWH PerspFeature.cp Illocution.assertAsk

Where C may stay untyped, a declarative question has both readings (66).

theorem Dayal2025.no_quasi_declarative_question : ¬AgreesC WHFeature.minusWH PerspFeature.cq

Without SAP a question needs Persp_CQ, which declarative syntax cannot host, so declarative questions do not quasi-subordinate (67).

structure Dayal2025.PolarTyping : Type

A language may type a bare polar clause at C (§4.4) by a polar complementizer (whether, se) or by a clause-typing Q-morpheme (ka).

• polarComplementizer : Bool
• qMorpheme : Bool

@[instance_reducible]

instance Dayal2025.instDecidableEqPolarTyping : DecidableEq PolarTyping

Equations

• Dayal2025.instDecidableEqPolarTyping = Dayal2025.instDecidableEqPolarTyping.decEq

def Dayal2025.instDecidableEqPolarTyping.decEq (x✝ x✝¹ : PolarTyping) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Dayal2025.instReprPolarTyping : Repr PolarTyping

Equations

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

def Dayal2025.instReprPolarTyping.repr : PolarTyping → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Dayal2025.instFintypePolarTyping : Fintype PolarTyping

Equations

• Dayal2025.instFintypePolarTyping = Fintype.ofEquiv ((_ : Bool) × Bool) Dayal2025.PolarTyping.proxyTypeEquiv

def Dayal2025.Typed (L : PolarTyping) (e : Clause.EmbeddingContext) : Prop

A simplex polar clause is clause-typed in a context when a lexical resource types it or the context supplies Persp_CQ above C ((72)).

Equations

• Dayal2025.Typed L e = (L.polarComplementizer = true ∨ L.qMorpheme = true ∨ Dayal2025.PeripheryLayer.perspP ≤ Dayal2025.layerOfContext e)

@[instance_reducible]

instance Dayal2025.instDecidableTyped (L : PolarTyping) (e : Clause.EmbeddingContext) : Decidable (Typed L e)

Equations

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

def Dayal2025.english : PolarTyping

Equations

• Dayal2025.english = { polarComplementizer := true, qMorpheme := false }

def Dayal2025.italian : PolarTyping

Equations

• Dayal2025.italian = { polarComplementizer := true, qMorpheme := false }

def Dayal2025.japanese : PolarTyping

Equations

• Dayal2025.japanese = { polarComplementizer := false, qMorpheme := true }

def Dayal2025.hindiUrdu : PolarTyping

Equations

• Dayal2025.hindiUrdu = { polarComplementizer := false, qMorpheme := false }

theorem Dayal2025.simplex_polar : (∀ (e : Clause.EmbeddingContext), Typed english e ∧ Typed italian e ∧ Typed japanese e) ∧ ¬Typed hindiUrdu Clause.EmbeddingContext.subordinated ∧ Typed hindiUrdu Clause.EmbeddingContext.quasiSubordinated ∧ Typed hindiUrdu Clause.EmbeddingContext.matrix

English and Italian subordinate simplex polar questions and Hindi-Urdu does not, while every language quasi-subordinates them, as in (69)–(71).

theorem Dayal2025.ya_nahi_obligatory_iff (e : Clause.EmbeddingContext) : HindiUrdu.Particles.ya_nahi.distribution Clause.SentenceType.polar e = some Clause.Occurrence.obligatory ↔ ¬Typed hindiUrdu e

The fragment's ya: nahĩ: is obligatory exactly where nothing else types the clause (71).

The paper's judgments

def Dayal2025.verbs : List English.Verbs.Verb

The English predicates of the paper, from the fragment.

Equations

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

def Dayal2025.contextOf : String → Option Clause.EmbeddingContext

The embedding context a row's embedding feature names.

Equations

• Dayal2025.contextOf "subordination" = some Clause.EmbeddingContext.subordinated
• Dayal2025.contextOf "quasi" = some Clause.EmbeddingContext.quasiSubordinated
• Dayal2025.contextOf "quotation" = some Clause.EmbeddingContext.quotation
• Dayal2025.contextOf "matrix" = some Clause.EmbeddingContext.matrix
• Dayal2025.contextOf x✝ = none

def Dayal2025.Fine (j : Judgment) : Prop

A judgment counts as licensed when it is acceptable or marginal, so that McCloskey's ? on (40b) is licensed.

Equations

• Dayal2025.Fine j = (j = Judgment.acceptable ∨ j = Judgment.marginal)

@[instance_reducible]

instance Dayal2025.instDecidableFine (j : Judgment) : Decidable (Fine j)

Equations

• Dayal2025.instDecidableFine j = { decide := decide (j = Judgment.acceptable) || decide (j = Judgment.marginal), reflects_decide := ⋯ }

theorem Dayal2025.selection_rows (row : Datum) : row ∈ Examples.all → ∀ v ∈ verbs, ∀ (e : Clause.EmbeddingContext), row.feature? "verb" = some v.form → (row.feature? "embedding").bind contextOf = some e → e ≠ Clause.EmbeddingContext.quasiSubordinated → (Fine row.judgment ↔ Selects (deriveSelectionClass v.toVerb) e)

Outside quasi-subordination an English predicate embeds an interrogative iff its lexical class, read off the fragment, selects the context's layer, as in (8)–(9), (11), (24) and (84)–(85).

def Dayal2025.assertsKnowledge : String → Bool

In the at-issue content of a responsive (43b), know and remember assert knowledge of the answer and forget asserts ignorance.

Equations

• Dayal2025.assertsKnowledge "know" = true
• Dayal2025.assertsKnowledge "remember" = true
• Dayal2025.assertsKnowledge x✝ = false

theorem Dayal2025.quasi_rows (row : Datum) : row ∈ Examples.all → ∀ v ∈ verbs, row.feature? "verb" = some v.form → (row.feature? "embedding").bind contextOf = some Clause.EmbeddingContext.quasiSubordinated → row.feature? "invested" = none → (Fine row.judgment ↔ Selects (deriveSelectionClass v.toVerb) Clause.EmbeddingContext.quasiSubordinated ∧ (deriveSelectionClass v.toVerb = SelectionClass.responsive → assertsKnowledge v.form = false ∨ row.feature? "negated" = some "true" ∨ row.feature? "questioned" = some "true"))

Quasi-subordination is licensed iff the class selects PerspP and, for a responsive, its content does not assert knowledge of the answer once negation or questioning is taken into account, as in (8)–(9), (38), (40), (43), (45)–(46) and (84)–(85). These are the instances of not_possiblyIgnorant_knows, possiblyIgnorant_forgets_iff and possiblyIgnorant_knows_question_iff in a context where the center may be ignorant. Rows the paper attributes to who is invested in the answer (§3.3) carry the feature invested and are set aside.

def Dayal2025.declarativeC : String → Option WHFeature

Declarative syntax leaves the WH-feature on C typed early in English and delayable in Hindi-Urdu and Italian (§4.4).

Equations

• Dayal2025.declarativeC "stan1293" = some Dayal2025.WHFeature.minusWH
• Dayal2025.declarativeC "hind1269" = some Dayal2025.WHFeature.alphaWH
• Dayal2025.declarativeC "ital1282" = some Dayal2025.WHFeature.alphaWH
• Dayal2025.declarativeC x✝ = none

theorem Dayal2025.declarative_question_rows (row : Datum) : row ∈ Examples.all → ∀ (f : WHFeature), row.feature? "syntax" = some "declarative" → row.feature? "embedding" = some "matrix" → declarativeC row.language = some f → (List.lookup "neutral" row.readings = some Judgment.acceptable ↔ ∃ (p : PerspFeature), Derivable f p Illocution.ask) ∧ List.lookup "biased" row.readings = some Judgment.acceptable

A declarative question has a neutral reading iff its language's C may stay untyped, and always has a biased one, as in (62)–(63).

def Dayal2025.typingOf : String → Option PolarTyping

A language's polar typing resources, by glottocode.

Equations

• Dayal2025.typingOf "stan1293" = some Dayal2025.english
• Dayal2025.typingOf "ital1282" = some Dayal2025.italian
• Dayal2025.typingOf "nucl1643" = some Dayal2025.japanese
• Dayal2025.typingOf "hind1269" = some Dayal2025.hindiUrdu
• Dayal2025.typingOf x✝ = none

theorem Dayal2025.simplex_rows (row : Datum) : row ∈ Examples.all → ∀ (L : PolarTyping) (e : Clause.EmbeddingContext), row.feature? "simplex" = some "true" → typingOf row.language = some L → (row.feature? "embedding").bind contextOf = some e → (Fine row.judgment ↔ Typed L e)

A simplex polar clause is acceptable in a context iff it is clause-typed there, as in (69)–(71).