Clauses as predicates of anchors

Embedded clauses as predicates of anchors — individuals from which a propositional domain is projected ([Hac06]; [Kra06]). On the standard analysis a that-clause denotes a proposition, ⟦that p⟧ = p. On the projection analysis the complementizer instead identifies p as the projection of an anchor individual, so a clause denotes a predicate of anchors. The Anchor class carries the mode of projection: CONT for content individuals ([Kra06]; [Kra13]; [Mou15]), SIT for situation individuals ([Bon22]; [Mol21]). The sorts stay distinct types, so sort-sensitive selection — content verbs rejecting situation clauses and vice versa, Greek oti vs pu ([Ang26]) — is type selection; the compositional machinery below is shared.

Because anchor nouns (belief, claim; situation, case) denote predicates of anchors of the same semantic type as clauses, noun and clause combine by predicate modification ([HK98]) rather than function application: nounComp. Clause-selecting verbs take the anchor as an argument, which existential closure binds at the edge of vP (existsClosure). With [Mou15]'s doxastic verb, which requires every accessible index to be a projection index (ofAccessibility), the closed report is the classical universal modal (existsClosure_ofAccessibility): the semantics of [Hin62] is a special case of the anchor architecture whenever the projection is surjective.

class Anchor (α : Type u_1) (I : outParam (Type u_2)) : Type (max u_1 u_2)

An anchor sort: individuals from which a propositional domain is projected. proj x is the projection of the anchor x — CONT for content individuals, SIT for situation individuals.

• proj : α → I → Prop

  The mode of projection: the domain an anchor projects.

def Anchor.comp {α : Type u_1} {I : Type u_2} [Anchor α I] (q : I → Prop) (x : α) : Prop

The complementizer identifies a clause with the anchor's projection: comp q x iff proj x = q.

Equations

• Anchor.comp q x = (Anchor.proj x = q)

def Anchor.nounComp {α : Type u_1} {I : Type u_2} [Anchor α I] (noun : α → I → Prop) (q : I → Prop) : α → I → Prop

Predicate modification of an anchor noun with a clause: nounComp noun q x i iff noun x i ∧ proj x = q.

Equations

• Anchor.nounComp noun q x i = (noun x i ∧ Anchor.comp q x)

def Anchor.existsClosure {α : Type u_1} {I : Type u_2} {E : Type u_3} [Anchor α I] (verb : E → α → I → Prop) (agent : E) (q : I → Prop) (i : I) : Prop

Existential closure over the anchor argument of a clause-selecting verb at the edge of vP: existsClosure V a q i iff ∃ x, V a x i ∧ proj x = q.

Equations

• Anchor.existsClosure verb agent q i = ∃ (x : α), verb agent x i ∧ Anchor.comp q x

def Anchor.ofAccessibility {α : Type u_1} {I : Type u_2} {E : Type u_3} [Anchor α I] (R : E → I → I → Prop) : E → α → I → Prop

The doxastic clause-selecting verb of [Mou15]: the agent is related to x at i iff every index accessible from i is a projection index of x (Dox ⊆ proj).

Equations

