Roberts and Özyıldız (2025): A causal explanation for the contrafactive gap

This file formalizes the paper's explanation of the absence of contrafactive predicates, verbs that would presuppose the falsity of their complement while asserting belief in it. The Predicate Lexicalization Constraint requires the presupposition of a predicate to be causally upstream of its at-issue content in the normative model of belief formation, a causal chain running from one variable to another when altering the first can alter the second, Upstream. In the belief-formation model a fact generates indicators for itself, experience of an indicator is acquaintance with it, acquaintance forms belief, and a fact generates no indicator for its negation, beliefModel; the truth of a proposition therefore manipulates belief in it, know_plc, whereas its falsity does not, contra_plc, which is the gap. Predicates carrying the contrafactive inference are eventive: the Dutch deception verb wijsmaken and hallucinate satisfy the constraint through an intervening node of deception or distortion, wijsmaken_plc, and cutting that node returns the deficient configuration. The postsuppositional Mandarin yǐwéi lies outside the constraint, so the attestation table of [Gla25] follows, attested_iff.

Implementation notes

Models are deterministic Boolean causal models whose exogenous variables are the fields of a context. The paper's first link makes the fact sufficient but not necessary for its indicators; in the normative model, without forged evidence, the indicator copies the fact. The normative context makes the experience conditions true and every other exogenous variable false, and the manipulation test intervenes on the presupposed fact alone. The paper's causal chain is a template over the choice of proposition and attitude holder, and the model is that template.

References

• T. Roberts, D. Özyıldız, A causal explanation for the contrafactive gap (2025)
• L. Glass, Attested versus unattested contrafactive belief verbs (2025)
• J. Pearl, Causality: models, reasoning, and inference (2009)

def RobertsOzyildiz2025.Upstream {U : Type u_1} {V : Type u_2} [DecidableEq V] (M : CausalModel U V fun (x : V) => Bool) [M.IsAcyclic] (u : U) (c e : V) : Prop

In the context u, the variable c is causally upstream of e when setting c true and setting it false give e different values.

Equations

• RobertsOzyildiz2025.Upstream M u c e = (M.solve (Function.update ⊥ c ↑true) u e ≠ M.solve (Function.update ⊥ c ↑false) u e)

@[instance_reducible]

