Universal Constraints on Clause-Embedding Predicates

@cite{roelofsen-uegaki-2020} @cite{uegaki-2022} @cite{spector-egr-2015} @cite{steinert-threlkeld-2020}

This file formalizes universal constraints on the possible denotations of clause-embedding predicates — the semantic analogue of conservativity for determiners (@cite{barwise-cooper-1981}).

Constraints

Four constraints have been proposed, forming a hierarchy:

C-distributivity  ⟹  P-to-Q Entailment  (but NOT vice versa)
C-distributivity  ⟹  Strawson C-distributivity  (but NOT vice versa)

Veridical Uniformity is independent of both.

Organization

• CDistributivity.lean: C-distributivity definition and proofs (semantic structure)
• This file: P-to-Q Entailment, Strawson C-dist, Veridical Uniformity, constraint hierarchy, and fictitious predicate rejection
• Phenomena/Questions/Studies/Uegaki2022.lean: empirical data (Table 8.2)

P-to-Q Entailment

@cite{roelofsen-uegaki-2020} propose a weaker constraint than C-distributivity:

P-to-Q Entailment: If there is an answer p to Q such that ⟦V⟧({p})(x) holds, then ⟦V⟧(Q)(x) also holds.

This is the one-directional version of C-distributivity (P→Q direction only). It is empirically superior: it rules in attested predicates that violate C-distributivity (care, mõtlema, daroo, wonder) while still ruling out fictitious predicates (*shknow, *knopinion, *all-open).

def Semantics.Attitudes.EmbeddingConstraints.IsPtoQEntailing {W : Type u_1} {E : Type u_2} (V : E → CDistributivity.QuestionDen W → W → Bool) : Prop

A predicate V is P-to-Q entailing iff for any term x and any exhaustivity-neutral interrogative complement Q, if there is an answer p to Q such that V x [p] w = true, then V x Q w = true.

This is weaker than C-distributivity: it only requires the P→Q direction, not the Q→P direction.

Equations

• Semantics.Attitudes.EmbeddingConstraints.IsPtoQEntailing V = ∀ (x : E) (Q : Semantics.Attitudes.CDistributivity.QuestionDen W) (w : W), ∀ p ∈ Q, V x [p] w = true → V x Q w = true

theorem Semantics.Attitudes.EmbeddingConstraints.cDistributive_implies_ptoq {W : Type u_1} {E : Type u_2} (V_prop : E → BProp W → W → Bool) (V_question : E → CDistributivity.QuestionDen W → W → Bool) (hCD : CDistributivity.IsCDistributive V_prop V_question) : IsPtoQEntailing V_question

C-distributivity implies P-to-Q entailment.

If V_Q(x, Q, w) ↔ ∃p ∈ Q. V_p(x, p, w), then in particular the ← direction gives us: V_p(x, p, w) → V_Q(x, Q, w) for any p ∈ Q. Since V_Q(x, [p], w) ↔ V_p(x, p, w), this yields P-to-Q entailment.

theorem Semantics.Attitudes.EmbeddingConstraints.degreeComparison_isPtoQEntailing {W : Type u_1} {E : Type u_2} (μ : CDistributivity.DegreeFn W E) (θ : CDistributivity.ThresholdFn W) (C : CDistributivity.QuestionDen W) : IsPtoQEntailing (CDistributivity.degreeComparisonQuestion μ θ C)

Degree-comparison predicates are P-to-Q entailing (follows from C-distributivity).

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

Strawson C-distributivity: a weaker variant of C-distributivity that accounts for presuppositional predicates (e.g., predicates of relevance like care).

A predicate V is Strawson C-distributive iff:

• (→) If V(x, Q), then there is an answer p to Q such that, if the presuppositions of V(x, p) are satisfied, then V(x, p).
• (←) If there is an answer p to Q such that V(x, p), then V(x, Q).

The key difference from plain C-distributivity: the → direction is weakened to only require the propositional version to hold when its presuppositions are met. This handles care, whose presupposition (belief that p) blocks the → direction in plain C-distributivity.

Equations

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

theorem Semantics.Attitudes.EmbeddingConstraints.cDist_implies_strawson {W : Type u_1} {E : Type u_2} (V_prop : E → BProp W → W → Bool) (V_question : E → CDistributivity.QuestionDen W → W → Bool) (presupSatisfied : E → BProp W → W → Bool) (hCD : CDistributivity.IsCDistributive V_prop V_question) : IsStrawsonCDistributive V_prop V_question presupSatisfied

Plain C-distributivity implies Strawson C-distributivity (with any presupposition predicate).

Veridical Uniformity

@cite{spector-egr-2015} propose that all responsive clause-embedding predicates are uniform w.r.t. veridicality: either veridical w.r.t. both declarative and interrogative complements, or non-veridical w.r.t. both.

