Bondarenko & Elliott (2026) @cite{bondarenko-elliott-2026}

Monotonicity via mereology in the semantics of attitude reports. Semantics and Pragmatics 19(2). DOI: 10.3765/sp.19.2.

Empirical puzzle (@cite{sharvit-2024})

NPI licensing in negated belief reports patterns differently for complement clauses vs. relative clauses inside a singular definite (@cite{bondarenko-elliott-2026} eq. 2):

*Katya doesn't believe [the rumor [that Anton has ever spread]].
 Katya doesn't believe [the rumor [that Anton has ever snowboarded]].

The puzzle: weak NPIs (any/ever) require a Strawson Downward-Entailing (SDE, eq. 18a) and not Strawson Upward-Entailing (not-SUE, eq. 18b) environment per the licensing condition (eq. 21). Two existing approaches both fail (@cite{bondarenko-elliott-2026} §3.2):

• Subset semantics (CONT(x) ⊆ ⟦S⟧): uniqueness collapse (eq. 24) makes singular definites both SUE and SDE, so NPIs should be allowed even in positive belief reports — wrong.
• Equality semantics (CONT(x) = ⟦S⟧): functionality makes the environment neither SUE nor SDE — NPIs blocked everywhere — wrong.

Proposal (@cite{bondarenko-elliott-2026} §4)

Adopt EQUALITY semantics (eq. 10) and add three mereological constraints:

• MSI (eq. 44): CONT preserves proper parthood. Every proper informational part p' < CONT(x) is the content of some proper sub-x.
• MSO (eq. 48): THEME preserves sub-eventualities. Every proper sub-e has a corresponding proper sub-THEME(e).
• TECM (eq. 59): For believe-class predicates, CONT(e) = CONT(THEME(e)).

Result (Section 5, eqs. 66–73): the Sharvit configuration becomes

• Positive Katya believes the rumor that p is SUE not SDE (eq. 66) — doesn't license NPIs.
• Negative Katya doesn't believe the rumor that p is SDE not SUE (eq. 67) — licenses NPIs.

The contrast in (2) follows.

Main results

• believes_closure_under_entailment (paper eq. 45) — MSI ⇒ positive belief is closed under informational entailment (direct-CP version).
• not_believes_reverses (eq. 46) — MSI ⇒ negation reverses the direction (direct-CP version).
• positive_sharvit_closure (paper eq. 69, §5) — the full Sharvit configuration: under MSI/MSO/TECM/BelievingDIV/RumorDIV/WorldLocatedDIV, if M believes the rumor that p and p' < p then M believes the rumor that p'. The chain TECM ∘ MSI ∘ BelievingDIV ∘ WorldLocatedDIV ∘ MSO ∘ RumorDIV ∘ TECM.
• negated_sharvit_SDE (paper eq. 72, §5) — contrapositive: the negated configuration is SDE wrt the restrictor.
• negated_sharvit_not_SUE (paper eq. 73, §5) — concrete witness model showing the negated configuration is not SUE wrt the restrictor. Combined with negated_sharvit_SDE this gives the full SDE-and-not-SUE monotonicity profile that the NPI licensing condition (paper eq. 21) requires. The strongest theorem of the paper — captures Sharvit's empirical contrast in (2).
• believes_closure_under_conjunction (§6.1, eq. 79) — summation closure on believings + content-of-sum-is-meet ⇒ closure under ∧.
• Mereology.not_isContentPart_of_singleton_not_le (§6.3, eq. 95) — generic Mereology lemma; the paper's discriminating witness for conjunctive parthood (Jago Def 5) is a one-line application.
• believes_does_not_always_close_under_intersection — cross-framework: B&E's mereological Believes does NOT close under conjunction the way Hintikka's boxAt does, witnessed by a non-believings-closed model.

Implementation notes

• Informational parthood (paper eq. 43, p ≤ q iff p ⊇ q) is the direction-flip of pointwise ≤ on Set W. We use the paper's convention via propLE for paper fidelity.
• The §5 theorems use the world parameter w via an abstract located : V → W → Prop relation with a WorldLocatedDIV downward-closure axiom (paper fn. 2: "possible worlds are maximal eventualities"). The simpler direct-CP closure lemmas (§4 / eqs. 45-46) drop the world since it threads uniformly.
• RumorDIV (parts of rumors are rumors) is an explicit axiom; the paper handwaves it in §4.4 ("rumors, much like more concrete entities, have a mereological structure") without formalizing.

