inductive Phenomena.Questions.Studies.QingEtAl2025.Language : Type

Languages represented in the data

• english : Language
• mandarin : Language
• japanese : Language
• turkish : Language

instance Phenomena.Questions.Studies.QingEtAl2025.instDecidableEqLanguage : DecidableEq Language

Equations

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

instance Phenomena.Questions.Studies.QingEtAl2025.instReprLanguage : Repr Language

Equations

• Phenomena.Questions.Studies.QingEtAl2025.instReprLanguage = { reprPrec := Phenomena.Questions.Studies.QingEtAl2025.instReprLanguage.repr }

def Phenomena.Questions.Studies.QingEtAl2025.instReprLanguage.repr : Language → ℕ → Std.Format

Equations

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

def Phenomena.Questions.Studies.QingEtAl2025.instBEqLanguage.beq : Language → Language → Bool

Equations

• Phenomena.Questions.Studies.QingEtAl2025.instBEqLanguage.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Questions.Studies.QingEtAl2025.instBEqLanguage : BEq Language

Equations

• Phenomena.Questions.Studies.QingEtAl2025.instBEqLanguage = { beq := Phenomena.Questions.Studies.QingEtAl2025.instBEqLanguage.beq }

structure Phenomena.Questions.Studies.QingEtAl2025.Observation : Type

An empirical observation: predicate name, language, and acceptability.

The semantic properties are stored in the corresponding Fragment entry. Here we just record the empirical acceptability judgments.

• form : String

  Predicate form

• language : Language

  Language

• gloss : String

  English gloss (for non-English)

• takesPolQ : Bool

  Empirical: Does it take polar questions?

• takesWhQ : Bool

  Empirical: Does it take wh-questions?

• notes : String

  Additional notes

def Phenomena.Questions.Studies.QingEtAl2025.instReprObservation.repr : Observation → ℕ → Std.Format

Equations

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

instance Phenomena.Questions.Studies.QingEtAl2025.instReprObservation : Repr Observation

Equations

• Phenomena.Questions.Studies.QingEtAl2025.instReprObservation = { reprPrec := Phenomena.Questions.Studies.QingEtAl2025.instReprObservation.repr }

def Phenomena.Questions.Studies.QingEtAl2025.instBEqObservation.beq : Observation → Observation → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Questions.Studies.QingEtAl2025.instBEqObservation.beq x✝¹ x✝ = false

instance Phenomena.Questions.Studies.QingEtAl2025.instBEqObservation : BEq Observation

Equations

• Phenomena.Questions.Studies.QingEtAl2025.instBEqObservation = { beq := Phenomena.Questions.Studies.QingEtAl2025.instBEqObservation.beq }

def Phenomena.Questions.Studies.QingEtAl2025.hopeEn : Observation

Equations

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

def Phenomena.Questions.Studies.QingEtAl2025.wishEn : Observation

Equations

• Phenomena.Questions.Studies.QingEtAl2025.wishEn = { form := "wish", language := Phenomena.Questions.Studies.QingEtAl2025.Language.english, takesPolQ := false, takesWhQ := false }

def Phenomena.Questions.Studies.QingEtAl2025.expectEn : Observation

Equations

• Phenomena.Questions.Studies.QingEtAl2025.expectEn = { form := "expect", language := Phenomena.Questions.Studies.QingEtAl2025.Language.english, takesPolQ := false, takesWhQ := false }

def Phenomena.Questions.Studies.QingEtAl2025.fearEn : Observation

Equations

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

def Phenomena.Questions.Studies.QingEtAl2025.dreadEn : Observation

Equations

• Phenomena.Questions.Studies.QingEtAl2025.dreadEn = { form := "dread", language := Phenomena.Questions.Studies.QingEtAl2025.Language.english, takesPolQ := true, takesWhQ := true }

def Phenomena.Questions.Studies.QingEtAl2025.worryEn : Observation

Equations

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

def Phenomena.Questions.Studies.QingEtAl2025.englishObs : List Observation

