Doxastic attitude semantics

Accessibility-based semantics for doxastic attitude verbs (believe, know, think) in the tradition of [Hin62]: R x w w' reads "w' is compatible with what x believes/knows in w", and ⟦x believes p⟧(w) is the universal modal over accessible worlds — BoxAt, with DiamondAt its existential dual, both quantifying over a finite worlds list as the decidable rendering.

A DoxasticPredicate bundles the accessibility relation with veridicality and opacity. Its proposition-taking semantics HoldsAt conjoins a veridicality check (VeridicalityHolds: veridical verbs require the complement at the evaluation world, veridical_entails_complement) with the universal modal, and toPartialProp exposes the same content as a Semantics.Presupposition.PartialProp — presupposition = veridicality check, assertion = modal — connecting doxastic verbs to the projection infrastructure. HoldsAtQuestion is the [Kar77b] question-taking semantics: knowing a question is knowing a true answer. believeTemplate/knowTemplate/thinkTemplate are the standard instantiations, and doxastic_k_axiom records closure under known implication.

Opacity: SubstitutionMayFail states that an opaque predicate can distinguish co-extensional complements, and DeDicto/DeRe give the two quantifier construals of an embedded indefinite. psychMode maps veridicality to [Sea83]'s psychological mode: veridical attitudes are perception-like (the world must cause the state), non-veridical ones belief-like.

The presuppositional typology of doxastic verbs ([Gla25]) lives in Studies/Glass2025.lean; the causal derivation of the contrafactive gap ([RO25]) in Studies/RobertsOzyildiz2025.lean; embedded scalar implicature ([GS13]) in Studies/GoodmanStuhlmuller2013.lean.

Accessibility modals

def Doxastic.BoxAt {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) (agent : E) (w : W) (worlds : List W) (p : W → Prop) : Prop

Universal modal: BoxAt R agent w worlds p iff p holds at every accessible world in worlds.

Equations

• Doxastic.BoxAt R agent w worlds p = ∀ w' ∈ worlds, R agent w w' → p w'

def Doxastic.DiamondAt {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) (agent : E) (w : W) (worlds : List W) (p : W → Prop) : Prop

Existential modal: DiamondAt R agent w worlds p iff p holds at some accessible world in worlds.

Equations

• Doxastic.DiamondAt R agent w worlds p = ∃ w' ∈ worlds, R agent w w' ∧ p w'

@[instance_reducible]

instance Doxastic.instDecidableBoxAtOfDecidablePred {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) [(a : E) → (w w' : W) → Decidable (R a w w')] (agent : E) (w : W) (worlds : List W) (p : W → Prop) [DecidablePred p] : Decidable (BoxAt R agent w worlds p)

Equations

• Doxastic.instDecidableBoxAtOfDecidablePred R agent w worlds p = Doxastic.instDecidableBoxAtOfDecidablePred._aux_1 R agent w worlds p

@[instance_reducible]

instance Doxastic.instDecidableDiamondAtOfDecidablePred {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) [(a : E) → (w w' : W) → Decidable (R a w w')] (agent : E) (w : W) (worlds : List W) (p : W → Prop) [DecidablePred p] : Decidable (DiamondAt R agent w worlds p)

Equations

• Doxastic.instDecidableDiamondAtOfDecidablePred R agent w worlds p = Doxastic.instDecidableDiamondAtOfDecidablePred._aux_1 R agent w worlds p