@[reducible, inline]

abbrev Phenomena.Attitudes.Studies.BondarenkoElliott2026.propLE {W : Type u_1} (p q : Set W) : Prop

Informational parthood for propositions (paper eq. 43): p ≤_BE q iff p is semantically entailed by q (p ⊇ q). Smaller p = bigger world set = weaker proposition.

Thin alias for the swapped Set W order: propLE p q := q ≤ p. Reflexivity, transitivity, and <-extraction lemmas all come from mathlib's Preorder (Set W) via this alias. We expose the paper-named symbols for docstring fidelity, not as a new ontology.

Equations

• Phenomena.Attitudes.Studies.BondarenkoElliott2026.propLE p q = (q ≤ p)

@[reducible, inline]

abbrev Phenomena.Attitudes.Studies.BondarenkoElliott2026.propLT {W : Type u_1} (p q : Set W) : Prop

Proper informational parthood: propLT p q := q < p.

Equations

• Phenomena.Attitudes.Studies.BondarenkoElliott2026.propLT p q = (q < p)

def Phenomena.Attitudes.Studies.BondarenkoElliott2026.MSI {V : Type u_1} {W : Type u_3} [Preorder V] (CONT : V → Option (Set W)) : Prop

MSI — Mapping to Sub-parts of the Input (paper eq. 44). A content function preserves proper informational parthood: every proper part p' <_BE CONT(x) is the content of some proper sub-x.