Equations

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

def Phenomena.Questions.Studies.QingEtAl2025.qidaiZh : Observation

Equations

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

def Phenomena.Questions.Studies.QingEtAl2025.danxinZh : Observation

Equations

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

def Phenomena.Questions.Studies.QingEtAl2025.xiwangZh : Observation

Equations

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

def Phenomena.Questions.Studies.QingEtAl2025.haipaZh : Observation

Equations

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

def Phenomena.Questions.Studies.QingEtAl2025.mandarinObs : List Observation

Equations

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

def Phenomena.Questions.Studies.QingEtAl2025.tanosimiJa : Observation

Equations

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

def Phenomena.Questions.Studies.QingEtAl2025.osoreJa : Observation

Equations

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

def Phenomena.Questions.Studies.QingEtAl2025.kitaiJa : Observation

Equations

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

def Phenomena.Questions.Studies.QingEtAl2025.shinpaiJa : Observation

Equations

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

def Phenomena.Questions.Studies.QingEtAl2025.japaneseObs : List Observation

Equations

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

def Phenomena.Questions.Studies.QingEtAl2025.korkTr : Observation

Equations

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

def Phenomena.Questions.Studies.QingEtAl2025.umTr : Observation

Equations

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

def Phenomena.Questions.Studies.QingEtAl2025.endiselenTr : Observation

Equations

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

def Phenomena.Questions.Studies.QingEtAl2025.turkishObs : List Observation

Equations

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

def Phenomena.Questions.Studies.QingEtAl2025.allObservations : List Observation

Equations

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

Verifying Predictions Against Observations

The verb entries in Fragments/ contain the semantic properties. We can verify that predictions match observations:

-- From Theory (BuilderProperties.lean), derived from Fragment entry:
Semantics.Attitudes.BuilderProperties.AttitudeBuilder.nvpClass hope.attitudeBuilder = some.class3_cDist_positive
-- This predicts: canTakeQuestion = false

-- From Phenomena/QingEtAl2025/Data.lean:
hopeEn.takesPolQ = false ∧ hopeEn.takesWhQ = false ✓

Cross-Linguistic Verification

Language	Predicate	Class	Predicted	Observed	✓/✗
English	hope	3	✗ questions	✗	✓
English	fear	2	✓ questions	✓	✓
English	worry	1	✓ questions	✓	✓
Mandarin	qidai	1	✓ questions	✓	✓
Mandarin	xiwang	3	✗ questions	✗	✓
Japanese	tanosimi	1	✓ questions	✓	✓
Japanese	kitai	3	✗ questions	✗	✓
Turkish	kork-	2	✓ questions	✓	✓
Turkish	um-	3	✗ questions	✗	✓

Example: The hope-wh puzzle (Section 1)

Why can't "hope" embed questions in English?

(1) *John hopes whether Mary will come. (2) *John hopes who will come.

Explanation (Qing et al.):

• hope is C-distributive: "hope Q" ≈ "∃p ∈ Q. hope p"
• hope is positive → has TSP: presupposes ∃p ∈ C. μ(x,p) > θ
• When Q ⊆ C: assertion ⊆ presupposition → trivial!

Example: Mandarin qidai (Section 3.1)

Why can positive "qidai" embed questions?

(5) Zhangsan qidai shei hui lai. "Zhangsan looks forward to who will come." ✓ Grammatical (unlike English *"hope who")

Explanation:

• qidai is positive (like hope)
• BUT qidai is NON-C-distributive!
• "qidai Q" ≠ "∃p ∈ Q. qidai p"
• Non-C-distributivity breaks the triviality derivation.

Example: Turkish kork- (Section 3.2)

Why does "kork-" have symmetric interpretation with questions?

(6) Ali kork-uyor kim gel-ecek diye. "Ali fears who will come." = Ali fears that X will come OR fears that Y will come...

Explanation:

• kork- is negative → no bouletic goal
• No preferred outcome → symmetric interpretation
• Contrast with "hopefully" which is asymmetric (positive valence)