inductive QingEtAl2025.Language : Type

Languages represented in the data

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

@[implicit_reducible]

instance QingEtAl2025.instDecidableEqLanguage : DecidableEq Language

Equations

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

@[implicit_reducible]

instance QingEtAl2025.instReprLanguage : Repr Language

Equations

• QingEtAl2025.instReprLanguage = { reprPrec := QingEtAl2025.instReprLanguage.repr }

def QingEtAl2025.instReprLanguage.repr : Language → ℕ → Std.Format

Equations

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

structure 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 QingEtAl2025.instReprObservation.repr : Observation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance QingEtAl2025.instReprObservation : Repr Observation

Equations

• QingEtAl2025.instReprObservation = { reprPrec := QingEtAl2025.instReprObservation.repr }

@[implicit_reducible]

instance QingEtAl2025.instBEqObservation : BEq Observation

Equations

• QingEtAl2025.instBEqObservation = { beq := QingEtAl2025.instBEqObservation.beq }

def QingEtAl2025.instBEqObservation.beq : Observation → Observation → Bool

Equations

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

def QingEtAl2025.hopeEn : Observation

Equations

• QingEtAl2025.hopeEn = { form := "hope", language := QingEtAl2025.Language.english, takesPolQ := false, takesWhQ := false, notes := "Class 3: C-dist + positive + TSP → anti-rogative" }

def QingEtAl2025.wishEn : Observation

Equations

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

def QingEtAl2025.expectEn : Observation

Equations

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

def QingEtAl2025.fearEn : Observation

Equations

• QingEtAl2025.fearEn = { form := "fear", language := QingEtAl2025.Language.english, takesPolQ := true, takesWhQ := true, notes := "Class 2: C-dist + negative → no TSP → takes questions" }

def QingEtAl2025.dreadEn : Observation

Equations

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

def QingEtAl2025.worryEn : Observation

Equations

• QingEtAl2025.worryEn = { form := "worry", language := QingEtAl2025.Language.english, takesPolQ := true, takesWhQ := true, notes := "Class 1: non-C-dist → takes questions" }

def QingEtAl2025.englishObs : List Observation

Equations

• QingEtAl2025.englishObs = [QingEtAl2025.hopeEn, QingEtAl2025.wishEn, QingEtAl2025.expectEn, QingEtAl2025.fearEn, QingEtAl2025.dreadEn, QingEtAl2025.worryEn]

def QingEtAl2025.qidaiZh : Observation

Equations

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

def QingEtAl2025.danxinZh : Observation

Equations

• QingEtAl2025.danxinZh = { form := "danxin", language := QingEtAl2025.Language.mandarin, gloss := "worry", takesPolQ := true, takesWhQ := true }

def QingEtAl2025.xiwangZh : Observation

Equations

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

def QingEtAl2025.haipaZh : Observation

Equations

• QingEtAl2025.haipaZh = { form := "haipa", language := QingEtAl2025.Language.mandarin, gloss := "fear", takesPolQ := true, takesWhQ := true }

def QingEtAl2025.mandarinObs : List Observation

Equations

• QingEtAl2025.mandarinObs = [QingEtAl2025.qidaiZh, QingEtAl2025.danxinZh, QingEtAl2025.xiwangZh, QingEtAl2025.haipaZh]

def QingEtAl2025.tanosimiJa : Observation

Equations

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

def QingEtAl2025.osoreJa : Observation

Equations

• QingEtAl2025.osoreJa = { form := "osore", language := QingEtAl2025.Language.japanese, gloss := "fear", takesPolQ := true, takesWhQ := true }

def QingEtAl2025.kitaiJa : Observation

Equations

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

def QingEtAl2025.shinpaiJa : Observation

Equations

• QingEtAl2025.shinpaiJa = { form := "shinpai", language := QingEtAl2025.Language.japanese, gloss := "worry", takesPolQ := true, takesWhQ := true }

def QingEtAl2025.japaneseObs : List Observation

Equations

• QingEtAl2025.japaneseObs = [QingEtAl2025.tanosimiJa, QingEtAl2025.osoreJa, QingEtAl2025.kitaiJa, QingEtAl2025.shinpaiJa]

def QingEtAl2025.korkTr : Observation

Equations

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

def QingEtAl2025.umTr : Observation

Equations

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

def QingEtAl2025.endiselenTr : Observation

Equations

• QingEtAl2025.endiselenTr = { form := "endişelen-", language := QingEtAl2025.Language.turkish, gloss := "worry", takesPolQ := true, takesWhQ := true }

def QingEtAl2025.turkishObs : List Observation

Equations

• QingEtAl2025.turkishObs = [QingEtAl2025.korkTr, QingEtAl2025.umTr, QingEtAl2025.endiselenTr]

def QingEtAl2025.allObservations : List Observation

Equations

• QingEtAl2025.allObservations = QingEtAl2025.englishObs ++ QingEtAl2025.mandarinObs ++ QingEtAl2025.japaneseObs ++ QingEtAl2025.turkishObs

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.Attitude.nvpClass hope.attitude = 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)