theorem Doxastic.doxastic_k_axiom {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) (agent : E) (p q : W → Prop) (w : W) (worlds : List W) (hp : BoxAt R agent w worlds p) (hpq : BoxAt R agent w worlds fun (w' : W) => p w' → q w') : BoxAt R agent w worlds q

Closure under known implication — the K axiom: if the agent believes p and believes p → q, the agent believes q.

Doxastic predicates

def Doxastic.VeridicalityHolds {W : Type u_1} (v : Veridicality) (p : W → Prop) (w : W) : Prop

VeridicalityHolds v p w is the veridicality check: veridical verbs require p w; non-veridical verbs require nothing.

Equations

• Doxastic.VeridicalityHolds Features.Veridicality.veridical p w = p w
• Doxastic.VeridicalityHolds Features.Veridicality.nonVeridical p w = True

@[instance_reducible]

instance Doxastic.instDecidableVeridicalityHoldsOfDecidablePred {W : Type u_1} (v : Veridicality) (p : W → Prop) [DecidablePred p] (w : W) : Decidable (VeridicalityHolds v p w)

Equations

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

structure Doxastic.DoxasticPredicate (W : Type u_3) (E : Type u_4) : Type (max u_3 u_4)

A doxastic attitude predicate: an accessibility relation bundled with veridicality and opacity.

• name : String

  Name of the predicate.

• access : E → W → W → Prop

  Accessibility relation.

• veridicality : Veridicality

  Veridicality (veridical or not).

• createsOpaqueContext : Bool

  Does it create an opaque context (substitution failures)?

def Doxastic.DoxasticPredicate.HoldsAt {W : Type u_1} {E : Type u_2} (V : DoxasticPredicate W E) (agent : E) (p : W → Prop) (w : W) (worlds : List W) : Prop

V.HoldsAt agent p w worlds iff the veridicality check passes at w and p holds at every accessible world: ⟦x V that p⟧(w) = VeridicalityHolds ∧ BoxAt.

Equations

• V.HoldsAt agent p w worlds = (Doxastic.VeridicalityHolds V.veridicality p w ∧ Doxastic.BoxAt V.access agent w worlds p)

@[instance_reducible]

instance Doxastic.instDecidableHoldsAtOfAccessOfDecidablePred {W : Type u_1} {E : Type u_2} (V : DoxasticPredicate W E) [(a : E) → (w w' : W) → Decidable (V.access a w w')] (agent : E) (p : W → Prop) [DecidablePred p] (w : W) (worlds : List W) : Decidable (V.HoldsAt agent p w worlds)

Equations

• Doxastic.instDecidableHoldsAtOfAccessOfDecidablePred V agent p w worlds = Doxastic.instDecidableHoldsAtOfAccessOfDecidablePred._aux_1 V agent p w worlds

theorem Doxastic.veridical_entails_complement {W : Type u_1} {E : Type u_2} (V : DoxasticPredicate W E) (hV : V.veridicality = Features.Veridicality.veridical) (agent : E) (p : W → Prop) (w : W) (worlds : List W) (holds : V.HoldsAt agent p w worlds) : p w

Veridical predicates entail their complement: if x knows p at w, then p w.

def Doxastic.DoxasticPredicate.toPartialProp {W : Type u_1} {E : Type u_2} (V : DoxasticPredicate W E) (agent : E) (p : W → Prop) (worlds : List W) : Semantics.Presupposition.PartialProp W

The predicate application as a PartialProp: presupposition = veridicality check, assertion = universal modal. HoldsAt is the conjunction of the two fields.

Equations

• V.toPartialProp agent p worlds = { presup := fun (w : W) => Doxastic.VeridicalityHolds V.veridicality p w, assertion := fun (w : W) => Doxastic.BoxAt V.access agent w worlds p }

def Doxastic.DoxasticPredicate.HoldsAtQuestion {W : Type u_1} {E : Type u_2} (V : DoxasticPredicate W E) (agent : E) (Q : (W → Prop) → Prop) (w : W) (worlds : List W) (answers : List (W → Prop)) : Prop

HoldsAtQuestion: the [Kar77b] question-taking semantics — ⟦x knows Q⟧(w) = some true answer in Q is known (for non-veridical predicates the truth requirement is dropped).

Equations

• V.HoldsAtQuestion agent Q w worlds answers = ∃ p ∈ answers, Q p ∧ Doxastic.VeridicalityHolds V.veridicality p w ∧ Doxastic.BoxAt V.access agent w worlds p

Standard templates

def Doxastic.believeTemplate {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) : DoxasticPredicate W E

Abstract believe: non-veridical, opaque.

Equations

• Doxastic.believeTemplate R = { name := "believe", access := R, veridicality := Features.Veridicality.nonVeridical }

def Doxastic.knowTemplate {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) : DoxasticPredicate W E

Abstract know: veridical, opaque.

Equations

• Doxastic.knowTemplate R = { name := "know", access := R, veridicality := Features.Veridicality.veridical }

def Doxastic.thinkTemplate {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) : DoxasticPredicate W E

Abstract think: non-veridical, opaque.

Equations

• Doxastic.thinkTemplate R = { name := "think", access := R, veridicality := Features.Veridicality.nonVeridical }

Opacity and construals

def Doxastic.SubstitutionMayFail {W : Type u_1} {E : Type u_2} (V : DoxasticPredicate W E) : Prop

An opaque predicate can distinguish co-extensional complements: some p, q agree at w but embed differently.

Equations

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

def Doxastic.DeRe {W : Type u_1} {E : Type u_2} {D : Type u_3} (V : DoxasticPredicate W E) (agent : E) (predicate : D → W → Prop) (domain : List D) (w : W) (worlds : List W) : Prop

De re construal: the quantifier scopes over the attitude — some individual in the domain is believed to satisfy the predicate. The de dicto construal, with the quantifier under the attitude, is HoldsAt applied to the existential complement.

Equations

• Doxastic.DeRe V agent predicate domain w worlds = ∃ x ∈ domain, V.HoldsAt agent (predicate x) w worlds

Psychological mode

def Doxastic.psychMode : Veridicality → PsychMode

[Sea83]'s psychological mode from veridicality: veridical attitudes are perception-like (the world must cause the state); non-veridical attitudes are belief-like (satisfaction requires only that the content match reality).

Equations

• Doxastic.psychMode Features.Veridicality.veridical = PsychMode.perception
• Doxastic.psychMode Features.Veridicality.nonVeridical = PsychMode.belief