C-Distributivity: Derivation from Compositional Semantics

@cite{uegaki-sudo-2019} @cite{uegaki-2022}

This file derives C-distributivity as a theorem rather than stipulating it.

For the broader constraint hierarchy (P-to-Q Entailment, Strawson C-distributivity, Veridical Uniformity, fictitious predicates), see EmbeddingConstraints.lean.

Insight

C-distributivity follows from the structure of the semantics:

• If ⟦x V Q⟧ := ∃p ∈ Q. ⟦x V p⟧, then V is C-distributive by construction
• If the question semantics involves something beyond existential quantification (e.g., uncertainty, resolution), then V is NOT C-distributive

Semantic Patterns

Pattern 1: Degree Comparison (hope, fear)

⟦x hopes p⟧ = μ_hope(x, p) > θ(C)
⟦x hopes Q⟧ = ∃p ∈ Q. μ_hope(x, p) > θ(C)

This is C-distributive because the question semantics IS the existential.

Pattern 2: Uncertainty-Based (worry, care)

⟦x worries about p⟧ = μ(x, p) > θ ∧ x is uncertain about p
⟦x worries about Q⟧ = x is uncertain which answer in Q is true
                    ≠ ∃p ∈ Q. x worries about p

This is NOT C-distributive because worry-about-Q involves global uncertainty.

@[reducible, inline]

abbrev Semantics.Attitudes.CDistributivity.QuestionDen (W : Type u_1) : Type u_1

A Hamblin question denotation: set of possible answers

Equations

• Semantics.Attitudes.CDistributivity.QuestionDen W = List (BProp W)

@[reducible, inline]

