@[reducible, inline]

abbrev Semantics.Attitudes.Doxastic.AccessRel (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

Doxastic accessibility relation type (Prop-valued, mathlib convention).

R agent evalWorld accessibleWorld holds iff accessibleWorld is compatible with what agent believes/knows in evalWorld. For computational evaluation add [DecidableRel (R agent)] instances at use sites.

Equations

• Semantics.Attitudes.Doxastic.AccessRel W E = (E → W → W → Prop)

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

Universal modal: holds at w iff p holds at all accessible worlds.

⟦□p⟧(w) = ∀w' ∈ worlds. R(agent, w, w') → p(w')

Equations

• Semantics.Attitudes.Doxastic.boxAt R agent w worlds p = ∀ w' ∈ worlds, R agent w w' → p w'

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

Existential modal: holds at w iff p holds at some accessible world.

⟦◇p⟧(w) = ∃w' ∈ worlds. R(agent, w, w') ∧ p(w')

Equations

• Semantics.Attitudes.Doxastic.diaAt R agent w worlds p = ∃ w' ∈ worlds, R agent w w' ∧ p w'

@[implicit_reducible]

instance Semantics.Attitudes.Doxastic.boxAt_decidable {W : Type u_1} {E : Type u_2} (R : AccessRel W E) [(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

• Semantics.Attitudes.Doxastic.boxAt_decidable R agent w worlds p = Semantics.Attitudes.Doxastic.boxAt_decidable._aux_1 R agent w worlds p

@[implicit_reducible]

instance Semantics.Attitudes.Doxastic.diaAt_decidable {W : Type u_1} {E : Type u_2} (R : AccessRel W E) [(a : E) → (w w' : W) → Decidable (R a w w')] (agent : E) (w : W) (worlds : List W) (p : W → Prop) [DecidablePred p] : Decidable (diaAt R agent w worlds p)

Equations

• Semantics.Attitudes.Doxastic.diaAt_decidable R agent w worlds p = Semantics.Attitudes.Doxastic.diaAt_decidable._aux_1 R agent w worlds p

Presuppositional Classification of Doxastic Verbs

@cite{glass-2025} proposes a typology of belief verbs based on their presuppositional profile — what they require of the Common Ground:

• Factive (know): presupposes p — CG must entail p
• Nonfactive (think): no presupposition — no CG requirement
• Contrafactive (hypothetical contra): would presuppose ¬p — UNATTESTED
• Weak contrafactive (Mandarin yǐwéi): postsupposition ◇¬p — CG compatible with ¬p

The key insight: this classification is DERIVED from the PrProp produced by DoxasticPredicate.toPrProp, not stipulated as a separate type. The presup field of the PrProp determines the classification.

Postsuppositions (yǐwéi's ◇¬p) are output-context constraints, formalized separately in Core.Postsupposition.

inductive Semantics.Attitudes.Doxastic.PresupClass : Type

Classification of a doxastic verb's presuppositional profile.

This emerges from the presup field of the PrProp produced by DoxasticPredicate.toPrProp. Not a primitive — a derived label.

• factive : PresupClass
• contrafactive : PresupClass
• nonfactive : PresupClass
• other : PresupClass

@[implicit_reducible]

instance Semantics.Attitudes.Doxastic.instDecidableEqPresupClass : DecidableEq PresupClass

Equations

• Semantics.Attitudes.Doxastic.instDecidableEqPresupClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Attitudes.Doxastic.instReprPresupClass.repr : PresupClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Attitudes.Doxastic.instReprPresupClass : Repr PresupClass

Equations

• Semantics.Attitudes.Doxastic.instReprPresupClass = { reprPrec := Semantics.Attitudes.Doxastic.instReprPresupClass.repr }

def Semantics.Attitudes.Doxastic.classifyVeridicality : Veridicality → PresupClass

Classify a doxastic verb by its veridicality.

Equations

• Semantics.Attitudes.Doxastic.classifyVeridicality Features.Veridicality.veridical = Semantics.Attitudes.Doxastic.PresupClass.factive
• Semantics.Attitudes.Doxastic.classifyVeridicality Features.Veridicality.nonVeridical = Semantics.Attitudes.Doxastic.PresupClass.nonfactive

theorem Semantics.Attitudes.Doxastic.veridical_is_factive : classifyVeridicality Features.Veridicality.veridical = PresupClass.factive

Veridical verbs are factive.

theorem Semantics.Attitudes.Doxastic.nonVeridical_is_nonfactive : classifyVeridicality Features.Veridicality.nonVeridical = PresupClass.nonfactive

Non-veridical verbs are nonfactive.

Causal Explanation of the Contrafactive Gap

Roberts & Özyıldız (2025) propose that the contrafactive gap follows from a general constraint on lexicalization: presupposed content must be causally upstream of at-issue content.

The Predicate Lexicalization Constraint (PLC)

A verbal predicate V with at-issue content α can have presupposition π iff in the normative world wₙ, a causal chain from π(wₙ) to α(wₙ) can be constructed for any assignment of the arguments of V.

Why Factives Work (know)

For "Delilah knows that Konstanz is in Germany":

• Presupposition: p (Konstanz is in Germany)
• At-issue: B(d)(p) (Delilah believes Konstanz is in Germany)

Causal chain: p → indic(p) → acq(d)(iₚ) → B(d)(p)

1. The fact p generates indicators (evidence) for p
2. Delilah can become acquainted with these indicators
3. This acquaintance leads to belief formation

Why Strong Contrafactives Don't Work (contra)

For hypothetical "Marianne contras that the Earth is flat":

• Presupposition: ¬p (Earth is round, i.e., ¬flat)
• At-issue: B(m)(p) (Marianne believes Earth is flat)

NO causal chain: ¬p (ROUND) does NOT generate indicators for p (FLAT)

• ROUND generates indicators for ROUND
• There's no typical causal path from ¬p to B(x)(p)

This asymmetry DERIVES the gap from independent causal-cognitive principles.

The belief formation causal model uses Core.Causal — the V2 SEM substrate (PMF-canonical Mechanism, BoolSEM specialization for the deterministic-binary case). The PLC predicate is defined via SEM.developDetOn with an explicit vertex list so kernel reduction works structurally (no native_decide; mathlib-quality rfl/decide proofs).

inductive Semantics.Attitudes.Doxastic.BeliefVar : Type

Standard variables in belief formation. Inductive enum so the type is Fintype and the developDet fixpoint reduces structurally.

• p : BeliefVar
• not_p : BeliefVar
• indic_p : BeliefVar
• indic_not_p : BeliefVar
• acq_a_ip : BeliefVar
• acq_a_inp : BeliefVar
• B_a_p : BeliefVar
• B_a_not_p : BeliefVar

@[implicit_reducible]

instance Semantics.Attitudes.Doxastic.instDecidableEqBeliefVar : DecidableEq BeliefVar

Equations

• Semantics.Attitudes.Doxastic.instDecidableEqBeliefVar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Attitudes.Doxastic.instFintypeBeliefVar : Fintype BeliefVar

Equations

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

def Semantics.Attitudes.Doxastic.instReprBeliefVar.repr : BeliefVar → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Attitudes.Doxastic.instReprBeliefVar : Repr BeliefVar

Equations

• Semantics.Attitudes.Doxastic.instReprBeliefVar = { reprPrec := Semantics.Attitudes.Doxastic.instReprBeliefVar.repr }

def Semantics.Attitudes.Doxastic.beliefGraph : Core.Causal.CausalGraph BeliefVar

The causal graph for belief formation. Chain structure: p → indic(p) → acq(a)(iₚ) → B(a)(p) (parallel chain for ¬p). Each derived vertex has its single causal predecessor as parent.

Equations

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

noncomputable def Semantics.Attitudes.Doxastic.beliefSEM : Core.Causal.BoolSEM BeliefVar

The belief-formation BoolSEM. Roots (p, ¬p) get Mechanism.const false (default; the input valuation overrides). Each derived vertex's mechanism is "true iff its sole parent is true" — the chain copies values forward.

Equations

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

@[implicit_reducible]

noncomputable instance Semantics.Attitudes.Doxastic.instIsDeterministicBeliefVarBoolBeliefSEM : Core.Causal.SEM.IsDeterministic beliefSEM

Equations

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

def Semantics.Attitudes.Doxastic.beliefVarList : List BeliefVar

Explicit vertex list for developDetOn. Topological order ensures one stepOnceDetOn pass propagates the entire chain.

Equations

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

noncomputable def Semantics.Attitudes.Doxastic.satisfiesPLC (presup atIssue : BeliefVar) : Prop

Predicate Lexicalization Constraint (PLC) (@cite{roberts-ozyildiz-2025}).

A verbal predicate with at-issue content α can have presupposition π iff setting π to true and running the belief-formation SEM's developDetOn produces α at the at-issue vertex.

Defined via developDetOn with the explicit beliefVarList so kernel reduction works structurally (no native_decide). One iteration of stepOnceDetOn over a topologically-ordered list propagates the entire chain; we use 8 = beliefVarList.length iterations conservatively.

Equations

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

@[implicit_reducible]

noncomputable instance Semantics.Attitudes.Doxastic.instDecidableSatisfiesPLC (presup atIssue : BeliefVar) : Decidable (satisfiesPLC presup atIssue)

Equations

• Semantics.Attitudes.Doxastic.instDecidableSatisfiesPLC presup atIssue = Classical.dec (Semantics.Attitudes.Doxastic.satisfiesPLC presup atIssue)

theorem Semantics.Attitudes.Doxastic.factive_satisfies_plc : satisfiesPLC BeliefVar.p BeliefVar.B_a_p

Theorem: Factives satisfy the PLC

For "x knows p":

• Presupposition: p
• At-issue: B(a)(p)
• Causal chain: p → indic(p) → acq(a)(iₚ) → B(a)(p) ✓

theorem Semantics.Attitudes.Doxastic.strong_contrafactive_violates_plc : ¬satisfiesPLC BeliefVar.not_p BeliefVar.B_a_p

Theorem: Strong contrafactives VIOLATE the PLC

For hypothetical "x contras p":

• Presupposition: ¬p
• At-issue: B(a)(p)
• NO causal chain from ¬p to B(a)(p) ✗

The fact that the Earth is round does not generate evidence that the Earth is flat.

theorem Semantics.Attitudes.Doxastic.contrafactive_gap : satisfiesPLC BeliefVar.p BeliefVar.B_a_p ∧ ¬satisfiesPLC BeliefVar.not_p BeliefVar.B_a_p

The Contrafactive Gap Theorem

The asymmetry between factives and strong contrafactives follows from the Predicate Lexicalization Constraint:

1. Factives (know): presup p → at-issue B(a)(p) — PLC SATISFIED
2. Strong contrafactives (contra): presup ¬p → at-issue B(a)(p) — PLC VIOLATED

This DERIVES the gap from the independently motivated causal constraint.

theorem Semantics.Attitudes.Doxastic.contrafactive_gap_is_structural : satisfiesPLC BeliefVar.p BeliefVar.B_a_p ∧ ¬satisfiesPLC BeliefVar.not_p BeliefVar.B_a_p ∧ satisfiesPLC BeliefVar.not_p BeliefVar.B_a_not_p

Corollary: The asymmetry is structural, not stipulated

The contrafactive gap emerges from the structure of belief formation:

• Beliefs are formed based on evidence
• Evidence for p comes from p being true
• Evidence for p does NOT come from ¬p being true

Therefore any predicate trying to presuppose ¬p while asserting B(x)(p) is describing a causally incoherent eventuality.

Weak Contrafactives (yǐwéi) and the PLC

Weak contrafactives like Mandarin yǐwéi don't violate the PLC because their projective content is fundamentally different:

1. Not a presupposition: @cite{glass-2025} argues yǐwéi's falsity inference is a postsupposition (about output context) not presupposition (input). Postsuppositions are formalized in Core.Postsupposition.

2. Different requirement: yǐwéi requires CG ◇ ¬p (CG compatible with ¬p), not CG ⊨ ¬p (CG entails ¬p)

3. No causal incoherence: "p is unsettled in CG" is compatible with "there's evidence for p that x acquired" — these are about different epistemic states (communal knowledge vs individual belief)

The PLC only constrains the relationship between presupposition and at-issue content within the SAME eventuality. Postsuppositions about discourse context update are not subject to this constraint.

def Semantics.Attitudes.Doxastic.presupClassToCausalVars : PresupClass → Option (BeliefVar × BeliefVar)

Map a PresupClass to the corresponding causal variables for PLC checking.

• Factive: presup = p, at-issue = B(a)(p)
• Contrafactive: presup = ¬p, at-issue = B(a)(p)

For nonfactive (no presupposition) and other, the PLC doesn't apply.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Attitudes.Doxastic.presupClassToCausalVars Semantics.Attitudes.Doxastic.PresupClass.factive = some (Semantics.Attitudes.Doxastic.BeliefVar.p, Semantics.Attitudes.Doxastic.BeliefVar.B_a_p)
• Semantics.Attitudes.Doxastic.presupClassToCausalVars Semantics.Attitudes.Doxastic.PresupClass.nonfactive = none
• Semantics.Attitudes.Doxastic.presupClassToCausalVars Semantics.Attitudes.Doxastic.PresupClass.other = none

noncomputable def Semantics.Attitudes.Doxastic.presupClassSatisfiesPLC (pc : PresupClass) : Option Bool

Check if a PresupClass satisfies the Predicate Lexicalization Constraint.

Returns none if the PLC doesn't apply (nonfactive, postsuppositions). Returns some true if it satisfies PLC, some false if it violates PLC.

Equations

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

def Semantics.Attitudes.Doxastic.presupClassIsValid : PresupClass → Bool

Is this presuppositional profile valid (attestable)?

Valid means: either satisfies PLC (factives) or not subject to PLC (nonfactives, postsuppositions). Invalid = violates PLC (contrafactives).

Direct (computable) classification. The PLC-derivation chain (via presupClassSatisfiesPLC) is given as presupClassIsValid_eq_via_plc below.

Equations

• Semantics.Attitudes.Doxastic.presupClassIsValid Semantics.Attitudes.Doxastic.PresupClass.factive = true
• Semantics.Attitudes.Doxastic.presupClassIsValid Semantics.Attitudes.Doxastic.PresupClass.nonfactive = true
• Semantics.Attitudes.Doxastic.presupClassIsValid Semantics.Attitudes.Doxastic.PresupClass.contrafactive = false
• Semantics.Attitudes.Doxastic.presupClassIsValid Semantics.Attitudes.Doxastic.PresupClass.other = true

theorem Semantics.Attitudes.Doxastic.presupClassIsValid_eq_via_plc (pc : PresupClass) : presupClassIsValid pc = (presupClassSatisfiesPLC pc).getD true

The PLC derivation: presupClassIsValid agrees with running the presupClassSatisfiesPLC chain (taking none as true). This bridges the direct classifier to the @cite{roberts-ozyildiz-2025} causal account.

theorem Semantics.Attitudes.Doxastic.factive_presup_valid : presupClassIsValid PresupClass.factive = true

Factive presuppositions are valid (satisfy PLC).

theorem Semantics.Attitudes.Doxastic.contrafactive_presup_invalid : presupClassIsValid PresupClass.contrafactive = false

Contrafactive presuppositions are invalid (violate PLC).

theorem Semantics.Attitudes.Doxastic.nonfactive_presup_valid : presupClassIsValid PresupClass.nonfactive = true

Nonfactive verbs are trivially valid (no presupposition to check).

def Semantics.Attitudes.Doxastic.veridicalityHolds {W : Type u_2} (v : Veridicality) (p : W → Prop) (w : W) : Prop

Veridicality constraint: if veridical, p must hold at the evaluation world.

For "know", we require p(w) at the evaluation world w.

Equations

• Semantics.Attitudes.Doxastic.veridicalityHolds Features.Veridicality.veridical p w = p w
• Semantics.Attitudes.Doxastic.veridicalityHolds Features.Veridicality.nonVeridical p w = True

@[implicit_reducible]

instance Semantics.Attitudes.Doxastic.veridicalityHolds_decidable {W : Type u_2} (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 Semantics.Attitudes.Doxastic.DoxasticPredicate (W : Type u_2) (E : Type u_3) : Type (max u_2 u_3)

A doxastic attitude predicate.

Bundles the accessibility relation with veridicality and other properties.

• name : String

  Name of the predicate

• access : AccessRel W E

  Accessibility relation

• veridicality : Veridicality

  Veridicality (veridical or not)

• createsOpaqueContext : Bool

  Does it create an opaque context? (substitution failures)

def Semantics.Attitudes.Doxastic.DoxasticPredicate.holdsAt {W : Type u_2} {E : Type u_3} (V : DoxasticPredicate W E) (agent : E) (p : W → Prop) (w : W) (worlds : List W) : Prop

Semantics for a doxastic predicate taking a proposition.

⟦x V that p⟧(w) = (veridicalityHolds V p w) ∧ ∀w'. R(x,w,w') → p(w')

For veridical predicates, we also require p(w).

Equations

• V.holdsAt agent p w worlds = (Semantics.Attitudes.Doxastic.veridicalityHolds V.veridicality p w ∧ Semantics.Attitudes.Doxastic.boxAt V.access agent w worlds p)

@[implicit_reducible]

instance Semantics.Attitudes.Doxastic.DoxasticPredicate.holdsAt_decidable {W : Type u_2} {E : Type u_3} (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

• V.holdsAt_decidable agent p w worlds = Semantics.Attitudes.Doxastic.DoxasticPredicate.holdsAt_decidable._aux_1 V agent p w worlds

def Semantics.Attitudes.Doxastic.DoxasticPredicate.toPrProp {W : Type u_2} {E : Type u_3} (V : DoxasticPredicate W E) (agent : E) (p : W → Prop) (worlds : List W) : Core.Presupposition.PrProp W

Convert a doxastic predicate application to a PrProp.

The decomposition makes the presuppositional structure explicit:

• presup = veridicality check (for veridical: p(w); for non-veridical: true)
• assertion = universal modal (∀w'. R(x,w,w') → p(w'))

holdsAt computes presup(w) && assertion(w) — the same as PrProp.holds.

Equations

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

theorem Semantics.Attitudes.Doxastic.DoxasticPredicate.toPrProp_presup {W : Type u_2} {E : Type u_3} (V : DoxasticPredicate W E) (agent : E) (p : W → Prop) (w : W) (worlds : List W) : (V.toPrProp agent p worlds).presup w = veridicalityHolds V.veridicality p w

toPrProp decomposes holdsAt: the presup field is the veridicality check and the assertion field is the modal.

theorem Semantics.Attitudes.Doxastic.DoxasticPredicate.toPrProp_assertion {W : Type u_2} {E : Type u_3} (V : DoxasticPredicate W E) (agent : E) (p : W → Prop) (w : W) (worlds : List W) : (V.toPrProp agent p worlds).assertion w = boxAt V.access agent w worlds p

def Semantics.Attitudes.Doxastic.contrafactivePrProp {W : Type u_2} {E : Type u_3} (R : AccessRel W E) (agent : E) (p : W → Prop) (worlds : List W) : Core.Presupposition.PrProp W

PrProp for a hypothetical contrafactive verb: presupposes ¬p, asserts agent believes p. UNATTESTED — see @cite{glass-2025}.

Equations

• Semantics.Attitudes.Doxastic.contrafactivePrProp R agent p worlds = { presup := fun (w : W) => ¬p w, assertion := fun (w : W) => Semantics.Attitudes.Doxastic.boxAt R agent w worlds p }

def Semantics.Attitudes.Doxastic.DoxasticPredicate.holdsAtQuestion {W : Type u_2} {E : Type u_3} (V : DoxasticPredicate W E) (agent : E) (Q : (W → Prop) → Prop) (w : W) (worlds : List W) (answers : List (W → Prop)) : Prop

Semantics for doxastic predicate taking a Hamblin question.

Following @cite{karttunen-1977}, "know Q" means knowing the true answer: ⟦x knows Q⟧(w) = ∃p ∈ Q. p(w) ∧ x knows p

For non-veridical predicates, we drop the p(w) requirement: ⟦x believes Q⟧(w) = ∃p ∈ Q. x believes p

Equations

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

def Semantics.Attitudes.Doxastic.believeTemplate {W : Type u_2} {E : Type u_3} (R : AccessRel W E) : DoxasticPredicate W E

Abstract "believe" predicate template.

Users instantiate with their specific accessibility relation.

Equations

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

def Semantics.Attitudes.Doxastic.knowTemplate {W : Type u_2} {E : Type u_3} (R : AccessRel W E) : DoxasticPredicate W E

Abstract "know" predicate template.

Veridical: knowing p requires p to be true.

Equations

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

def Semantics.Attitudes.Doxastic.thinkTemplate {W : Type u_2} {E : Type u_3} (R : AccessRel W E) : DoxasticPredicate W E

Abstract "think" predicate template.

Non-veridical, typically less commitment than "believe".

Equations

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

theorem Semantics.Attitudes.Doxastic.veridical_entails_complement {W : Type u_2} {E : Type u_3} (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 is true at w.

theorem Semantics.Attitudes.Doxastic.nonVeridical_not_entails {W : Type u_2} {E : Type u_3} [Inhabited W] [Inhabited E] (V : DoxasticPredicate W E) (hV : V.veridicality = Features.Veridicality.nonVeridical) : ∃ (agent : E) (p : W → Prop) (w : W) (worlds : List W), V.holdsAt agent p w worlds ∧ ¬p w

Non-veridical predicates don't entail their complement.

There exist cases where x believes p but p is false.

theorem Semantics.Attitudes.Doxastic.doxastic_k_axiom {W : Type u_2} {E : Type u_3} (V : DoxasticPredicate W E) (agent : E) (p q : W → Prop) (w : W) (worlds : List W) (hp : boxAt V.access agent w worlds p) (hpq : boxAt V.access agent w worlds fun (w' : W) => p w' → q w') : boxAt V.access agent w worlds q

Doxastic predicates are closed under known implication.

If x knows p and x knows (p → q), then x knows q. (This is the K axiom of modal logic)

Substitution and Opacity

Opaque contexts block substitution of co-referential terms.

Even if a = b (extensionally), "x believes Fa" may differ from "x believes Fb" because the agent may not know a = b.

This is formalized by the createsOpaqueContext field: when true, the predicate operates on intensions (functions from worlds), not extensions.

def Semantics.Attitudes.Doxastic.substitutionMayFail {W : Type u_2} {E : Type u_3} (V : DoxasticPredicate W E) : Prop

For opaque predicates, substitution failure is possible.

This is a statement that the predicate distinguishes intensions that happen to have the same extension at the evaluation world.

Equations

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

def Semantics.Attitudes.Doxastic.deDicto {W : Type u_2} {E : Type u_3} (V : DoxasticPredicate W E) (agent : E) (p : W → Prop) (w : W) (worlds : List W) : Prop

De dicto reading: quantifier under the attitude.

"John believes someone is a spy" (de dicto) = John believes ∃x. spy(x)

Equations

• Semantics.Attitudes.Doxastic.deDicto V agent p w worlds = V.holdsAt agent p w worlds

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

De re reading: quantifier over the attitude.

"John believes someone is a spy" (de re) = ∃x. John believes spy(x)

Here we need a domain of individuals to quantify over.

Equations

• Semantics.Attitudes.Doxastic.deRe V agent predicate domain w worlds = ∃ x ∈ domain, V.holdsAt agent (predicate x) w worlds

Attitude Embedding and Scalar Implicature

When scalar expressions are embedded under attitudes, the implicature can be computed locally (inside the attitude) or globally (about speaker):

Global: Speaker implicates ¬(speaker believes all) Local: x believes (some ∧ ¬all) [apparent local reading]

@cite{goodman-stuhlmuller-2013} show the "local" reading arises from pragmatic inference about speaker knowledge, not true local computation.

See Phenomena/ScalarImplicatures/Studies/GoodmanStuhlmuller2013PMF.lean for the RSA treatment.

def Semantics.Attitudes.Doxastic.psychMode : Veridicality → Core.Discourse.PsychMode

Map veridicality to @cite{searle-1983}'s psychological mode.

Veridical attitudes (know, realize) are like perception: the world must cause the mental state (you can only know p if p is the case and your epistemic state is appropriately caused by p's being the case). Non-veridical attitudes (believe, think) are like belief: satisfaction depends only on whether p obtains, not on the causal chain.

Equations

• Semantics.Attitudes.Doxastic.psychMode Features.Veridicality.veridical = Core.Discourse.PsychMode.perception
• Semantics.Attitudes.Doxastic.psychMode Features.Veridicality.nonVeridical = Core.Discourse.PsychMode.belief

theorem Semantics.Attitudes.Doxastic.veridical_self_referential : (psychMode Features.Veridicality.veridical).causalSelfRef = Core.Discourse.CausalSelfRef.worldToState ∧ (psychMode Features.Veridicality.nonVeridical).causalSelfRef = Core.Discourse.CausalSelfRef.none

Veridical attitudes are causally self-referential (world→state); non-veridical attitudes are not. This connects the linguistic veridicality distinction to @cite{searle-1983}'s metaphysics: knowledge requires the world to cause the knowing, while belief requires only that the content match reality.