Doxastic attitude semantics

Accessibility semantics for doxastic attitude verbs (believe, know, think) in Hintikka's tradition: w ~[R x] w' reads "w' is compatible with what x believes or knows in w", and ⟦x believes p⟧(w) is the relational box □[R x] p w, so closure under known implication is the K axiom ModalLogic.box_K.

A DoxasticPredicate pairs an accessibility relation with a veridicality value and a factivity class. Applied to a complement it is a trivalent proposition (DoxasticPredicate.sentence) that presupposes the complement when the predicate is factive and asserts the box, together with the complement when it is veridical. Veridicality is thus an entailment (veridical_entails_complement) and factivity a presupposition, which a context admits only if it entails the complement (support_sentence). Over reflexive accessibility both requirements are redundant by the T axiom (holdsAt_iff_box).

References

• [Hin62]

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

A veridical verb requires its complement p to hold at w, and a non-veridical one requires nothing.

Equations

• Doxastic.VeridicalityHolds Doxastic.Veridicality.veridical p w = p w
• Doxastic.VeridicalityHolds Doxastic.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

• Doxastic.instDecidableVeridicalityHoldsOfDecidablePred Doxastic.Veridicality.veridical p w = Doxastic.instDecidableVeridicalityHoldsOfDecidablePred._aux_1 p w
• Doxastic.instDecidableVeridicalityHoldsOfDecidablePred Doxastic.Veridicality.nonVeridical p w = { decide := true, reflects_decide := ⋯ }

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

A doxastic attitude predicate is an accessibility relation for each attitude holder, with a veridicality value and a factivity class.

• access : E → SetRel W W

  w ~[access x] w' when w' is compatible with the attitude of x in w.

• veridicality : Veridicality

  Whether the predicate entails its complement.

• factivity : Option Presupposition.Factivity

  The factivity class of a predicate that presupposes its complement, none otherwise.

noncomputable def Doxastic.DoxasticPredicate.sentence {W : Type u_1} {E : Type u_2} (V : DoxasticPredicate W E) (agent : E) (p : W → Prop) : W → SignType

Applied to a holder and a complement, the predicate is a trivalent proposition that presupposes the complement if the predicate is factive and asserts the box, together with the complement if it is veridical.

Equations

• V.sentence agent p = {w : W | ∀ x ∈ V.factivity, p w}.indicator fun (w : W) => SignType.ofProp (Doxastic.VeridicalityHolds V.veridicality p w ∧ ModalLogic.Box (V.access agent) p w)

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

⟦x V that p⟧(w) is true when sentence is.

Equations

• V.HoldsAt agent p w = (V.sentence agent p w = 1)

theorem Doxastic.DoxasticPredicate.holdsAt_iff {W : Type u_1} {E : Type u_2} (V : DoxasticPredicate W E) (agent : E) (p : W → Prop) (w : W) : V.HoldsAt agent p w ↔ (∀ x ∈ V.factivity, p w) ∧ VeridicalityHolds V.veridicality p w ∧ ModalLogic.Box (V.access agent) p w

theorem Doxastic.DoxasticPredicate.support_sentence {W : Type u_1} {E : Type u_2} (V : DoxasticPredicate W E) (agent : E) (p : W → Prop) : Function.support (V.sentence agent p) = {w : W | ∀ x ∈ V.factivity, p w}

A factive predicate is defined exactly where its complement is true, and a non-factive one everywhere.

@[instance_reducible]

instance Doxastic.DoxasticPredicate.instDecidableHoldsAtOfFintypeOfMemProdSetRelAccessMkOfDecidablePred {W : Type u_1} {E : Type u_2} (V : DoxasticPredicate W E) (agent : E) (p : W → Prop) (w : W) [Fintype W] [(v : W) → Decidable ((w, v) ∈ V.access agent)] [DecidablePred p] : Decidable (V.HoldsAt agent p w)

Equations

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

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

A veridical predicate entails its complement, so if x knows p at w, then p w.

theorem Doxastic.DoxasticPredicate.holdsAt_iff_box {W : Type u_1} {E : Type u_2} {V : DoxasticPredicate W E} {agent : E} {p : W → Prop} {w : W} [(V.access agent).IsRefl] : V.HoldsAt agent p w ↔ ModalLogic.Box (V.access agent) p w

Over reflexive accessibility the veridicality and factivity requirements are redundant, and the predicate holds exactly when its complement is true at every accessible world.