Roberts & Özyıldız 2025: The causal derivation of the contrafactive gap

[RO25] derive the contrafactive gap — the absence of verbs presupposing ¬p while asserting belief in p — from the Predicate Lexicalization Constraint (PLC): presupposed content must be causally upstream of at-issue content. A verbal predicate with at-issue content α can carry presupposition π only if a causal chain runs from π to α in the normative belief-formation model p → indic(p) → acq(a)(iₚ) → B(a)(p): the fact generates indicators, acquaintance with which causes belief.

Factives satisfy the PLC (factive_satisfies_plc: the chain from p to B(a)(p) exists); strong contrafactives violate it (strong_contrafactive_violates_plc: ¬p generates indicators for ¬p, not for p, so no chain reaches B(a)(p)) — the gap follows (contrafactive_gap), and structurally so (contrafactive_gap_is_structural: presupposing ¬p while asserting B(a)(¬p) is fine). Weak contrafactives like Mandarin yǐwéi escape: their falsity inference is a postsupposition about the output context ([Gla25]), not a presupposition inside the same eventuality, so the PLC does not apply. presupClassIsValid_eq_via_plc derives [Gla25]'s attestation table from the causal account.

The belief-formation model is a deterministic BoolSEM over the Causation substrate; the PLC check runs developDetOn over a topologically ordered vertex list so proofs reduce structurally.

The belief-formation causal model

inductive RobertsOzyildiz2025.BeliefVar : Type

Variables of belief formation: the fact, its negation, their indicators, acquaintance with the indicators, and the resulting beliefs. An enum so 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

@[instance_reducible]

instance RobertsOzyildiz2025.instDecidableEqBeliefVar : DecidableEq BeliefVar

Equations

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

@[instance_reducible]

instance RobertsOzyildiz2025.instFintypeBeliefVar : Fintype BeliefVar

Equations

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

def RobertsOzyildiz2025.instReprBeliefVar.repr : BeliefVar → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance RobertsOzyildiz2025.instReprBeliefVar : Repr BeliefVar

Equations

• RobertsOzyildiz2025.instReprBeliefVar = { reprPrec := RobertsOzyildiz2025.instReprBeliefVar.repr }

def RobertsOzyildiz2025.beliefGraph : Causation.CausalGraph BeliefVar

The causal graph: the chain p → indic(p) → acq(a)(iₚ) → B(a)(p) and its parallel ¬p chain.

Equations

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

noncomputable def RobertsOzyildiz2025.beliefSEM : Causation.BoolSEM BeliefVar

The belief-formation BoolSEM: roots default to false (the input valuation overrides); each derived vertex copies its sole parent.

Equations

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

@[instance_reducible]

noncomputable instance RobertsOzyildiz2025.instIsDeterministicBeliefVarBoolBeliefSEM : Causation.SEM.IsDeterministic beliefSEM

Equations

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

def RobertsOzyildiz2025.beliefVarList : List BeliefVar

Topologically ordered vertex list: one stepOnceDetOn pass propagates the whole chain.

Equations

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

The Predicate Lexicalization Constraint

noncomputable def RobertsOzyildiz2025.SatisfiesPLC (presup atIssue : BeliefVar) : Prop

The PLC: presupposition presup can be lexicalized with at-issue content atIssue iff setting the presupposition true and running the belief-formation model produces the at-issue content.

Equations

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

@[instance_reducible]

noncomputable instance RobertsOzyildiz2025.instDecidableSatisfiesPLC (presup atIssue : BeliefVar) : Decidable (SatisfiesPLC presup atIssue)

Equations

• RobertsOzyildiz2025.instDecidableSatisfiesPLC presup atIssue = Classical.dec (RobertsOzyildiz2025.SatisfiesPLC presup atIssue)

theorem RobertsOzyildiz2025.factive_satisfies_plc : SatisfiesPLC BeliefVar.p BeliefVar.B_a_p

Factives satisfy the PLC: the chain from p reaches B(a)(p).

theorem RobertsOzyildiz2025.strong_contrafactive_violates_plc : ¬SatisfiesPLC BeliefVar.not_p BeliefVar.B_a_p

Strong contrafactives violate the PLC: ¬p generates indicators for ¬p, not for p, so no chain reaches B(a)(p).

theorem RobertsOzyildiz2025.contrafactive_gap : SatisfiesPLC BeliefVar.p BeliefVar.B_a_p ∧ ¬SatisfiesPLC BeliefVar.not_p BeliefVar.B_a_p

The contrafactive gap: the factive/contrafactive asymmetry follows from the PLC.

theorem RobertsOzyildiz2025.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

The asymmetry is structural: presupposing ¬p while asserting B(a)(¬p) is causally coherent — only the crossed profile is ruled out.

Deriving the attestation table

def RobertsOzyildiz2025.presupClassToCausalVars : Glass2025.PresupClass → Option (BeliefVar × BeliefVar)

The causal variables checked by the PLC for each presuppositional class: factives pair p with B(a)(p), contrafactives ¬p with B(a)(p); the PLC does not apply to nonfactives (no presupposition) or postsuppositional profiles.

Equations

• RobertsOzyildiz2025.presupClassToCausalVars Glass2025.PresupClass.factive = some (RobertsOzyildiz2025.BeliefVar.p, RobertsOzyildiz2025.BeliefVar.B_a_p)
• RobertsOzyildiz2025.presupClassToCausalVars Glass2025.PresupClass.contrafactive = some (RobertsOzyildiz2025.BeliefVar.not_p, RobertsOzyildiz2025.BeliefVar.B_a_p)
• RobertsOzyildiz2025.presupClassToCausalVars Glass2025.PresupClass.nonfactive = none
• RobertsOzyildiz2025.presupClassToCausalVars Glass2025.PresupClass.other = none

noncomputable def RobertsOzyildiz2025.presupClassSatisfiesPLC (pc : Glass2025.PresupClass) : Option Bool

PLC verdict per class: none where the PLC does not apply.

Equations

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

theorem RobertsOzyildiz2025.presupClassIsValid_eq_via_plc (pc : Glass2025.PresupClass) : Glass2025.presupClassIsValid pc = (presupClassSatisfiesPLC pc).getD true

[Gla25]'s attestation table is derived from the PLC: a class is attested iff it satisfies the PLC or the PLC does not apply.

def RobertsOzyildiz2025.contrafactivePartialProp {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) (agent : E) (p : W → Prop) (worlds : List W) : Semantics.Presupposition.PartialProp W

PartialProp of the hypothetical contrafactive: presupposes ¬p, asserts belief in p — the causally incoherent profile.

Equations

• RobertsOzyildiz2025.contrafactivePartialProp R agent p worlds = { presup := fun (w : W) => ¬p w, assertion := fun (w : W) => Doxastic.BoxAt R agent w worlds p }