Content Individuals (@cite{kratzer-2006}; @cite{liefke-2024} §4.3) @cite{kratzer-2006}

@cite{baker-jara-ettinger-saxe-tenenbaum-2017} @cite{liefke-2024} @cite{moulton-2015} @cite{hintikka-1962} @cite{hintikka-1962}

A content individual is a first-class mental state carrying propositional content — the denotation of content DPs like John's belief that p, the claim, every rumor, her wish.

Ontological Status

Content individuals are the shared sort underlying beliefs, desires, and percepts (@cite{liefke-2024} §4.3). What distinguishes a belief from a desire or a percept is not the ontological sort — it is the attitude relation (the verb) that embeds it.

In BToM, these correspond to the type parameters over which the observer's posterior is defined. In memo, they are the frames created by thinks[...].

Identity vs. Entailment

Two ways to relate a content individual x_c to a proposition p:

Relation	Definition	Gloss	Source
Identity	CONT(x_c) = p	p IS the content	@cite{kratzer-2006}
Entailment	CONT(x_c) ⊆ p	p FOLLOWS from content	@cite{hintikka-1962}

Identity is strictly stronger (§3 below).

structure Core.ContentIndividual (W : Type u_1) : Type u_1

A content individual: a first-class mental state carrying propositional content.

This is @cite{kratzer-2006}'s content individual — the denotation of content DPs like John's belief that p, the claim, every rumor, her wish. It is the shared ontological sort underlying beliefs, desires, and percepts (@cite{liefke-2024} §4.3), and the frame created by thinks[...] in memo.

The cont field is Kratzer's CONT function: the propositional content this mental state carries. Two distinct content individuals can share the same content (my belief that p ≠ your belief that p).

• cont : BProp W

  Propositional content: CONT(c)

def Core.ContentIndividual.fromAccessibility {W : Type u_1} {E : Type u_2} (R : E → W → W → Bool) (agent : E) (w : W) : ContentIndividual W

Construct a content individual from a Hintikka-style accessibility relation. Given agent a at world w, the content is the set of accessible worlds.

This shows that the classical doxastic semantics is a special case: a single deterministic content individual whose CONT is λw'. R(a, w, w'). Works for doxastic (believe), bouletic (want), and perceptual (see) accessibility alike — the sort is the same.

Equations

• Core.ContentIndividual.fromAccessibility R agent w = { cont := R agent w }

def Core.ContentIndividual.trueAt {W : Type u_1} (c : ContentIndividual W) (w : W) : Bool

A content individual is true at a world iff its content holds there.

Equations

• c.trueAt w = c.cont w

def Core.ContentIndividual.sameContent {W : Type u_1} (c₁ c₂ : ContentIndividual W) : Prop

Two content individuals have the same content.

Equations

• c₁.sameContent c₂ = (c₁.cont = c₂.cont)

def Core.ContentIndividual.entails {W : Type u_1} (xc : ContentIndividual W) (p : BProp W) : Prop

Content entailment: the content of x_c entails proposition p (CONT ⊆ p).

Every world where the content holds, p also holds: ∀w. CONT(x_c)(w) = true → p(w) = true

This is the Hintikka reading of attitude reports: "x believes that p" means p follows from x's belief content. @cite{kratzer-2006} and @cite{moulton-2015} use the stronger notion of content identity (CONT = p).

Equations

• xc.entails p = ∀ (w : W), xc.cont w = true → p w = true

theorem Core.ContentIndividual.eq_implies_entails {W : Type u_1} (xc : ContentIndividual W) (p : BProp W) : xc.cont = p → xc.entails p

Content identity implies content entailment: CONT(x_c) = p → CONT(x_c) ⊆ p.

theorem Core.ContentIndividual.entails_not_implies_eq : ¬∀ (p : BProp Bool) (xc : ContentIndividual Bool), xc.entails p → xc.cont = p

Content entailment does not imply content identity.

Counterexample: empty content (λ_ => false) entails any proposition p, but CONT ≠ p when p is nonempty.

This is the key semantic distinction:

• Hintikka: "John believes that p" ⟺ p follows from John's beliefs
• Kratzer/Moulton: "John believes that p" ⟺ p IS John's belief content