Veridical Uniformity is independent of C-distributivity and P-to-Q Entailment. It captures a different dimension: whether the predicate is truth-entailing, not whether question semantics reduces to propositional semantics.

def Semantics.Attitudes.EmbeddingConstraints.IsVeridicalDecl {W : Type u_1} {E : Type u_2} (V : E → CDistributivity.QuestionDen W → W → Bool) : Prop

A predicate V is veridical w.r.t. declarative complements iff V(x, {p}, w) entails p(w).

@cite{roelofsen-uegaki-2020} eq. 1 / @cite{spector-egr-2015}: ⌜x Vs p⌝ ⇒ ⌜p⌝

Equations

• Semantics.Attitudes.EmbeddingConstraints.IsVeridicalDecl V = ∀ (x : E) (p : BProp W) (w : W), V x [p] w = true → p w = true

def Semantics.Attitudes.EmbeddingConstraints.IsVeridicalInterrog {W : Type u_1} {E : Type u_2} (V : E → CDistributivity.QuestionDen W → W → Bool) : Prop

A predicate V is veridical w.r.t. interrogative complements iff V(x, Q, w) and p(w) with p ∈ Q together entail V(x, {p}, w).

@cite{roelofsen-uegaki-2020} eq. 3 / @cite{spector-egr-2015}: ⌜x Vs Q⌝ ∧ ⌜p⌝ ∧ p ∈ Q ⇒ ⌜x Vs p⌝

Equations

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

def Semantics.Attitudes.EmbeddingConstraints.IsVeridicallyUniform {W : Type u_1} {E : Type u_2} (V : E → CDistributivity.QuestionDen W → W → Bool) : Prop

A responsive predicate V is veridically uniform iff it is either veridical w.r.t. both declarative and interrogative complements, or non-veridical w.r.t. both.

@cite{roelofsen-uegaki-2020} eq. 5 / @cite{spector-egr-2015}: V is veridically uniform iff (VDecl(V) ↔ VInterrog(V)).

Equations

• Semantics.Attitudes.EmbeddingConstraints.IsVeridicallyUniform V = (Semantics.Attitudes.EmbeddingConstraints.IsVeridicalDecl V ↔ Semantics.Attitudes.EmbeddingConstraints.IsVeridicalInterrog V)

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

Veridical Uniformity is independent of C-distributivity: a predicate can be C-distributive without being veridically uniform.

Counterexample: V_question always returns true for any non-empty Q.

• Non-veridical w.r.t. declaratives: V({false}, w) = true but false(w) = false
• Veridical w.r.t. interrogatives: trivially (V always returns true for singletons)
• Not uniform: veridical-interrog but not veridical-decl.

Constraint Hierarchy

The four constraints form a partial order under semantic strength (implication). The Hasse diagram:

      cDist
     ╱     ╲
  ptoQ   strawsonCDist

  vu  (incomparable with all three)

C-distributivity is the strongest: it implies both P-to-Q entailment and Strawson C-distributivity. The other pairs are all incomparable.

inductive Semantics.Attitudes.EmbeddingConstraints.Constraint : Type

The four universal constraints on clause-embedding predicates.

• cDist : Constraint
• ptoQ : Constraint
• strawsonCDist : Constraint
• vu : Constraint

instance Semantics.Attitudes.EmbeddingConstraints.instDecidableEqConstraint : DecidableEq Constraint

Equations

• Semantics.Attitudes.EmbeddingConstraints.instDecidableEqConstraint x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Attitudes.EmbeddingConstraints.instReprConstraint.repr : Constraint → ℕ → Std.Format

Equations

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

instance Semantics.Attitudes.EmbeddingConstraints.instReprConstraint : Repr Constraint

Equations

• Semantics.Attitudes.EmbeddingConstraints.instReprConstraint = { reprPrec := Semantics.Attitudes.EmbeddingConstraints.instReprConstraint.repr }

def Semantics.Attitudes.EmbeddingConstraints.instBEqConstraint.beq : Constraint → Constraint → Bool

Equations

• Semantics.Attitudes.EmbeddingConstraints.instBEqConstraint.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Attitudes.EmbeddingConstraints.instBEqConstraint : BEq Constraint

Equations

• Semantics.Attitudes.EmbeddingConstraints.instBEqConstraint = { beq := Semantics.Attitudes.EmbeddingConstraints.instBEqConstraint.beq }

instance Semantics.Attitudes.EmbeddingConstraints.Constraint.instLE : LE Constraint

Equations

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

instance Semantics.Attitudes.EmbeddingConstraints.Constraint.instLT : LT Constraint

Equations

• Semantics.Attitudes.EmbeddingConstraints.Constraint.instLT = { lt := fun (c₁ c₂ : Semantics.Attitudes.EmbeddingConstraints.Constraint) => c₁ ≤ c₂ ∧ ¬c₂ ≤ c₁ }

