@[reducible, inline]

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

Doxastic accessibility relation type.

R(agent, evalWorld, accessibleWorld) = true iff accessibleWorld is compatible with what agent believes/knows in evalWorld.

Equations

• Semantics.Attitudes.Doxastic.AccessRel W E = Core.ModalLogic.AgentAccessRel W E

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 → Bool) : Bool

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

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

Equations

• Semantics.Attitudes.Doxastic.boxAt R agent w worlds p = worlds.all fun (w' : W) => !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 → Bool) : Bool

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

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

Equations

• Semantics.Attitudes.Doxastic.diaAt R agent w worlds p = worlds.any fun (w' : W) => R agent w w' && p w'

inductive Semantics.Attitudes.Doxastic.Veridicality : Type

A doxastic predicate is veridical if believing/knowing p entails p is true.

Veridical: know, realize, discover Non-veridical: believe, think, suspect

• veridical : Veridicality
• nonVeridical : Veridicality

instance Semantics.Attitudes.Doxastic.instDecidableEqVeridicality : DecidableEq Veridicality

Equations

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

def Semantics.Attitudes.Doxastic.instReprVeridicality.repr : Veridicality → ℕ → Std.Format

Equations

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

instance Semantics.Attitudes.Doxastic.instReprVeridicality : Repr Veridicality

Equations

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

instance Semantics.Attitudes.Doxastic.instBEqVeridicality : BEq Veridicality

Equations

• Semantics.Attitudes.Doxastic.instBEqVeridicality = { beq := Semantics.Attitudes.Doxastic.instBEqVeridicality.beq }

def Semantics.Attitudes.Doxastic.instBEqVeridicality.beq : Veridicality → Veridicality → Bool

Equations

• Semantics.Attitudes.Doxastic.instBEqVeridicality.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Semantics.Attitudes.Doxastic.CGPolarity : Type

Common Ground requirement polarity: does the verb place requirements on p or ¬p?

@cite{glass-2025} distinguishes belief verbs by whether their projective content concerns p (positive) or ¬p (negative).

• positive : CGPolarity
• negative : CGPolarity

instance Semantics.Attitudes.Doxastic.instDecidableEqCGPolarity : DecidableEq CGPolarity

Equations

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

def Semantics.Attitudes.Doxastic.instReprCGPolarity.repr : CGPolarity → ℕ → Std.Format

Equations

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

instance Semantics.Attitudes.Doxastic.instReprCGPolarity : Repr CGPolarity

Equations

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

instance Semantics.Attitudes.Doxastic.instBEqCGPolarity : BEq CGPolarity

Equations

• Semantics.Attitudes.Doxastic.instBEqCGPolarity = { beq := Semantics.Attitudes.Doxastic.instBEqCGPolarity.beq }

def Semantics.Attitudes.Doxastic.instBEqCGPolarity.beq : CGPolarity → CGPolarity → Bool

Equations

• Semantics.Attitudes.Doxastic.instBEqCGPolarity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Semantics.Attitudes.Doxastic.CGStrength : Type

Common Ground requirement strength: entailment (□) or compatibility (◇)?

• necessity: CG must entail the condition (∀w ∈ c. φ(w))
• possibility: CG must be compatible with the condition (∃w ∈ c. φ(w))

• necessity : CGStrength
• possibility : CGStrength

instance Semantics.Attitudes.Doxastic.instDecidableEqCGStrength : DecidableEq CGStrength

Equations

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

instance Semantics.Attitudes.Doxastic.instReprCGStrength : Repr CGStrength

Equations

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

def Semantics.Attitudes.Doxastic.instReprCGStrength.repr : CGStrength → ℕ → Std.Format

Equations

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

instance Semantics.Attitudes.Doxastic.instBEqCGStrength : BEq CGStrength

Equations

• Semantics.Attitudes.Doxastic.instBEqCGStrength = { beq := Semantics.Attitudes.Doxastic.instBEqCGStrength.beq }

def Semantics.Attitudes.Doxastic.instBEqCGStrength.beq : CGStrength → CGStrength → Bool

Equations

• Semantics.Attitudes.Doxastic.instBEqCGStrength.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Semantics.Attitudes.Doxastic.CGRequirement : Type

Common Ground requirement for belief verbs.

@cite{glass-2025} proposes a 2×2 typology based on polarity × strength:

• Factive (know): positive × necessity → CG ⊨ p
• Nonfactive (think): no requirement
• Weak contrafactive (yǐwéi): negative × possibility → CG ◇ ¬p
• Strong contrafactive (contra): negative × necessity → CG ⊨ ¬p (UNATTESTED)

The key insight: weak contrafactives exist (Mandarin yǐwéi), but strong contrafactives requiring ¬p to be Common Ground are systematically absent.

• polarity : CGPolarity
• strength : CGStrength

def Semantics.Attitudes.Doxastic.instDecidableEqCGRequirement.decEq (x✝ x✝¹ : CGRequirement) : Decidable (x✝ = x✝¹)

Equations

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

instance Semantics.Attitudes.Doxastic.instDecidableEqCGRequirement : DecidableEq CGRequirement

Equations

• Semantics.Attitudes.Doxastic.instDecidableEqCGRequirement = Semantics.Attitudes.Doxastic.instDecidableEqCGRequirement.decEq

instance Semantics.Attitudes.Doxastic.instReprCGRequirement : Repr CGRequirement

Equations

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

def Semantics.Attitudes.Doxastic.instReprCGRequirement.repr : CGRequirement → ℕ → Std.Format

Equations

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

def Semantics.Attitudes.Doxastic.instBEqCGRequirement.beq : CGRequirement → CGRequirement → Bool

Equations

• Semantics.Attitudes.Doxastic.instBEqCGRequirement.beq { polarity := a, strength := a_1 } { polarity := b, strength := b_1 } = (a == b && a_1 == b_1)
• Semantics.Attitudes.Doxastic.instBEqCGRequirement.beq x✝¹ x✝ = false

instance Semantics.Attitudes.Doxastic.instBEqCGRequirement : BEq CGRequirement

Equations

• Semantics.Attitudes.Doxastic.instBEqCGRequirement = { beq := Semantics.Attitudes.Doxastic.instBEqCGRequirement.beq }

def Semantics.Attitudes.Doxastic.CGRequirement.factive : CGRequirement

Factive requirement: CG entails p (know, realize)

Equations

• Semantics.Attitudes.Doxastic.CGRequirement.factive = { polarity := Semantics.Attitudes.Doxastic.CGPolarity.positive, strength := Semantics.Attitudes.Doxastic.CGStrength.necessity }

def Semantics.Attitudes.Doxastic.CGRequirement.weakContrafactive : CGRequirement

Weak contrafactive: CG compatible with ¬p (Mandarin yǐwéi)

Equations

• Semantics.Attitudes.Doxastic.CGRequirement.weakContrafactive = { polarity := Semantics.Attitudes.Doxastic.CGPolarity.negative, strength := Semantics.Attitudes.Doxastic.CGStrength.possibility }

def Semantics.Attitudes.Doxastic.CGRequirement.strongContrafactive : CGRequirement

Strong contrafactive: CG entails ¬p (hypothetical "contra" - UNATTESTED)

Equations

• Semantics.Attitudes.Doxastic.CGRequirement.strongContrafactive = { polarity := Semantics.Attitudes.Doxastic.CGPolarity.negative, strength := Semantics.Attitudes.Doxastic.CGStrength.necessity }

def Semantics.Attitudes.Doxastic.CGRequirement.satisfied {W : Type u_1} (req : CGRequirement) (contextSet : List W) (p : W → Bool) : Bool

Is this requirement satisfied given a context set and proposition?

Equations

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

Deriving CG Requirements from Semantic Structure

@cite{glass-2025} shows that for DOXASTIC verbs, the CG requirement is NOT a separate lexical property - it follows from VERIDICALITY:

• Veridical (know): presupposes p → factive CG requirement
• Non-veridical (believe): no presupposition → no CG requirement

The key insight: cgRequirement should be DERIVED, not stipulated.

Postsuppositions (yǐwéi)

yǐwéi is special: it has a POSTSUPPOSITION (output-context constraint), not a presupposition (input-context constraint). Its requirement ◇¬p applies AFTER the utterance updates the context.

This is genuinely lexical (exceptional) and not derivable from veridicality.

def Semantics.Attitudes.Doxastic.deriveCGRequirement (v : Veridicality) : Option CGRequirement

Derive CG requirement from veridicality for doxastic verbs.

This captures the systematic relationship:

• Veridical verbs presuppose their complement → factive requirement
• Non-veridical verbs have no presupposition → no requirement

Note: Postsuppositions (like yǐwéi's ◇¬p) are NOT captured here because they're about output context, not input presupposition.

Equations

• Semantics.Attitudes.Doxastic.deriveCGRequirement Semantics.Attitudes.Doxastic.Veridicality.veridical = some Semantics.Attitudes.Doxastic.CGRequirement.factive
• Semantics.Attitudes.Doxastic.deriveCGRequirement Semantics.Attitudes.Doxastic.Veridicality.nonVeridical = none

theorem Semantics.Attitudes.Doxastic.veridical_implies_factive : deriveCGRequirement Veridicality.veridical = some CGRequirement.factive

Theorem: Factives have factive CG requirements.

This is a DERIVATION, not a stipulation. The factive presupposition follows from the verb being veridical.

theorem Semantics.Attitudes.Doxastic.nonVeridical_implies_none : deriveCGRequirement Veridicality.nonVeridical = none

Theorem: Non-veridical verbs have no CG requirement.

This is why believe/think don't presuppose anything about p.

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.

structure Semantics.Attitudes.Doxastic.CausalVar : Type

A variable in a causal model. Variables can be exogenous (external) or endogenous (determined by structural equations).

• name : String

instance Semantics.Attitudes.Doxastic.instDecidableEqCausalVar : DecidableEq CausalVar

Equations

• Semantics.Attitudes.Doxastic.instDecidableEqCausalVar = Semantics.Attitudes.Doxastic.instDecidableEqCausalVar.decEq

def Semantics.Attitudes.Doxastic.instDecidableEqCausalVar.decEq (x✝ x✝¹ : CausalVar) : Decidable (x✝ = x✝¹)

Equations

• Semantics.Attitudes.Doxastic.instDecidableEqCausalVar.decEq { name := a } { name := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Semantics.Attitudes.Doxastic.instReprCausalVar.repr : CausalVar → ℕ → Std.Format

Equations

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

instance Semantics.Attitudes.Doxastic.instReprCausalVar : Repr CausalVar

Equations

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

instance Semantics.Attitudes.Doxastic.instBEqCausalVar : BEq CausalVar

Equations

• Semantics.Attitudes.Doxastic.instBEqCausalVar = { beq := Semantics.Attitudes.Doxastic.instBEqCausalVar.beq }

def Semantics.Attitudes.Doxastic.instBEqCausalVar.beq : CausalVar → CausalVar → Bool

Equations

• Semantics.Attitudes.Doxastic.instBEqCausalVar.beq { name := a } { name := b } = (a == b)
• Semantics.Attitudes.Doxastic.instBEqCausalVar.beq x✝¹ x✝ = false

def Semantics.Attitudes.Doxastic.instHashableCausalVar.hash : CausalVar → UInt64

Equations

• Semantics.Attitudes.Doxastic.instHashableCausalVar.hash { name := a } = mixHash 0 (hash a)

instance Semantics.Attitudes.Doxastic.instHashableCausalVar : Hashable CausalVar

Equations

• Semantics.Attitudes.Doxastic.instHashableCausalVar = { hash := Semantics.Attitudes.Doxastic.instHashableCausalVar.hash }

structure Semantics.Attitudes.Doxastic.CausalEdge : Type

A causal edge represents direct causal influence: (parent, child) means the value of parent directly influences the value of child.

• parent : CausalVar
• child : CausalVar

instance Semantics.Attitudes.Doxastic.instReprCausalEdge : Repr CausalEdge

Equations

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

def Semantics.Attitudes.Doxastic.instReprCausalEdge.repr : CausalEdge → ℕ → Std.Format

Equations

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

instance Semantics.Attitudes.Doxastic.instBEqCausalEdge : BEq CausalEdge

Equations

• Semantics.Attitudes.Doxastic.instBEqCausalEdge = { beq := Semantics.Attitudes.Doxastic.instBEqCausalEdge.beq }

def Semantics.Attitudes.Doxastic.instBEqCausalEdge.beq : CausalEdge → CausalEdge → Bool

Equations

• Semantics.Attitudes.Doxastic.instBEqCausalEdge.beq { parent := a, child := a_1 } { parent := b, child := b_1 } = (a == b && a_1 == b_1)
• Semantics.Attitudes.Doxastic.instBEqCausalEdge.beq x✝¹ x✝ = false

structure Semantics.Attitudes.Doxastic.CausalModel : Type

A causal model M = (U, V, E) where:

• exog: Exogenous variables (determined externally)
• endog: Endogenous variables (determined by structural equations)
• edges: Causal edges representing direct influence

This is a simplified @cite{pearl-2000} causal model for our purposes.

• exog : List CausalVar
• endog : List CausalVar
• edges : List CausalEdge

def Semantics.Attitudes.Doxastic.instReprCausalModel.repr : CausalModel → ℕ → Std.Format

Equations

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

instance Semantics.Attitudes.Doxastic.instReprCausalModel : Repr CausalModel

Equations

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

def Semantics.Attitudes.Doxastic.CausalModel.allVars (M : CausalModel) : List CausalVar

All variables in the model

Equations

• M.allVars = M.exog ++ M.endog

def Semantics.Attitudes.Doxastic.CausalModel.parents (M : CausalModel) (v : CausalVar) : List CausalVar

Get parents of a variable (direct causes)

Equations

• M.parents v = List.map (fun (x : Semantics.Attitudes.Doxastic.CausalEdge) => x.parent) (List.filter (fun (x : Semantics.Attitudes.Doxastic.CausalEdge) => x.child == v) M.edges)

def Semantics.Attitudes.Doxastic.CausalModel.children (M : CausalModel) (v : CausalVar) : List CausalVar

Get children of a variable (direct effects)

Equations

• M.children v = List.map (fun (x : Semantics.Attitudes.Doxastic.CausalEdge) => x.child) (List.filter (fun (x : Semantics.Attitudes.Doxastic.CausalEdge) => x.parent == v) M.edges)

def Semantics.Attitudes.Doxastic.CausalModel.hasCausalChain (M : CausalModel) (v1 v2 : CausalVar) : Bool

Check if there's a causal path from v₁ to v₂.

A causal chain exists from v₁ to v₂ iff altering v₁ can alter v₂. This is the transitive closure of the edge relation.

Equations

• M.hasCausalChain v1 v2 = Semantics.Attitudes.Doxastic.CausalModel.hasCausalChain.search M v2 [v1] [] (M.allVars.length + 1)

def Semantics.Attitudes.Doxastic.CausalModel.hasCausalChain.search (M : CausalModel) (v2 : CausalVar) (frontier visited : List CausalVar) (fuel : ℕ) : Bool

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Attitudes.Doxastic.CausalModel.hasCausalChain.search M v2 frontier visited 0 = false

Standard variables in belief formation causal models.

def Semantics.Attitudes.Doxastic.BeliefVars.p : CausalVar

The proposition p being true/false

Equations

• Semantics.Attitudes.Doxastic.BeliefVars.p = { name := "p" }

def Semantics.Attitudes.Doxastic.BeliefVars.not_p : CausalVar

The negation ¬p

Equations

• Semantics.Attitudes.Doxastic.BeliefVars.not_p = { name := "¬p" }

def Semantics.Attitudes.Doxastic.BeliefVars.indic_p : CausalVar

Indicators (evidence) for p: indic(p)

Equations

• Semantics.Attitudes.Doxastic.BeliefVars.indic_p = { name := "indic(p)" }

def Semantics.Attitudes.Doxastic.BeliefVars.indic_not_p : CausalVar

Indicators (evidence) for ¬p: indic(¬p)

Equations

• Semantics.Attitudes.Doxastic.BeliefVars.indic_not_p = { name := "indic(¬p)" }

def Semantics.Attitudes.Doxastic.BeliefVars.acq_a_ip : CausalVar

Agent a acquires indicator for p: acq(a)(iₚ)

Equations

• Semantics.Attitudes.Doxastic.BeliefVars.acq_a_ip = { name := "acq(a)(iₚ)" }

def Semantics.Attitudes.Doxastic.BeliefVars.acq_a_inp : CausalVar

Agent a acquires indicator for ¬p: acq(a)(i¬ₚ)

Equations

• Semantics.Attitudes.Doxastic.BeliefVars.acq_a_inp = { name := "acq(a)(i¬ₚ)" }

def Semantics.Attitudes.Doxastic.BeliefVars.B_a_p : CausalVar

Agent believes p: B(a)(p)

Equations

• Semantics.Attitudes.Doxastic.BeliefVars.B_a_p = { name := "B(a)(p)" }

def Semantics.Attitudes.Doxastic.BeliefVars.B_a_not_p : CausalVar

Agent believes ¬p: B(a)(¬p)

Equations

• Semantics.Attitudes.Doxastic.BeliefVars.B_a_not_p = { name := "B(a)(¬p)" }

def Semantics.Attitudes.Doxastic.beliefFormationModel : CausalModel

The standard causal model for knowledge/belief formation.

This captures the Roberts & Özyıldız insight that:

1. Facts generate indicators (evidence)
2. Agents acquire indicators through experience
3. Acquisition of indicators leads to belief formation

Key structural equations:

• indic(p) := p ∨ q (p is sufficient for its indicators; q = other sources)
• acq(a)(iₚ) := indic(p) ∧ exp(a)(iₚ) (acquaintance requires indicator + experience)
• B(a)(p) := acq(a)(iₚ) (belief results from acquaintance with evidence)

Equations

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

def Semantics.Attitudes.Doxastic.satisfiesPLC (presup atIssue : CausalVar) (M : CausalModel := beliefFormationModel) : Bool

Predicate Lexicalization Constraint (PLC)

A verbal predicate with at-issue content α can have presupposition π iff there exists a causal chain from π to α in the belief formation model.

This is the central constraint from Roberts & Özyıldız (2025).

Equations

• Semantics.Attitudes.Doxastic.satisfiesPLC presup atIssue M = M.hasCausalChain presup atIssue

theorem Semantics.Attitudes.Doxastic.factive_satisfies_plc : satisfiesPLC BeliefVars.p BeliefVars.B_a_p = true

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 BeliefVars.not_p BeliefVars.B_a_p = false

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) ✗

This is because ¬p generates indicators for ¬p, not for p. The fact that the Earth is round does not generate evidence that the Earth is flat.

theorem Semantics.Attitudes.Doxastic.contrafactive_gap : satisfiesPLC BeliefVars.p BeliefVars.B_a_p = true ∧ satisfiesPLC BeliefVars.not_p BeliefVars.B_a_p = false

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 : beliefFormationModel.hasCausalChain BeliefVars.p BeliefVars.B_a_p = true ∧ beliefFormationModel.hasCausalChain BeliefVars.not_p BeliefVars.B_a_p = false ∧ beliefFormationModel.hasCausalChain BeliefVars.not_p BeliefVars.B_a_not_p = true

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)

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.

theorem Semantics.Attitudes.Doxastic.weak_vs_strong_contrafactive : CGRequirement.weakContrafactive ≠ CGRequirement.strongContrafactive

Weak contrafactive is NOT a strong contrafactive - different structure. The requirement is ∃w ∈ CG. ¬p(w), not ∀w ∈ CG. ¬p(w).

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

Veridicality constraint: if veridical, accessible worlds ⊆ actual world's p-value.

For "know", we require: p(w) = true for the evaluation world w.

Equations

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

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 → Bool) (w : W) (worlds : List W) : Bool

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) = true.

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)

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

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 := Semantics.Attitudes.Doxastic.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 := Semantics.Attitudes.Doxastic.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 := Semantics.Attitudes.Doxastic.Veridicality.nonVeridical }