noncomputable instance RobertsOzyildiz2025.instDecidableUpstreamOfFintype {U : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (M : CausalModel U V fun (x : V) => Bool) [M.IsAcyclic] (u : U) (c e : V) : Decidable (Upstream M u c e)

Equations

• RobertsOzyildiz2025.instDecidableUpstreamOfFintype M u c e = { decide := !decide (M.solve (Function.update ⊥ c ↑true) u e = M.solve (Function.update ⊥ c ↑false) u e), reflects_decide := ⋯ }

theorem RobertsOzyildiz2025.not_upstream_of_not_reflTransGen {U : Type u_1} {V : Type u_2} [DecidableEq V] {M : CausalModel U V fun (x : V) => Bool} [M.IsAcyclic] {c e : V} (h : ¬Relation.ReflTransGen M.graph.Adj c e) (u : U) : ¬Upstream M u c e

A variable with no directed path to another is not upstream of it.

The belief-formation model

inductive RobertsOzyildiz2025.V : Type

The variables of belief formation for a proposition and for its negation: the fact, an indicator for it, the agent's experience of the indicator, acquaintance with it, and the resulting belief.

• p : V
• indicP : V
• expP : V
• acqP : V
• beliefP : V
• notP : V
• indicNotP : V
• expNotP : V
• acqNotP : V
• beliefNotP : V

@[instance_reducible]

instance RobertsOzyildiz2025.instDecidableEqV : DecidableEq V

Equations

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

@[instance_reducible]

instance RobertsOzyildiz2025.instFintypeV : Fintype V

Equations

• RobertsOzyildiz2025.instFintypeV = { elems := { val := ↑RobertsOzyildiz2025.V.enumList, nodup := RobertsOzyildiz2025.V.enumList_nodup }, complete := RobertsOzyildiz2025.instFintypeV._proof_1 }

def RobertsOzyildiz2025.instReprV.repr : V → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• RobertsOzyildiz2025.instReprV.repr RobertsOzyildiz2025.V.p prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RobertsOzyildiz2025.V.p")).group prec✝

@[instance_reducible]

instance RobertsOzyildiz2025.instReprV : Repr V

Equations

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

def RobertsOzyildiz2025.edges : Finset (V × V)

A fact generates an indicator for itself, experience of the indicator gives acquaintance with it, and acquaintance forms belief; the chains for a proposition and for its negation do not cross.

Equations

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

structure RobertsOzyildiz2025.Context : Type

The context settles the facts and whether the agent experiences their indicators, each false unless set.

• p : Bool
• expP : Bool
• notP : Bool
• expNotP : Bool

def RobertsOzyildiz2025.beliefModel : CausalModel Context V fun (x : V) => Bool

The normative model of belief formation: an indicator exists when its fact holds, acquaintance is the existence of the indicator together with experience of it, and belief follows acquaintance. The context settles the facts and the experience conditions.

Equations

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

@[instance_reducible]

instance RobertsOzyildiz2025.instDecidableRelVAdjGraphContextBoolBeliefModel : DecidableRel beliefModel.graph.Adj

Equations

• RobertsOzyildiz2025.instDecidableRelVAdjGraphContextBoolBeliefModel w v = RobertsOzyildiz2025.instDecidableRelVAdjGraphContextBoolBeliefModel._aux_1 w v

instance RobertsOzyildiz2025.instIsAcyclicContextVBoolBeliefModel : beliefModel.IsAcyclic

def RobertsOzyildiz2025.normative : Context

In the normative context the agent experiences whatever indicators exist.

Equations

• RobertsOzyildiz2025.normative = { expP := true, expNotP := true }

The Predicate Lexicalization Constraint

theorem RobertsOzyildiz2025.know_plc : Upstream beliefModel normative V.p V.beliefP

Know satisfies the constraint: the truth of the complement manipulates belief in it, through the indicator and acquaintance with it.

theorem RobertsOzyildiz2025.contra_plc : ¬Upstream beliefModel normative V.notP V.beliefP

The hypothetical contra violates the constraint: the falsity of the complement does not manipulate belief in it, because a fact generates indicators only for itself, so no path runs from the falsity to the belief.

theorem RobertsOzyildiz2025.contra_plc' : ¬Upstream beliefModel normative V.p V.beliefNotP

The template of the generalized constraint, oriented as the paper draws it: the fact does not manipulate belief in its negation.

def RobertsOzyildiz2025.SatisfiesPLC : Glass2025.Profile → Prop

The constraint's verdict on the profiles of [Gla25]: for a factive and for the hypothetical strong contrafactive, whether the presupposed fact manipulates belief in the complement; a nonfactive presupposes nothing and yǐwéi's falsity inference is a postsupposition on the output context, so the constraint does not apply.

Equations

• One or more equations did not get rendered due to their size.
• RobertsOzyildiz2025.SatisfiesPLC Glass2025.Profile.nonfactive = True
• RobertsOzyildiz2025.SatisfiesPLC Glass2025.Profile.weakContrafactive = True

theorem RobertsOzyildiz2025.attested_iff (pr : Glass2025.Profile) : pr.Attested ↔ SatisfiesPLC pr

The attestation table follows from the constraint: a profile is attested iff it satisfies the constraint where the constraint applies.

Eventive predicates with the contrafactive inference

inductive RobertsOzyildiz2025.W : Type

The variables of wijsmaken: the complement's falsity, the object's prior lack of the belief, the subject's fooling the object, and the object's resulting belief.

• notRich : W
• notBeliefPrior : W
• fool : W
• beliefRich : W

@[instance_reducible]

instance RobertsOzyildiz2025.instDecidableEqW : DecidableEq W

Equations

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

@[instance_reducible]

instance RobertsOzyildiz2025.instFintypeW : Fintype W

Equations

• RobertsOzyildiz2025.instFintypeW = { elems := { val := ↑RobertsOzyildiz2025.W.enumList, nodup := RobertsOzyildiz2025.W.enumList_nodup }, complete := RobertsOzyildiz2025.instFintypeW._proof_1 }

def RobertsOzyildiz2025.instReprW.repr : W → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance RobertsOzyildiz2025.instReprW : Repr W

Equations

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

def RobertsOzyildiz2025.wijsmakenEdges : Finset (W × W)

Falsity and prior lack of belief are jointly necessary for fooling, which is sufficient for the belief.

Equations

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

structure RobertsOzyildiz2025.WijsmakenContext : Type

The context settles the complement's falsity and the object's prior lack of the belief.

• notRich : Bool
• notBeliefPrior : Bool

def RobertsOzyildiz2025.wijsmaken (eventive : Bool) : CausalModel WijsmakenContext W fun (x : W) => Bool

The model of wijsmaken, and the model with the eventive node cut, on which the belief no longer depends on anything.

Equations

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

@[instance_reducible]

instance RobertsOzyildiz2025.instDecidableRelWAdjGraphWijsmakenContextBoolWijsmaken (eventive : Bool) : DecidableRel (wijsmaken eventive).graph.Adj

Equations

• RobertsOzyildiz2025.instDecidableRelWAdjGraphWijsmakenContextBoolWijsmaken eventive w v = RobertsOzyildiz2025.instDecidableRelWAdjGraphWijsmakenContextBoolWijsmaken._aux_1 eventive w v

instance RobertsOzyildiz2025.instIsAcyclicWijsmakenContextWBoolWijsmaken (eventive : Bool) : (wijsmaken eventive).IsAcyclic

def RobertsOzyildiz2025.noPriorBelief : WijsmakenContext

The context in which the object did not already hold the belief.

Equations

• RobertsOzyildiz2025.noPriorBelief = { notBeliefPrior := true }

theorem RobertsOzyildiz2025.wijsmaken_plc : Upstream (wijsmaken true) noPriorBelief W.notRich W.beliefRich

Wijsmaken satisfies the constraint: the complement's falsity manipulates the object's belief, through the act of fooling.

theorem RobertsOzyildiz2025.wijsmaken_cut : ¬Upstream (wijsmaken false) noPriorBelief W.notRich W.beliefRich

With the eventive node cut, the falsity presupposition is no longer upstream of the belief: the configuration of contra.

inductive RobertsOzyildiz2025.H : Type

The variables of hallucinate: the complement's falsity, the distortion of the input, and the resulting belief.

• notLoves : H
• distortion : H
• beliefLoves : H

@[instance_reducible]

instance RobertsOzyildiz2025.instDecidableEqH : DecidableEq H

Equations

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

@[instance_reducible]

instance RobertsOzyildiz2025.instFintypeH : Fintype H

Equations

• RobertsOzyildiz2025.instFintypeH = { elems := { val := ↑RobertsOzyildiz2025.H.enumList, nodup := RobertsOzyildiz2025.H.enumList_nodup }, complete := RobertsOzyildiz2025.instFintypeH._proof_1 }

@[instance_reducible]

instance RobertsOzyildiz2025.instReprH : Repr H

Equations

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

def RobertsOzyildiz2025.instReprH.repr : H → ℕ → Std.Format

Equations

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

def RobertsOzyildiz2025.hallucinateEdges : Finset (H × H)

Falsity is necessary for distortion, which is necessary for the belief.

Equations

• RobertsOzyildiz2025.hallucinateEdges = {(RobertsOzyildiz2025.H.notLoves, RobertsOzyildiz2025.H.distortion), (RobertsOzyildiz2025.H.distortion, RobertsOzyildiz2025.H.beliefLoves)}

structure RobertsOzyildiz2025.HallucinateContext : Type

The context settles the complement's falsity.

• notLoves : Bool

def RobertsOzyildiz2025.hallucinate (eventive : Bool) : CausalModel HallucinateContext H fun (x : H) => Bool

The model of hallucinate, and the model with the distortion cut.

Equations

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

@[instance_reducible]

instance RobertsOzyildiz2025.instDecidableRelHAdjGraphHallucinateContextBoolHallucinate (eventive : Bool) : DecidableRel (hallucinate eventive).graph.Adj

Equations

• RobertsOzyildiz2025.instDecidableRelHAdjGraphHallucinateContextBoolHallucinate eventive w v = RobertsOzyildiz2025.instDecidableRelHAdjGraphHallucinateContextBoolHallucinate._aux_1 eventive w v

instance RobertsOzyildiz2025.instIsAcyclicHallucinateContextHBoolHallucinate (eventive : Bool) : (hallucinate eventive).IsAcyclic

theorem RobertsOzyildiz2025.hallucinate_plc : Upstream (hallucinate true) { } H.notLoves H.beliefLoves

Hallucinate satisfies the constraint through the distortion.

theorem RobertsOzyildiz2025.hallucinate_cut : ¬Upstream (hallucinate false) { } H.notLoves H.beliefLoves

With the distortion cut, the falsity presupposition is no longer upstream of the belief.