instance Semantics.Attitudes.EmbeddingConstraints.Constraint.instDecidableEq : DecidableEq Constraint

Equations

• Semantics.Attitudes.EmbeddingConstraints.Constraint.instDecidableEq = inferInstance

instance Semantics.Attitudes.EmbeddingConstraints.Constraint.instPreorder : Preorder Constraint

Equations

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

instance Semantics.Attitudes.EmbeddingConstraints.Constraint.instPartialOrder : PartialOrder Constraint

Equations

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

theorem Semantics.Attitudes.EmbeddingConstraints.Constraint.ptoQ_le_cDist : ptoQ ≤ cDist

P-to-Q Entailment is weaker than C-distributivity.

theorem Semantics.Attitudes.EmbeddingConstraints.Constraint.strawsonCDist_le_cDist : strawsonCDist ≤ cDist

Strawson C-distributivity is weaker than C-distributivity.

theorem Semantics.Attitudes.EmbeddingConstraints.Constraint.ptoQ_strawson_incomparable : ¬ptoQ ≤ strawsonCDist ∧ ¬strawsonCDist ≤ ptoQ

P-to-Q and Strawson C-dist are incomparable (neither implies the other).

theorem Semantics.Attitudes.EmbeddingConstraints.Constraint.vu_cDist_incomparable : ¬vu ≤ cDist ∧ ¬cDist ≤ vu

VU is incomparable with C-dist.

theorem Semantics.Attitudes.EmbeddingConstraints.Constraint.vu_ptoQ_incomparable : ¬vu ≤ ptoQ ∧ ¬ptoQ ≤ vu

VU is incomparable with P-to-Q.

theorem Semantics.Attitudes.EmbeddingConstraints.Constraint.vu_strawson_incomparable : ¬vu ≤ strawsonCDist ∧ ¬strawsonCDist ≤ vu

VU is incomparable with Strawson C-dist.

Semantic Soundness

The order relationships are justified by semantic implication theorems already proved above:

• cDistributive_implies_ptoq: C-dist ⟹ P-to-Q (justifies ptoQ ≤ cDist)
• cDist_implies_strawson: C-dist ⟹ Strawson C-dist (justifies strawsonCDist ≤ cDist)
• cDist_not_implies_veridicalUniformity: C-dist ⇏ VU (justifies ¬(vu ≤ cDist))

Semantic Separations

The incomparability results require counterexamples showing non-implications. These are proved as separation theorems below.

theorem Semantics.Attitudes.EmbeddingConstraints.ptoQ_not_implies_strawsonCDist : ∃ (W : Type) (E : Type) (V_question : E → CDistributivity.QuestionDen W → W → Bool), IsPtoQEntailing V_question ∧ ∀ (V_prop presup : E → BProp W → W → Bool), (V_prop = fun (x : E) (x_1 : BProp W) (x_2 : W) => false) → (presup = fun (x : E) (x_1 : BProp W) (x_2 : W) => true) → ¬IsStrawsonCDistributive V_prop V_question presup

P-to-Q does NOT imply Strawson C-distributivity.

Counterexample: V_question always returns true, V_prop always returns false.

• Satisfies P-to-Q: if V([p], w) = true and p ∈ Q, then V(Q, w) = true. (V([p]) = true trivially, and V(Q) = true trivially.)
• Violates Strawson C-dist (Q→P direction): V_question(Q) = true but ¬∃p ∈ Q, presup(p) → V_prop(p) = true, because V_prop is always false. Specifically, with presup = true and a non-empty Q, the → direction fails.

theorem Semantics.Attitudes.EmbeddingConstraints.strawsonCDist_not_implies_ptoQ : ∃ (W : Type) (E : Type) (V_question : E → CDistributivity.QuestionDen W → W → Bool), (∃ (V_prop : E → BProp W → W → Bool) (presup : E → BProp W → W → Bool), IsStrawsonCDistributive V_prop V_question presup) ∧ ¬IsPtoQEntailing V_question

Strawson C-distributivity does NOT imply P-to-Q Entailment.

Counterexample: V_question(Q) = (Q.length == 1), V_prop always false, presup always false.

• Strawson (→): V_question(Q) = true → |Q| = 1 → Q non-empty → ∃p ∈ Q, (false → false). ✓
• Strawson (←): ∃p ∈ Q, V_prop(p) = true is impossible (V_prop = false), so ← vacuously true. ✓
• P-to-Q fails: V_question([p]) = true, p ∈ [p, q], but V_question([p, q]) = false. ✓

The key insight: Strawson uses a separate V_prop, while P-to-Q is about V_question alone. With V_prop = false and presup = false, Strawson(←) is vacuously true, freeing V_question to violate P-to-Q without constraint from the ← direction.

