Content Composition @cite{moulton-2015}

@cite{kratzer-2006} @cite{heim-kratzer-1998} @cite{hintikka-1962}

CPs as predicates of content individuals, not propositions.

The Core Shift

Standard analysis: ⟦that p⟧ = p (type ⟨s,t⟩ — a proposition)

Kratzer/Moulton: ⟦that p⟧ = λx_c. CONT(x_c) = p (type ⟨e,st⟩ — a predicate on content individuals)

The complementizer C identifies a proposition as the content of a content individual using @cite{kratzer-2006}'s CONT function. Attitude verbs select for content individuals (type e), and the that-clause combines via existential closure:

⟦John believes that p⟧ = ∃x_c. believe(John, x_c) ∧ CONT(x_c) = p

Key Consequences

1. Content nouns (belief, claim, rumor) are predicates on content individuals — same type as CPs — so they combine by Predicate Modification
2. That-clauses are NOT arguments of the verb; they are predicates that modify the ∃-closed vP
3. Attitude verb nominalizations are NASNs, not ASNs, because the content individual is ∃-bound (not an external argument)

Cross-Linguistic Variation

• English that-clauses: predicates (type ⟨e,st⟩), combine by PM
• Korean ko-clauses: saturators (type e), function-apply directly
• German dass-clauses: position from V2/cluster, not from CP-as-argument

def Semantics.Attitudes.ContentComposition.compC {W : Type u_1} (p : BProp W) (xc : Core.ContentIndividual W) : Prop

The complementizer C: takes a proposition p and identifies it as the content of a content individual x_c.

⟦C⟧(p)(x_c) ⟺ CONT(x_c) = p

This is @cite{moulton-2015} (15). The result is type ⟨e,st⟩ — a predicate on content individuals — not a proposition ⟨s,t⟩.

Equations

• Semantics.Attitudes.ContentComposition.compC p xc = (xc.cont = p)

@[reducible, inline]

abbrev Semantics.Attitudes.ContentComposition.ContentNoun (W : Type u_1) : Type u_1

A content noun: a world-indexed predicate on content individuals.

Content nouns — belief, claim, rumor, idea, wish — denote properties of content individuals. They are type ⟨e,st⟩, the same semantic type as CPs.

Equations

• Semantics.Attitudes.ContentComposition.ContentNoun W = (Core.ContentIndividual W → W → Prop)

def Semantics.Attitudes.ContentComposition.contentNounCP {W : Type u_1} (noun : ContentNoun W) (p : BProp W) : ContentNoun W

Predicate Modification for content nouns and CPs (@cite{moulton-2015}, (17)).

⟦belief that p⟧ = λx_c.λw. belief(x_c)(w) ∧ CONT(x_c) = p

Because both the content noun and the CP are type ⟨e,st⟩, they combine by intersection.

Equations

• Semantics.Attitudes.ContentComposition.contentNounCP noun p xc w = (noun xc w ∧ Semantics.Attitudes.ContentComposition.compC p xc)

theorem Semantics.Attitudes.ContentComposition.contentNounCP_determines_content {W : Type u_1} (noun : ContentNoun W) (p : BProp W) (xc : Core.ContentIndividual W) (w : W) : contentNounCP noun p xc w → compC p xc

The CP determines the content: if x_c satisfies a content-noun-CP combination, then CONT(x_c) = p.

@[reducible, inline]

