Bondarenko and Elliott (2026): Monotonicity via mereology in the semantics of attitude reports

[Sha24]'s puzzle: a weak NPI is licensed in the relative clause of Katya doesn't believe the rumor that Anton has ever spread but not in the complement clause of Katya doesn't believe the rumor that Anton has ever snowboarded. Weak NPIs need an environment that is Strawson downward- and not Strawson upward-entailing. Under the content-based approach to clausal embedding, subset semantics for the that-clause makes the singular definite both, by uniqueness collapse, while equality semantics (CONT x = ⟦S⟧) makes it neither, by functionality. [BE26] keep equality semantics and add mereological structure to attitudinal eventualities and their contents, with informational parthood p' ≤ p iff p ⊆ p': the content function reflects proper parthood (MSI), the theme function preserves it (MSO), a believing has the content of its theme (TECM), and parts of believings are believings of the same holder (BelievingDIV).

MSI alone closes belief under entailment (believes_of_ssubset, not_believes_of_ssubset). For Katya believes the rumor that p, the chain TECM ∘ MSI ∘ BelievingDIV ∘ MSO closes the positive sentence under weakening of the rumor's content (believesTheRumorThat_of_ssubset), so its negation is Strawson downward-entailing in the restrictor (not_believesTheRumorThat_of_ssubset), while a model in which the agent believes the weaker rumor but not the stronger shows that the negation is not Strawson upward-entailing (negated_not_sue) — the profile the licensing condition demands. Closure under conjunction needs two further principles, that the content of a sum is the intersection of the contents and that one holder's believings are closed under sum (believes_inter); without them belief need not close (not_believes_inter). Finally, the paper's refinement of informational parthood to Fine's conjunctive parthood on alternative sets is Truthmaker.IsConjunctivePart, with alternatives ordered informationally in (Set W)ᵒᵈ. Between single alternatives it is entailment (isConjunctivePart_singleton_iff_subset), and its witness that disjunction introduction fails — Jessica married an American linguist does not make Jessica married a linguist or a philosopher a conjunctive part — is not_isConjunctivePart_disjunction.

References

• [BE26]
• [Che73]
• [Sha24]

Constraints on the lexical maps

The content, theme and holder maps are partial, so they return Option; a content is a set of worlds, and p ⊂ p' says p' is informationally a proper part of p.

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

The content map maps to sub-parts of the input when every proper informational part of a content is the content of a proper part of its bearer.

Equations

• BondarenkoElliott2026.MSI CONT = ∀ ⦃x : V⦄ ⦃p p' : Set W⦄, CONT x = some p → p ⊂ p' → ∃ x' < x, CONT x' = some p'

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

The theme map maps to sub-parts of the output when every proper part of an eventuality has a theme that is a proper part of the eventuality's theme.

Equations

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

def 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

A predicate P of eventualities satisfies theme-event content matching when every P-eventuality has the content of its theme.

Equations

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

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

Parts of a believing are believings of the same holder — divisive reference ([Che73]) for attitudinal eventualities.

• div : Mereology.DIV believe
• holder ⦃e e' : V⦄ ⦃M : E⦄ : HOLDER e = some M → e' ≤ e → HOLDER e' = some M

def BondarenkoElliott2026.LocatedDIV {V : Type u_1} {W : Type u_3} [Preorder V] (located : V → W → Prop) : Prop

Location at a world is inherited by parts, as worlds are maximal eventualities.

Equations

• BondarenkoElliott2026.LocatedDIV located = ∀ ⦃e e' : V⦄ ⦃w : W⦄, e' ≤ e → located e w → located e' w

Belief and closure under entailment

def 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 M believes p: a believing of M with content p.

Equations

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

theorem BondarenkoElliott2026.believes_of_ssubset {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)} {M : E} {p p' : Set W} (hMSI : MSI CONT) (hDIV : BelievingDIV believe HOLDER) (hlt : p ⊂ p') (h : Believes believe HOLDER CONT M p) : Believes believe HOLDER CONT M p'

Belief is closed under informational weakening.