theorem Semantics.Attitudes.EmbeddingConstraints.vu_not_implies_cDist : ∃ (W : Type) (E : Type) (V_question : E → CDistributivity.QuestionDen W → W → Bool), IsVeridicallyUniform V_question ∧ ∀ (V_prop : E → BProp W → W → Bool), (V_prop = fun (x : E) (x_1 : BProp W) (x_2 : W) => true) → ¬CDistributivity.IsCDistributive V_prop V_question

VU does NOT imply C-distributivity.

Counterexample: V always returns false.

• Veridically uniform: IsVeridicalDecl holds vacuously (V({p}) = false), IsVeridicalInterrog holds vacuously (V(Q) = false). Both directions of the biconditional hold.
• NOT C-distributive: V_question(x, [{p}], w) = false even though V_prop(x, p, w) = true (for suitable V_prop).

theorem Semantics.Attitudes.EmbeddingConstraints.vu_not_implies_ptoQ : ∃ (W : Type) (E : Type) (V : E → CDistributivity.QuestionDen W → W → Bool), IsVeridicallyUniform V ∧ ¬IsPtoQEntailing V

VU does NOT imply P-to-Q Entailment.

Same counterexample as vu_not_implies_cDist: V always false. P-to-Q fails because V([p]) = false, so the antecedent is never satisfied, wait — that makes P-to-Q vacuously TRUE.

Revised counterexample: V(Q) = Q.isEmpty (true when Q has no alternatives).

• VU: V([p]) = false always (singleton is non-empty), so IsVeridicalDecl holds vacuously. IsVeridicalInterrog: V(Q) = true requires Q empty, but then p ∈ Q is impossible, so holds vacuously. Both hold → biconditional true.
• P-to-Q fails: need V([p]) = true. But V([p]) = [p].isEmpty = false. So P-to-Q is vacuously true again!

V always false makes P-to-Q vacuously true. We need V that satisfies VU but has V([p]) = true for some p while V(Q) = false for some Q ∋ p.

V(Q, w) = Q.length == 1 && (match Q.head? with | some p => p w | none => false). i.e., singleton + answer is true.

• V([p], w) = true iff p w = true
• V([p, q], w) = false always
• IsVeridicalDecl: V([p], w) = true → p w = true ✓
• IsVeridicalInterrog: V(Q, w) = true → p ∈ Q → p w → V([p], w). V(Q, w) = true requires Q singleton, say Q = [q], and q w = true. p ∈ [q] means p = q. V([p]) = V([q]) = (q w = true) = true ✓
• VU: IsVeridicalDecl holds, IsVeridicalInterrog holds → biconditional ✓
• P-to-Q: V([p], w) = true (so p w = true), p ∈ [p, q]. V([p, q], w) = false. P-to-Q fails! ✓

theorem Semantics.Attitudes.EmbeddingConstraints.ptoQ_not_implies_vu : ∃ (W : Type) (E : Type) (V : E → CDistributivity.QuestionDen W → W → Bool), IsPtoQEntailing V ∧ ¬IsVeridicallyUniform V

P-to-Q Entailment does NOT imply VU.

The counterexample from cDist_not_implies_veridicalUniformity works here too, since C-dist implies P-to-Q and that example violates VU.

theorem Semantics.Attitudes.EmbeddingConstraints.strawsonCDist_not_implies_vu : ∃ (W : Type) (E : Type) (V_question : E → CDistributivity.QuestionDen W → W → Bool), (∃ (V_prop : E → BProp W → W → Bool) (presup : E → BProp W → W → Bool), IsStrawsonCDistributive V_prop V_question presup) ∧ ¬IsVeridicallyUniform V_question

Strawson C-distributivity does NOT imply VU.

Same V_question as P-to-Q case above (Q.any true), with V_prop = true, presup = true.

theorem Semantics.Attitudes.EmbeddingConstraints.vu_not_implies_strawsonCDist : ∃ (W : Type) (E : Type) (V_question : E → CDistributivity.QuestionDen W → W → Bool), IsVeridicallyUniform V_question ∧ ∀ (V_prop presup : E → BProp W → W → Bool), (V_prop = fun (x : E) (p : BProp W) (w : W) => p w) → (presup = fun (x : E) (x_1 : BProp W) (x_2 : W) => true) → ¬IsStrawsonCDistributive V_prop V_question presup

VU does NOT imply Strawson C-distributivity.

Counterexample: V_question(Q, w) = Q.all(fun p => p w) — universal.

• VU: IsVeridicalDecl holds (V([p], w) = p w = true → p w = true). IsVeridicalInterrog: V(Q, w) = true → all p ∈ Q have p w = true → for any p ∈ Q with p w = true, V([p], w) = p w = true. ✓
• ¬Strawson (←): With V_prop(p, w) = p w, presup = true: ∃p ∈ Q, p w = true → V_question(Q) = Q.all(⋯)? Only if ALL p ∈ Q are true. Take Q = [true, false]: ∃p ∈ Q, p w = true (namely true), but V_question(Q) = false.

