Mandarin Predicate Lexicon Fragment

@cite{qing-uegaki-2025} @cite{glass-2025}

Mandarin predicates relevant to @cite{qing-uegaki-2025}. Properties like C-distributivity and NVP class are DERIVED from the attitude field.

structure Fragments.Mandarin.Predicates.MandarinVerbEntryextends Semantics.Lexical.VerbCore : Type

Mandarin verb entry: extends VerbCore with no inflectional morphology (Mandarin is an isolating language).

• form : String
• complementType : ComplementType
• subjectEntailments : Option ArgumentStructure.EntailmentProfile.EntailmentProfile
• objectEntailments : Option ArgumentStructure.EntailmentProfile.EntailmentProfile
• controlType : ControlType
• altComplementType : Option ComplementType
• altControlType : ControlType
• unaccusative : Bool
• voiceType : Option VoiceType
• passivizable : Bool
• implicitObj : Option ImplicitInterp
• implicitGoal : Option ImplicitInterp
• speechActVerb : Bool
• vendlerClass : Option Features.VendlerClass
• degreeAchievementScale : Option Features.DegreeAchievement.DegreeAchievementScale
• verbIncClass : Option Aspect.Incremental.VerbIncClass
• presupType : Option PresupTriggerType
• postsupType : Option PostsupType
• projectionBehavior : Option ProjectionBehavior
• selectsDimension : Option Features.Dimension.Dimension
• cosType : Option Features.ChangeOfState.CoSType
• implicative : Option Features.Implicative
• causative : Option Features.Causative
• causalSource : Option Causation.Psych.CausalSource
• opaqueContext : Bool
• attitude : Option Features.Attitude
• takesQuestionBase : Bool
• complementSig : Option Core.NaturalLogic.EntailmentSig
• senseTag : SenseTag
• levinClass : Option LevinClass
• rootProfile : Option Roots.RootProfile

def Fragments.Mandarin.Predicates.instReprMandarinVerbEntry.repr : MandarinVerbEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Mandarin.Predicates.instReprMandarinVerbEntry : Repr MandarinVerbEntry

Equations

• Fragments.Mandarin.Predicates.instReprMandarinVerbEntry = { reprPrec := Fragments.Mandarin.Predicates.instReprMandarinVerbEntry.repr }

def Fragments.Mandarin.Predicates.instBEqMandarinVerbEntry.beq : MandarinVerbEntry → MandarinVerbEntry → Bool

Equations

• Fragments.Mandarin.Predicates.instBEqMandarinVerbEntry.beq { toVerbCore := a } { toVerbCore := b } = (a == b)
• Fragments.Mandarin.Predicates.instBEqMandarinVerbEntry.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Fragments.Mandarin.Predicates.instBEqMandarinVerbEntry : BEq MandarinVerbEntry

Equations

• Fragments.Mandarin.Predicates.instBEqMandarinVerbEntry = { beq := Fragments.Mandarin.Predicates.instBEqMandarinVerbEntry.beq }

def Fragments.Mandarin.Predicates.MandarinVerbEntry.mk' (core : Semantics.Lexical.VerbCore) : MandarinVerbEntry

Smart constructor: sets only the citation form (no inflection).

Equations

• Fragments.Mandarin.Predicates.MandarinVerbEntry.mk' core = { toVerbCore := core }

def Fragments.Mandarin.Predicates.qidai : MandarinVerbEntry

期待 "qidai" — look forward to (Class 1: positive, non-C-distributive, takes questions).

Equations

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

def Fragments.Mandarin.Predicates.danxin : MandarinVerbEntry

担心 "danxin" — worry (Class 1: negative, non-C-distributive).

Equations

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

def Fragments.Mandarin.Predicates.xiwang : MandarinVerbEntry

希望 "xiwang" — hope (Class 3: positive, C-distributive, anti-rogative).

Equations

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

def Fragments.Mandarin.Predicates.haipa : MandarinVerbEntry

害怕 "haipa" — fear (Class 2: negative, C-distributive, takes questions).

Equations

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

yǐwéi: Postsupposition via postsupType

yǐwéi "be under the impression" has a POSTSUPPOSITION (output-context constraint) that ¬p is compatible with the Common Ground after the utterance. This is NOT a presupposition and cannot be derived from veridicality alone (@cite{glass-2025}, @cite{glass-2023}).

