Clauses as predicates of anchors

On the standard analysis a that-clause denotes a proposition. On the projection analysis of Hacquard and Kratzer, a clause instead denotes a predicate of anchors, individuals from which a propositional domain is projected: the complementizer identifies the clause's proposition with the projection of the anchor. Content individuals, such as beliefs and claims, project their content; situation individuals, such as cases and circumstances, project the situations they refer to. The two sorts are distinct types, so that a verb's selection of content or situation clauses, as in Greek oti against pu, is type selection, while the compositional machinery is shared. An anchor noun combines with a clause by predicate modification, and a clause-selecting verb takes the anchor as an argument that existential closure binds. With Moulton's doxastic verb, which requires every accessible index to project from the anchor, the closed report is Hintikka's universal modal whenever every proposition is the projection of some anchor.

Main definitions

• Anchor: a sort of anchors with its projection.
• Anchor.comp, Anchor.nounComp, Anchor.existsClosure: the complementizer, predicate modification of an anchor noun, and existential closure of a verb's anchor argument.
• Anchor.ofAccessibility: Moulton's doxastic verb.
• ContentIndividual, SituationIndividual: the two sorts of anchors.

Main statements

• Anchor.existsClosure_ofAccessibility: with a surjective projection, an existentially closed report with Moulton's verb is the universal modal.
• ContentIndividual.eq_implies_entails, ContentIndividual.entails_not_implies_eq: identity of content, Kratzer's and Moulton's relation, is strictly stronger than entailment, Hintikka's.

Implementation notes

A content individual has its content as its only field, so two individuals with the same content are identified; the difference between my belief that p and yours is not captured. Kratzer's shape, an atom with a content at each world, would capture it once a study needs the distinction. The situation sort carries no parthood order, so consumers choose their own situation type.

References

• [Hac06]
• [Kra06]
• [Kra13]
• [Mou15]
• [Bon22]
• [Mol21]
• [Ang26]
• [HK98]
• [Hin62]
• [Kra89]
• [Lie24]
• [Mol19]
• [Mol24]

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

An anchor sort is a type of individuals each of which projects a propositional domain over the indices I.

• proj : α → I → Prop

  proj x is the domain the anchor x projects.

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

The complementizer holds of an anchor whose projection is the clause's proposition.

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

An anchor noun combines with a clause by predicate modification.

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 at the edge of the verb phrase binds the anchor argument of a clause-selecting verb.

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 → SetRel I I) : E → α → I → Prop

Moulton's doxastic verb relates the agent to an anchor at i when every index accessible from i lies in the anchor's projection.

Equations

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

theorem Anchor.existsClosure_ofAccessibility {α : Type u_1} {I : Type u_2} {E : Type u_3} [Anchor α I] (R : E → SetRel I I) (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 Moulton's doxastic verb is Hintikka's universal modal.

Content individuals

A content individual is a mental state or speech act with propositional content, the denotation of content nominals such as John's belief that p, the claim or every rumor. Beliefs, desires and percepts share the sort; what distinguishes them is the attitude relation that embeds them [Lie24].

structure ContentIndividual (W : Type u_1) : Type u_1

A content individual carries a propositional content.

• cont : W → Prop

  The content of the individual.

@[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, so the projection is surjective.

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

A content individual entails p when every world of its content is a p-world.

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

Identity of content implies entailment.

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

Entailment does not imply identity of content, since empty content entails every proposition.

Situation individuals

A situation individual refers to situations in Kratzer's sense [Kra89], the denotation of situation nominals such as the case that the father is absent. Bondarenko observes that verbs selecting content clauses, such as say and believe, reject situation clauses, and verbs selecting situation clauses, such as regret, reject content clauses [Bon22]; see also [Mol19] and [Mol24].

structure SituationIndividual (S : Type u_1) : Type u_1

A situation individual refers to a set of situations.

• sit : S → Prop

  The situations the individual refers to.

@[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 that of some individual, so the projection is surjective.