theorem Semantics.Attitudes.Doxastic.veridical_entails_complement {W : Type u_2} {E : Type u_3} (V : DoxasticPredicate W E) (hV : V.veridicality = Veridicality.veridical) (agent : E) (p : W → Bool) (w : W) (worlds : List W) (holds : V.holdsAt agent p w worlds = true) : p w = true

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 = Veridicality.nonVeridical) : ∃ (agent : E) (p : W → Bool) (w : W) (worlds : List W), V.holdsAt agent p w worlds = true ∧ p w = false

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 → Bool) (w : W) (worlds : List W) (hp : boxAt V.access agent w worlds p = true) (hpq : (boxAt V.access agent w worlds fun (w' : W) => !p w' || q w') = true) : boxAt V.access agent w worlds q = true

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 → Bool) (w : W) (worlds : List W) : Bool

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 → Bool) (domain : List D) (w : W) (worlds : List W) : Bool

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 = domain.any fun (x : D) => 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 RSA/Implementations/GoodmanStuhlmuller2013.lean for the RSA treatment.

def Semantics.Attitudes.Doxastic.Veridicality.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.Veridicality.veridical.psychMode = Core.Discourse.PsychMode.perception
• Semantics.Attitudes.Doxastic.Veridicality.nonVeridical.psychMode = Core.Discourse.PsychMode.belief

theorem Semantics.Attitudes.Doxastic.veridical_self_referential : Veridicality.veridical.psychMode.causalSelfRef = Core.Discourse.CausalSelfRef.worldToState ∧ Veridicality.nonVeridical.psychMode.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.