Clausal distributivity

A clause-embedding predicate is clausally distributive — written C(lausal)-distributive in [QOR+25] — when its question semantics is existential quantification over its propositional semantics: ⟦x V Q⟧ ↔ ∃p ∈ Q. ⟦x V p⟧ ([US19]; [Ueg22]). IsDistributive states the property for a pair of propositional and question semantics, so it is proved from a predicate's semantic structure rather than stipulated per predicate.

The degree-comparison preferentials of Preference.lean are distributive by construction (Preferential.mkDegreeComparison_isDistributive); predicates whose question semantics outruns the existential — global uncertainty for worry, decision-relevance for care ([EKSU17]) — are not (Preferential.worry_not_distributive). Veridical preferentials instantiate the world-sensitive form (Studies/UegakiSudo2019.lean).

Questions are alternative lists over Finset W propositions, matching the question representation of Semantics/Attitudes/Desire/.

def Distributivity.IsDistributive {W : Type u_1} {E : Type u_2} (Vprop : E → Finset W → W → Prop) (Vquestion : E → List (Finset W) → W → Prop) : Prop

A predicate with propositional semantics Vprop and question semantics Vquestion is clausally distributive iff Vquestion x Q w ↔ ∃ p ∈ Q, Vprop x p w.

Equations

• Distributivity.IsDistributive Vprop Vquestion = ∀ (x : E) (Q : List (Finset W)) (w : W), Vquestion x Q w ↔ ∃ p ∈ Q, Vprop x p w