def Semantics.Attitudes.BuilderProperties.PreferentialBuilder.isCDistributive : Core.Verbs.PreferentialBuilder → Bool

C-distributivity is derived from the semantic builder structure.

This function mirrors the proved theorems:

• degreeComparisonPredicate_isCDistributive: degree-comparison → C-dist
• worry_not_cDistributive: uncertainty-based → NOT C-dist
• (analogous for relevance-based)

The computation is justified by the semantic structure:

• Degree-comparison: ⟦x V Q⟧ = ∃p ∈ Q. μ(x,p) > θ — existential over propositional
• Uncertainty-based: ⟦x V Q⟧ involves global uncertainty, not existential
• Relevance-based: ⟦x V Q⟧ involves resolution/relevance, not existential

Equations

• Semantics.Attitudes.BuilderProperties.PreferentialBuilder.isCDistributive (Core.Verbs.PreferentialBuilder.degreeComparison valence) = true
• Semantics.Attitudes.BuilderProperties.PreferentialBuilder.isCDistributive Core.Verbs.PreferentialBuilder.uncertaintyBased = false
• Semantics.Attitudes.BuilderProperties.PreferentialBuilder.isCDistributive (Core.Verbs.PreferentialBuilder.relevanceBased valence) = false

def Semantics.Attitudes.BuilderProperties.PreferentialBuilder.nvpClass (b : Core.Verbs.PreferentialBuilder) : Preferential.NVPClass

NVP class is derived from C-distributivity and valence.

This matches Preferential.classifyNVP but computed from the builder:

• Class 1: Non-C-distributive (worry, qidai) — can embed questions regardless of valence
• Class 2: C-distributive + negative (fear, dread) — can embed questions (no TSP)
• Class 3: C-distributive + positive (hope, wish) — anti-rogative (TSP → triviality)

The derivation chain:

1. Builder structure → C-distributivity (this file)
2. Builder → valence (in Fragment, lexical property)
3. C-distributivity + valence → NVP class (this function)

Equations

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

def Semantics.Attitudes.BuilderProperties.AttitudeBuilder.cDistributive : Core.Verbs.AttitudeBuilder → Option Bool