Fictitious Predicates: Negative Tests

@cite{roelofsen-uegaki-2020} and @cite{steinert-threlkeld-2020} consider predicates that are conceivable but unattested cross-linguistically. P-to-Q Entailment predicts their non-existence by ruling them out.

These negative tests increase interconnection density: they show the constraint has empirical bite beyond just describing attested predicates.

def Semantics.Attitudes.EmbeddingConstraints.shknow {W : Type u_1} {E : Type u_2} (believes : E → (W → Bool) → Bool) (entertains : E → CDistributivity.QuestionDen W → Bool) : E → CDistributivity.QuestionDen W → W → Bool

*shknow (@cite{spector-egr-2015}): "know" with declaratives but "wonder" with interrogatives. Violates P-to-Q Entailment because knowing p (the declarative reading) does NOT entail wondering Q (the interrogative reading).

Paper's definition (@cite{roelofsen-uegaki-2020} eq. 37, in inquisitive semantics): ⟦shknow⟧ᵂ = λQ λx. (|alt(Q)|=1 ∧ DOXᵂₓ ∈ Q) ∨ (|alt(Q)|≠1 ∧ DOXᵂₓ ∉ Q ∧ INQᵂₓ ⊆ Q)

Our Hamblin simplification: branches on Q.length and uses abstract believes/entertains functions instead of DOX/INQ membership. This preserves the essential violation property while avoiding the need for inquisitive semantics infrastructure (downward closure, support).

Equations

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

theorem Semantics.Attitudes.EmbeddingConstraints.shknow_violates_ptoq {W : Type u_1} {E : Type u_2} (believes : E → (W → Bool) → Bool) (entertains : E → CDistributivity.QuestionDen W → Bool) (x : E) (p q : BProp W) (w : W) (hp_bel : believes x p = true) (hpq : p ≠ q) : ¬IsPtoQEntailing (shknow believes entertains)

*shknow violates P-to-Q Entailment: knowing p does not entail wondering Q.

def Semantics.Attitudes.EmbeddingConstraints.allOpen {W : Type u_1} {E : Type u_2} (believes : E → (W → Bool) → Bool) : E → CDistributivity.QuestionDen W → W → Bool

*all-open (@cite{roelofsen-uegaki-2020} §4.6): "consider all possibilities open." Defined as: ⟦all-open⟧(Q)(x) = ∀p ∈ Q. ¬B(x, p̄)

x's beliefs are compatible with every answer. This predicate quantifies universally over alternatives, violating P-to-Q Entailment.

Equations

• Semantics.Attitudes.EmbeddingConstraints.allOpen believes x Q _w = List.all Q fun (p : BProp W) => !believes x fun (w : W) => !p w

theorem Semantics.Attitudes.EmbeddingConstraints.allOpen_violates_ptoq {W : Type u_1} {E : Type u_2} (believes : E → (W → Bool) → Bool) (x : E) (p q : BProp W) (w : W) (hp_compat : (believes x fun (w : W) => !p w) = false) (hq_incompat : (believes x fun (w : W) => !q w) = true) : ¬IsPtoQEntailing (allOpen believes)

*all-open violates P-to-Q Entailment: being compatible with one answer p does not entail being compatible with ALL answers in Q.

def Semantics.Attitudes.EmbeddingConstraints.knopinion {W : Type u_1} {E : Type u_2} (believes : E → (W → Bool) → Bool) : E → CDistributivity.QuestionDen W → W → Bool

*knopinion (@cite{steinert-threlkeld-2020}): "know" with declaratives, "have no opinion about" with interrogatives.

Paper's definition (@cite{roelofsen-uegaki-2020} eq. 38, in inquisitive semantics): ⟦knopinion⟧ᵂ = λQ λx. w ∈ DOXᵂₓ ∧ (DOXᵂₓ ∈ Q ∨ DOXᵂₓ ∈ ¬Q)

This is a uniform definition (no branching on |alt(Q)|): factivity + either resolving or fully ignorant.

Our Hamblin simplification: branches on Q.length with believes/all ¬believes. Structurally different from the paper's definition, but preserves the essential P-to-Q violation: knowing p does not entail having no opinion about Q.

Equations

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

theorem Semantics.Attitudes.EmbeddingConstraints.knopinion_violates_ptoq {W : Type u_1} {E : Type u_2} (believes : E → (W → Bool) → Bool) (x : E) (p q : BProp W) (w : W) (hp_bel : believes x p = true) (hpq : p ≠ q) : ¬IsPtoQEntailing (knopinion believes)

*knopinion violates P-to-Q Entailment: knowing p does not entail having no opinion about Q.

Attested Predicates Satisfy P-to-Q Entailment

The negative tests above show fictitious predicates violate P-to-Q. Here we prove that attested predicates satisfy it, completing the paper's argument.

Modal Bases for Clause-Embedding Predicates

