Clausal distributivity

A clause-embedding predicate relates an agent to a set of propositions: the answers of a question, or the singleton of a declarative's proposition. The predicate is clausally distributive when it relates an agent to a question exactly when it relates her to some answer. Most responsive predicates are distributive, such as know. A predicate that relates an agent to a question while relating her to none of its answers is not; this is the diagnostic Elliott and colleagues apply to care and Qing and colleagues to worry.

Main definitions

• Distributivity.IsDistributive: the predicate relates an agent to a question exactly when it relates her to some answer.

Main statements

• Distributivity.not_isDistributive_of_forall_not: a predicate that holds of a question but of none of its answers is not distributive.

References

• [SE15]
• [US19]
• [Ueg22]
• [EKSU17]
• [QOR+25]

def Distributivity.IsDistributive {W : Type u_1} {E : Type u_2} (V : E → Set (Set W) → W → Prop) : Prop

A clause-embedding predicate V is clausally distributive when it relates an agent to a set of propositions exactly when it relates her to the singleton of one of them.

Equations

• Distributivity.IsDistributive V = ∀ (x : E) (Q : Set (Set W)) (w : W), V x Q w ↔ ∃ (p : Set W), p ∈ Q ∧ V x {p} w

theorem Distributivity.not_isDistributive_of_forall_not {W : Type u_1} {E : Type u_2} {V : E → Set (Set W) → W → Prop} {x : E} {Q : Set (Set W)} {w : W} (hQ : V x Q w) (h : ∀ (p : Set W), p ∈ Q → ¬V x {p} w) : ¬IsDistributive V

A predicate that holds of a question but of none of its answers is not distributive.