abbrev Semantics.Attitudes.CDistributivity.DegreeFn (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

Preference/attitude degree function

Equations

• Semantics.Attitudes.CDistributivity.DegreeFn W E = (E → BProp W → ℚ)

@[reducible, inline]

abbrev Semantics.Attitudes.CDistributivity.ThresholdFn (W : Type u_1) : Type u_1

Contextual threshold function

Equations

• Semantics.Attitudes.CDistributivity.ThresholdFn W = (Semantics.Attitudes.CDistributivity.QuestionDen W → ℚ)

def Semantics.Attitudes.CDistributivity.IsCDistributive {W : Type u_1} {E : Type u_2} (V_prop : E → BProp W → W → Bool) (V_question : E → QuestionDen W → W → Bool) : Prop

A predicate V is C-distributive iff its question semantics is equivalent to existential quantification over its propositional semantics.

Formally: V is C-distributive iff ∀ x Q w, V_Q(x, Q, w) ↔ ∃p ∈ Q, V_p(x, p, w)

Where V_p is the propositional semantics and V_Q is the question semantics.

Equations

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

def Semantics.Attitudes.CDistributivity.degreeComparisonProp {W : Type u_1} {E : Type u_2} (μ : DegreeFn W E) (θ : ThresholdFn W) (C : QuestionDen W) (x : E) (p : BProp W) (_w : W) : Bool

Degree-comparison propositional semantics.

⟦x V p⟧(w, C) = μ(x, p) > θ(C)

This is the pattern for hope, fear, expect, wish, etc. The degree μ(x, p) measures how strongly x prefers/fears p.

Equations

• Semantics.Attitudes.CDistributivity.degreeComparisonProp μ θ C x p _w = decide (μ x p > θ C)

def Semantics.Attitudes.CDistributivity.degreeComparisonQuestion {W : Type u_1} {E : Type u_2} (μ : DegreeFn W E) (θ : ThresholdFn W) (C : QuestionDen W) (x : E) (Q : QuestionDen W) (_w : W) : Bool

Degree-comparison question semantics (existential).

⟦x V Q⟧(w, C) = ∃p ∈ Q. μ(x, p) > θ(C)

This is the standard Hamblin-style composition: pointwise application with existential closure.

Equations

• Semantics.Attitudes.CDistributivity.degreeComparisonQuestion μ θ C x Q _w = List.any Q fun (p : BProp W) => decide (μ x p > θ C)

theorem Semantics.Attitudes.CDistributivity.degreeComparison_isCDistributive {W : Type u_1} {E : Type u_2} (μ : DegreeFn W E) (θ : ThresholdFn W) (C : QuestionDen W) : IsCDistributive (degreeComparisonProp μ θ C) (degreeComparisonQuestion μ θ C)

Theorem: Degree-comparison predicates are C-distributive.

This follows directly from the definition: the question semantics IS the existential over the propositional semantics.

Why Worry/Care are NOT C-Distributive

@cite{elliott-etal-2017} @cite{spector-egr-2015}

The key insight from @cite{elliott-etal-2017} is that predicates like "worry" and "care" have question semantics that go beyond existential quantification.

Worry Semantics

⟦x worries about p⟧ = μ(x, p) > θ ∧ x is uncertain about p ⟦x worries about Q⟧ = x is uncertain which answer in Q is true ∧ has concern about the open possibilities

The uncertainty component is global for questions but pointwise for propositions. This breaks C-distributivity.

Care/Relevance Semantics

⟦x cares about Q⟧ = resolving Q is relevant to x's goals ≠ ∃p ∈ Q. resolving whether p is relevant

Example: "Al cares about where to dock his boat"

• This is about the DECISION, not about any particular location
• Al doesn't "care that the boat docks at location A" (odd reading)

Mandarin qidai (期待, "look forward to")

qidai appears to have similar non-C-distributive semantics:

• ⟦x qidai Q⟧ involves anticipation of resolution
• Not reducible to existential over individual answers

This explains why qidai (positive valence, Class 1) takes questions while hope (positive valence, Class 3) doesn't: they have different semantic structures despite similar preference content.

theorem Semantics.Attitudes.CDistributivity.exists_nonCDistributive_worry : ∃ (W : Type) (E : Type) (V_prop : E → BProp W → W → Bool) (V_question : E → QuestionDen W → W → Bool), ¬IsCDistributive V_prop V_question

There exist semantics for "worry" that are not C-distributive.

Concrete counterexample: question semantics requires global uncertainty (conjunctive condition beyond existential), so V_question can be false even when V_prop holds for some answer.

theorem Semantics.Attitudes.CDistributivity.exists_nonCDistributive_care : ∃ (W : Type) (E : Type) (V_prop : E → BProp W → W → Bool) (V_question : E → QuestionDen W → W → Bool), ¬IsCDistributive V_prop V_question

There exist semantics for "care" that are not C-distributive.

Same construction: relevance-based question semantics is not reducible to existential quantification over propositional semantics.

Semantic Structure → C-Distributivity → NVP Class

The key theorem chain:

1. Semantic structure determines C-distributivity

   • Degree-comparison → C-distributive (PROVED)
   • Uncertainty/relevance-based → non-C-distributive (AXIOMATIZED)

2. C-distributivity + valence determines NVP class

   • Non-C-distributive → Class 1 (takes questions)
   • C-distributive + negative → Class 2 (takes questions)
   • C-distributive + positive → Class 3 (anti-rogative)

3. NVP class determines question-taking

   • Class 1, 2 → takes questions
   • Class 3 → anti-rogative (triviality)

This gives us a genuine derivation:

hopeSemantics is degree-comparison
  → (by degreeComparison_isCDistributive) hope is C-distributive
  → (by classifyNVP) hope is Class 3
  → (by class3_yields_triviality) hope + Q is trivial
  → (by L-analyticity) *hope who is ungrammatical

The first step is now PROVED rather than stipulated.

def Semantics.Attitudes.CDistributivity.isDegreeComparisonLike {W : Type u_1} {E : Type u_2} (V_prop : E → BProp W → W → Bool) (V_question : E → QuestionDen W → W → Bool) : Prop

A predicate is "degree-comparison-like" if its question semantics is defined as existential quantification over propositional semantics.

Equations

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

theorem Semantics.Attitudes.CDistributivity.degreeComparisonLike_implies_cDistributive {W : Type u_1} {E : Type u_2} (V_prop : E → BProp W → W → Bool) (V_question : E → QuestionDen W → W → Bool) (h : isDegreeComparisonLike V_prop V_question) : IsCDistributive V_prop V_question

Degree-comparison-like predicates are automatically C-distributive.

Main Results

1. degreeComparison_isCDistributive: Any predicate with degree-comparison semantics (⟦V Q⟧ = ∃p ∈ Q. μ(x,p) > θ) is C-distributive.

2. degreeComparisonLike_implies_cDistributive: General theorem that existential question semantics implies C-distributivity.

3. exists_nonCDistributive_worry, exists_nonCDistributive_care: Concrete counterexamples showing non-C-distributive semantics exist.

Per-predicate instantiations (hope, fear, etc.) are in Preferential.lean. Constraint hierarchy and fictitious predicates are in EmbeddingConstraints.lean.