Following @cite{ciardelli-groenendijk-roelofsen-2018} and @cite{roelofsen-uegaki-2020}, we use:

• DOX x w — doxastic state: set of worlds x considers possible in w
• INQ x w — inquisitive state: set of subsets of DOX that x entertains in w

A clause-embedding predicate's semantics can be expressed in terms of how these modal bases relate to the complement denotation Q.

@[reducible, inline]

abbrev Semantics.Attitudes.EmbeddingConstraints.DoxState (W : Type u_1) : Type u_1

Doxastic state: the set of worlds an agent considers possible.

Equations

• Semantics.Attitudes.EmbeddingConstraints.DoxState W = (W → Bool)

@[reducible, inline]

abbrev Semantics.Attitudes.EmbeddingConstraints.BouState (W : Type u_1) : Type u_1

Bouletic state: the set of worlds compatible with an agent's preferences.

Equations

• Semantics.Attitudes.EmbeddingConstraints.BouState W = (W → Bool)

@[reducible, inline]

abbrev Semantics.Attitudes.EmbeddingConstraints.InqState (W : Type u_1) : Type u_1

Inquisitive state: the issues an agent entertains. Modeled as a list of propositions (subsets of DOX) that the agent would like to resolve.

Equations

• Semantics.Attitudes.EmbeddingConstraints.InqState W = List (W → Bool)

def Semantics.Attitudes.EmbeddingConstraints.wonderSem {W : Type u_1} {E : Type u_2} (dox : E → W → W → Bool) (inq : E → W → InqState W) (covers : (W → Bool) → (W → Bool) → Bool) : E → CDistributivity.QuestionDen W → W → Bool

Wonder semantics (@cite{roelofsen-uegaki-2020} eq. 33): ⟦wonder⟧ = λQ λx. DOX_x ∉ Q ∧ INQ_x ⊆ Q

The first conjunct (ignorance) says x's doxastic state doesn't resolve Q. The second (entertainment) says x entertains the issue expressed by Q.

We parametrize on a covers relation (s ⊆ p) to avoid requiring Fintype W. The ignorance component checks that NO alternative in Q covers DOX. The entertainment component checks that every issue in INQ is covered by some alternative in Q.

Equations

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

theorem Semantics.Attitudes.EmbeddingConstraints.wonder_satisfies_ptoq {W : Type u_1} {E : Type u_2} (dox : E → W → W → Bool) (inq : E → W → InqState W) (covers : (W → Bool) → (W → Bool) → Bool) (hDoxInINQ : ∀ (x : E) (w : W), dox x w ∈ inq x w) : IsPtoQEntailing (wonderSem dox inq covers)

Wonder trivially satisfies P-to-Q Entailment because the declarative semantics is always false.

For a singleton complement {p}, ⟦wonder⟧({p})(x)(w) requires both:

• ignorance: ¬(covers DOX p) — DOX is NOT a subset of p
• entertainment: covers DOX p (the only alternative is p, so INQ ⊆ {p} requires each issue to be covered by p; if DOX itself is an issue, this requires covers DOX p)

These are contradictory when DOX is among the inquisitive issues. More generally, if any s ∈ INQ has covers s p = covers DOX p (e.g., DOX ∈ INQ), the conjunction is false.

The general proof: if INQ contains DOX, the singleton semantics is always false, making P-to-Q vacuously true.

def Semantics.Attitudes.EmbeddingConstraints.darooSem {W : Type u_1} {E : Type u_2} (inq : E → W → InqState W) (covers : (W → Bool) → (W → Bool) → Bool) : E → CDistributivity.QuestionDen W → W → Bool

Daroo semantics (@cite{roelofsen-uegaki-2020} eq. 24, @cite{uegaki-roelofsen-2018}): ⟦daroo⟧ = λQ λx. INQ_sp ⊆ Q

Unlike wonder, daroo lacks the ignorance component (DOX ∉ Q). This makes daroo compatible with both declarative and interrogative complements:

• With declarative p: INQ_sp ⊆ {p}↓ iff DOX_sp ⊆ p (x believes p)
• With interrogative Q: INQ_sp ⊆ Q (x entertains the issue of Q)

Equations

• Semantics.Attitudes.EmbeddingConstraints.darooSem inq covers x Q w = List.all (inq x w) fun (s : W → Bool) => List.any Q fun (p : BProp W) => covers s p

theorem Semantics.Attitudes.EmbeddingConstraints.daroo_satisfies_ptoq {W : Type u_1} {E : Type u_2} (inq : E → W → InqState W) (covers : (W → Bool) → (W → Bool) → Bool) : IsPtoQEntailing (darooSem inq covers)

Daroo satisfies P-to-Q Entailment: if INQ ⊆ {p} and p ∈ Q, then INQ ⊆ Q.