• Anchor.ofAccessibility R agent x i = ∀ (i' : I), R agent i i' → Anchor.proj x i'

theorem Anchor.existsClosure_ofAccessibility {α : Type u_1} {I : Type u_2} {E : Type u_3} [Anchor α I] (R : E → I → I → Prop) (a : E) (q : I → Prop) (i : I) (hp : Function.Surjective proj) : existsClosure (ofAccessibility R) a q i ↔ ModalLogic.box (R a) q i

For a surjective projection, an existentially closed report with the accessibility-based verb is the classical universal modal of [Hin62].

Content individuals

A content individual is a first-class mental state carrying propositional content — [Kra06]'s denotation for content DPs like John's belief that p, the claim, every rumor, her wish. Content individuals are the shared ontological sort underlying beliefs, desires, and percepts ([Lie24]); what distinguishes a belief from a desire or a percept is not the sort but the attitude relation that embeds it. In Bayesian theory-of-mind models ([BJEST17], Pragmatics/BToM.lean) they correspond to the type parameters over which the observer's posterior is defined.

Content individuals are the content-mode instance of the Anchor class: the projection is CONT, so Anchor.comp is the that-complementizer of [Kra06] and [Mou15] and Anchor.existsClosure composes attitude reports. cont_surjective — every proposition is the content of some individual — makes Anchor.existsClosure_ofAccessibility applicable, recovering the classical doxastic semantics of [Hin62].

Two ways to relate a content individual x_c to a proposition p: identity, CONT(x_c) = p, the notion of [Kra06] and [Mou15] (p is the content, Anchor.comp); and entailment, CONT(x_c) ⊆ p, the notion of [Hin62] (p follows from the content, entails). Identity is strictly stronger: eq_implies_entails and the counterexample entails_not_implies_eq.

structure ContentIndividual (W : Type u_1) : Type u_1

A content individual: a first-class mental state carrying propositional content. The cont field is [Kra06]'s CONT function.

Caveat: because cont is the only field, this formalization identifies individuals with their contents — the intuition "my belief that p ≠ your belief that p" is NOT captured. A Kratzerian atom-plus-model shape (cont : E → W → (W → Prop)) would capture it, deferred until a study states an identity-vs-content theorem.

• cont : W → Prop

  Propositional content: CONT(c)

@[reducible, inline]

abbrev ContentVerb (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A content-selecting verb (say, believe) relates an agent to a content individual at a world — the content-sort sibling of SituationVerb.

Equations

• ContentVerb W E = (E → ContentIndividual W → W → Prop)

@[instance_reducible]

instance ContentIndividual.instAnchor {W : Type u_1} : Anchor (ContentIndividual W) W

Equations

• ContentIndividual.instAnchor = { proj := ContentIndividual.cont }

theorem ContentIndividual.cont_surjective {W : Type u_1} : Function.Surjective cont

Every proposition is the content of some individual — the belief that p — so the content-mode projection is surjective.

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

Content entailment: xc.entails p iff every content world of xc is a p-world (CONT ⊆ p) — the reading of attitude reports in [Hin62], where [Kra06] and [Mou15] use content identity.

Equations

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

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

Content identity implies content entailment.

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

Content entailment does not imply content identity: empty content entails every proposition.

Situation individuals

A situation individual is a first-class entity referring to a situation — the denotation of situation DPs like the case that the father is absent. Where content nouns (belief, claim, rumor) range over content individuals in the sense of [Kra06], situation nouns (situation, case, circumstance, event) range over situations in the sense of [Kra89] — partial points of evaluation ordered by parthood. The empirical motivation for the dual sort is [Bon22]'s observation that situation-denoting clauses show selectional behaviour distinct from content-denoting clauses (see also [Mol19], [Mol21], [Mol24]): verbs that select content (say, believe) reject situation-denoting clauses, and verbs that select situations (be happy that, regret that) reject content-denoting clauses. The two sorts are coordinate, not subordinate, and each instantiates Anchor — situation individuals with SIT as the projection, so Anchor.comp is the situation-clause complementizer and Anchor.existsClosure composes situation reports.

In Modern Greek, oti-clauses denote content and combine with content-selecting verbs; pu-clauses denote situations and combine with situation-selecting verbs ([Ang26], following [Bon22]). The same cut appears with other exponents (Korean -ko vs -num kes, Japanese to vs koto); the mapping is language-specific and not assumed here.

structure SituationIndividual (S : Type u_1) : Type u_1

A situation individual: a first-class entity referring to a situation, the situation-sort sibling of ContentIndividual. The sit field is the situation predicate SIT: the set of situations the entity refers to. The situation-index sort S is typically a Intensional.SituationFrame.Index carrying a parthood preorder, but no order is required here, so downstream consumers can specialize freely.

• sit : S → Prop

  Situation predicate: SIT(s_i)

@[reducible, inline]

abbrev SituationVerb (S : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A situation-selecting verb (be happy that, regret) relates an agent to a situation individual at a situation — the situation-sort sibling of ContentVerb.

Equations

• SituationVerb S E = (E → SituationIndividual S → S → Prop)

@[instance_reducible]

instance instAnchorSituationIndividual {S : Type u_1} : Anchor (SituationIndividual S) S

Equations

• instAnchorSituationIndividual = { proj := SituationIndividual.sit }

theorem SituationIndividual.sit_surjective {S : Type u_1} : Function.Surjective sit

Every situation predicate is the SIT of some individual, so the situation-mode projection is surjective — the situation-sort analogue of ContentIndividual.cont_surjective, making Anchor.existsClosure_ofAccessibility applicable to situation reports.