See MSI_iff_strictPartReflecting for the identification with the generic Mereology.StrictPartReflecting (instantiated at the OrderDual of Set W's subset order, since paper eq. 43 uses the flipped convention p' <_BE p iff p ⊊ p').

Equations

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

def Phenomena.Attitudes.Studies.BondarenkoElliott2026.MSO {V : Type u_1} {E : Type u_2} [Preorder V] [Preorder E] (THEME : V → Option E) : Prop

MSO — Mapping to Sub-parts of the Output (paper eq. 48). A theme function preserves proper sub-eventualities: every proper sub-e has a corresponding proper sub-THEME(e).

Equivalent to Mereology.StrictPartPreserving (the relationship is Iff.rfl since both use the standard < on E).

Equations

• Phenomena.Attitudes.Studies.BondarenkoElliott2026.MSO THEME = ∀ ⦃e e' : V⦄ ⦃te : E⦄, e' < e → THEME e = some te → ∃ x' < te, THEME e' = some x'

theorem Phenomena.Attitudes.Studies.BondarenkoElliott2026.MSO_iff_strictPartPreserving {V : Type u_1} {E : Type u_2} [Preorder V] [Preorder E] (THEME : V → Option E) : MSO THEME ↔ Mereology.StrictPartPreserving THEME

MSO is exactly Mereology.StrictPartPreserving.

def Phenomena.Attitudes.Studies.BondarenkoElliott2026.TECM {V : Type u_1} {E : Type u_2} {W : Type u_3} (P : V → Prop) (CONT_v : V → Option (Set W)) (CONT_e : E → Option (Set W)) (THEME : V → Option E) : Prop

TECM — Theme-Event Content Matching (paper eqs. 59, 65). For believe-class predicates P, the content of an event equals the content of its theme.

Stated as Option-equality (faithful to the paper's eq. 65 form CONT(e) = CONT(THEME(e))). The paper restricts to e ∈ Dom(CONT) ∩ Dom(THEME); this restriction is implicit here since when both CONT_v e and CONT_e te are none, the equality is vacuous.

Equations

• Phenomena.Attitudes.Studies.BondarenkoElliott2026.TECM P CONT_v CONT_e THEME = ∀ ⦃e : V⦄ ⦃te : E⦄, P e → THEME e = some te → CONT_v e = CONT_e te

def Phenomena.Attitudes.Studies.BondarenkoElliott2026.HolderPreservedUnderParts {V : Type u_1} {E : Type u_2} [Preorder V] (HOLDER : V → Option E) : Prop

The believe-predicate's holder is preserved under parthood.

Equations

• Phenomena.Attitudes.Studies.BondarenkoElliott2026.HolderPreservedUnderParts HOLDER = ∀ ⦃e e' : V⦄ ⦃M : E⦄, HOLDER e = some M → e' ≤ e → HOLDER e' = some M

def Phenomena.Attitudes.Studies.BondarenkoElliott2026.BelievingDIV {V : Type u_1} {E : Type u_2} [Preorder V] (believe : V → Prop) (HOLDER : V → Option E) : Prop

Believing-DIV (paper footnote 18). All parts of a believing-event are themselves believing-events with the same holder. The mereological analogue of divisive reference (@cite{cheng-1973} for mass nouns).

Factored as the conjunction of two reusable conditions: Mereology.DIV believe (every part of a believing is itself a believing — the actual divisive-reference clause) and HolderPreservedUnderParts HOLDER (the same holder threads through all parts of a single eventuality).

Equations

• Phenomena.Attitudes.Studies.BondarenkoElliott2026.BelievingDIV believe HOLDER = (Mereology.DIV believe ∧ Phenomena.Attitudes.Studies.BondarenkoElliott2026.HolderPreservedUnderParts HOLDER)

Cross-paper bridge to @cite{pasternak-2019}. B&E's BelievingDIV is a strengthening of Pasternak's MentalStateHomogeneity (which is itself defined as Mereology.DIV over a preorder, modulo biconditional reflexivity — see Pasternak2019.mentalStateHomogeneity_iff). The strengthening adds HolderPreservedUnderParts: B&E require not only that all parts of a believing are believings (Pasternak's homogeneity), but that all parts share the same holder. The bridge theorem makes formal what is otherwise a silent agreement: B&E's belief mereology IS Pasternak's mental-state mereology, restricted to belief and augmented with the per-eventuality-holder-uniqueness axiom B&E need for their MSI/TECM machinery (paper §3).

theorem Phenomena.Attitudes.Studies.BondarenkoElliott2026.belief_div_specializes_pasternak_homogeneity {V : Type u_1} {E : Type u_2} [Preorder V] (believe : V → Prop) (HOLDER : V → Option E) (h : BelievingDIV believe HOLDER) : Pasternak2019.MentalStateHomogeneity believe

def Phenomena.Attitudes.Studies.BondarenkoElliott2026.Believes {V : Type u_1} {E : Type u_2} {W : Type u_3} (believe : V → Prop) (HOLDER : V → Option E) (CONT : V → Option (Set W)) (M : E) (p : Set W) : Prop

Equality semantics for Mitya believes p (paper eq. 11, simplified): there exists a believing-eventuality with holder M and content p.

The paper has ∃e ≤ w[…] for "located in world w"; for the Strawson-entailment claims about propositions (sets of worlds) the world parameter doesn't enter the proof structure, so we drop it.

Equations

• Phenomena.Attitudes.Studies.BondarenkoElliott2026.Believes believe HOLDER CONT M p = ∃ (e : V), believe e ∧ HOLDER e = some M ∧ CONT e = some p

theorem Phenomena.Attitudes.Studies.BondarenkoElliott2026.believes_closure_under_entailment {V : Type u_1} {E : Type u_2} {W : Type u_3} [Preorder V] {believe : V → Prop} {HOLDER : V → Option E} {CONT : V → Option (Set W)} (h_msi : MSI CONT) (h_div : BelievingDIV believe HOLDER) {M : E} {p p' : Set W} (h_lt : propLT p' p) (h_bel : Believes believe HOLDER CONT M p) : Believes believe HOLDER CONT M p'

Lemma — paper eq. 45: MSI implies positive belief is closed under informational entailment. If M believes p and p' <_BE p (i.e., p ⊋ p' as sets — p' is properly weaker), then M believes p'.

Proof (paper sketch): from Believes M p get a believing-e with CONT(e) = p. By MSI applied to p' < p = CONT(e), find e' < e with CONT(e') = p'. By BelievingDIV, e' is itself a believing with holder M.

theorem Phenomena.Attitudes.Studies.BondarenkoElliott2026.not_believes_reverses {V : Type u_1} {E : Type u_2} {W : Type u_3} [Preorder V] {believe : V → Prop} {HOLDER : V → Option E} {CONT : V → Option (Set W)} (h_msi : MSI CONT) (h_div : BelievingDIV believe HOLDER) {M : E} {p p' : Set W} (h_lt : propLT p' p) (h_neg : ¬Believes believe HOLDER CONT M p') : ¬Believes believe HOLDER CONT M p

Lemma — paper eq. 46: MSI implies negated belief is downward entailing in the propositional argument. If ¬Believes M p' and p' <_BE p, then ¬Believes M p.

Section 5 of @cite{bondarenko-elliott-2026}.

The full LF for "Mitya believes the rumor that p" combines four ingredients (paper eqs. 62–65):

1. Equality semantics for the that-clause (eq. 62).
2. MSI on CONT (eq. 63).
3. MSO on THEME (eq. 64).
4. TECM tying believe-events' content to their theme's content (eq. 65).

The paper's main result (Section 5) is that the configuration

`Mitya believes the rumor that p`

is Strawson Upward-Entailing (SUE) but not SDE with respect to the restrictor of the indefinite inside the that-clause, and the negated version

`Mitya doesn't believe the rumor that p`

is SDE but not SUE. The latter satisfies the NPI licensing condition (eq. 21); the former does not. The contrast in (2) follows.

We prove the SDE direction for the negated configuration below (negated_sharvit_SDE). The "not-SUE" direction (functionality of CONT under uniqueness presupposition) is documented in the paper's eq. 73 and relies on functionality of CONT rather than on MSI/MSO/TECM — a sketch follows the theorem.

def Phenomena.Attitudes.Studies.BondarenkoElliott2026.TheRumorThat {E : Type u_2} {W : Type u_3} (rumor : E → Prop) (CONT_e : E → Option (Set W)) (p : Set W) (r : E) : Prop

Equality-semantics rendering of "the rumor that p" — the unique rumor with content p (paper eqs. 60a/61a's iota construction, simplified). Existence and uniqueness are the standard Fregean presuppositions of the.

Equations

• Phenomena.Attitudes.Studies.BondarenkoElliott2026.TheRumorThat rumor CONT_e p r = (rumor r ∧ CONT_e r = some p)

def Phenomena.Attitudes.Studies.BondarenkoElliott2026.BelievesTheRumorThat {V : Type u_1} {E : Type u_2} {W : Type u_3} (believe : V → Prop) (HOLDER THEME : V → Option E) (rumor : E → Prop) (CONT_e : E → Option (Set W)) (M : E) (p : Set W) : Prop

"Mitya believes the rumor that p" (paper eq. 60a, equality version). Existential over believing-events whose theme is the unique p-rumor.

Equations

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

Paper §5 chains MSI ∘ MSO ∘ TECM ∘ BelievingDIV ∘ RumorDIV ∘ WorldLocatedDIV to derive the SDE-not-SUE asymmetry that captures Sharvit's NPI contrast. We prove the closure direction (positive_sharvit_closure) and the SDE direction (negated_sharvit_SDE) via contraposition.

The world parameter (∃e ≤ w[…], paper fn. 2: "possible worlds are maximal eventualities") is reintroduced via an abstract located : V → W → Prop relation with downward-closure under the eventuality preorder.

def Phenomena.Attitudes.Studies.BondarenkoElliott2026.RumorDIV {E : Type u_2} [Preorder E] (rumor : E → Prop) : Prop

Parts of rumors are rumors — the rumor-side analogue of BelievingDIV. Implicit in paper §4.4 ("rumors, much like more concrete entities, have a mereological structure").

Equations

• Phenomena.Attitudes.Studies.BondarenkoElliott2026.RumorDIV rumor = ∀ ⦃r r' : E⦄, rumor r → r' ≤ r → rumor r'

def Phenomena.Attitudes.Studies.BondarenkoElliott2026.WorldLocatedDIV {V : Type u_1} {W : Type u_3} [Preorder V] (located : V → W → Prop) : Prop

"Located at world w" is preserved under parts of eventualities. Paper fn. 2 grounds this: worlds are maximal eventualities, so located e w := e ≤ w for events and worlds in a shared lattice; here we abstract that as a preorder-down-closed binary relation.

Equations

• Phenomena.Attitudes.Studies.BondarenkoElliott2026.WorldLocatedDIV located = ∀ ⦃e e' : V⦄ ⦃w : W⦄, e' ≤ e → located e w → located e' w

def Phenomena.Attitudes.Studies.BondarenkoElliott2026.BelievesTheRumorThatAt {V : Type u_1} {E : Type u_2} {W : Type u_3} (believe : V → Prop) (HOLDER : V → Option E) (located : V → W → Prop) (THEME : V → Option E) (rumor : E → Prop) (CONT_e : E → Option (Set W)) (M : E) (p : Set W) (w : W) : Prop

Equality semantics for "Mitya believes the rumor that p" at world w (paper eqs. 60a/61a, with the ∃e ≤ w world parameter restored).

Equations

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

theorem Phenomena.Attitudes.Studies.BondarenkoElliott2026.positive_sharvit_closure {V : Type u_1} {E : Type u_2} {W : Type u_3} [Preorder V] [Preorder E] {believe : V → Prop} {HOLDER : V → Option E} {CONT_v : V → Option (Set W)} {CONT_e : E → Option (Set W)} {THEME : V → Option E} {rumor : E → Prop} {located : V → W → Prop} (h_msi : MSI CONT_v) (h_mso : MSO THEME) (h_tecm : TECM believe CONT_v CONT_e THEME) (h_div : BelievingDIV believe HOLDER) (h_rumor_div : RumorDIV rumor) (h_world_div : WorldLocatedDIV located) {M : E} {p p' : Set W} {w : W} (h_lt : propLT p' p) (h_pos : BelievesTheRumorThatAt believe HOLDER located THEME rumor CONT_e M p w) : BelievesTheRumorThatAt believe HOLDER located THEME rumor CONT_e M p' w

Theorem (paper eq. 69, Strawson direction): under MSI/MSO/TECM

• BelievingDIV + RumorDIV + WorldLocatedDIV, the Sharvit configuration's positive sentence is closed under (proper) informational entailment: if M believes the rumor that p and p' < p (informationally weaker), then M believes the rumor that p'.

This is the SUE direction for the positive sentence (paper eq. 66a). Proof structure: TECM ∘ MSI ∘ BelievingDIV ∘ WorldLocatedDIV ∘ MSO ∘ RumorDIV ∘ TECM.

theorem Phenomena.Attitudes.Studies.BondarenkoElliott2026.negated_sharvit_SDE {V : Type u_1} {E : Type u_2} {W : Type u_3} [Preorder V] [Preorder E] {believe : V → Prop} {HOLDER : V → Option E} {CONT_v : V → Option (Set W)} {CONT_e : E → Option (Set W)} {THEME : V → Option E} {rumor : E → Prop} {located : V → W → Prop} (h_msi : MSI CONT_v) (h_mso : MSO THEME) (h_tecm : TECM believe CONT_v CONT_e THEME) (h_div : BelievingDIV believe HOLDER) (h_rumor_div : RumorDIV rumor) (h_world_div : WorldLocatedDIV located) {M : E} {p p' : Set W} {w : W} (h_lt : propLT p' p) (h_neg : ¬BelievesTheRumorThatAt believe HOLDER located THEME rumor CONT_e M p' w) : ¬BelievesTheRumorThatAt believe HOLDER located THEME rumor CONT_e M p w

Theorem (paper eq. 72, SDE direction): under the §5 axioms, the negated Sharvit configuration is Strawson Downward-Entailing wrt the restrictor of the indefinite inside the embedded CP. Concretely: if M does not believe the rumor that p' and p' < p (informationally weaker), then M does not believe the rumor that p.

The proof is the contrapositive of positive_sharvit_closure. This is the direction that licenses NPIs in Katya doesn't believe the rumor that Anton has ever snowboarded (paper eq. 67b).

Paper eq. 73 establishes the not-SUE direction of the negated Sharvit configuration: the implication ¬B(stronger) → ¬B(weaker) does NOT hold under the §5 axioms. Equivalently, there exists a model satisfying MSI/MSO/TECM/BelievingDIV/RumorDIV/WorldLocatedDIV where the agent believes the weaker rumor but not the stronger.

Combined with negated_sharvit_SDE (eq. 72), this pins down the FULL monotonicity profile of the negated configuration: SDE and not SUE — exactly what the NPI licensing condition (paper eq. 21) requires. The contrast between (67a) and (67b) — and hence Sharvit's empirical puzzle — follows.

@[implicit_reducible]

instance Phenomena.Attitudes.Studies.BondarenkoElliott2026.instDecidableEqNotSUESubj : DecidableEq Phenomena.Attitudes.Studies.BondarenkoElliott2026.NotSUESubj✝

Equations

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

theorem Phenomena.Attitudes.Studies.BondarenkoElliott2026.negated_sharvit_not_SUE : ∃ (V : Type) (E : Type) (W : Type) (x : Preorder V) (x_1 : Preorder E) (believe : V → Prop) (HOLDER : V → Option E) (CONT_v : V → Option (Set W)) (CONT_e : E → Option (Set W)) (THEME : V → Option E) (rumor : E → Prop) (located : V → W → Prop) (M : E) (p : Set W) (p' : Set W) (w : W), MSI CONT_v ∧ MSO THEME ∧ TECM believe CONT_v CONT_e THEME ∧ BelievingDIV believe HOLDER ∧ RumorDIV rumor ∧ WorldLocatedDIV located ∧ propLT p' p ∧ BelievesTheRumorThatAt believe HOLDER located THEME rumor CONT_e M p' w ∧ ¬BelievesTheRumorThatAt believe HOLDER located THEME rumor CONT_e M p w

Theorem (paper eq. 73): the negated Sharvit configuration is NOT Strawson Upward-Entailing wrt the embedded restrictor.

There exists a model satisfying all §5 axioms (MSI, MSO, TECM, BelievingDIV, RumorDIV, WorldLocatedDIV) and a pair p, p' with propLT p' p (p' weaker than p) such that the agent believes the rumor that p' (weaker) but does NOT believe the rumor that p (stronger).

Witness: V = Unit, W = Bool; one event with content Set.univ themed to the unique Set.univ-rumor; Set.univ has no proper supersets so MSI is vacuous; the {true}-rumor exists in the lexicon (NotSUESubj.Sr1) but no event has it as theme.

Combined with negated_sharvit_SDE, this gives the FULL monotonicity profile (SDE and not SUE) that the NPI licensing condition (paper eq. 21) requires.

Paper §6.1 introduces a second closure property — closure under conjunction (eq. 76) — that classical Hintikkan modal semantics enjoys but the file's MSI-only account does not derive on its own. The fix adds two principles:

• Summation of contentful entities (eq. 78): CONT(x ⊕ y) = CONT(x) ∩ CONT(y). Paper notes: "Once we assume that an attitude holder's believings are closed under mereological summation, we guarantee that the existence of a believing with content p and a believing with content q guarantees the existence of a believing with content p ∩ q." (eq. 79.)
• Believings closed under summation (implicit in eq. 79.c): the sum of two believings of the same holder is a believing of that holder.

def Phenomena.Attitudes.Studies.BondarenkoElliott2026.CONTSum {V : Type u_1} {W : Type u_3} [SemilatticeSup V] (CONT : V → Option (Set W)) : Prop

Content-of-sum-is-intersection (paper eq. 78). When both summands are contentful, the content of their mereological sum is the intersection of their contents.

Equations

• Phenomena.Attitudes.Studies.BondarenkoElliott2026.CONTSum CONT = ∀ ⦃x y : V⦄ ⦃px py : Set W⦄, CONT x = some px → CONT y = some py → CONT (x ⊔ y) = some (px ∩ py)

def Phenomena.Attitudes.Studies.BondarenkoElliott2026.BelievingsClosedUnderSum {V : Type u_1} {E : Type u_2} [SemilatticeSup V] (believe : V → Prop) (HOLDER : V → Option E) : Prop

Believings closed under summation (implicit in paper eq. 79.c). The mereological sum of two believings of the same holder is itself a believing of that holder.

Equations

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

theorem Phenomena.Attitudes.Studies.BondarenkoElliott2026.believes_closure_under_conjunction {V : Type u_1} {E : Type u_2} {W : Type u_3} [SemilatticeSup V] {believe : V → Prop} {HOLDER : V → Option E} {CONT : V → Option (Set W)} (h_cont_sum : CONTSum CONT) (h_bel_sum : BelievingsClosedUnderSum believe HOLDER) {M : E} {p q : Set W} (h_p : Believes believe HOLDER CONT M p) (h_q : Believes believe HOLDER CONT M q) : Believes believe HOLDER CONT M (p ∩ q)

Theorem (paper eq. 79): closure under conjunction. If the agent believes p and believes q, then under summation closure on contents (eq. 78) and on believings, the agent believes p ∩ q (the propositional conjunction).

Section 6.3 of @cite{bondarenko-elliott-2026} notes that informational parthood via classical entailment (eq. 88) faces the disjunction-introduction problem (eq. 91):

Mitya believes that Jessica married an American philosopher.
↛ Mitya believes that Jessica married a linguist or a philosopher.

even though Jessica married an American philosopher classically entails Jessica married a linguist or a philosopher. The paper proposes Fine's conjunctive parthood (eq. 94, footnote 27) as a refinement.

This is exactly Mereology.IsContentPart (Jago Def 5, re-exported through Theories/Semantics/Truthmaker/Basic.lean). With argument order matching the paper's convention "Q' is conjunctive part of Q", we have:

paper "Q' is conjunctive part of Q" ↔ Mereology.IsContentPart Q Q'

Below we exhibit the paper's witness (eq. 95): with Q = {p₃} ("Jessica married an American linguist") and Q' = {p₁, p₂} ("Jessica married a linguist", "Jessica married a philosopher"), Q' is not a conjunctive part of Q because p₃ ⊄ p₂ ("being an American linguist doesn't entail being a philosopher").

theorem Phenomena.Attitudes.Studies.BondarenkoElliott2026.conjunctive_parthood_blocks_disj_intro {W : Type u_1} (p₁ p₂ p₃ : Set W) (_h_p3_p1 : p₃ ⊆ p₁) (h_not_p3_p2 : ¬p₃ ⊆ p₂) : ¬Mereology.IsContentPart (fun (x : Set W) => x = p₃) {p₁, p₂}

§6.3 discriminating witness (paper eq. 95). Given three propositions p₁ (linguist), p₂ (philosopher), p₃ (American linguist) with the natural entailment relations, the alternative set {p₁, p₂} is NOT a conjunctive part of {p₃} — even though classically {p₃} ⊨ {p₁, p₂} via union.

What fails: the second conjunct of paper eq. 94 ("every p' ∈ Q' has some p ∈ Q with p ⊆ p'"). Take p₂ ∈ Q' = {p₁, p₂}; the only candidate p ∈ Q = {p₃} is p₃ itself, but p₃ ⊆ p₂ is false. The proof is a one-line application of the generic Mereology.not_isContentPart_of_singleton_not_le.

Paper §1 motivates the content-based approach by contrast with the classical Hintikka-style modal semantics: Hintikka's □p ↔ ∀w' accessible, p(w') always closes under classical entailment, whereas the empirical data (paper §1, esp. be surprised that p ∧ q ↛ be surprised that p) shows that some attitude verbs do NOT close.

In the B&E framework, closure under conjunction is contingent on the extra axioms CONTSum + BelievingsClosedUnderSum (paper §6.1). For verbs like be surprised that fail those axioms, B&E correctly predicts non-closure. Hintikka's framework cannot accommodate this.

We make the divergence visible as a Lean theorem: Hintikka always closes under intersection; B&E does not always close (witnessed by a model where CONTSum is violated).

A self-contained hintikkaBox is used here rather than importing Theories/Semantics/Attitudes/Doxastic.boxAt directly — same definition, no transitive deps.

def Phenomena.Attitudes.Studies.BondarenkoElliott2026.hintikkaBox {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) (x : E) (w : W) (worlds : List W) (p : Set W) : Prop

Hintikka-style box modality: p is believed iff every accessible world makes p true. Equivalent to Doxastic.boxAt; defined here self-contained to avoid the heavyweight Doxastic import.

Equations

• Phenomena.Attitudes.Studies.BondarenkoElliott2026.hintikkaBox R x w worlds p = ∀ w' ∈ worlds, R x w w' → w' ∈ p

theorem Phenomena.Attitudes.Studies.BondarenkoElliott2026.hintikkaBox_inter {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) (x : E) (w : W) (worlds : List W) (p q : Set W) : hintikkaBox R x w worlds p → hintikkaBox R x w worlds q → hintikkaBox R x w worlds (p ∩ q)

Hintikka closes under intersection (universal-quantifier distribution). This is the over-closure that B&E §1 argues against on empirical grounds.

theorem Phenomena.Attitudes.Studies.BondarenkoElliott2026.believes_does_not_always_close_under_intersection : ∃ (V : Type) (E : Type) (W : Type) (x : Preorder V) (believe : V → Prop) (HOLDER : V → Option E) (CONT : V → Option (Set W)) (M : E) (p : Set W) (q : Set W), Believes believe HOLDER CONT M p ∧ Believes believe HOLDER CONT M q ∧ ¬Believes believe HOLDER CONT M (p ∩ q)

B&E's Believes does NOT always close under intersection (the headline cross-framework refutation). Witness: a model with two believing-events of the same holder, contents {true} and {false} over Bool-worlds, but no event with content ∅. The contents fail CONTSum; the agent "believes" each disjoint proposition but not their (empty) intersection.

This makes the B&E vs Hintikka clash a Lean theorem rather than a docstring claim.