If every s in INQ is covered by the sole alternative p in the singleton, and p ∈ Q, then every s in INQ is covered by some alternative in Q (namely p itself). This is pure list-level monotonicity.

def Semantics.Attitudes.EmbeddingConstraints.careSem {W : Type u_1} {E : Type u_2} (dox : E → W → DoxState W) (bou : E → W → BouState W) (doxSupports : DoxState W → CDistributivity.QuestionDen W → Bool) (settled : BouState W → (W → Bool) → Bool) : E → CDistributivity.QuestionDen W → W → Bool

Care semantics (@cite{roelofsen-uegaki-2020} eq. 23, based on @cite{elliott-etal-2017} and @cite{theiler-etal-2018}): ⟦care⟧ᵂ = λQ λx : DOXᵂₓ ⊆ ⋃Q ∧ ∃p ∈ alt(Q). BOUᵂₓ ⊆ p ∨ BOUᵂₓ ∩ p = ∅

The first conjunct (doxastic support) says x's beliefs are compatible with Q. The second conjunct (bouletic settlement) says some answer settles x's preferences (either all preference worlds satisfy p, or none do).

doxSupports s Q checks DOX ⊆ ⋃Q (every doxastic world is in some answer). settled b p checks BOU ⊆ p ∨ BOU ∩ p = ∅ (preferences are settled by p).

Equations

• Semantics.Attitudes.EmbeddingConstraints.careSem dox bou doxSupports settled x Q w = (doxSupports (dox x w) Q && List.any Q fun (p : BProp W) => settled (bou x w) p)

theorem Semantics.Attitudes.EmbeddingConstraints.care_satisfies_ptoq {W : Type u_1} {E : Type u_2} (dox : E → W → DoxState W) (bou : E → W → BouState W) (doxSupports : DoxState W → CDistributivity.QuestionDen W → Bool) (settled : BouState W → (W → Bool) → Bool) (hMono : ∀ (s : DoxState W) (p : BProp W) (Q : CDistributivity.QuestionDen W), doxSupports s [p] = true → p ∈ Q → doxSupports s Q = true) : IsPtoQEntailing (careSem dox bou doxSupports settled)

Care satisfies P-to-Q Entailment (@cite{roelofsen-uegaki-2020} §4.2, fn. 5).

If care({p})(x), then DOX ⊆ p (x believes p) and BOU is settled by p. Since p ∈ Q: DOX ⊆ p ⊆ ⋃Q (doxastic support is monotone), and the bouletic witness carries over. Hence care(Q)(x).

The proof requires monotonicity of doxastic support: if DOX supports {p} and p ∈ Q, then DOX supports Q. This holds because DOX ⊆ p ⊆ ⋃Q.

def Semantics.Attitudes.EmbeddingConstraints.mõtlemaSem {W : Type u_1} {E : Type u_2} (inq : E → W → InqState W) (dox img : E → W → W → Bool) (covers : (W → Bool) → (W → Bool) → Bool) : E → CDistributivity.QuestionDen W → W → Bool

Mõtlema semantics (@cite{roelofsen-uegaki-2020} eq. 32, @cite{roberts-2018}):

⟦mõtlema⟧ʷ = λQ λx. INQʷₓ ⊆ Q ∨ ∃p ∈ alt(Q): DOXʷₓ ⊆ p̄ ∧ IMGʷₓ ⊆ p

Two disjunctive readings:

• 'daroo' reading: INQ ⊆ Q (x entertains the issue expressed by Q)
• 'imagine' reading: ∃p ∈ Q, x believes ¬p but imagines p

Hamblin simplification: covers replaces set containment; img models the imagination state IMGʷₓ.

Equations

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

theorem Semantics.Attitudes.EmbeddingConstraints.mõtlema_satisfies_ptoq {W : Type u_1} {E : Type u_2} (inq : E → W → InqState W) (dox img : E → W → W → Bool) (covers : (W → Bool) → (W → Bool) → Bool) : IsPtoQEntailing (mõtlemaSem inq dox img covers)

Mõtlema satisfies P-to-Q Entailment (@cite{roelofsen-uegaki-2020} §4.4).

On the 'daroo' reading: if INQ ⊆ {p}↓ and p ∈ Q, then INQ ⊆ Q (same monotonicity argument as daroo). On the 'imagine' reading: if ∃p ∈ {p₀}, believes ¬p ∧ imagines p holds for p = p₀, and p₀ ∈ Q, then the same witness works for Q. Either disjunct of the singleton semantics provides a witness for Q.

def Semantics.Attitudes.EmbeddingConstraints.wondowsSem {W : Type u_1} {E : Type u_2} (factive : E → W → Bool) (doxSupports : E → CDistributivity.QuestionDen W → W → Bool) (believes : E → (W → Bool) → Bool) : E → CDistributivity.QuestionDen W → W → Bool