theorem BondarenkoElliott2026.not_believes_of_ssubset {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)} {M : E} {p p' : Set W} (hMSI : MSI CONT) (hDIV : BelievingDIV believe HOLDER) (hlt : p ⊂ p') (h : ¬Believes believe HOLDER CONT M p') : ¬Believes believe HOLDER CONT M p

Negated belief is downward-entailing in its content.

The Sharvit configuration: believes the rumor that p

def BondarenkoElliott2026.BelievesTheRumorThat {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 M believes the rumor that p at world w: a believing of M located at w whose theme is a rumor with content p.

Equations

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

theorem BondarenkoElliott2026.believesTheRumorThat_of_ssubset {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} {M : E} {p p' : Set W} {w : W} (hMSI : MSI CONT_v) (hMSO : MSO THEME) (hTECM : TECM believe CONT_v CONT_e THEME) (hDIV : BelievingDIV believe HOLDER) (hRumor : Mereology.DIV rumor) (hLoc : LocatedDIV located) (hlt : p ⊂ p') (h : BelievesTheRumorThat believe HOLDER located THEME rumor CONT_e M p w) : BelievesTheRumorThat believe HOLDER located THEME rumor CONT_e M p' w

The positive sentence is closed under weakening of the rumor's content. The believing's content is its theme's (TECM), which has a part with the weaker content (MSI) that is a located believing of the same holder (BelievingDIV) themed to a part of the rumor (MSO), which is a rumor with that content (TECM again).

theorem BondarenkoElliott2026.not_believesTheRumorThat_of_ssubset {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} {M : E} {p p' : Set W} {w : W} (hMSI : MSI CONT_v) (hMSO : MSO THEME) (hTECM : TECM believe CONT_v CONT_e THEME) (hDIV : BelievingDIV believe HOLDER) (hRumor : Mereology.DIV rumor) (hLoc : LocatedDIV located) (hlt : p ⊂ p') (h : ¬BelievesTheRumorThat believe HOLDER located THEME rumor CONT_e M p' w) : ¬BelievesTheRumorThat believe HOLDER located THEME rumor CONT_e M p w

The negated sentence is Strawson downward-entailing in the rumor's content — the direction that licenses Katya doesn't believe the rumor that Anton has ever snowboarded.

theorem BondarenkoElliott2026.negated_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 ∧ Mereology.DIV rumor ∧ LocatedDIV located ∧ p ⊂ p' ∧ BelievesTheRumorThat believe HOLDER located THEME rumor CONT_e M p' w ∧ ¬BelievesTheRumorThat believe HOLDER located THEME rumor CONT_e M p w

The negated sentence is not Strawson upward-entailing. Some model satisfying all of the constraints has Katya believe the weaker rumor (content Set.univ) but not the stronger one (content {true}). Functionality of the content map, not the mereological constraints, is what blocks the inference.

Closure under conjunction

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

The content of a sum of contentful entities is the intersection of their contents.

Equations

• 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 BondarenkoElliott2026.SumClosed {V : Type u_1} {E : Type u_2} [SemilatticeSup V] (believe : V → Prop) (HOLDER : V → Option E) : Prop

One holder's believings are closed under sum.

Equations

• BondarenkoElliott2026.SumClosed believe HOLDER = ∀ ⦃e e' : V⦄ ⦃M : E⦄, believe e → believe e' → HOLDER e = some M → HOLDER e' = some M → believe (e ⊔ e') ∧ HOLDER (e ⊔ e') = some M

theorem BondarenkoElliott2026.believes_inter {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)} (hCONT : CONTSum CONT) (hSum : SumClosed believe HOLDER) {M : E} {p q : Set W} (hp : Believes believe HOLDER CONT M p) (hq : Believes believe HOLDER CONT M q) : Believes believe HOLDER CONT M (p ∩ q)

Belief is closed under conjunction given CONTSum and SumClosed.

theorem BondarenkoElliott2026.not_believes_inter : ∃ (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)

Without those principles belief need not close under conjunction, as an agent may have believings of content {true} and {false} and none of content ∅.

Conjunctive parthood

Alternatives are ordered informationally, so toDual p ≤ toDual p' in (Set W)ᵒᵈ when p' ⊆ p.

theorem BondarenkoElliott2026.isConjunctivePart_singleton_iff_subset {W : Type u_3} (p q : Set W) : Truthmaker.IsConjunctivePart {OrderDual.toDual q} {OrderDual.toDual p} ↔ p ⊆ q

Between single alternatives conjunctive parthood is entailment. It's raining is a conjunctive part of it's raining heavily, since raining heavily entails raining.

theorem BondarenkoElliott2026.not_isConjunctivePart_disjunction {W : Type u_3} (p₁ p₂ p₃ : Set W) (h : ¬p₃ ⊆ p₂) : ¬Truthmaker.IsConjunctivePart {OrderDual.toDual p₁, OrderDual.toDual p₂} {OrderDual.toDual p₃}

Disjunction introduction fails for conjunctive parthood. With p₃ Jessica married an American linguist, p₁ a linguist and p₂ a philosopher, the alternative set {p₁, p₂} is not a conjunctive part of {p₃}, since p₃ does not entail p₂.