Encoded structurally as postsupType := some .weakContrafactive in VerbCore, formalized as Core.Postsupposition.weakContrafactive, and exercised in Glass2025.

def Fragments.Mandarin.Predicates.yiwei : MandarinVerbEntry

以为 "yǐwéi" — be under the impression that (weak contrafactive).

Has postsupposition ◇¬p (CG compatible with ¬p after utterance). This cannot be derived from veridicality; see @cite{glass-2025} and @cite{glass-2023}. The postsupposition is recorded structurally via postsupType and exercised in Glass2025.

Equations

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

Liu & Yip 2026 complement-taking predicates

Seven additional Mandarin CTPs cited by @cite{liu-yip-2026} (lists in (18) and (19)) for the you-skipping pattern. Theory-light: only consensus typology — surface form, finite vs nonfinite complement selection, and @cite{noonan-2007} CTPClass. The [+D] / [-D] selectional refinement within nonfinite TPs (Lin & Liu 2009) is theory-laden and lives in Phenomena/Complementation/Studies/LiuYip2026.lean as a Studies-side projection per the audit's "derive don't stipulate" discipline.

def Fragments.Mandarin.Predicates.xiang : MandarinVerbEntry

想 xiang 'want' — desiderative; nonfinite-taking. Liu & Yip 2026 (18).

Equations

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

def Fragments.Mandarin.Predicates.rang : MandarinVerbEntry

让 rang 'let' — manipulative; nonfinite-taking. Liu & Yip 2026 (18).

Equations

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

def Fragments.Mandarin.Predicates.xiangxin : MandarinVerbEntry

相信 xiangxin 'believe' — propositional attitude; finite-taking (CP-only). Liu & Yip 2026 (19) — blocks you-skipping.

Equations

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

def Fragments.Mandarin.Predicates.quan : MandarinVerbEntry

劝 quan 'urge' — manipulative; nonfinite-taking. Liu & Yip 2026 (18).

Equations

• Fragments.Mandarin.Predicates.quan = Fragments.Mandarin.Predicates.MandarinVerbEntry.mk' { form := "quan", complementType := Semantics.Lexical.ComplementType.infinitival }

def Fragments.Mandarin.Predicates.bi : MandarinVerbEntry

逼 bi 'force' — manipulative; nonfinite-taking. Liu & Yip 2026 (18) (listed as bi(po)).

Equations

• Fragments.Mandarin.Predicates.bi = Fragments.Mandarin.Predicates.MandarinVerbEntry.mk' { form := "bi", complementType := Semantics.Lexical.ComplementType.infinitival }

def Fragments.Mandarin.Predicates.dasuan : MandarinVerbEntry

打算 dasuan 'plan' — desiderative; nonfinite-taking. Liu & Yip 2026 (18). Liu & Yip Appendix A discusses dasuan's ambiguity between Type II (TP) and Type III (vP) selection.

Equations

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

def Fragments.Mandarin.Predicates.shefa : MandarinVerbEntry

设法 shefa 'try' — achievement; nonfinite-taking. Liu & Yip 2026 (18). @cite{noonan-2007} classifies 'try' under the achievement CTP class.

Equations

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

def Fragments.Mandarin.Predicates.allVerbs : List MandarinVerbEntry

Equations

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

def Fragments.Mandarin.Predicates.lookup (form : String) : Option MandarinVerbEntry

Equations

• Fragments.Mandarin.Predicates.lookup form = List.find? (fun (x : Fragments.Mandarin.Predicates.MandarinVerbEntry) => x.form == form) Fragments.Mandarin.Predicates.allVerbs

Drift sentries on the Liu&Yip2026 cohort

theorem Fragments.Mandarin.Predicates.liuyip_partition : ([xiang, rang, quan, bi, dasuan, shefa].all fun (x : MandarinVerbEntry) => decide (x.complementType = Semantics.Lexical.ComplementType.infinitival)) = true ∧ xiangxin.complementType = Semantics.Lexical.ComplementType.finiteClause

The seven Liu & Yip 2026 predicates split into 6 nonfinite-takers (allow you-skipping per (18)) and 1 finite-taker (blocks it per (19)).