*wondows (@cite{steinert-threlkeld-2020}, @cite{roelofsen-uegaki-2020} eq. 35): "know" with declaratives, "be uncertain" with interrogatives.

⟦wondows⟧ʷ = λQ λx. w ∈ DOXʷₓ ∧ DOXʷₓ ⊆ info(Q) ∧ ∀p ∈ alt(Q): DOXʷₓ ∩ p ≠ ∅

Three conjuncts: factivity (w ∈ DOX), informational support (DOX ⊆ ⋃Q), and all-open (compatible with every alternative). The third conjunct corresponds to allOpen and is what violates P-to-Q Entailment.

Hamblin simplification: factive checks w ∈ DOX, doxSupports checks DOX ⊆ info(Q), and the all-open component reuses the allOpen pattern.

Equations

• Semantics.Attitudes.EmbeddingConstraints.wondowsSem factive doxSupports believes x Q w = (factive x w && doxSupports x Q w && List.all Q fun (p : BProp W) => !believes x fun (w' : W) => !p w')

theorem Semantics.Attitudes.EmbeddingConstraints.wondows_violates_ptoq {W : Type u_1} {E : Type u_2} (factive : E → W → Bool) (doxSupports : E → CDistributivity.QuestionDen W → W → Bool) (believes : E → (W → Bool) → Bool) (x : E) (p q : BProp W) (w : W) (h_factive : factive x w = true) (h_dox_singleton : doxSupports x [p] w = true) (_h_dox_pair : doxSupports x [p, q] w = true) (hp_compat : (believes x fun (w' : W) => !p w') = false) (hq_incompat : (believes x fun (w' : W) => !q w') = true) : ¬IsPtoQEntailing (wondowsSem factive doxSupports believes)

*wondows violates P-to-Q Entailment (@cite{roelofsen-uegaki-2020} §4.6).

The all-open component (∀p ∈ Q. DOX ∩ p ≠ ∅) makes the predicate anti-monotone in Q: being compatible with one answer p does not entail being compatible with ALL answers in a larger Q. Same mechanism as allOpen.

Results

P-to-Q Entailment (@cite{roelofsen-uegaki-2020})

• IsPtoQEntailing: Definition of the constraint
• cDistributive_implies_ptoq: C-distributivity ⟹ P-to-Q Entailment
• degreeComparison_isPtoQEntailing: Degree-comparison predicates satisfy it

Positive P-to-Q Proofs (@cite{roelofsen-uegaki-2020} §§4.2–4.5)

• wonder_satisfies_ptoq: wonder is P-to-Q entailing (vacuously — declarative semantics is contradictory due to ignorance + singleton)
• daroo_satisfies_ptoq: daroo is P-to-Q entailing (INQ monotonicity)
• care_satisfies_ptoq: care is P-to-Q entailing (doxastic support monotonicity)
• mõtlema_satisfies_ptoq: mõtlema is P-to-Q entailing (both disjuncts monotone)

Strawson C-Distributivity (@cite{uegaki-2019})

• IsStrawsonCDistributive: Weakened C-distributivity accounting for presuppositions
• cDist_implies_strawson: Plain C-dist ⟹ Strawson C-dist

Fictitious Predicate Rejection (@cite{roelofsen-uegaki-2020} §4.6)

• shknow_violates_ptoq: *shknow (know+wonder hybrid) ruled out
• knopinion_violates_ptoq: *knopinion (know+no-opinion hybrid) ruled out
• allOpen_violates_ptoq: *all-open (universal compatibility) ruled out
• wondows_violates_ptoq: *wondows (know+uncertain hybrid) ruled out

Veridical Uniformity (@cite{spector-egr-2015})

• IsVeridicalDecl: ⟦V that p⟧(x) entails p (eq. 1)
• IsVeridicalInterrog: ⟦V Q⟧(x) ∧ p ∧ p ∈ Q entails ⟦V that p⟧(x) (eq. 3)
• IsVeridicallyUniform: both or neither (eq. 5)
• cDist_not_implies_veridicalUniformity: C-dist ⇏ Veridical Uniformity

Constraint Hierarchy (Mathlib PartialOrder)

• Constraint: inductive with .cDist, .ptoQ, .strawsonCDist, .vu
• PartialOrder Constraint: ptoQ ≤ cDist, strawsonCDist ≤ cDist, vu incomparable
• Separation theorems (all 6 non-implication directions proved):
  • ptoQ_not_implies_strawsonCDist: P-to-Q ⇏ Strawson C-dist
  • strawsonCDist_not_implies_ptoQ: Strawson C-dist ⇏ P-to-Q
  • vu_not_implies_cDist: VU ⇏ C-dist
  • vu_not_implies_ptoQ: VU ⇏ P-to-Q
  • vu_not_implies_strawsonCDist: VU ⇏ Strawson C-dist
  • ptoQ_not_implies_vu, strawsonCDist_not_implies_vu: ⇏ VU