abbrev Semantics.Attitudes.ContentComposition.AttitudeVerbCI (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

An attitude verb in the Kratzer/Moulton architecture: relates an agent to a content individual (not to a proposition directly).

believe : λx_c. λx_agent. λw. believe(x_agent, x_c, w)

Equations

• Semantics.Attitudes.ContentComposition.AttitudeVerbCI W E = (E → Core.ContentIndividual W → W → Prop)

def Semantics.Attitudes.ContentComposition.existsContentClosure {W : Type u_1} {E : Type u_2} (verb : AttitudeVerbCI W E) (agent : E) (p : BProp W) (w : W) : Prop

Existential closure over content individuals (@cite{moulton-2015}, (21)–(23)).

Closes off the content individual variable at the edge of vP:

λw. ∃x_c. V(agent, x_c, w) ∧ CONT(x_c) = p

"John believes that p" is true at w iff there exists a content individual x_c such that John stands in the belief relation to x_c at w and the content of x_c is p.

Equations

• Semantics.Attitudes.ContentComposition.existsContentClosure verb agent p w = ∃ (xc : Core.ContentIndividual W), verb agent xc w ∧ Semantics.Attitudes.ContentComposition.compC p xc

def Semantics.Attitudes.ContentComposition.hintikkaVerb {W : Type u_1} {E : Type u_2} (R : E → W → W → Bool) : AttitudeVerbCI W E

An attitude verb derived from a Hintikka accessibility relation.

Given R(agent, w, w'), the verb holds of agent and x_c at w iff x_c's content equals the set of accessible worlds:

V(agent, x_c, w) ⟺ CONT(x_c) = R(agent)(w)

This shows that the classical doxastic semantics is a special case of the content-individual architecture: there is one canonical content individual per agent-world pair, namely ContentIndividual.fromAccessibility R agent w.

Equations

• Semantics.Attitudes.ContentComposition.hintikkaVerb R agent xc w = (xc.cont = R agent w)

theorem Semantics.Attitudes.ContentComposition.hintikka_existsClosure {W : Type u_1} {E : Type u_2} (R : E → W → W → Bool) (a : E) (p : BProp W) (w : W) : existsContentClosure (hintikkaVerb R) a p w ↔ R a w = p

Under a Hintikka verb, identity closure reduces to propositional identity with the accessibility set.

∃x_c[hintikkaVerb(R)(a, x_c, w) ∧ CONT(x_c) = p] ⟺ R(a)(w) = p

The existential is uniquely witnessed by the canonical content individual fromAccessibility R a w.

def Semantics.Attitudes.ContentComposition.existsContentEntails {W : Type u_1} {E : Type u_2} (verb : AttitudeVerbCI W E) (agent : E) (p : BProp W) (w : W) : Prop

Existential closure with entailment instead of identity.

∃x_c. V(agent, x_c, w) ∧ CONT(x_c) ⊆ p

This is the weaker condition: some content individual of the agent's has content that entails p (not necessarily equals p).

Equations

• Semantics.Attitudes.ContentComposition.existsContentEntails verb agent p w = ∃ (xc : Core.ContentIndividual W), verb agent xc w ∧ xc.entails p

theorem Semantics.Attitudes.ContentComposition.existsClosure_implies_entailsClosure {W : Type u_1} {E : Type u_2} (verb : AttitudeVerbCI W E) (agent : E) (p : BProp W) (w : W) : existsContentClosure verb agent p w → existsContentEntails verb agent p w

Identity closure implies entailment closure.

theorem Semantics.Attitudes.ContentComposition.hintikka_entailsClosure {W : Type u_1} {E : Type u_2} (R : E → W → W → Bool) (a : E) (p : BProp W) (w : W) : existsContentEntails (hintikkaVerb R) a p w ↔ ∀ (w' : W), R a w w' = true → p w' = true

Under a Hintikka verb, entailment closure reduces to the standard universal modal — the classical Hintikka semantics.

∃x_c[hintikkaVerb(R)(a, x_c, w) ∧ CONT(x_c) ⊆ p] ⟺ ∀w'. R(a, w, w') = true → p(w') = true

Compare with hintikka_existsClosure (§4), where identity closure reduces to R(a)(w) = p. The two results together make the distinction precise:

Closure mode	Reduces to	Semantic gloss
Identity	R(a)(w) = p	p IS the belief content
Entailment	∀w'. R(a,w,w') → p(w')	p FOLLOWS FROM beliefs

def Semantics.Attitudes.ContentComposition.existsContentNounCP {W : Type u_1} (noun : ContentNoun W) (p : BProp W) (w : W) : Prop

Content-noun existential closure: "a belief that p exists at w".

∃x_c. noun(x_c, w) ∧ CONT(x_c) = p

This is how content DPs like the belief that Fred left or every rumor that p get their denotation: the content noun restricts the domain of content individuals and the CP identifies the content.

Equations

• Semantics.Attitudes.ContentComposition.existsContentNounCP noun p w = ∃ (xc : Core.ContentIndividual W), Semantics.Attitudes.ContentComposition.contentNounCP noun p xc w

def Semantics.Attitudes.ContentComposition.attitudeWithContentNoun {W : Type u_1} {E : Type u_2} (noun : ContentNoun W) (verb : AttitudeVerbCI W E) (agent : E) (p : BProp W) (w : W) : Prop

A full attitude report with a content noun: "John's belief that p" = ∃x_c. belief(x_c, w) ∧ V(John, x_c, w) ∧ CONT(x_c) = p

Equations

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