Get C-distributivity for preferential attitudes. Returns none for doxastic attitudes (C-distributivity doesn't apply).

Equations

• Semantics.Attitudes.BuilderProperties.AttitudeBuilder.cDistributive (Core.Verbs.AttitudeBuilder.doxastic veridicality) = none
• Semantics.Attitudes.BuilderProperties.AttitudeBuilder.cDistributive (Core.Verbs.AttitudeBuilder.preferential b) = some (Semantics.Attitudes.BuilderProperties.PreferentialBuilder.isCDistributive b)

def Semantics.Attitudes.BuilderProperties.AttitudeBuilder.nvpClass : Core.Verbs.AttitudeBuilder → Option Preferential.NVPClass

Get NVP class for preferential attitudes. Returns none for doxastic attitudes (NVP classification doesn't apply).

Equations

• Semantics.Attitudes.BuilderProperties.AttitudeBuilder.nvpClass (Core.Verbs.AttitudeBuilder.doxastic veridicality) = none
• Semantics.Attitudes.BuilderProperties.AttitudeBuilder.nvpClass (Core.Verbs.AttitudeBuilder.preferential b) = some (Semantics.Attitudes.BuilderProperties.PreferentialBuilder.nvpClass b)

def Semantics.Attitudes.BuilderProperties.VerbEntry.cDistributive (v : Fragments.English.Predicates.Verbal.VerbEntry) : Option Bool

C-distributivity is derived from the attitude builder

Equations

• Semantics.Attitudes.BuilderProperties.VerbEntry.cDistributive v = v.attitudeBuilder.bind Semantics.Attitudes.BuilderProperties.AttitudeBuilder.cDistributive

def Semantics.Attitudes.BuilderProperties.VerbEntry.nvpClass (v : Fragments.English.Predicates.Verbal.VerbEntry) : Option Preferential.NVPClass

NVP class is derived from the attitude builder

Equations

• Semantics.Attitudes.BuilderProperties.VerbEntry.nvpClass v = v.attitudeBuilder.bind Semantics.Attitudes.BuilderProperties.AttitudeBuilder.nvpClass

def Semantics.Attitudes.BuilderProperties.VerbEntry.takesQuestion (v : Fragments.English.Predicates.Verbal.VerbEntry) : Bool

Can take questions: Derived for preferential verbs, base field for others.

For preferential verbs: determined by NVP class (Class 1, 2 can; Class 3 cannot) For non-preferential verbs: uses takesQuestionBase field

Equations

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

def Semantics.Attitudes.BuilderProperties.VerbEntry.isAntiRogative (v : Fragments.English.Predicates.Verbal.VerbEntry) : Bool

Is this verb anti-rogative (cannot take question complements canonically)?

Anti-rogative predicates are Class 3 NVPs: C-distributive + positive + TSP.

Equations

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

def Semantics.Attitudes.BuilderProperties.VerbEntry.canEmbedQuestion (v : Fragments.English.Predicates.Verbal.VerbEntry) : Bool

Can this verb canonically embed a question?

Based on @cite{qing-uegaki-2025} classification:

• Class 1 (non-C-distributive): Yes
• Class 2 (C-dist + negative): Yes
• Class 3 (C-dist + positive): No (anti-rogative)
• Non-preferential attitudes with takesQuestion: Yes

Equations

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

def Semantics.Attitudes.BuilderProperties.antiRogativeVerbs : List Fragments.English.Predicates.Verbal.VerbEntry

Get all anti-rogative verbs (Class 3 NVPs).

Equations

• Semantics.Attitudes.BuilderProperties.antiRogativeVerbs = List.filter Semantics.Attitudes.BuilderProperties.VerbEntry.isAntiRogative Fragments.English.Predicates.Verbal.allVerbs

def Semantics.Attitudes.BuilderProperties.questionEmbeddingVerbs : List Fragments.English.Predicates.Verbal.VerbEntry

Get all question-embedding verbs.

Equations

• Semantics.Attitudes.BuilderProperties.questionEmbeddingVerbs = List.filter Semantics.Attitudes.BuilderProperties.VerbEntry.canEmbedQuestion Fragments.English.Predicates.Verbal.allVerbs

theorem Semantics.Attitudes.BuilderProperties.hope_builder_cDistributive : PreferentialBuilder.isCDistributive (Core.Verbs.PreferentialBuilder.degreeComparison Preferential.AttitudeValence.positive) = true

Hope (degree-comparison positive) is C-distributive

theorem Semantics.Attitudes.BuilderProperties.fear_builder_cDistributive : PreferentialBuilder.isCDistributive (Core.Verbs.PreferentialBuilder.degreeComparison Preferential.AttitudeValence.negative) = true

Fear (degree-comparison negative) is C-distributive

theorem Semantics.Attitudes.BuilderProperties.worry_builder_not_cDistributive : PreferentialBuilder.isCDistributive Core.Verbs.PreferentialBuilder.uncertaintyBased = false

Worry (uncertainty-based) is NOT C-distributive

theorem Semantics.Attitudes.BuilderProperties.qidai_builder_not_cDistributive : PreferentialBuilder.isCDistributive (Core.Verbs.PreferentialBuilder.relevanceBased Preferential.AttitudeValence.positive) = false

Qidai (relevance-based) is NOT C-distributive

theorem Semantics.Attitudes.BuilderProperties.hope_builder_class3 : PreferentialBuilder.nvpClass (Core.Verbs.PreferentialBuilder.degreeComparison Preferential.AttitudeValence.positive) = Preferential.NVPClass.class3_cDist_positive

Hope is Class 3 (C-dist + positive → anti-rogative)

theorem Semantics.Attitudes.BuilderProperties.fear_builder_class2 : PreferentialBuilder.nvpClass (Core.Verbs.PreferentialBuilder.degreeComparison Preferential.AttitudeValence.negative) = Preferential.NVPClass.class2_cDist_negative

Fear is Class 2 (C-dist + negative → takes questions)

theorem Semantics.Attitudes.BuilderProperties.worry_builder_class1 : PreferentialBuilder.nvpClass Core.Verbs.PreferentialBuilder.uncertaintyBased = Preferential.NVPClass.class1_nonCDist

Worry is Class 1 (non-C-dist → takes questions)

theorem Semantics.Attitudes.BuilderProperties.qidai_builder_class1 : PreferentialBuilder.nvpClass (Core.Verbs.PreferentialBuilder.relevanceBased Preferential.AttitudeValence.positive) = Preferential.NVPClass.class1_nonCDist

Qidai is Class 1 (non-C-dist → takes questions despite positive valence)