Formalizing Statistical Causality via Modal Logic
Yusuke Kawamoto1,2 , Tetsuya Sato3 , and Kohei Suenaga4
1

AIST, Tokyo, Japan
PRESTO, JST, Tokyo, Japan
3
Tokyo Institute of Technology, Tokyo, Japan
4
Kyoto University, Kyoto, Japan
2

Abstract. We propose a formal language for describing and explaining
statistical causality. Concretely, we define Statistical Causality Language(StaCL) for expressing causal effects and specifying the requirements forcausal inference. StaCL incorporates modal operators for interventions
to express causal properties between probability distributions in different
possible worlds in a Kripke model. We formalize axioms for probability
distributions, interventions, and causal predicates using StaCL formulas.
These axioms are expressive enough to derive the rules of Pearl’s docalculus. Finally, we demonstrate by examples that StaCL can be used
to specify and explain the correctness of statistical causal inference.

1

Introduction

Statistical causality has been gaining significant importance in a variety of research fields. In particular, in life sciences, more and more researchers have beenusing statistical techniques to discover causal relationships from experiments
and observations. However, these statistical methods can easily be misused or
misinterpreted. In fact, it is reported that many research articles have serious
errors in the applications and interpretations of statistical methods [8, 26].
A common mistake is to misinterpret statistical correlation as statisticalcausality. Notably, when we analyze observational data without experimental
interventions, we may overlook some requirements for causal inference and makewrong calculations, leading to incorrect conclusions about the causality.
For this reason, the scientific community has developed guidelines on manyrequirements for statistical analyses [36, 28]. However, since there is no formal
language to describe the entire procedures and their requirements, we refer toguidelines manually and cannot formally guarantee the correctness of analyses.
To address these problems, we propose a logic-based approach to formalizing and explaining the correctness of statistical causal inference. Specifically,
we introduce a formal language called statistical causality language (StaCL) toformally describe and check the requirements for statistical causal inference. We
consider this work as the first step to building a framework for formally guaranteeing and explaining the reliability of scientific research.
Contributions. Our main contributions are as follows:2

Y. Kawamoto et al.

– We propose statistical causality language (StaCL) for formalizing and explaining statistical causality by using modal operators for interventions.
– We define a Kripke model for statistical causality. To formalize not only
statistical correlation but also statistical causality, we introduce a data generator in a possible world to model a causal diagram in a Kripke model.
– We introduce the notion of causal predicates to express statistical causality
and interpret them using a data generator instead of a valuation in a Kripke
model. In contrast, (classical) predicates are interpreted using a valuation ina Kripke model to express only statistical correlations.
– We introduce a sound deductive system AXCP for StaCL with axioms forprobability distributions, interventions, and causal predicates. These axioms
are expressive enough to reason about all causal effects identifiable by Pearl’s
do-calculus [29]. We show that AXCP can reason about the correctness of
causal inference methods (e.g., backdoor adjustment). Unlike prior work,
AXCP does not aim to conduct causal inference about a specific causal
diagram; rather, it concerns the correctness of the inference methods for any
diagram. To the best of our knowledge, ours appears to be the first modal
logic that can specify and reason about the requirements for causal inference.
Related Work. Many studies on causal reasoning rely on causal diagrams [30].
Whereas they aim to reason about a specific diagram, our logic-based approachaims to specify and reason about the requirements for causal inference methods.
Logic-based approaches for formalizing causal reasoning have been proposed.
To name a few, Halpern and Pearl provide logic-based definitions of actual causes
where logical formulas with events formalize counterfactuals [12, 13, 11]. Probabilistic logical languages [19] are proposed to axiomatize causal reasoning withobservation, intervention, and counterfactual inference. Unlike our logic, however, their framework does not aim to syntactically derive the correctness ofstatistical causal inference. The causal calculus [27] is used to provide a logicalrepresentation [4, 3] of Pearl [30]’s structural causal model. The counterfactualobservational language [1] can reason about interventionist counterfactuals andhas an axiomatization that is complete w.r.t. a causal team semantics. A modal
logic in [2] integrates causal and epistemic reasoning. While these works deal
with deterministic cases only, our StaCL can reason about statistical causality
in probabilistic settings.
There have been studies on incorporating probabilities into team semantics [15]. For example, team semantics is used to deal with the dependence andindependence among random variables [6, 5]. A probabilistic team semantics isprovided for a first-order logic that can deal with conditional independence [7]. A
team semantics is also introduced for logic with exact/approximate dependence
and independence atoms [14]. Unlike our StaCL, however, these works do notallow for deriving the do-calculus or the correctness of causal inference methods.
Concerning the axiomatic characterization of causality, Galles and Pearl [9]prove that the axioms of composition, effectiveness, and reversibility are soundand complete with respect to the structural causal models. They also show thatthe reversibility axiom can be derived from the composition axiom if the causal

Formalizing Statistical Causality via Modal Logic

3

diagram is acyclic (i.e., has no feedback loop). Halpern [10] provides axiomatizations for more general classes of causal models with feedback and with equations
that may have no solutions. In contrast, our deductive system AXCP has axioms
for causal predicates and two forms of interventions that can derive the rules of
Pearl’s do-calculus [29], while being equipped with axioms corresponding to thecomposition and effectiveness axioms mentioned above only for acyclic diagrams.
For the efficient computation of causal reasoning, constraint solving is applied[17, 18, 34]. Probabilistic logic programming is used to encode and reason about
a specific causal diagram [31]. These are orthogonal to the goal of our work.
Finally, a few studies propose modal logic for statistical methods. Statistical
epistemic logic [20–22] specifies various properties of machine learning. Belief
Hoare logic [24, 25] can reason about statistical hypothesis testing programs.
However, unlike our StaCL, these cannot reason about statistical causality.

2

Illustrating Example

We first present a simple example to explain our framework.
Example 1 (Drug’s efficacy). We attempt to check a drug’s efficacy for a disease
by observing a situation where some patients take a drug and the others do not.
Table 1 shows the recovery rates and the numbers of patients treated with/without the drug. For both males and females, more patients recover by taking
the drug. However, for the combined population, the recovery rate with the drug
(0.73) is less than that without it (0.80). This inconsistency is called Simpson’s
paradox [33], showing the difficulty of identifying causality from observed data.
To model this, we define three variables: a treatment x (1 for drug, 0 for
no-drug), an outcome y (1 for recovery, 0 for non-recovery), and a gender z.
Fig. 1a depicts their causal dependency; the arrow x A y denotes that y depends
on x. The causal effect p(y|do(x = c)) of a treatment x = c on an outcome y [30]is defined as the distribution of y in case y were generated from x = c (Fig. 1b).
However, since the gender z influences the choice of the treatment x in reality(Fig. 1a), the causal effect p(y|do(x = c)) depends on the common cause z of x
and y and differs from the correlation p(y|x = c). Indeed, in Table 1, 80 % offemales chose to take the drug (x = 1) while only 20 % of males did so; thisdependency of x on the gender z leads to Simpson’s paradox in Table 1. Thus,
calculating the causal effect requires an “adjustment” for z, as explained below.
Overview of the Framework. We describe reasoning about the causal effectin Example 1 using logical formulas in our formal language StaCL (Section 5).
def
We define φRCT = ⌈c/x⌉(c0 = y) to express a randomized controlled trial(RCT), where we randomly divide the patients into two groups: one taking the
drug (x = 1) and the other not (x = 0). This random choice of the treatment x is
expressed by the intervention ⌈c/x⌉ for c = 0, 1 in the diagram G⌈c/x⌉ (Fig. 1b).
Since x is independent of z in G⌈c/x⌉, the causal effect p(y|do(x = c)) of x on theoutcome y is given as y’s distribution c0 observed in the experiment in G⌈c/x⌉.

4

Y. Kawamoto et al.

Table 1: Recovery rates of patients
with/without taking a drug.
Drug No-drug
x=1
x=0
Male
0.90
0.85
(18/20) (68/80)
Female 0.69
0.60
(55/80) (12/20)
Total
0.73
0.80
(73/100) (80/100)

z

@
R
@

-y
x
(a) The actual diagram G with a gender (confounder) z, a treatment x, and an outcome y.
c
z
?

@
R
@

-y
x
(b) The diagram G⌈c/x⌉ with an intervention to x.
Fig. 1: Causal diagrams in Example 1.

def

In contrast, φBDA = (f = y|z,x=c ∧ c1 = z ∧ c0 = f (c1 ) ↓y ) describes
the inference about the causal effect from observation without intervention tox (Fig. 1a). This saves the cost of the experiment and avoids ethical issues in
random treatments. Instead, to avoid Simpson’s paradox, the inference φBDA
conducts a backdoor adjustment (Section 7) to cope with the confounder z.
Concretely, the backdoor adjustment φBDA computes x’s causal effect on ydef
as follows. We first obtain the conditional distribution f = y|z,x=c and the priordef
c1 = z. Then we conduct the adjustment by calculating the joint distributiondef
f (c1 ) from f and c1 and then taking the marginal distribution c0 = f (c1 ) ↓y .
The resulting c0 is the same as the c0 in the RCT experiment φRCT ; that is, thebackdoor adjustment φBDA can compute the causal effect obtained by φRCT .
For this adjustment, we need to check the requirement pa(z, x) ∧ pos(x :: z),that is, z is x’s parent in the diagram G and the joint distribution x :: z satisfies
the positivity (i.e., it takes each value with a non-zero probability).
Now we formalize the correctness of this causal inference method (for any
diagram G) as the judgment expressing that under the above requirements, thebackdoor adjustment computes the same causal effect as the RCT experiment:pa(z, x) ∧ pos(x :: z) ⊢g φRCT ↔ φBDA .

(1)

By deriving this judgment in a deductive system called AXCP (Section 6), weshow the correctness of this causal inference method for any diagram (Section 7).
We show all proofs of the technical results in Appendix.

3

Language for Data Generation

In this section, we introduce a language for describing data generation.
Constants and Causal Variables. We introduce a set Const of constants
to denote probability distributions of data values and a set dConst ⊆ Constof deterministic constants, each denoting a single data value (strictly speaking,denoting a distribution having a single data value with probability 1).
We introduce a finite set CVar of causal variables. A tuple ⟨x1 , . . . , xk ⟩ ofcausal variables represents the joint distribution of k variables x1 , . . . , xk . We

Formalizing Statistical Causality via Modal Logic

5

denote the set of all non-empty (resp. possibly empty) tuples of variables by
CVar+ (resp. CVar∗ ). We use the bold font for a tuple; e.g., x = ⟨x1 , . . . , xk ⟩. We
write size(x) for the dimension k of a tuple x. We assume that the variables ina tuple x are sorted lexicographically.
For disjoint tuples x and y, x :: y denotes the joint distribution of x and y.
Formally, ‘::’ is not a function symbol, but a meta-operator on CVar∗ ; x::y is thetuple obtained by merging x and y and sorting the variables lexicographically.
We use conditional causal variables y|z,x=c to denote the conditional distribution of y given z and x = c. We write FVar for the set of all conditional causal
variables. For a conditional distribution y|x and a prior distribution x, we writey|x (x) for the joint distribution x :: y.
Terms. We define terms to express how data are generated. Let Fsym be a
set of function symbols denoting algorithms. We define the set CTerm of causal
terms as the terms of depth at most 1; i.e., u ::= c | f (v, . . . , v) where c ∈ Const,f ∈ Fsym, and v ∈ CVar ∪ Const. For example, f (c) denotes a data generated
by an algorithm f with input c. We denote the set of variables (resp. the set of
constants) occurring in a term u by fv(u) (resp. fc(u)).
We also define the set Term of terms by the BNF: u ::= x | c | f (u, . . . , u),where x ∈ CVar+ , c ∈ Const, and f ∈ Fsym ∪ FVar. Unlike CTerm, terms in Term
may repeatedly apply functions to describe multiple steps of data generation.
We introduce the special function symbol ↓x for marginalization. y ↓x denotes the marginal distribution of x given a joint distribution y; e.g., for a joint
distribution x = ⟨x0 , x1 ⟩, x ↓x0 expresses the marginal distribution x0 . We also
introduce the special constant ⊥ for undefined values.
Data Generators. To describe how data are generated, we introduce the notionof a data generator as a function g : CVar → CTerm ∪ {⊥} that maps a causal
variable x to a causal term representing how the data assigned to x is generated.
If g(y) = u for u ∈ CTerm and y ∈ CVar, we write u Ag y. For instance, thedata generator g in Fig. 2 models the situation in Example 1. To express thata variable x’s value is generated by an algorithm f1 with an input z, the data
generator g maps x to f1 (z), i.e., f1 (z) Ag x. Since the causal term f1 (z)’s depth
is at most 1, z represents the direct cause of x. We denote the set of all variables
x satisfying g(x) ̸= ⊥ by dom(g), and the range of g by range(g).
We assume the following at-most-once
Causal diagram condition: Each function symbol and conData generator g
G given from g
stant can be used at most once in a single
dom(g) = {x, y, z}zdata generator. This ensures that different
f1 (z) Ag x@
R@sampling uses different randomness and isxy
f2 (z, x) Ag ydenoted by different symbols.
We say that a data generator g is finite
Fig. 2: The data generator andifdom(g)
is a finite set. We say that a datacausal diagram for Example 1.
generator g is closed if no undefined variableoccurs in the terms that g assigns to variables, namely, fv(range(g)) ⊆ dom(g).
We write x ≺g y iff y’s value depends on x’s, i.e., there are variables z1 , . . . , zi(i ≥ 2) such that z1 = x, zi = y, and zj ∈ fv(g(zj+1 )) for 1 ≤ j ≤ i − 1. A data

6

Y. Kawamoto et al.

generator g is acyclic if ≺g is a strict partial order over dom(g). Then we can
avoid the cyclic definitions of g. E.g., the data generator g1 defined by f (z)Ag1 x
and f (c) Ag1 z is acyclic, whereas g2 by f (z) Ag2 x and f (x) Ag2 z is cyclic.

4

Kripke Model for Statistical Causality

In this section, we introduce a Kripke model for statistical causality.
We write O for the set of all data values we deal with, such as the Boolean
values, integers, real numbers, and lists of data values. We write ⊥ for the undefined value. For a set S, we denote the set of all probability distributions over S
by DS. For a probability distribution m ∈ DS, we write supp(m) for the set of
m’s non-zero probability elements.
Causal Diagrams. To model causal relations corresponding to a given data
generator g, we consider a causal diagram G = (U, V, E) [30] where U ∪ V is theset of all nodes and E is the set of all edges such that:def– U = fc(range(g)) ⊆ Const is a set of symbols called exogenous variables that
denote distributions of data;def– V = dom(g) ⊆ CVar is a set of symbols called endogenous variables that may
depend on other variables;def– E = {x → y ∈ V × V | x ∈ fv(g(y))} ∪ {c → y ∈ U × V | c ∈ fc(g(y))} is the setof all structural equations, i.e., directed edges (arrows) denoting the directcausal relations between variables defined by the data generator g.
For instance, in Fig. 2, Example 1 is modeled as the causal diagram G.
Since a causal term’s depth is at most 1, g specifies all information for defining
G. By g’s acyclicity, G is a directed acyclic graph (DAG) (See Proposition 4 inAppendix A.2 for details).
Pre-/Post-Intervention Distributions. For a causal diagram G = (U, V, E)
and a tuple y ⊆ V , we write PG (y) for the joint distribution of y over Osize(y)generated according to G. As shown in the standard textbooks (e.g., [30]), PG (V )is factorized into conditional distributions according to G as follows:
def Q
PG (V ) = yi ∈V PG (yi | pa G (yi )),(2)
where pa G (yi ) is the set of parent variables of yi in G. For example, in Fig. 2,
for V = {x, y, z}, PG (V ) = PG (y | x, z) PG (x | z) PG (z).
For tuples x ⊆ V and o ⊆ O with size(x) = size(o), the post-intervention
distribution PG (V | do(x=o)) is the joint distribution of V after x is assigned oand all the variables dependent on x in G are updated by x := o as follows:Q yi ∈V \x PG (yi | pa G (yi ))def
PG (V | do(x = o)) =for values of V consistent with x = o0otherwise.
For instance, in Fig. 2, PG (y, z|do(x = o)) = PG (y|x = o, z) PG (z) for any o ∈ O.

Formalizing Statistical Causality via Modal Logic

7

Possible Worlds. We introduce the notion of a possible world to define theprobability distribution of causal variables from a data generator. Formally, apossible world is a tuple (g, ξ, m) of (i) a finite and acyclic data generator g :CVar → CTerm ∪ {⊥}, (ii) an interpretation ξ that maps a function symbol in
Fsym with arity k ≥ 0 to a function from Ok to DO, and (iii) a memory mthat maps a tuple of variables to a joint distribution of data values, which isdetermined by g and ξ. We denote these components of a world w by gw , ξw ,and mw , and the set of all defined variables in w by Var(w) = dom(mw ).
The interpretation ξ can be constructed using a probability distribution I
over an index set I and a family {ξ r }r∈I of interpretations each mapping afunction symbol f with arity k ≥ 0 to a deterministic function ξ r (f ) from Ok to
O. Then ξ(f ) maps data values o to the probability distribution over O obtainedby randomly drawing an index r from I and then computing ξ r (f )(o).
If k = 0, f is a constant and ξ r (f ) ∈ O, hence ξ(f ) ∈ DO is a distribution ofdata values. For the undefined constant, we assume ξ r (⊥) = ⊥.
Interpretation of Terms. Terms are interpreted in a possible world w =(ξ, g, m) as follows. First, for each index r ∈ I, we define the interpretation[[_]]rξ,g that maps a tuple of k terms to k data values in O or ⊥ by:[[x]]rξ,g = [[g(x)]]rξ,g[[⟨u1 , . . . , uk ⟩]]rξ,g = ([[u1 ]]rξ,g , . . . , [[uk ]]rξ,g )[[c]]rξ,g = ξ r (c)[[f (u1 , . . . , uk )]]rξ,g = ξ r (f )([[⟨u1 , . . . , uk ⟩]]rξ,g ).

For instance, in Fig. 2, we have [[x]]rξ,g = [[g(x)]]rξ,g = [[f1 (z)]]rξ,g = ξ r (f1 )([[z]]rξ,g ),where the interpretation of z does not depend on that of x due to g’s acyclicity.
We define the probability distribution [[u]]w over O by randomly drawing r andthen computing [[u]]rξ,g . Similarly, we define [[⟨u1 , . . . , uk ⟩]]w via [[⟨u1 , . . . , uk ⟩]]rξ,g .
We remark that the interpretation [[_]]w defines the joint distribution PGw
of all variables in the causal diagram Gw ; e.g., [[y|z ]]w = PGw (y | z) (See Proposition 5 in Appendix A.2 for details). A function symbol f is interpreted as thefunction ξ(f ) that maps data values in O to the distribution over O. We define
the memory m by m(x) = [[x]]w for all x ∈ CVar+ . Notice that [[_]]w is definedusing g and ξ without using m.
We expand the interpretation [[_]]w to a conditional causal variable y|z,x=c ∈FVar to interpret it as a function that maps a value c′ of z to the distribution[[(x :: y :: z)|z=c′ ,x=c ]]w . We then have [[y|z,x=c (z|x=c )]]w = [[y|z,x=c ]]w ([[z|x=c ]]w ).
For the sake of reasoning in Section 6, for each data generator g, x ∈ CVar+ ,and y|z,x=c ∈ FVar, we introduce a constant c(g,x) and a function symbolf (g,y|z,x=c ) . For brevity, we often omit the superscripts of these symbols.
Eager/Lazy Interventions. We introduce two forms of interventions andtheir corresponding intervened worlds. Intuitively, in a causal diagram, an eager
intervention ⌈c/x⌉ expresses the removal of all arrows pointing to a variable x byreplacing x’s value with c.
In contrast, a lazy intervention ⌊c/x⌋ expresses the removal of all arrows
emerging from x, which does not change the value of x itself but affects thevalues of the variables dependent on x, computed using [[c]] (instead of [[x]]) as
the value of x.

8

Y. Kawamoto et al.

For instance, Fig. 3 shows how two interventions ⌈c/x⌉ and ⌊c/x⌋ change thedata generator and the causal diagram in a world w that models Example 1.
For a world w and a c ∈ dConst,
World Data generator Causal diagram
wedefine an eagerly intervened worldz
f1 (z) A x;
c/x⌉ as the world where [[c]]w⌈
w is asw@
R@
f2 (z, x) A ysigned to x and is used to compute thexyother variables dependent on x. Forczc A x;w⌈c/x⌉@
mally, w⌈c/x⌉ is defined by ξw⌈c/x⌉ =?
R@
f2 (z, x) A y-yx
ξw , gw⌈c/x⌉ (y) = c if y = x, andz
f1 (z) A x;
gw⌈c/x⌉ (y) = gw (y) if y ̸= x. For inw⌊c/x⌋@
R@
stance, in Fig. 3, in the world w⌈c/x⌉, we
f2 (z, c) A y
x cy
use the value of c to compute [[x]]w⌈c/x⌉ =ξw (c) and [[y]]w⌈c/x⌉ = [[f2 (z, x)]]w⌈c/x⌉ =Fig. 3: Eager/lazy interventions.
[[f2 (z, c)]]w .
Then the interpretation [[_]]w⌈c/x⌉ defines the joint distribution of all variablesin the causal diagram Gw after the intervention x := [[c]]w ; e.g., [[y|z ]]w⌈c/x⌉ =PGw (y | do(x = [[c]]w ), z) (See Proposition 5 in Appendix A.2 for details).
We next define a lazily intervened world w⌊c/x⌋ as the world where x’s value
is unchanged but the other variables dependent on x are computed using [[c]]w
instead of [[x]]w . Formally, w⌊c/x⌋ is defined by ξw⌊c/x⌋ = ξw , gw⌊c/x⌋ (y) = x if y =x, and gw⌊c/x⌋ (y) = gw (y)[x 7→ c] if y ̸= x. E.g., in Fig. 3, [[x]]w⌊c/x⌋ = [[f1 (z)]]w .
For x = ⟨x1 , . . . , xk ⟩ and c = ⟨c1 , . . . , ck ⟩, we define ⌈c/x⌉ from the simultaneous replacement gw⌈c1/x1 ,...,ck/xk ⌉ . We also define ⌊c/x⌋ analogously.
Kripke Model. Let Psym be a set of predicate symbols. For a variable tuple
x and a deterministic constant tuple c, we introduce an intervention relationwR⌈c/x⌉ w′ that expresses a transition from a world w to another w′ by theintervention ⌈c/x⌉; namely, R⌈c/x⌉ = {(w, w′ ) ∈ W × W | w′ = w⌈c/x⌉}.
Then we define a Kripke model for statistical causality as a tuple M = (W,(R⌈c/x⌉)x∈CVar+,c∈dConst+ , V) consisting of: (1) a set W of all possible worlds overthe set CVar of causal variables; (2) for each x ∈ CVar+ and c ∈ dConst+ ,an intervention relation R⌈c/x⌉ ; (3) a valuation V that maps a k-ary predicate
symbol η ∈ Psym to a set V(η) of k-tuples of distributions.
Notice that different worlds w and w′ in W may have different data generators
gw and gw′ corresponding to different causal diagrams; that is, W specifies all
possible causal diagrams. Furthermore, different worlds w and w′ may also havedifferent interpretations ξw and ξw′ of function symbols if we do not have theknowledge of functions [23].

5

Statistical Causality Language

Predicates and Causal Predicates. Classical predicates in Psym describe
statistical correlation among the distributions of variables, and are interpretedusing a valuation V. For example, pos(x) expresses that x takes each value inthe domain O with a non-zero probability. However, predicates cannot express
the statistical causality among variables, whose interpretation relies on a causal

Formalizing Statistical Causality via Modal Logic

9

diagram. Thus, we introduce a set CPsym of causal predicates (e.g., dsep, nanc,allnanc) and interpret them using a data generator g instead of a valuation V.
Syntax and Semantics of StaCL. We define the set Fml of formulas: Forη ∈ Psym, χ ∈ CPsym, x ∈ Var+ , u ∈ Term+ , c ∈ Const+ , and f ∈ Fsym ∪ FVar,
φ ::= η(x, . . . , x) | χ(x, . . . , x) | u = u | f = f | true | ¬φ | φ ∧ φ | ⌈c/x⌉φ | ⌊c/x⌋φ.
Intuitively, ⌈c/x⌉φ (resp. ⌊c/x⌋φ) expresses that φ is satisfied in the eager (resp.
lazy) intervened world. We assume that each variable appears at most once in
x in ⌈c/x⌉ and ⌊c/x⌋. We use syntax sugar false, ∨, →, and ↔ as usual. Notethat the formulas have no quantifiers over variables.
We interpret a formula in a world w in a Kripke model M by:
M, w |= η(x1 , . . . , xk ) iff ([[x1 ]]w , . . . , [[xk ]]w ) ∈ V(η)′

M, w |= u = u iff [[u]]w = [[u′ ]]w
M, w |= ¬φ iff M, w ̸|= φ
M, w |= ⌈c/x⌉φ iff M, w⌈c/x⌉ |= φM, w |= f = f ′ iff [[f ]]w = [[f ′ ]]w
M, w |= φ ∧ φ′ iff M, w |= φ and M, w |= φ′M, w |= ⌊c/x⌋φ iff M, w⌊c/x⌋ |= φ,where w⌈c/x⌉ and w⌊u/x⌋ are intervened worlds and the interpretation of atomic
formulas with causal predicates χ is given below. For brevity, we often omit M.
Note that η(x1 , . . . , xk ) represents a property of k independent distributions[[x1 ]]w , . . . , [[xk ]]w , where the randomness ri in each [[xi ]]rwi is chosen independently.
In contrast, η(⟨x1 , . . . , xk ⟩) expresses a property of a single joint distribution,
since the same r is used in all of [[x1 ]]rw , . . ., [[xk ]]rw .
Atomic formulas with causal predicates χ are interpreted using a causal diagram Gw corresponding to gw . Let ANC(y) is the set of all ancestors of y in Gw ,and PA(y) be the set of all parent variables of y in Gw . Then:w |= dsep(x, y, z) iff x and y are d-separated by z in Gw
w |= nanc(x, y) iff x ∩ ANC(y) = ∅ and x ∩ y = ∅w |= allnanc(x, y, z) iff x = y \ ANC(z)w |= pa(x, y) iff x = PA(y) and x ∩ y = ∅,where the d-separation 5 of x and y by z [35] is a sufficient condition for theconditional independence of x and y given z (See Appendix A for details).
Formalization of Causal Effect. Conventionally, the conditional probabilityof y given z = o2 after an intervention x = o1 is expressed using the do-operator
by P (y | do(x = o1 ), z = o2 ). This causal effect can be expressed using StaCL:
Proposition 1 (Causal effect) Let w be a world, x, y, z ∈ Var(w)+ be disjoint, c ∈ dConst+ , c′ ∈ Const+ , and f ∈ Fsym. Then:(i) w |= ⌈c/x⌉(c′ = y) iff there is a distribution PGw that is factorized according
to Gw and satisfies PGw (y | do(x = c)) = [[c′ ]]w .
An undirected path in a causal diagram Gw is said to be d-separated by z if it haseither (a) a chain v ′ A v A v ′′ s.t. v ∈ z, (b) a fork v ′v A v ′′ s.t. v ∈ z, or (c) acollider v ′ A vv ′′ s.t. v ̸∈ z ∪ ANC(z). x and y are said to be d-separated by z if
all undirected paths between variables in x and in z are d-separated by z.
A

A

5

10





Y. Kawamoto et al.

Axioms for probability distributions
EqC⊢g c(g,x) = x
EqF⊢g f (g,y|z,x=c ) = y|z,x=c
PD⊢g (pos(x) ∧ c0 = x ∧ f = y|x ∧ c1 = x :: y) → c1 =f (c0 )MPD⊢g x1 ↓x2 = x2 if x2 ⊆ x1

Fig. 4: The axioms of AX for probability distributions, where x, x1 , x2 , y ∈CVar+ are disjoint, c0 , c1 , c(g,x) ∈ Const, f, f (g,y|z,x=c ) ∈ Fsym.


Axioms for eager interventions
DGEI⊢g ⌈c/x⌉φ iff ⊢g⌈c/x⌉ φ
EffectEI⊢g ⌈c/x⌉(x = c)
EqEI
⊢g u1 = u2 ↔ ⌈c/x⌉(u1 = u2 ) if fv(u1 ) = fv(u2 ) = ∅SplitEI⊢g ⌈c1/x1 , c2/x2 ⌉φ → ⌈c1/x1 ⌉⌈c2/x2 ⌉φ′SimulEI⊢g ⌈c1/x1 ⌉⌈c2/x2 ⌉φ → ⌈c1/x′1 , c2/x2 ⌉φ if x′1 = x1 \x2 , c′1 = c1 \c2
RptEI⊢g ⌈c/x⌉φ → ⌈c/x⌉⌈c/x⌉φ
CmpEI⊢g ⌈c1/x1 ⌉(x2 = c2 ) ∧ ⌈c1/x1 ⌉(x3 = u) → ⌈c1/x1 , c2/x2 ⌉(x3 = u)DistrEI ¬⊢g (⌈c/x⌉¬φ) ↔ (¬⌈c/x⌉φ)
DistrEI ∧⊢g (⌈c/x⌉(φ1 ∧ φ2 )) ↔ (⌈c/x⌉φ1 ∧ ⌈c/x⌉φ2 )Axioms for lazy interventions
CondLI⊢g (f = y|x=c ) ↔ ⌊c/x⌋(f = y|x=c ) Other axioms are analogous to eager interventions except for EffectEI .



Axioms for the exchanges of eager and lazy interventions
ExpdEILI ⊢g (⌈c/x⌉c′ = y) ↔ (⌊c/x⌋c′ = y)
ExcdEILI ⊢g pos(z) → (⌈c/x⌉f = y|z )↔(⌊c/x⌋f = y|z )







Fig. 5: The axioms of AX, where x, x1 , x2 , x3 , y, z ∈ CVar+ are disjoint, f ∈Fsym, c, c1 , c2 ∈ dConst+ , c′ ∈ Const+ , u, u1 , u2 ∈ Term+ , and φ, φ1 , φ2 ∈ Fml.

(ii) w |= ⌈c/x⌉(f = y|z ) iff there is a distribution PGw that is factorized according
to Gw and satisfies PGw (y | do(x = c), z) = [[f ]]w .

If x and y are d-separated by z, they are conditionally independent givenz [35] (but not vice versa). StaCL can express this by |=g (dsep(x, y, z)∧pos(z) →y|z,x=c = y|z , where pos(z) means that z takes each value with a positive
probability, and |=g φ is defined as w |=g φ for all world w having the data
generator g. Furthermore, if [[x]]w and [[y]]w are conditionally independent given[[z]]w for any world w with the data generator gw , then they are d-separated by z:|=g (pos(z) → y|z,x=c = y|z ) implies |=g dsep(x, y, z) (See Proposition 15 inAppendix C.1).

Formalizing Statistical Causality via Modal Logic

6

11

Axioms for StaCL

We present a sound deductive system for StaCL in the Hilbert style. Our system
consists of axioms and rules for the judgments of the form Γ ⊢g φ.
The deductive system is stratified into two groups. The system AX, determined by the axioms in Figs. 4 and 5, concerns the derivation of Γ ⊢g φ that
does not involve causal predicates (e.g., pa, nanc, dsep). The system AXCP , determined by the axioms in Fig. 6, concerns the derivation of a formula φ possibly
equipped with causal predicates in a judgment Γ ⊢g φ.
In these systems, we deal only with the reasoning that is independent of acausal diagram. Indeed, in Section 7, we will present examples of reasoning using
the deductive system AXCP that do not refer to a specific causal diagram.
Axioms of AX. Fig. 4 shows the axioms of the deductive system AX, where
we omitted the axioms for propositional logic and equations (PT for the propositional tautologies, MP for the modus ponens, Eq1 for the reflexivity, and Eq2
for the substitutions for formulas). EqC and EqF represent the definitions ofconstants and function symbols corresponding to causal variables. PD describes
the relationships among the prior distribution x, the conditional distribution y|xof y given x, and the joint distribution x :: y. MPD represents the computation↓x2 of the marginal distribution x2 from a joint distribution x1 .
The axioms named with the subscript EI deal with eager intervention. Remarkably, DGEI reduces the derivation of ⊢g ⌈c/x⌉φ, which involves an intervention modality ⌈c/x⌉, to the derivation of ⊢g⌈c/x⌉ φ, which does not involve themodality under the modified data generator g⌈c/x⌉. The axioms DistrEI ¬ andDistrEI ∧ allow for pushing intervention operators outside logical connectives.
The axioms with the subscript LI deal with lazy intervention; they are analogous to the corresponding EI-rules. The axioms with the subscript EILI describe
when an eager intervention can be exchanged with a lazy intervention.
Axioms of AXCP . Fig. 6 shows the axioms for AXCP . DsepCI represents thatd-separation implies conditional independence. DsepSm, DsepDc, DsepWu,
and DsepCn are the semi-graphoid axioms [35], characterizing the d-separation.
However, these well-known axioms are not sufficient to derive the relationships
between d-separation and interventions. Therefore, we introduce two axioms
DsepEI and DsepLI in Fig. 6 for the d-separation before/after interventions,and four axioms to reason about the relationships between the causal predicate
nanc and the interventions/d-separation (named Nanc{1,2,3,4} in Fig. 6). By
AllNanc, PaNanc, and PaDsep, we transform the formulas using allnanc
and pa into those with nanc or dsep.
def
Properties of Axiomatization. For a data generator g, a set Γ = {ψ1 , . . . , ψn }of formulas, and a formula φ, we write Γ ⊢g φ if there is a derivation of ⊢g (ψ1 ∧· · · ∧ ψn ) → φ using axioms of AX or AXCP . We write Γ |=g φ if for all model
M and all world w having the data generator g, M, w |= φ. Then we obtain thesoundness of AX and AXCP .
Theorem 1 (Soundness) Let g be a finite, closed, and acyclic data generator.
Γ ⊆ Fml, and φ ∈ Fml. If Γ ⊢g φ then Γ |=g φ.

12









Y. Kawamoto et al.

Axioms for d-separation
DsepCI⊢g (dsep(x, y, z) ∧ pos(z)) → y|z,x=c = y|z
DsepSm⊢g dsep(x, y, z) ↔ dsep(y, x, z)
DsepDc⊢g dsep(x, y ∪ y ′ , z) → (dsep(x, y, z) ∧ dsep(x, y ′ , z))
DsepWu⊢g dsep(x, y ∪ v, z) → dsep(x, y, z ∪ v)
DsepCn⊢g (dsep(x, y, z)∧dsep(x, v, z ∪ y)) → dsep(x, y ∪ v, z)
Axioms for d-separation with interventions
DsepEI⊢g (⌈c/z⌉dsep(x, y, z)) ↔ dsep(x, y, z)
DsepLI⊢g (⌊c/z⌋dsep(x, y, z)) ↔ dsep(x, y, z)

Axioms with other causal predicatesNanc1⊢g (nanc(x, y)∧nanc(x, z)) → (f = y|z ↔ ⌈c/x⌉(f = y|z ))Nanc2⊢g nanc(x, y) ↔ ⌈c/x⌉nanc(x, y)
Nanc3⊢g nanc(x, y) → ⌈c/x⌉dsep(x, y, ∅)Nanc4⊢g (nanc(x, z) ∧ dsep(x, y, z)) → nanc(x, y)
AllNanc ⊢g allnanc(x, y, z) → nanc(x, z)
PaNanc⊢g pa(x, y) → nanc(y, x)
PaDsep⊢g pa(z, x) → ⌊c/x⌋dsep(x, y, z)+Fig. 6: The additional axioms for AXCP where x, y, y ′, z, v ∈CVar are disjoint,c ∈ dConst+ , and f ∈ Fsym.
See Appendices B and C for the proof. As shown in Section 7, AXCP isexpressive enough to derive the rules of Pearl’s do-calculus [29]; it can reason
about all causal effects identifiable by the do-calculus (without referring to a
specific causal diagram). Furthermore, AX includes/derives the axioms used in
the previous work [1] that are complete w.r.t. a different semantics without
dealing with probability distributions. We leave investigating whether AX iscomplete w.r.t. our Kripke model for future work. We also remark that AXCP hasaxioms corresponding to the composition and effectiveness axioms introduced byGalles and Pearl [9].

7Reasoning About Statistical Causality

Deriving the Rules of the Do-Calculus. Using StaCL, we express the docalculus’s rules [29], which are sufficient to compute all identifiable causal effects
from observable quantities [16, 32]. Let fv(φ) be the set of all variables occurringin a formula φ, and cdv(φ) be the set of all conditioning variables in φ.
Proposition 2 (Do-calculus rules) Let v, x, y, z ∈ CVar+ be disjoint, x1 , x2 ∈CVar+ , and c0 , c1 , c2 ∈ dConst+ . Let S = cdv(φ0 ) ∪ cdv(φ1 ).
1. Do1.

Introduction/elimination of conditioning:V⊢g ⌈c0/v⌉(dsep(x, y, z) ∧ s∈S pos(s)) → ((⌈c0/v⌉φ0 ) ↔ ⌈c0/v⌉φ1 )Formalizing Statistical Causality via Modal Logic

13

Nanc3
⊢g ψnanc → ((⌈c/x⌉ψ2 )↔ψ2 )EqEI
Do3⊢g ψd1 → ((⌈c/x⌉ψ0 )↔ψ1 )⊢g ψd2 → ((⌈c/x⌉ψ2 )↔ψ2 )⊢g (⌈c/x⌉ψ3 )↔ψ3
ψpre ⊢g (⌈c/x⌉ψ0 ∧ ⌈c/x⌉ψ2 ∧ ⌈c/x⌉ψ3 ) ↔ (ψ1 ∧ ψ2 ∧ ψ3 )DistrEI ∧ψpre ⊢g (⌈c/x⌉(ψ0 ∧ ψ2 ∧ ψ3 )) ↔ (ψ1 ∧ ψ2 ∧ ψ3 )
EqC , EqF , Eq2
ψpre ⊢g (⌈c/x⌉c0 = (y|z (z)) ↓y ) ↔ (ψ1 ∧ ψ2 ∧ ψ3 )PD, Eq2
ψpre ⊢g (⌈c/x⌉c0 = (y :: z) ↓y ) ↔ (ψ1 ∧ ψ2 ∧ ψ3 )MPD, Eq2
ψpre ⊢g (⌈c/x⌉c0 = y) ↔ (ψ1 ∧ ψ2 ∧ ψ3 )Do2

Fig. 7: Sketch of a derivation tree for the correctness of the backdoor adjustment
def
def(Section 2) using AXCP where ψpos = pos(z ::x), ψd1 = ⌊c/x⌋dsep(x, y, z)∧ψpos ,
def
def
def
ψd2 = ⌈c/x⌉dsep(x, z, ∅) ∧ ψpos , ψnanc = nanc(x, z) ∧ ψpos , ψpre = ψd1 ∧ ψnanc ,
def
def
def
def
ψ0 = (f = y|z ), ψ1 = (f = y|z,x=c ), ψ2 = (c1 = z), and ψ3 = (c0 = f (c1 ) ↓y ).

where φ1 is obtained by replacing some occurrences of y|z in φ0 with y|z,x=c1 ;2. Do2. Exchange between intervention and conditioning:V⊢g ⌈c0/v⌉⌊c1/x⌋(dsep(x, y, z) ∧ s∈S pos(s)) → ((⌈c0/v, c1/x⌉φ0 ) ↔ ⌈c0/v⌉φ1 )where φ1 is obtained by replacing every occurrence of y|z in φ0 with y|z,x=c1 ;3. Do3 Introduction/elimination of intervention:⊢g ⌈c0/v⌉(allnanc(x1 , x, y) ∧ ⌈c1/x1 ⌉(dsep(x, y, z) ∧ pos(z)))→ ((⌈c0/v⌉φ) ↔ ⌈c0/v, c1/x1 , c2/x2 ⌉φ)
defwhere fv(φ) = {y|z } and x = x1 :: x2 .
By using the deductive system AXCP , we can derive those rules. Thanks to
the modal operators for lazy interventions, our derivation of those rules is partly
different from Pearl’s [29] in that it does not use diagrams augmented with theintervention arc of the form Fx A x (See Appendix D for details).
Reasoning About Statistical Adjustment. We present how AXCP can beused to reason about the correctness of the backdoor adjustment discussed in
Section 2 (See Appendix A.6 for the details of the backdoor adjustment). Fig. 7
shows the derivation of the judgment:ψpre ⊢g (⌈c/x⌉c0 = y) ↔ (ψ1 ∧ ψ2 ∧ ψ3 ).

(3)This judgment asserts the correctness of the backdoor adjustment in any
def
causal diagram. Recall that φRCT = (⌈c/x⌉c0 = y) expresses the RCT and
def
φBDA = (ψ1 ∧ ψ2 ∧ ψ3 ) expresses the backdoor adjustment. The correctness ofthe backdoor adjustment (φRCT ↔ φBDA ) depends on the precondition ψpre .
By reading the derivation tree in a bottom-up manner, we observe that theproof first converts (⌈c/x⌉c0 = y) to a formula to which EqC and EqF areapplicable. Then, the derived axioms Do2 and Do3 in Proposition 2 are used
to complete the proof at the leaves of the derivation.

14

Y. Kawamoto et al.

In Section 2, we stated the correctness of the backdoor adjustment in (1)using a simpler requirement pa(z, x) instead of ψd1 and ψnanc . We can derive
the judgment (1) from (3), thanks to the axioms PaDsep and PaNanc.
The derivation does not mention the data generator g representing the causal
diagram G. This exhibits that our logic successfully separates the reasoning
about the properties of arbitrary causal diagrams from those depending on a
specific causal diagram. Once we prove ψpre ⊢g φRCT ↔ φBDA using AXCP , one
can claim the correctness of the causal inference (φRCT ↔ φBDA ) by checking
that the requirement ψpre indeed holds for a specific causal diagram G.

8Conclusion

We proposed statistical causality language (StaCL) to formally describe andexplain the correctness of statistical causal inference. We introduced the notion of
causal predicates and Kripke models equipped with data generators. We defineda sound deductive system AXCP that can deduce all causal effects derived using
Pearl’s do-calculus. In ongoing and future work, we study the completeness of AX
and AXCP and develop a decision procedure for AXCP for automated reasoning.
Acknowledgements. We thank Kenji Fukumizu for providing helpful information on the literature on causal inference. The authors are supported by ERATO
HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST.
Yusuke Kawamoto is supported by JST, PRESTO Grant Number JPMJPR2022,
Japan, and by JSPS KAKENHI Grant Number 21K12028, Japan. Tetsuya Satois supported by JSPS KAKENHI Grant Number 20K19775, Japan. Kohei Suenaga is supported by JST CREST Grant Number JPMJCR2012, Japan.

References
1. Barbero, F., Sandu, G.: Team semantics for interventionist counterfactuals: Observations vs. interventions. J. Philos. Log. 50(3), 471–521 (2021).
https://doi.org/10.1007/s10992-020-09573-6
2. Barbero, F., Schulz, K., Smets, S., Velázquez-Quesada, F.R., Xie, K.: Thinking
about causation: A causal language with epistemic operators. In: Proc. the third
International Workshop on Dynamic Logic (DaLí’20). LNCS, vol. 12569, pp. 17–32.
Springer (2020). https://doi.org/10.1007/978-3-030-65840-3\_2
3. Bochman, A.: A logical theory of causality. MIT Press (2021)
4. Bochman, A., Lifschitz, V.: Pearl’s causality in a logical setting. In: Proc.
the Twenty-Ninth AAAI Conference on Artificial Intelligence. pp. 1446–1452.
AAAI Press (2015), http://www.aaai.org/ocs/index.php/AAAI/AAAI15/paper/view/9686
5. Corander, J., Hyttinen, A., Kontinen, J., Pensar, J., Väänänen, J.: A logical approach to context-specific independence. Ann. Pure Appl. Log. 170(9), 975–992(2019). https://doi.org/10.1016/j.apal.2019.04.004
6. Durand, A., Hannula, M., Kontinen, J., Meier, A., Virtema, J.: Approximationand dependence via multiteam semantics. In: Gyssens, M., Simari, G.R. (eds.)

Formalizing Statistical Causality via Modal Logic

15

Proc. the 9th International Symposium on the Foundations of Information andKnowledge Systems (FoIKS’16). LNCS, vol. 9616, pp. 271–291. Springer (2016).
https://doi.org/10.1007/978-3-319-30024-5\_15
7. Durand, A., Hannula, M., Kontinen, J., Meier, A., Virtema, J.: Probabilistic teamsemantics. In: Proc. the 10th International Symposium on the Foundations of Information and Knowledge Systems (FoIKS’18). LNCS, vol. 10833, pp. 186–206.
Springer (2018). https://doi.org/10.1007/978-3-319-90050-6\_11
8. Fernandes-Taylor, S., Hyun, J.K., Reeder, R.N., Harris, A.H.: Common statisticaland research design problems in manuscripts submitted to high-impact medical
journals. BMC Research Notes 4(1), 304 (2011). https://doi.org/10.1186/17560500-4-304, https://doi.org/10.1186/1756-0500-4-304
9. Galles, D., Pearl, J.: An axiomatic characterization of causal counterfactuals. Foundations of Science 3, 151–182 (1998)
10. Halpern, J.Y.: Axiomatizing causal reasoning. J. Artif. Intell. Res. 12, 317–337(2000). https://doi.org/10.1613/jair.648, https://doi.org/10.1613/jair.648
11. Halpern, J.Y.: A modification of the Halpern-Pearl definition of causality. In: Proc.
IJCAI’15. pp. 3022–3033. AAAI Press (2015)12. Halpern, J.Y., Pearl, J.: Causes and explanations: A structural-model approach part II: explanations. In: Proc. IJCAI’01. pp. 27–34. Morgan Kaufmann (2001)
13. Halpern, J.Y., Pearl, J.: Causes and explanations: A structural-model approach:Part 1: Causes. In: Proc. UAI’01. pp. 194–202. Morgan Kaufmann (2001)
14. Hirvonen, Å., Kontinen, J., Pauly, A.: Continuous team semantics. In: Proc.
the 15th Annual Conference on Theory and Applications of Models ofComputation (TAMC’19). LNCS, vol. 11436, pp. 262–278. Springer (2019).
https://doi.org/10.1007/978-3-030-14812-6\_16
15. Hodges, W.: Compositional semantics for a language of imperfect information. Log.
J. IGPL 5(4), 539–563 (1997). https://doi.org/10.1093/jigpal/5.4.539
16. Huang, Y., Valtorta, M.: Pearl’s calculus of intervention is complete. In: Proc.
UAI’06. p. 217–224. AUAI Press (2006)
17. Hyttinen, A., Eberhardt, F., Järvisalo, M.: Constraint-based causal discovery: Conflict resolution with answer set programming. In: Proc. the Thirtieth Conference
on Uncertainty in Artificial Intelligence (UAI’14). pp. 340–349. AUAI Press (2014)18. Hyttinen, A., Eberhardt, F., Järvisalo, M.: Do-calculus when the true graph is
unknown. In: Proc. the Thirty-First Conference on Uncertainty in Artificial Intelligence (UAI’15). pp. 395–404. AUAI Press (2015)
19. Ibeling, D., Icard, T.: Probabilistic reasoning across the causal hierarchy. In:
Proc. the Thirty-Fourth AAAI Conference on Artificial Intelligence (AAAI’20). pp.
10170–10177. AAAI Press (2020), https://aaai.org/ojs/index.php/AAAI/article/
view/6577
20. Kawamoto, Y.: Statistical epistemic logic. In: The Art of Modelling Computational
Systems: A Journey from Logic and Concurrency to Security and Privacy. LNCS,
vol. 11760, pp. 344–362. Springer (2019). https://doi.org/10.1007/978-3-030-311759\_20
21. Kawamoto, Y.: Towards logical specification of statistical machine learning. In:
Proc. SEFM. pp. 293–311 (2019). https://doi.org/10.1007/978-3-030-30446-1\_16
22. Kawamoto, Y.: An epistemic approach to the formal specification of statistical machine learning. Software and Systems Modeling 20(2), 293–310 (2020).
https://doi.org/10.1007/s10270-020-00825-2
23. Kawamoto, Y., Mano, K., Sakurada, H., Hagiya, M.: Partial knowledgeof functions and verification of anonymity. Transactions of the Japan

16

Y. Kawamoto et al.

Society for Industrial and Applied Mathematics 17(4), 559–576 (2007).
https://doi.org/10.11540/jsiamt.17.4\_559
24. Kawamoto, Y., Sato, T., Suenaga, K.: Formalizing statistical beliefs in hypothesis testing using program logic. In: Proc. KR’21. pp. 411–421 (2021).
https://doi.org/10.24963/kr.2021/39
25. Kawamoto, Y., Sato, T., Suenaga, K.: Sound and relatively complete belief Hoare
logic for statistical hypothesis testing programs. CoRR abs/2208.07074 (2022)
26. Makin, T.R., de Xivry, J.J.O.: Science forum: Ten common statistical mistakes towatch out for when writing or reviewing a manuscript. Elife 8, e48175 (2019)27. McCain, N., Turner, H.: Causal theories of action and change. In: Proc. the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference (AAAI’97/IAAI’97). pp. 460–465. AAAI
Press / The MIT Press (1997)
28. Moher, D., Hopewell, S., Schulz, K.F., Montori, V., Gøtzsche, P.C., Devereaux, P.,
Elbourne, D., Egger, M., Altman, D.G.: Consort 2010 explanation and elaboration:
updated guidelines for reporting parallel group randomised trials. International
journal of surgery 10(1), 28–55 (2012)
29. Pearl, J.: Causal diagrams for empirical research. Biometrika 82(4), 669–688(1995), http://www.jstor.org/stable/2337329
30. Pearl, J.: Causality. Cambridge university press (2009)
31. Rückschloß, K., Weitkämper, F.: Exploiting the full power of Pearl’s causality inprobabilistic logic programming. In: Proc. the 9th Workshop on Probabilistic Logic
Programming (PLP’22). CEUR Workshop Proceedings, vol. 3193. CEUR-WS.org(2022), http://ceur-ws.org/Vol-3193/paper1PLP.pdf
32. Shpitser, I., Pearl, J.: Identification of conditional interventional distributions. In:
Proc. UAI’06. p. 437–444. AUAI Press (2006)
33. Simpson, E.H.: The interpretation of interaction in contingency tables. Journalof the Royal Statistical Society. Series B (Methodological) 13(2), 238–241 (1951),
http://www.jstor.org/stable/2984065
34. Triantafillou, S., Tsamardinos, I.: Constraint-based causal discovery from multiple
interventions over overlapping variable sets. J. Mach. Learn. Res. 16, 2147–2205(2015)
35. Verma, T., Pearl, J.: Causal networks: semantics and expressiveness. In: Proc.
UAI’88. pp. 69–78. North-Holland (1988)
36. Von Elm, E., Altman, D.G., Egger, M., Pocock, S.J., Gøtzsche, P.C., Vandenbroucke, J.P.: The strengthening the reporting of observational studies in epidemiology (strobe) statement: guidelines for reporting observational studies. Bulletinof the World Health Organization 85, 867–872 (2007)

Appendix
We present the following technical details:– Appendix A presents the details of our models and causality.
– Appendix B proves the soundness of the deductive system AX for StaCL.
– Appendix C shows the soundness of the deductive system AXCP for StaCL
with causal predicates.
– Appendix D presents the details of the reasoning and the explanation about
statistical causality using StaCL.

Formalizing Statistical Causality via Modal Logic

17

We first introduce notations. We present key notations in Tables 2 and 3.
For tuples x and x′ of variables, we write x ⊆ x′ iff every variable in x
appears in x′ . x \ y is the tuple of variables obtained by removing all variables
in y from x. As with ::, the symbol ‘\’ is a meta-operator on sets of variables,
and not a function symbol. For brevity, we identify a singleton tuple ⟨x⟩ as its
element x.
For u, u′ ∈ Term and x ∈ CVar, the substitution u[x 7→ u′ ] is the term
obtained by replacing every occurrence of x in u with u′ .
We recall that a memory is a joint probability distribution m ∈ D(Var →O ∪ {⊥}) of data values of all variables in Var. We write m(x) for the joint
distribution of all variables in x.

A

Details on Models and Causality

In this section, we show a couple of remarks on the interpretation of terms(Appendix A.1), the relationships between data generators and causal diagrams(Appendix A.2), and properties on memories (Appendix A.3). Then we present
more details on causal predicates (Appendix A.4), causal effects (Appendix A.5),
and causal diagrams (Appendix A.6).

Table 2: Notations in syntax.
Symbol Description
CVar
Set of causal variable
FVar
Set of conditional causal variables
fv(φ) Set of all free variables in a formula φ
cdv(φ) Set of all conditioning variables in a formula φFsym Set of function symbols
pFsym Set of probabilistic function symbols
dFsym Set of deterministic function symbols
Const Set of constants
dConst Set of deterministic constants⊥
Constant denoting the undefined value
CTerm Set of causal terms
Term Set of terms
Psym Set of predicates
CPsym Set of causal predicatesFml
Set of (causality) formulas

A.1

Remarks on the Interpretation of Terms

We present remarks on the at-most-once condition, on deterministic functions,and on the well-definedness of the interpretation of terms.

18

Y. Kawamoto et al.

Table 3: Notations in semantics.
SymbolDescription

M
Kripke modelW
Set of all possible worlds
R⌈c/x⌉
Intervention relation
V
ValuationO
Domain of data values
DO
Set of all probability distributions over Ow
Possible worldw⌈c/x⌉
Eagerly intervened worldw⌊c/x⌋
Lazily intervened world
gw
Data generator in a world w
x ≺g yy’s value depends on x’s in a data generator grξw = {ξw}r∼I Interpretation of function symbols in a world w
mw
Memory on variables in a world w
Gw = (U, V, E) Causal diagram in a world w
pa Gw (v)
All parent variables of v in Gw
PGw (V )Joint distribution of all variables V in Gw

Remark on At-Most-Once Condition We remark on the at-most-once condition. In Section 3, we assumed that a data generator satisfies the following
at-most-once condition: Each function symbol f and each constant c can beused at most once in a single data generator. For example, we may consider thedata generator g3 defined by c Ag3 z and f (z, z) Ag1 y as it is. Then g3 rewrites
y into f (c, c) after substitutions. In contrast, the data generator g4 defined byc Ag4 z1 , c Ag4 z2 , f (z1 , z2 ) Ag4 y(4)also rewrites y into f (c, c), but does not satisfy the at-most-once condition. Thus,
the two calls of the constant c should be distinguished and replaced with two
symbols c1 and c2 (denoting the same distribution of data values as c):
c1 Ag4 z1 , c2 Ag4 z2 , f (z1 , z2 ) Ag4 y.

(5)Then g4 rewrites y into f (c1 , c2 ). This at-most-once condition clarifies that an
occurrence of a probabilistic constant ci represents a single independent sampling. In the former definition (4) of g4 , which does not satisfy the at-most-once
condition, it is not clear whether (i) c is sampled once and its (single) value isassigned to both y1 and y2 , or (ii) it is sampled twice and the drawn (two) values are assigned to y1 and y2 . By imposing the at-most-once condition as in thelatter definition (5), we can clarify that there are two occurrences of samplingthat may use different randomness.
Remark on Interpretation of Terms We remark that two copies of the samedata value are obtained from the distribution [[⟨c, c⟩]]w , whereas two different val-

Formalizing Statistical Causality via Modal Logic

19

ues may be drawn from [[⟨c1 , c2 ⟩]]w for constants c1 , c2 denoting the same distribution, i.e., [[c1 ]]w = [[c2 ]]w . Indeed, for a randomly chosen r, the former results in[[⟨c, c⟩]]rξ,g = (ξ r (c), ξ r (c)). In contrast, the latter results in [[⟨c1 , c2 ⟩]]rξ,g = (ξ r (c1 ),ξ r (c2 )), where two data values are sampled independently. Notice that this definition is consistent with the at-most-once condition on a data generator g.
Remark on Deterministic Functions As a remark, we consider probabilisticand deterministic functions. Let pFsym ⊆ Fsym be the set of all probabilistic
function symbols, each denoting a randomized algorithm that produces a data
value using a randomness drawn internally (e.g., a function that returns a number
defobtained by adding a random number to an input). Let dFsym = Fsym\pFsym be
the set of all deterministic function symbols, denoting deterministic algorithms(e.g., + and −).
If f ∈ dFsym, the interpretation of f is independent of the randomness; i.e.,′ξ r (f ) = ξ r (f ) for all r, r′ ∈ I, hence ξ(f ) maps k data values o to the Dirac
distribution δξr (f )(o) , having a single value ξ r (f )(o) with probability 1.
We may relax the at-most-once condition in Section 3 so that deterministic
function symbols do not have to satisfy the condition. This is because the interpretation of a deterministic function symbol f is the same in every occurrenceof f .
Well-definedness of the Interpretation We next show that the interpretation [[_]]w of terms in a world w is unique thanks to the assumption on the strict
partial order ≺ over the defined causal variables dom(gw ) as follows.
Proposition 3 (Well-definedness of [[_]]w ) Let u be a term and w = (ξ, g, m)
be a world such that g is closed. Then we have [[u]]w ∈ DOk .
Proof. Since g is closed, we have fv(range(g)) ⊆ dom(g). By the definition of[[u]]w in Section 4, it suffices to show [[u]]rξ,g ∈ Ok for each r ∈ I.
By the definition of the possible world w, g is finite and acyclic. Then,≺g is the strict partial order over dom(g) defined in Section 3. For a tuplex = ⟨x1 , . . . , xk ⟩ of variables, let cntv (x) be the number of variables z such thatz ≺g xi for some i = 1, . . . , k. Since dom(g) is a finite set, cntv (x) is finite.
Let r ∈ I. We first show that for any x = ⟨x1 , . . . , xk ⟩ ∈ dom(g)k , we haver[[x]]ξ,g ∈ Ok by induction on cntv (x).
– Case cntv (x) = 0. By definition, there is no variable z such that z ≺gw xi for
any i = 1, . . . , k; hence fv(g(x)) = ∅. Since g is closed, for each i = 1, . . . , k,[[g(xi )]]w is defined and represented as [[ci ]]w or [[fi (ci1 , . . . , cil )]]w for constantsci , ci1 , . . . , cil . Therefore,[[x]]rξ,g = [[⟨g(x1 ), . . . , g(xk )⟩]]rξ,g ∈ Ok
follows immediately from the definition of ξ r .

20

Y. Kawamoto et al.
def– Case cntv (x) > 0. Let z = ⟨z1 , . . . , zl ⟩ ⊆ fv(g(x)) for l ≥ 1. From thestrict partial order structure of ≺g , we have cntv (z) < cntv (x). By induction hypothesis, [[z]]rξ,g ∈ Ol . Then, by the definition of fv(g(x)), for eachi = 1, 2, . . . , l, g(xi ) can be represented as a constant ci or a causal termfi (v1 , . . . vl ) where vj ∈ CVar ∪ Const for each j = 1, 2, . . . , l. In the former case, [[g(xi )]]rξ,g = [[ci ]]rξ,g = ξ r (ci ) ∈ O by definition. In the latter case,[[g(xi )]]rξ,g = [[fi (v1 , . . . vl )]]rξ,g . If vi ∈ Const then [[vi ]]rξ,g ∈ O is immediate; if
vj ∈ CVar then we obtain vj ∈ fv(g(x)), and hence [[vj ]]rξ,g ∈ O. Therefore,
we conclude:[[fi (v1 , . . . , vl )]]rξ,g = ξ r (fi )([[⟨v1 , . . . , vl ⟩]]rξ,g )= ξ r (fi )([[v1 ]]rξ,g , · · · , [[vl ]]rξ,g ) ∈ O.
The rest of the proof is immediately by induction on the structures of tuplesof terms.
□

A.2

Relationships Between Data Generators and Causal Diagrams

We show that each data generator corresponds to a DAG (directed acyclic graph)of the causal model as follows.
Proposition 4 (Acyclicity of G) Let G be the causal diagram corresponding
to a finite and acyclic data generator g. Then G is a finite directed acyclic graph.
Proof. Let G = (U, V, E). Since g is finite, dom(g) and range(g) are finite. By
definition, for each x A y ∈ E, we have x ≺g y. Since ≺g is a strict partial order,
so is A. Therefore, G is a finite directed acyclic graph.
□
Next, we show that the interpretation [[_]]w defines the joint distribution PGw
of all variables in the causal diagram Gw .
Proposition 5 (Relationship between [[_]]w and PGw ) Let w be a world,
Gw be the causal diagram corresponding to the data generator gw , x, y ∈ CVar+ ,z ∈ CVar∗ , and c ∈ dConst+ . Then there is a joint distribution PGw that factorizes according to Gw , and that satisfies:
1. [[y|z ]]w = PGw (y | z)
2. [[y|z ]]w⌈c/x⌉ = PGw (y | do(x = [[c]]w ), z).
def

Proof. We fix a world w. For brevity, we write G = Gw . We recall that G is thedef
def
triple (U, V, E) consisting of U = fc(range(gw )), V = dom(gw ), and the set E ofstructural equations defined by gw . Let PG (V ) be the probability distribution
defined in (2).

Formalizing Statistical Causality via Modal Logic

21

We inductively define the set Leaf k of variables of depth k from leaves andits subset LFk having a parent variable by:
V 0 = V,E 0 = E,
Leaf k = {v ∈ V k | for all v ′ ∈ V k , v A v ′ ∈/ E k },
LFk = {v ∈ Leaf k | there is a v ′′ ∈ V k , v ′′ A v ∈/ E k },
V k+1 = V k \ LFk ,E k+1 = E k ∩ ((U ∪ V k+1 ) × V k+1 ).
This procedure terminates when LFk = ∅. Since gw is finite and acyclic, theabove procedure terminates in a finite number N of steps.
Notice that, by the definition of causal terms, for any k < N and and anyv ∈ V k , gw (v) is of the form f (z1 , . . . , zl ) for some f ∈ Fsym and z1 , . . . , zl ∈CVar.
For each k = 0, 1. . . . , N , we consider the restricted diagram G k = (U, V k , E k ).
We first claim that [[V k ]]w = PG k (V k ) for any k = 0, 1, . . . , N . We prove thisby induction on k as follows.
The base case is k = N . Since no variable in V N has a parent variable, there
is a c ∈ Const+ such that gw (V N ) = c. Hence,
PG (V N ) = [[c]]w = [[gw (V N )]]w = [[V N ]]w .
Next, we consider the case k < N . Since the above procedure terminates
exactly at N steps, we obtain LFk ̸= ∅. By applying the induction hypothesis(the case of k + 1), we obtain PG k+1 (V k \ LFk ) = PG k+1 (V k+1 ) = [[V k+1 ]]w =[[V k \ LFk ]]w . Since each causal term is of depth at most 1 by definition, theset pa G k (v) of all parents of a variable v in the causal diagram G k is given by
fv(gw (v)). Hence,
PG k (V k ) = PG k+1 (LFk ) · PG k+1 (V k \ LFk ) Y=
PG k (v | pa G k (v)) · PG k+1 (V k \ LFk )
v∈LFk

=

 Y


PG k (v | pa G k (v)) · [[V k \ LFk ]]wv∈LFk(by induction hypothesis)= [[V k ]]w .
(since each causal term is of depth at most 1)
Therefore, we conclude:
PG (V ) = PG 0 (V 0 ) = [[V 0 ]]w = [[V ]]w .

22

Y. Kawamoto et al.

Now the first equation in the proposition is obtained as follows.
w[[y|z ]]w = [[y::z]][[z]]w([[V ]] )|= ([[V ]]ww )|zy::z(V ))|(P= (PGGw (V ))|zy::zw=

PGw (y::z)
PGw (z)= PGw (y | z).
Similarly, the second equation in the proposition is obtained as follows. Let
Gw′ be the causal diagram obtained by an intervention x := [[c]]w in Gw .
[[y|z ]]w⌈c/x⌉ =[[y::z]]w⌈c/x⌉[[z]]w⌈c/x⌉([[V ]]c)|w⌈ /x⌉ y::z
= ([[V ]]w⌈c/x⌉ )|z(PG ′ (V ))|y::z= (P w′ (V ))|zGw(y::z | do(x = [[c]] ))P= PGwG (z | do(x = [[c]]ww))w= PGw (y | do(x = [[c]]w ), z).
□A.3

Properties on Memories

We present basic properties on memories. Intuitively, we show that:(i) the same formulas φy with free variables y are satisfied in any worlds w and
w′ having the same memory on y;(ii) an eager and a lazy interventions to x result in the same distribution of thevariables y disjoint from x;(iii) disjoint worlds w and w′ have data generators gw and gw′ with disjoint
domains.
Proposition 6 (Properties on mw ) Let w and w′ be worlds, x, y ∈ Var+ , c ∈ dConst+ ,and φy ∈ Fml with fv(φy ) = y.
(i) If mw (y) = mw′ (y) ̸= ⊥, then w |= φy iff w′ |= φy .
(ii) If x ∩ y = ∅, then mw⌈c/x⌉ (y) = mw⌊c/x⌋ (y).
(iii) If Var(w)∩Var(w′ ) = ∅ (namely, dom(mw )∩dom(mw′ ) = ∅), then dom(gw )∩dom(gw′ ) = ∅.
Proof. (i) Assume that mw (y) = mw′ (y) ̸= ⊥. Then we prove w |= φy iffw′ |= φy by induction on φy .

Formalizing Statistical Causality via Modal Logic

23

def

If φy = η(y) for η ∈ Psym, then:w |= η(y)iff mw (y) ∈ V(η)
iff mw′ (y) ∈ V(η)(by mw (y) = mw′ (y) ̸= ⊥)′iff w |= η(y).
The other cases are straightforward by definitions.
(ii) Assume x ∩ y = ∅. By definition, we obtain:mw⌈c/x⌉ (y) = [[gw⌈c/x⌉ (y)]]w⌈c/x⌉= [[gw (y)]]w⌈c/x⌉= [[gw (y)[x 7→ c]]]w⌈c/x⌉(by x ∩ y = ∅)= [[gw (y)[x 7→ c]]]w⌊c/x⌋(by x ∩ fv(gw (y)[x 7→ c]) = ∅)= [[gw⌊c/x⌋ (y)]]w⌊c/x⌋= mw⌊c/x⌋ (y).
(iii) By the definition of possible worlds, we have dom(gw ) ⊆ dom(mw ) anddom(gw′ ) ⊆ dom(mw′ ). Therefore, we obtain dom(gw )∩dom(gw′ ) ⊆ dom(mw )∩ dom(mw′ ) = ∅.
□A.4

Causal Predicates

Next, we present more details on causal predicates. Among the causal predicateslisted below, our deduction system AXCP requires only dsep, nanc, and allnanc.
For the sake of convenience, we can use pa, but it is sufficient for us to derive
the formulas equipped with pa from those with nanc. Thus, we do not deal withaxioms of the other predicates in this paper.
We show a list of causal predicates as follows.
– dsep(x, y, z) x and y are d-separated by z;– pa(x, y) x is the set of all parents of variables in y;– npa(x, y) x is a set of non-parents of variables in y;– anc(x, y) x is the set of all ancestors of variables in y;– nanc(x, y) x is a set of non-ancestors of variables in y;– allnanc(x, y, z) x is the set of all variables in y that are not ancestors ofany variables in z.
These causal predicates are interpreted using a data generator gw in a world w
as follows.
Definition 1 (Semantics of dsep, pa, npa, anc, nanc, allnanc). Let w be aworld, and Gw be the causal diagram corresponding to gw . Let PA(y) be the setof all parent variables of y:PA(y) = {x ∈ Var(w) | x A y ′ , y ′ ∈ y}.

24

Y. Kawamoto et al.

Let ANC(y) is the set of all ancestors variables of y:
ANC(y) = {x ∈ Var(w) | x A+ y ′ , y ′ ∈ y}where A+ is the transitive closure of A. The interpretations of the causal predicates dsep, pa, npa, anc, nanc, allnanc are given as follows:
w |= dsep(x, y, z) iff x and y are d-separated by z in Gw
w |= pa(x, y) iff x = PA(y) and x ∩ y = ∅w |= npa(x, y) iff x ∩ PA(y) = ∅ and x ∩ y = ∅w |= anc(x, y) iff x = ANC(y) and x ∩ y = ∅w |= nanc(x, y) iff x ∩ ANC(y) = ∅ and x ∩ y = ∅w |= allnanc(x, y, z) iff x = y \ ANC(z),where we recall the notion of d-separation in Appendix A.6.
Proposition 7 (Relationships among causal predicates) The causal predicates pa, npa, anc, and nanc satisfy the relationships:
1. |= pa(x, y) → anc(x, y).
2. |= anc(x, y) → nanc(y, x).
3. |= nanc(y, x) → npa(y, x).
Proof. These claim are straightforward from Definition 1.
A.5□

Causal EffectWe show that the causal effect can be expressed using a StaCL formula as follows.
Proposition 1 (Causal effect) Let w be a world, x, y, z ∈ Var(w)+ be disjoint, c ∈ dConst+ , c′ ∈ Const+ , and f ∈ Fsym. Then:(i) w |= ⌈c/x⌉(c′ = y) iff there is a distribution PGw that is factorized according
to Gw and satisfies PGw (y | do(x = c)) = [[c′ ]]w .
(ii) w |= ⌈c/x⌉(f = y|z ) iff there is a distribution PGw that is factorized according
to Gw and satisfies PGw (y | do(x = c), z) = [[f ]]w .
Proof. We show the first claim as follows. By Proposition 5, there is a joint
distribution PGw that is factorized according to Gw and that satisfies [[y]]w⌈c/x⌉ =PGw (y | do(x = [[c]]w )). Thus, we obtain:w |= ⌈c/x⌉(c′ = y)iff w⌈c/x⌉ |= c′ = yiff [[y]]w⌈c/x⌉ = [[c′ ]]w
iff PGw (y | do(x = [[c]]w )) = [[c′ ]]w .

Formalizing Statistical Causality via Modal Logic

25

Analogously, the second claim is obtained as follows. By Proposition 5, there
is a joint distribution PGw that is factorized according to Gw and that satisfies[[y|z ]]w⌈c/x⌉ = PGw (y | do(x = [[c]]w ), z). Thus, we obtain:w |= ⌈c/x⌉(c′ = y|z )iff w⌈c/x⌉ |= c′ = y|ziff [[y|z ]]w⌈c/x⌉ = [[c′ ]]w
iff PGw (y | do(x = c), z) = [[c′ ]]w .
□A.6

Details on Causal Diagrams

Next, we recall the notion of d-separation [35] as follows.
Definition 2 (d-separation). Let x, y, z be disjoint sets of variables, anddef
ANC∗ (z) = z ∪ ANC(z) be the union of z and the set of z’s all ancestors. An
undirected path p is said to be d-separated by z if it satisfies one of the following
conditions:(a) p has a chain v ′ A v A v ′′ s.t. v ∈ z.
(b) p has a fork v ′ v A v ′′ s.t. v ∈ z.
(c) p has a collider v ′ A v v ′′ s.t. v ̸∈ ANC∗ (z).
AAx and y are d-separated by z if all undirected paths between variables in x andin z are d-separated by z.
We also recall the notion of back-door path as follows.
Definition 3 (Back-door path). For variables x and y, a back-door path fromx to y in a causal diagram G is an arbitrary undirected path between x and y in
G that starts with an arrow pointing to x (i.e., an undirected path of the form
x v · · · y). For tuples of variables x and y, a back-door path from x to y is anarbitrary back-door path from x ∈ x to y ∈ y.
A

We remark on the relationships between back-door paths and two kinds ofinterventions as follows.
Remark 1. An eager intervention ⌈c/x⌉ can remove all back-door paths from x
to y, because all of these paths have arrows pointing to x and ⌈c/x⌉ removes all
such arrows.
In contrast, a lazy intervention ⌊c/x⌋ can remove all undirected paths between x and y except for all back-door paths from x to y, because ⌊c/x⌋ removes all arrows emerging from x while keeping all arrows pointing to x. Thus,⌊c/x⌋dsep(x, y, z) represents that all back-door paths from x to y are d-separated
by z.

26

Y. Kawamoto et al.

These relationships are used to reason about the causality, e.g., when we
derive the second rule of Pearl’s do-calculus using our StaCL (Proposition 2).
Now we recall the back-door criteria and the back-door adjustment in Pearl’s
causal model.
Definition 4 (Back-door criterion). For two sets x and y of variables, a set
z of variables satisfies the back-door criterion in a causal diagram G if (i) no
variable in z is a descendent of an element of x in G and (ii) all back-door paths
from x to y are d-separated by z in G.
The back-door criterion is expressed as the following StaCL formula:nanc(x, z) ∧ ⌊c/x⌋dsep(x, y, z).
When z satisfies the back-door criterion in a causal diagram G, then thecausal effect of x on y is given by:
PG (y | do(x)) =X

PG (y | z, x) PG (z).

z

In Fig. 7 in Section 7, we show a derivation tree for the correctness of computing the causal effect using the backdoor adjustment.

B

Proof for the Soundness of AX

We show that the deductive system AX of StaCL is sound w.r.t. the Kripke
semantics for statistical causality (Theorem 1).
We first remark that AX satisfies the deduction theorem.
Proposition 8 (Deduction) Let Γ ⊆ Fml, and φ1 , φ2 ∈ Fml. Then Γ ⊢g φ1 →φ2 iff Γ, φ1 ⊢g φ2 .
Proof. The direction from left to right is straightforward by the application of
MP. The other direction is shown as usual by induction on the derivation. □We prove the soundness of AX as follows. We show the validity of the axioms
for basic constructs (Appendix B.1), for eager interventions (Appendix B.2), forlazy interventions (Appendix B.3), and for the exchanges of eager/lazy interventions (Appendix B.4).

Formalizing Statistical Causality via Modal Logic

B.1

27

Validity of the Basic Axioms

Here are the basic axioms of AX without interventions.
PT⊢g φ for a propositional tautology φMP

φ1 , φ1 → φ2 ⊢g φ2

Eq1⊢g x = x

Eq2⊢g x = y → (φ1 → φ2 )where φ2 is the formula obtained by replacing
any number of occurrences of x in φ1 with y

EqC⊢g c(g,x) = x

EqF⊢g f (g,y|z,x=c ) = y|z,x=c

PD⊢g (pos(x) ∧ c0 =x ∧ f =y|x ∧ c1 =x :: y) → c1 =f (c0 )MPD ⊢g x1 ↓x2 = x2

if x2 ⊆ x1

The validity of the rules PT, MP, Eq1, Eq2, is straightforward. The validityof EqC and EqF is by the definition of the interpretation of the constants andfunction symbols introduced for the purpose of reasoning (Section 4):
ξ r (c(g,x) ) = [[x]]rξ,gξ r (f (g,y|z,x=c ) ) = [[y|z,x=c ]]rξ,g .
We show the validity of PD and MPD as follows.
Proposition 9 (Probability distributions) Let x, x1 , x2 , y ∈ CVar+ , c0 , c1 ∈Const, and f ∈ Fsym.
⊢g (pos(x) ∧ c0 =x ∧ f =y|x ∧ c1 =x :: y)→ c1 =f (c0 ).
(ii) MPD ⊢g x1 ↓x2 = x2 if x2 ⊆ x1 .
(i) PD

Proof. Let w = (gw , ξw , mw ) be a world such that x, x1 , x2 , y ∈ Var(w)+ .
(i) We show the validity of PD as follows. Suppose that w |= pos(x) ∧ c0 =x ∧f =y|x ∧ c1 =x :: y. Then we have [[x]]w (o′x ) > 0 for all o′x ∈ O|x| , [[c0 ]]w =[[x]]w , [[c1 ]]w = [[x :: y]]w , and [[f ]]w = [[y|x ]]w . Since [[x]]w (o′x ) > 0, we have:P [[x :: y]]w (o′x ,o′y )([[y|x ]]w (o′x )) = o′· δ(o′x ,o′y ) .
[[x]]w (o′ )yThus, for each ox ∈ O|x|and oy ∈ Ox|y|, we have:[[f (c0 )]]w (ox , oy )= ([[f ]]w [[c0 ]]w )(ox , oy )= ([[y|x ]]w [[x]]w )(ox , oy )XX[[x :: y]]w (o′x ,o′y )=[[x]]w (o′x ) · δ(o′x ,o′y ) (ox , oy )[[x]]w (o′ )
o′x

o′y

= [[x :: y]]w (ox , oy )= [[c1 ]]w (ox , oy ).

x

28

Y. Kawamoto et al.

Therefore, we obtain w |= c1 =f (c0 ).
(ii) We show the validity of MPD as follows. Let ⊗ be the product of probability
distributions of data values. Let x1 = {x1 , . . . , xk }. Assume that ∅ ≠ x2 ⊆
x1 . Then we may write x2 = {xl(1) , . . . , xl(k′ ) } for some 1 ≤ k ′ ≤ k andmonotone increasing function l : {1, . . . , k ′ } → {1, . . . , k}. Using this, we
obtain:[[x1 ↓x2 ]]w= [[↓x2 ]]w [[x1 ]]w= ((o1 , . . . , ok ) 7→ (ol(1) , . . . , ol(k′ ) ))[[⟨x1 , . . . , xk ⟩]]w
= ((o1 , . . . , ok ) 7→ (ol(1) , . . . , ol(k′ ) ))[[x1 ]]w ⊗ · · · ⊗ [[xk ]]w= [[xl(1) ]]w ⊗ · · · ⊗ [[xl(k′ ) ]]w= [[⟨xl(1) , . . . , xl(k′ ) ⟩]]w = [[x2 ]]w .
Therefore, we obtain w |= x1 ↓x2 = x2 if x2 ⊆ x1 .
B.2□

Validity of the Axioms for Eager Interventions

Here are the axioms of AX with the eager interventions ⌈·⌉.
DGEI

⊢g ⌈c/x⌉φ iff ⊢g⌈c/x⌉ φ

EffectEI⊢g ⌈c/x⌉(x = c)

EqEI

⊢g u1 = u2 ↔ ⌈c/x⌉(u1 = u2 )if fv(u1 ) = fv(u2 ) = ∅SplitEI⊢g ⌈c1/x1 , c2/x2 ⌉φ → ⌈c1/x1 ⌉⌈c2/x2 ⌉φSimulEI⊢g ⌈c1/x1 ⌉⌈c2/x2 ⌉φ → ⌈c1/x′1 , c2/x2 ⌉φ′

for x′1 = x1 \ x2 and c′1 = c1 \ c2
RptEI⊢g ⌈c/x⌉φ → ⌈c/x⌉⌈c/x⌉φ

CmpEI⊢g ⌈c1/x1 ⌉(x2 = c2 ) ∧ ⌈c1/x1 ⌉(x3 = u)
→ ⌈c1/x1 , c2/x2 ⌉(x3 = u)DistrEI ¬⊢g (⌈c/x⌉¬φ) ↔ (¬⌈c/x⌉φ)

DistrEI ∧⊢g (⌈c/x⌉(φ1 ∧ φ2 )) ↔ (⌈c/x⌉φ1 ∧ ⌈c/x⌉φ2 )

Next, we show basic laws of eager interventions as follows.
Proposition 10 (Basic laws of ⌈·⌉) Let x, x1 , x2 , x3 , y, z ∈ CVar+ be disjoint, c, c1 , c2 ∈ dConst+ , u, u1 , u2 ∈ Term+ , and φ ∈ Fml.
1. DGEI |=g ⌈c/x⌉φ iff |=g⌈c/x⌉ φ.
2. EffectEI |= ⌈c/x⌉(x = c).
3. EqEI |= u1 = u2 ↔ ⌈c/x⌉(u1 = u2 )if fv(u1 ) = fv(u2 ) = ∅.

Formalizing Statistical Causality via Modal Logic

4. SplitEI
5. SimulEI
6. RptEI
7. CmpEI29|= ⌈c1/x1 , c2/x2 ⌉φ → ⌈c1/x1 ⌉⌈c2/x2 ⌉φ.
′|= ⌈c1/x1 ⌉⌈c2/x2 ⌉φ → ⌈c1/x′1 , c2/x2 ⌉φ′
for x1 = x1 \ x2 and c′1 = c1 \ c2 .
|= ⌈c/x⌉φ → ⌈c/x⌉⌈c/x⌉φ.
|= ⌈c1/x1 ⌉(x2 = c2 ) ∧ ⌈c1/x1 ⌉(x3 = u)
→ ⌈c1/x1 , c2/x2 ⌉(x3 = u).

Proof. Let w = (gw , ξw , mw ) be a world such that x, x1 , x2 , x3 , y, z ∈ Var(w)+ .
1. Assume that |=g⌈c/x⌉ φ. Then for any world w′ having the data generator g,
we have w′ ⌈c/x⌉ |= φ, hence w′ |= ⌈c/x⌉φ. Therefore, |=g ⌈c/x⌉φ. The otherdirection is also shown analogously.
2. By the definition of an eagerly intervened world in Section 4, we have gw⌈c/x⌉ (x) =c. By ξw = ξw⌈c/x⌉ , [[c]]w = [[c]]w⌈c/x⌉ .
Then [[x]]w⌈c/x⌉ = [[gw⌈c/x⌉ (x)]]w⌈c/x⌉ = [[c]]w⌈c/x⌉ . Hence w⌈c/x⌉ |= x = c.
Therefore, w |= ⌈c/x⌉(x = c).
3. Assume that fv(u1 ) = fv(u2 ) = ∅. Then for each i = 1, 2, [[ui ]]w = [[ui ]]w⌈c/x⌉ .
Hence, |= u1 = u2 ↔ ⌈c/x⌉(u1 = u2 ).
4. The proof is straightforward from the definition.
5. The proof is straightforward from the definition.
6. The proof is straightforward from the definition.
7. Assume that w |= ⌈c1/x1 ⌉(x2 = c2 ) ∧ ⌈c1/x1 ⌉(x3 = u). Then gw⌈c1/x1 ⌉ (x2 ) =c2 and gw⌈c1/x1 ⌉ (x3 ) = u. Let w′ = w⌈c1/x1 ⌉. Thus,[[gw⌈c1/x1 ,c2/x2 ⌉ (x3 )]]w⌈c1/x1 ,c2/x2 ⌉= [[gw′ ⌈c2/x2 ⌉ (x3 )]]w′ ⌈c2/x2 ⌉= [[gw′ (x3 )]]w′ ⌈c2/x2 ⌉= [[u]]w⌈c1/x1 ,c2/x2 ⌉ .
Therefore, w |= ⌈c1/x1 , c2/x2 ⌉(x3 = u).

□

The eager intervention operator ⌈·⌉ is distributive w.r.t. logical connectives.
Proposition 11 (Distributive laws of ⌈·⌉) Let x ∈ CVar+ , c ∈ dConst+ ,and φ, φ′ ∈ Fml.
(i) DistrEI ¬(ii) DistrEI →|= ⌈c/x⌉¬φ ↔ ¬⌈c/x⌉φ.
|= ⌈c/x⌉(φ → φ′ ) ↔ ⌈c/x⌉φ → ⌈c/x⌉φ′ .

Similarly, the eager intervention operator ⌈·⌉ is distributive w.r.t. ∨ and ∧.
Proof. Let w be a world such that x ∈ Var(w)+ .
(i)
w |= ⌈c/x⌉¬φ iff w⌈c/x⌉ |= ¬φiff w⌈c/x⌉ ̸|= φ
iff w ̸|= ⌈c/x⌉φ
iff w |= ¬⌈c/x⌉φ.

30

Y. Kawamoto et al.

(ii) We first show the direction from left to right as follows.
w |= ⌈c/x⌉(φ → φ′ ) and w |= ⌈c/x⌉φ=⇒ w⌈c/x⌉ |= φ → φ′ and w⌈c/x⌉ |= φ=⇒ w⌈c/x⌉ |= φ′=⇒ w |= ⌈c/x⌉φ′ .
We next show the other direction as follows. Assume that w |= ⌈c/x⌉φ →⌈c/x⌉φ′ . Then:w⌈c/x⌉ |= φ=⇒ w |= ⌈c/x⌉φ=⇒ w |= ⌈c/x⌉φ′(by assumption)′=⇒ w⌈c/x⌉ |= φ .
Hence w |= ⌈c/x⌉(φ → φ′ ) iff w |= ⌈c/x⌉φ → ⌈c/x⌉φ′ .
B.3□

Validity of the Axioms for Lazy Interventions

Here are the axioms of AX with the lazy interventions ⌊·⌋.
DGLI

⊢g ⌊c/x⌋φ iff ⊢g⌊c/x⌋ φ

CondLI⊢g (f = y|x=c ) ↔ ⌊c/x⌋(f = y|x=c )EqLI⊢g u1 = u2 ↔ ⌊c/x⌋(u1 = u2 )if fv(u1 ) = fv(u2 ) = ∅SplitLI⊢g ⌊c1/x1 , c2/x2 ⌋φ → ⌊c1/x1 ⌋⌊c2/x2 ⌋φSimulLI⊢g ⌊c1/x1 ⌋⌊c2/x2 ⌋φ → ⌊c1/x′1 , c2/x2 ⌋φ′

if x′1 = x1 \ x2 and c′1 = c1 \ c2
RptLI⊢g ⌊c/x⌋φ → ⌊c/x⌋⌊c/x⌋φ

CmpLI


⊢g ⌊c1/x1 ⌋(x2 = c2 ) ∧ ⌊c1/x1 ⌋(x3 = u)
→ ⌊c1/x1 , c2/x2 ⌋(x3 = u)DistrLI ¬DistrLI∧⊢g (⌊c/x⌋¬φ) ↔ (¬⌊c/x⌋φ)⊢g (⌊c/x⌋(φ1 ∧ φ2 )) ↔ (⌊c/x⌋φ1 ∧ ⌊c/x⌋φ2 )Proposition 12 (Basic properties of ⌊·⌋) Let x, x1 , x2 , x3 , y ∈ CVar+ be disjoint, c, c1 , c2 ∈ dConst+ , u, u1 , u2 ∈ Term+ , f ∈ Fsym, and φ ∈ Fml.
1. DGLI|=g ⌊c/x⌋φ iff ⊢g⌊c/x⌋ φ.
2. CondLI|= (f = y|x=c ) ↔ ⌊c/x⌋(f = y|x=c ).
3. EqLI|= u1 = u2 ↔ ⌊c/x⌋(u1 = u2 ) if fv(u1 ) = fv(u2 ) = ∅.
4. SplitLI |= ⌊c1/x1 , c2/x2 ⌋φ → ⌊c1/x1 ⌋⌊c2/x2 ⌋φ′
5. SimulLI |= ⌊c1/x1 ⌋⌊c2/x2 ⌋φ → ⌊c1/x′1 , c2/x2 ⌋φ if x′1 =x1 \x2 and c′1 =c1 \c2 .

Formalizing Statistical Causality via Modal Logic

6. RptLI
7. CmpLI

31|= ⌊c/x⌋φ → ⌊c/x⌋⌊c/x⌋φ.
|= ⌊c1/x1 ⌋(x2 = c2 ) ∧ ⌊c1/x1 ⌋(x3 = u)
→ ⌊c1/x1 , c2/x2 ⌋(x3 = u).

Proof. Let w = (gw , ξw , mw ) be a world such that x, x1 , x2 , x3 , y ∈ Var(w)+ .
1. The proof is similar to Proposition 10.
2. Let gw (x) = u, Gw be the causal diagram corresponding to gw , and DEC(x)be the set of all descendant variables of x. Let y0 , y1 be possibly empty
tuples of variables such that y = y0 :: y1 , y0 ⊆ DEC(x), and y1 ∩ DEC(x) = ∅.
Then on every undirected path between y0 and y1 in Gw , x are on chainsor forks. Hence PGw (y0 :: y1 |x) = PGw (y0 |x) · PGw (y1 |x). Thus, we obtain:[[y|x=c ]]w= PGw (y0 :: y1 |x = c)
= PGw (y0 |x = c) · PGw (y1 |x = c)
= PGw⌊c/x⌋ (y0 |x = c) · PGw ⌊c/x⌋ (y1 |x = c)
= PGw⌊c/x⌋ (y0 :: y1 |x = c)
= [[y|x=c ]]w⌊c/x⌋ .
Therefore, w |= f = y|x=c iff w |= ⌊c/x⌋f = y|x=c .
3. Assume that fv(u1 ) = fv(u2 ) = ∅. Then for each i = 1, 2, [[ui ]]w = [[ui ]]w⌊c/x⌋ .
Hence, |= u1 = u2 ↔ ⌊c/x⌋(u1 = u2 ).
4. The proof is straightforward from the definition.
5. The proof is straightforward from the definition.
6. The proof is straightforward from the definition.
7. Assume that w |= ⌊c1/x1 ⌋(x2 = c2 ) ∧ ⌊c1/x1 ⌋(x3 = u). Then gw⌊c1/x1 ⌋ (x2 ) =c2 and gw⌊c1/x1 ⌋ (x3 ) = u. Let w′ = w⌊c1/x1 ⌋. Thus,[[gw⌊c1/x1 ,c2/x2 ⌋ (x3 )]]w⌊c1/x1 ,c2/x2 ⌋= [[gw′ ⌊c2/x2 ⌋ (x3 )]]w′ ⌊c2/x2 ⌋= [[gw′ (x3 )[x2 7→ c2 ]]]w′ ⌊c2/x2 ⌋= [[u[x2 7→ c2 ]]]w′ ⌊c2/x2 ⌋= [[u]]w′ ⌊c2/x2 ⌋ .
= [[u]]w⌊c1/x1 ,c2/x2 ⌋ .
Therefore, w |= ⌊c1/x1 , c2/x2 ⌋(x3 = u).

□

The lazy intervention operator⌊·⌋ is also distributive w.r.t. logical connectives.
Proposition 13 (Distributive laws of ⌊·⌋) Let x ∈ CVar+ , c ∈ dConst+ ,and φ, φ′ ∈ Fml.
(i) DistrLI ¬(ii) DistrLI →|= ⌊c/x⌋¬φ ↔ ¬⌊c/x⌋φ.
|= ⌊c/x⌋(φ → φ′ ) ↔ ⌊c/x⌋φ → ⌊c/x⌋φ′ .

Similarly, the lazy intervention operator ⌊·⌋ is distributive w.r.t. ∨ and ∧.
Proof. The proofs are analogous to those for Proposition 11.

□

32

Y. Kawamoto et al.

B.4

Validity of the Exchanges of Eager/Lazy Interventions

Here are the axioms of AX for the exchanges of eager/lazy interventions.
ExpdEILI ⊢g (⌈c/x⌉c′ = y) ↔ (⌊c/x⌋c′ = y)
ExcdEILI ⊢g pos(z) → (⌈c/x⌉f = y|z )↔(⌊c/x⌋f = y|z )Proposition 14 (Exchanges of ⌈·⌉ and ⌊·⌋) Let x, y, z ∈ CVar+ , c, c′ ∈ dConst+ ,and f ∈ Fsym.
(i) ExpdEILI |= (⌈c/x⌉c′ = y) ↔ (⌊c/x⌋c′ = y).
(ii) ExcdEILI |= pos(z) → (⌈c/x⌉f = y|z )↔(⌊c/x⌋f = y|z ) .
Proof. (i) Let w be a world. By Proposition 6 (ii), we have: [[y]]w⌈c/x⌉ = mw⌈c/x⌉ (y) =mw⌊c/x⌋ (y) = [[y]]w⌊c/x⌋ . Therefore, we obtain the claim.
(ii) Let w be a world such that w |= pos(z). Let c1 , c2 ∈ dConst+ . By the firstclaim, we have w |= (⌈c/x⌉c1 = y :: z) ↔ (⌊c/x⌋c1 = y :: z) and w |=(⌈c/x⌉c2 = z) ↔ (⌊c/x⌋c2 = z). Then we have:[[y|z ]]w⌈c/x⌉ =[[y :: z]]w⌈c/x⌉[[z]]w⌈c/x⌉=[[y :: z]]w⌊c/x⌋[[z]]w⌊c/x⌋= [[y|z ]]w⌊c/x⌋
Therefore, we obtain the claim.
B.5□

Remarks on Axioms and Invalid Formulas

From our axioms, we can derive the following formulas that are considered asaxioms in the previous work [1].
Unq⊢g ⌈u/x⌉(y = d) → ⌈u/x⌉(y ̸= d′ ) for d ̸= d′

We show examples formulas that are not valid in our model. The following
formulas suggest the difference between the intervention ⌈c/x⌉φ and the conditioning (x = c) → φ.
– Strengthened intervention:⌈u1/x1 ⌉φ ̸|= ⌈u1/x1 , u2/x2 ⌉φ.
– Pseudo transitivity:(⌈u/x⌉y = d) ∧ ⌈d/y⌉φ ̸|= ⌈u/x⌉φ.
– Weak pseudo transitivity:(⌈u/x⌉y = d) ∧ ⌈u/x, d/y⌉φ ̸|= ⌈u/x⌉φ.
– Pseudo contraposition:⌈u/x⌉d = y ̸|= ⌈d/y⌉(x = u).

Formalizing Statistical Causality via Modal Logic

33– Replacing conjunction with intervention:x = u ∧ φ ̸|= ⌈u/x⌉φ.
– Pseudo Modus Ponens:(x = u ∧ ⌈u/x⌉φ) ̸|= φ.
– Pseudo Modus Tollens:(¬φ ∧ ⌈u/x⌉φ) ̸|= (x ̸= u).
Similar formulas are not valid also in [1], which does not deal with probability
distributions.
B.6

Remark on Defining Lazy Interventions as Syntax Sugar

We remark that a lazy intervention ⌊c/x⌋ can be defined as syntax sugar if we
expand data generators.
Recall that ⌊c/x⌋φ expresses that φ is satisfied in the lazy intervened world:M, w |= ⌊c/x⌋φ iff M, w⌊c/x⌋ |= φ.
To define ⌊c/x⌋φ as syntax sugar, we expand the data generator gw as follows. For
each x ∈ dom(gw ), we introduce a fresh auxiliary variable x′ , add gw (x′ ) = x,
and replace every occurrence of x in range(gw ) with x′ . Then the corresponding
causal diagram has arrows x A x′ and x′ A y instead of x A y. Now the lazyintervention ⌊c/x⌋φ can be defined as the eager intervention ⌈c/x′ ⌉φ.
In summary, we can replace the lazy intervention ⌊c/x⌋φ with its corresponding eager intervention ⌈c/x′ ⌉φ by considering a model M that have possible
worlds equipped only with expanded data generators.

C

Proof for the Soundness of AXCPIn this section, we prove the soundness of AXCP w.r.t. the Kripke semantics forstatistical causality by showing the validity of the axioms with the d-separation
predicate dsep (Appendix C.1), with the non-ancestor causal predicate nanc(Appendix C.2), and with other causal predicates (Appendix C.3)
C.1

Validity of the Axioms with d-Separation

Here are the axioms of AXCP with the d-separation dsep.
DsepCI⊢g (dsep(x, y, z) ∧ pos(z)) → y|z,x=c = y|z

DsepSm⊢g dsep(x, y, z) ↔ dsep(y, x, z)

DsepDc⊢g dsep(x, y∪y ′ , z) → (dsep(x, y, z) ∧ dsep(x, y ′ , z))

DsepWu⊢g dsep(x, y∪v, z) → dsep(x, y, z∪v)

DsepCn⊢g (dsep(x, y, z)∧dsep(x, v, z∪y)) → dsep(x, y∪v, z)

DsepEI⊢g (⌈c/z⌉dsep(x, y, z)) ↔ dsep(x, y, z)

DsepLI⊢g (⌊c/z⌋dsep(x, y, z)) ↔ dsep(x, y, z)

DsepLIC⊢g dsep(x, y, z ∪ z ′ ) → ⌊c/z⌋dsep(x, y, z ′ )34

Y. Kawamoto et al.

We first show the validity of DsepCI. It is well-known that the d-separation ina causal diagram G implies the conditional independence, but not vice versa [30].
However, if [[x]]w and [[y]]w are conditionally independent given [[z]]w for any
interpretation [[_]]w factorizing G (i.e., for any world w with the data generator
gw corresponding to G), then they are d-separated by z.
Proposition 15 (d-separation and conditional independence) Let x, y ∈CVar+ and z ∈ CVar∗ be disjoint. Let c ∈ dConst+ .
1. DsepCI|= (dsep(x, y, z) ∧ pos(z)) → y|z,x=c = y|z .
2. For any finite, closed, acyclic data generator g, we have:|=g (pos(z) → y|z,x=c = y|z )implies|=g dsep(x, y, z).

(6)

Proof. We show the first claim as follows. Let w be a world. Assume that w |=dsep(x, y, z) ∧ pos(z). Then in the causal diagram Gw , x and y are d-separated
by z. Thus, x and y are conditionally independent given z. Therefore, w |=y|z,x=c = y|z .
We show the second claim as follows. Assume that |=g (pos(z) → y|z,x=c =y|z ). Then, for any world w with a data generator g, [[x]]w and [[y]]w are conditionally independent given [[z]]w . Let G be the causal diagram corresponding tog. We recall that if x and y are conditionally independent given z for any joint
distribution PG factorized according to G, then they are d-separated by z in G
(see e.g., [30]). Therefore, we obtain |=g dsep(x, y, z).
□d-separation is known to satisfy the semi-graphoid axioms [35], which we candescribe using our logic as follows:
Proposition 16 (Semi-graphoid) Let x, y, y ′ ∈ CVar+ and z, v ∈ CVar∗ bedisjoint. Then dsep satisfies:
1. DsepSm (symmetry):|= dsep(x, y, z) ↔ dsep(y, x, z).
2. DsepDc (decomposition):|= dsep(x, y ∪ y ′ , z) → (dsep(x, y, z) ∧ dsep(x, y ′ , z)).
3. DsepWu (weak union):|= dsep(x, y ∪ v, z)→dsep(x, y, z ∪ v).
4. DsepCn (contraction):|= (dsep(x, y, z) ∧ dsep(x, v, z ∪ y)) → dsep(x, y ∪ v, z).
The causal predicates and interventions satisfy the following axioms, which
are later used in Appendix D to prove the soundness of Pearl’s do-calculus
rules (Proposition 2). We prove the validity of these axioms and an additional
property DsepLIC as follows.
Proposition 17 (Relationships between dsep and ⌈·⌉) Let x, y ∈ CVar+and z, z ′ ∈ CVar∗ be disjoint, and c ∈ dConst+ .

Formalizing Statistical Causality via Modal Logic

1. DsepEI1
2. DsepEI2
3. DsepLI1
4. DsepLI2
5. DsepLIC

35|= (⌈c/z⌉dsep(x, y, z)) → dsep(x, y, z).
|= dsep(x, y, z) → ⌈c/x⌉dsep(x, y, z).
|= (⌊c/z⌋dsep(x, y, z)) → dsep(x, y, z).
|= dsep(x, y, z) → ⌊c/x⌋dsep(x, y, z).
|= dsep(x, y, z ∪ z ′ ) → ⌊c/z⌋dsep(x, y, z ′ ).

Proof. Let w be a world such that x, y ∈ Var(w)+ and z, z ′ ∈ Var(w)∗ . Recall that a data generator corresponds to a causal diagram that is defined as adirected acyclic graph (DAG) in Section 4. Let G be the causal diagram corresponding to the data generator gw in the world w.
Then the causal diagram G⌈c/x⌉ corresponding to gw⌈c/x⌉ is obtained byremoving all arrows pointing to x in G. Similarly, the causal diagram G⌊c/x⌋
corresponding to gw⌊c/x⌋ is obtained by removing all arrows emerging from x
in G.
1. Assume that w |= ⌈c/z⌉dsep(x, y, z). Then w⌈c/z⌉ |= dsep(x, y, z). Let p be
an undirected path between x and y in G⌈c/x⌉. Since x and y are d-separated
by z in the diagram G⌈c/z⌉, we have:(a) there is no path p in G⌈c/z⌉ that has a chain v ′ A v A v ′′ s.t. v ∈ z;(b) there is no path p in G⌈c/z⌉ that has a fork v ′ v A v ′′ s.t. v ∈ z;(c) if G⌈c/z⌉ has a path with a collider v ′ A v v ′′ , then v ̸∈ ANC∗ (z).
By (a), if G has an undirected path with a chain v ′ A v A v ′′ , then v ∈ z,
because v ̸∈ z contradicts (a).
v A v ′′ , then v ∈ z,
By (b), if G has an undirected path with a fork v ′because v ̸∈ z contradicts (b).
Let p be an undirected path in G⌈c/z⌉ that has a collider v ′ A vv ′′ . By(c), we have v ̸∈ ANC∗ (z) in G⌈c/z⌉. Then, G also has the same path p, andthe arrows connecting with v in G are the same as those in G⌈c/z⌉. Hence,
we obtain v ̸∈ ANC∗ (z) in G.
Therefore, w |= dsep(x, y, z).
2. Assume that w |= dsep(x, y, z). Then in the diagram G, x and y are dseparated by z. By definition, G⌈c/x⌉ is the same as G except that it has noarrows pointing to x. Hence, also in G⌈c/x⌉, x and y are d-separated by z.
Therefore, w |= ⌈c/x⌉dsep(x, y, z).
3. Assume that w |= ⌊c/z⌋dsep(x, y, z). Then w⌊c/z⌋ |= dsep(x, y, z). Let p be
an undirected path between x and y in G⌊c/x⌋. Since x and y are d-separated
by z in the diagram G⌊c/z⌋, we have:(a) there is no path p in G⌊c/z⌋ that has a chain v ′ A v A v ′′ s.t. v ∈ z;(b) there is no path p in G⌊c/z⌋ that has a fork v ′ v A v ′′ s.t. v ∈ z;(c) if G⌊c/z⌋ has a path with a collider v ′ A v v ′′ , then v ̸∈ ANC∗ (z).
By (a), if G has an undirected path with a chain v ′ A v A v ′′ , then v ∈ z,
because v ̸∈ z contradicts (a).
By (b), if G has an undirected path with a fork v ′v A v ′′ , then v ∈ z,
because v ̸∈ z contradicts (b).
Let p be an undirected path in G⌊c/z⌋ that has a collider v ′ A vv ′′ . By(c), we obtain v ̸∈ ANC∗ (z) in G⌊c/z⌋. Then, G also has the path p, and may
A

A

A

A

A

A

A

A

36

Y. Kawamoto et al.

have additional arrows pointing to v and no arrows pointing from v. Hence,
we obtain v ̸∈ ANC∗ (z) in G.
Therefore, w |= dsep(x, y, z).
4. The proof for Claim 4 is analogous to that for Claim 2.
5. Assume that w |= dsep(x, y, z ∪ z ′ ). Then in the diagram G, x and y are
d-separated by z ∪ z ′ . By definition, G⌊c/z⌋ has no arrows emerging from z.
If G⌊c/x⌋ has no undirected path between x and y, then x and y are dseparated by z ′ , hence w |= ⌊c/x⌋dsep(x, y, z ′ ).
Otherwise, let p be an undirected path between x and y in G⌊c/x⌋. Since
x and y are d-separated by z ∪ z ′ , we fall into one of the three cases in
Definition 2.
(a) If p has a chain v ′ → v → v ′′ s.t. v ∈ z ∪ z ′ , then v ∈ z ′ , because G⌊c/z⌋
has no arrows pointing from z. Hence, p is d-separated by z ′ .
(b) For the same reason as (a), if p has a fork v ′ ← v → v ′′ s.t. v ∈ z ∪ z ′ ,then v ∈ z ′ . Hence, p is d-separated by z ′ .
(c) If p has a collider v ′ → v ← v ′′ s.t. v ̸∈ ANC∗ (z ∪ z ′ ), then v ̸∈ ANC∗ (z ′ ).
Thus p is d-separated by z ′.
Therefore, w |= ⌊c/x⌋dsep(x, y, z ′ ).
□Remark 2. In contrast with Claim 5 in Proposition 17, there exists a world ws.t.
w ̸|= dsep(x, y, z ∪ z ′ ) → ⌈c/z⌉dsep(x, y, z ′ ).
To see this, assume that w |= dsep(x, y, z ∪ z ′ ). Suppose that w has a causal
diagram G where there is an undirected path p between x and y that has a forkv ′ ← v → v ′′ s.t. v ∈ z and no other variable in z ∪ z ′ appears on p. Then G⌈c/z⌉
also has the path p, because the intervention ⌈c/z⌉ removes no arrows in p. Hence,p is d-separated by z but not by z ′ in G⌈c/z⌉. Therefore, w ̸|= ⌈c/z⌉dsep(x, y, z ′ ).

C.2

Validity of the Axioms with nancHere are the axioms of AXCP with the non-anscestor predicate nanc and aproperty Nanc0.
Nanc0⊢g nanc(x, y) → ((c′ = y) ↔ ⌈c/x⌉(c′ = y))

Nanc1⊢g (nanc(x, y) ∧ nanc(x, z)) → (f =y|z ↔ ⌈c/x⌉(f =y|z ))Nanc2⊢g nanc(x, y) ↔ ⌈c/x⌉nanc(x, y)

Nanc3⊢g nanc(x, y) → ⌈c/x⌉dsep(x, y, ∅)Nanc4⊢g (nanc(x, z) ∧ dsep(x, y, z)) → nanc(x, y)Concerning nanc, the axioms Nanc1 to Nanc4 are sufficient for us to derive
the rules of Pearl’s do-calculus.

Formalizing Statistical Causality via Modal Logic

37

Proposition 18 (Validity of axioms with nanc) Let x, y, z ∈ CVar+ be disjoint, c ∈ dConst+ , c′ ∈ Const+ , and f ∈ Fsym.
1. Nanc0|= nanc(x, y) → (c′ = y ↔ ⌈c/x⌉(c′ = y)).
2. Nanc1|= (nanc(x, y) ∧ nanc(x, z)) → (f =y|z ↔ ⌈c/x⌉(f =y|z )).
3. Nanc2|= nanc(x, y) ↔ ⌈c/x⌉nanc(x, y).
4. Nanc3|= nanc(x, y) → ⌈c/x⌉dsep(x, y, ∅).
5. Nanc4|= (nanc(x, z) ∧ dsep(x, y, z)) → nanc(x, y).
Proof. Let w = (gw , ξw , mw ) be a world such that x, y, z ∈ Var(w)+ .
1. Assume that w |= nanc(x, y). Let Gw be the causal diagram corresponding
to the data generator gw . Then x ∩ ANC(y) = ∅ in Gw . This means that thevalue of y does not depend on that of x. Thus we obtain:mw⌈c/x⌉ (y) = [[gw⌈c/x⌉ (y)]]w⌈c/x⌉= [[gw⌈c/x⌉ (y)]]w= [[gw (y)]]w(by ξw⌈c/x⌉ = ξw )(by gw⌈c/x⌉ (y) = gw (y))= mw (y).
Thus, w |= c′ = y iff w⌈c/x⌉ |= c′ = y. Therefore, w |= c′ =y ↔ ⌈c/x⌉(c′ =y).
2. Let c0 , c1 ∈ Const. Assume that w |= nanc(x, y) ∧ nanc(x, z). Then w |=nanc(x, y :: z). By Claim 1, w |= c0 = y :: z ↔ ⌈c/x⌉(c0 = y :: z) and w |=c1 = z ↔ ⌈c/x⌉(c1 = z). By [[y :: z]]w⌈c/x⌉ = [[y :: z]]w and [[z]]w⌈c/x⌉ = [[z]]w ,we have [[y|z ]]w⌈c/x⌉ = [[y|z ]]w . Therefore, w |= f = y|z ↔ ⌈c/x⌉(f = y|z ).
3. We show the direction from left to right as follows. Assume that w |=nanc(x, y). Then, in the diagram G, all variables in x are non-ancestorsof the variables in y; i.e., G has no directed path from x to y. Since theeager intervention ⌈c/x⌉ removes only arrows pointing to x, G⌈c/x⌉ still has
no directed path from x to y. Therefore, w |= ⌈c/x⌉nanc(x, y).
The other direction is shown in a similar way, since the eager intervention⌈c/x⌉ only remove arrows pointing to x.
4. Assume that w |= nanc(x, y). By Claim 3, w |= ⌈c/x⌉nanc(x, y), hencew⌈c/x⌉ |= nanc(x, y). Then, in the diagram G⌈c/x⌉, all variables in x are
non-ancestors of the variables in y; i.e., G⌈c/x⌉ has no directed path from x
to y.
Suppose that G⌈c/x⌉ has no undirected path between x and y. By Definition 2, x and y are d-separated by ∅, namely, they are independent. Hence,w⌈c/x⌉ |= dsep(x, y, ∅). Therefore, w |= ⌈c/x⌉dsep(x, y, ∅).
Suppose that G⌈c/x⌉ has some undirected path p between x and y. By thedefinition of the eager intervention, G⌈c/x⌉ has no arrows pointing to x, hence

38

Y. Kawamoto et al.

has arrows pointing from x. On the other hand, since G⌈c/x⌉ has no directed
path from x to y, p is not directed. Thus, p has a collider node v; i.e., it is of
the form x → · · · → v ← · · · y. Then, by (c) in Definition 2, p is d-separatedby ∅; namely, w⌈c/x⌉ |= dsep(x, y, ∅). Therefore, w |= ⌈c/x⌉dsep(x, y, ∅).
5. We show the contraposition as follows. Assume that w |= ¬nanc(x, y) ∧dsep(x, y, z). Then it is sufficient to prove w |= ¬nanc(x, z).
Recall the definition in Appendix A.4. By assumption, x ∩ ANC(y) ̸= ∅. Then
there are x0 ∈ x and y0 ∈ y s.t. x0 is an ancestor of y0 , i.e., x0 ∈ ANC(y0 ).
Then there exists a directed path from x0 to y0 . Let p be a directed path fromx0 to y0 . By w |= dsep(x, y, z), p is d-separated by z. By (a) of Definition 2,
there is a variable z0 ∈ z on p, hence x0 ∈ ANC(z0 ). Therefore, x∩ANC(z) ̸= ∅,i.e., w |= ¬nanc(x, z).
□
C.3

Validity of the Axioms with Other Causal Predicates

Here are the axioms of AXCP that replace allnanc with nanc and pa with nancor dsep.
AllNanc⊢g allnanc(x, y, z) → nanc(x, z)
PaNanc⊢g pa(x, y) → nanc(y, x)

PaDsep⊢g pa(z, x) → ⌊c/x⌋dsep(x, y, z)

We prove the validity of these axioms as follows.
Proposition 19 (Validity of axioms with other causal predicates) Let x, y, z ∈CVar+ be disjoint, and c ∈ dConst+ .
1. AllNanc
2. PaNanc
3. PaDsep|= allnanc(x, y, z) → nanc(x, z).
|= pa(x, y) → nanc(y, x).
|= pa(z, x) → ⌊c/x⌋dsep(x, y, z).

Proof. Let w = (gw , ξw , mw ) be a world such that x, y, z ∈ Var(w)+ .
1. This claim is straightforward from the definitions of the semantics of allnanc
and nanc.
2. This claim is straightforward from Proposition 7.
3. Assume that w |= pa(z, x). Then, in the diagram G, z is the set of all
variables pointing to x.
If G⌊c/x⌋ has no undirected path between x and y, then x and y are dseparated by z, hence w |= ⌊c/x⌋dsep(x, y, z).
Otherwise, let p be an undirected path between x and y in G⌊c/x⌋. By
definition, G⌊c/x⌋ has no arrows emerging from x. Since z is the set of all
variables pointing to x, p has:
– either a chain x0 ← z0 ← v s.t. x0 ∈ x, z0 ∈ z, and v ̸∈ x ∪ z,
– or a fork x0 ← z0 → v s.t. x0 ∈ x, z0 ∈ z, and v ̸∈ x ∪ z.
Thus, p is d-separated by z0 . Hence, in G⌊c/x⌋, x and y are d-separated byz. Therefore, w |= ⌊c/x⌋dsep(x, y, z).
□Formalizing Statistical Causality via Modal Logic

D

39

Details of the Derivation of the Do-Calculus Rules
Using AXCPIn this section, we formalize and derive the three rules of Pearl’s do-calculus [29]using our statistical causal language (StaCL).
By Proposition 1, StaCL formulas correspond to the do-calculus notations
as follows.
– ⌈c/x⌉(c′ = y) describes the post-intervention distribution PGw (y | do(x = c))of y. For instance, given a world w, w |= ⌈c/x⌉c′ = y represents PGw (y |do(x = c)) = [[c′ ]]w . Note that the do(x = c) operation is expressed as theeager intervention ⌈c/x⌉ in our formulation.
– ⌈c/x⌉(f = y|z ) describes the post-intervention conditional distribution PGw (y |do(x = c), z) of y given z. Note that the conditioning on z takes place after
the intervention do(x = c) is performed.
To formalize the rules of the do-calculus, we denote the set of all conditioning
variables appearing in a formula φ by:
cdv(φ) = {z | y|z ∈ fv(φ) ∩ FVar} ∪ {(z :: x)|x=c | y|z,x=c ∈ fv(φ) ∩ FVar}.
Now we formalize the rules of Pearl’s do-calculus in Proposition 2. After that,
we explain the meaning of these rules.
Proposition 2 (Do-calculus rules) Let v, x, y, z ∈ CVar+ be disjoint, x1 , x2 ∈CVar+ , and c0 , c1 , c2 ∈ dConst+ . Let S = cdv(φ0 ) ∪ cdv(φ1 ).
1. Do1.

Introduction/elimination of conditioning:⊢g ⌈c0/v⌉(dsep(x, y, z) ∧

V

c0
c0
s∈S pos(s)) → ((⌈ /v ⌉φ0 ) ↔ ⌈ /v ⌉φ1 )where φ1 is obtained by replacing some occurrences of y|z in φ0 with y|z,x=c1 ;2. Do2. Exchange between intervention and conditioning:⊢g ⌈c0/v⌉⌊c1/x⌋(dsep(x, y, z) ∧Vs∈S pos(s)) → ((⌈c0/v , c1/x⌉φ ) ↔ ⌈c0/v ⌉φ )01

where φ1 is obtained by replacing every occurrence of y|z in φ0 with y|z,x=c1 ;3. Do3 Introduction/elimination of intervention:⊢g ⌈c0/v⌉(allnanc(x1 , x, y) ∧ ⌈c1/x1 ⌉(dsep(x, y, z) ∧ pos(z)))→ ((⌈c0/v⌉φ) ↔ ⌈c0/v, c1/x1 , c2/x2 ⌉φ)
defwhere fv(φ) = {y|z } and x = x1 :: x2 .
We explain these three rules as follows.

40

Y. Kawamoto et al.

1. The first rule allows for adding/removing the conditioning on x when x andy are d-separated by z (hence when they are conditionally independent givenz).
In the do-calculus, this is expressed by:
P (y | do(v), z) = P (y | do(v), z, x)
if (x ⊥
⊥ y | v, z)Gv
where
– Gv is the diagram obtained by deleting all arrows pointing to nodes in v;– (x ⊥⊥ y | v, z)Gv represents that x and y are d-separated by v ∪ z in thecausal diagram Gv .
In our formulation, the deletion of arrows pointing to v is expressed by theeager intervention ⌈c0/v⌉.
2. The second rule represents that the conditioning on x and the intervention tox result in the same conditional distribution of y given z under the condition
that all back-door paths from x to y (Definition 3) are d-separated by v ∪ z(Definition 2).6
In the do-calculus, this is expressed by:
P (y | do(v), x, z) = P (y | do(v), do(x), z)
if (x ⊥
⊥ y | z, v)Gvx
where Gvx is the diagram obtained by deleting all arrows pointing to nodesin v and deleting all arrows emerging from nodes in x.
In our formulation, the “upper manipulation” v is expressed by the eager
intervention ⌈c0/v⌉ whereas the “lower-manipulation” x is expressed by thelazy intervention ⌊c1/x⌋.
Recall that the lazy intervention ⌊c1/x⌋ removes all arrows emerging fromx, and hence preserves only back-door paths from x to y while removing allother undirected paths between x and y (Remark 1). Thus, ⌊c1/x⌋dsep(x, y, z)
represents that all back-door paths from x to y are d-separated by z.
3. The third rule allows for adding/removing the intervention to x withoutchanging the conditional probability distribution of y given z under a certain
condition.
In the do-calculus, this is expressed by:
P (y | do(v), z) = P (y | do(v), do(x), z)
if (x ⊥
⊥ y | z, v)Gvx\ANC(z)where Gvx\ANC(z) is the diagram obtained by deleting all arrows pointing tonodes in v and then deleting those in x \ ANC(z).
Now, we derive these three rules using AXCP as follows.
6This condition is denoted by ⌊c1/x⌋dsep(x, y, z ∪ v) and follows from Proposition 17
and dsep(x, y, z ∪ v).

Formalizing Statistical Causality via Modal Logic

41

Proof. Let w be a world such that v, x, y, z, x1 , x2 ∈ CVar(w)+ .
defVs∈S pos(s).

⊢g⌈c0/v⌉ (dsep(x, y, z) ∧ pos(z)) → (y|z,x=c1 = y|z )(7)

1. We prove the first claim as follows. Let ψpre = dsep(x, y, z) ∧Then:
By DsepCI,By (7), Eq2, PT, MP,⊢g⌈c0/v⌉ ψpre → (φ0 ↔ φ1 )(8)

By (8), DGEI , MP,⊢g ⌈c0/v⌉(ψpre → (φ0 ↔ φ1 ))
∧

(9)

→

By (9), DistrEI , DistrEI , PT, MP,⊢g (⌈c0/v⌉ψpre ) → ((⌈c0/v⌉φ0 ) ↔ ⌈c0/v⌉φ1 ).
Therefore, Claim (1) follows.
def

2. We prove the second claim as follows. Let ψpre = dsep(x, y, z)∧
Then:

V

s∈S pos(s).

By DsepCI,⊢g⌈c0/v⌉⌊c1/x⌋ (dsep(x, y, z) ∧ pos(z)) → (y|z,x=c1 = y|z )(10)

By (10), DGEI , MP,⊢g⌈c0/v⌉ ⌊c1/x⌋ (dsep(x, y, z) ∧ pos(z)) → (y|z,x=c1 = y|z )



(11)

→

By (11), DistrEI , MP,⊢g⌈c0/v⌉ (⌊c1/x⌋(dsep(x, y, z) ∧ pos(z)))→ (⌊c1/x⌋y|z,x=c1 = y|z )(12)By (12), EqF , PT, MP,⊢g⌈c0/v⌉ (⌊c1/x⌋(dsep(x, y, z) ∧ pos(z)))→ (⌊c1/x⌋f = y|z,x=c1 ↔ ⌊c1/x⌋f = y|z )(13)

By (13), CondLI , PT, MP,⊢g⌈c0/v⌉ (⌊c1/x⌋(dsep(x, y, z) ∧ pos(z)))→ (f = y|z,x=c1 ↔ ⌊c1/x⌋f = y|z )(14)

By (14), ExcdEILI , PT, MP,⊢g⌈c0/v⌉ (⌊c1/x⌋(dsep(x, y, z) ∧ pos(z)))→ (f = y|z,x=c1 ↔ ⌈c1/x⌉f = y|z )(15)

By (15), Eq2, PT, MP,⊢g⌈c0/v⌉ (⌊c1/x⌋ψpre ) → ((⌈c1/x⌉φ0 ) ↔ φ1 )(16)

By (16), DGEI , MP,⊢g ⌈c0/v⌉ (⌊c1/x⌋ψpre ) → ((⌈c1/x⌉φ0 ) ↔ φ1 )→By (17), DistrEI , PT, MP,



(17)

42

Y. Kawamoto et al.

⊢g (⌈c0/v⌉⌊c1/x⌋ψpre ) → ((⌈c0/v⌉⌈c1/x⌉φ0 ) ↔ ⌈c0/v⌉φ1 )(18)

By (18), SimulEI , MP,⊢g (⌈c0/v⌉⌊c1/x⌋ψpre ) → ((⌈c0/v, c1/x⌉φ0 ) ↔ ⌈c0/v⌉φ1 ).
Therefore, Claim (2) follows.
def

3. We prove the third claim as follows. Let f ∈ Fsym, ψdp = dsep(x, y, z) ∧def
defpos(z), ψpre = allnanc(x1 , x, y)∧⌈c1/x1 ⌉ψdp , and ψdo2 = ⌊c2/x2 ⌋(dsep(x2 , y, z)∧defpos(z)). Let g 0 = g⌈c0/v⌉. Then:
By PT, MP,⊢g0 ψpre → ⌈c1/x1 ⌉ψdp

(19)

By DsepDc, PT, MP,⊢g 0 ⌈c1/x1 ⌉ ψdp → (dsep(x1 , y, z) ∧ pos(z))(20)⊢g 0 ⌈c1/x1 ⌉ ψdp → (dsep(x2 , y, z) ∧ pos(z))(21)

By DsepCI, MP,⊢g 0 ⌈c1/x1 ⌉ (dsep(x2 , y, z) ∧ pos(z)) → (y|z,x2 =c2 = y|z )(22)

By EqF , PT, MP,⊢g 0 ⌈c1/x1 ⌉ (f0 = y|z )(23)

By DGEI , MP,⊢g0 ⌈c1/x1 ⌉(f0 = y|z )(24)

By (21), DsepLI2 ,PT,MP,⊢g 0 ⌈c1/x1 ⌉ ψdp → ⌊c2/x2 ⌋(dsep(x2 , y, z) ∧ pos(z))(25)

By AllNanc, PT, MP,⊢g0 ψpre → nanc(x1 , z)

(26)

By (26), Nanc2, PT, MP,⊢g0 ψpre → ⌈c1/x1 ⌉nanc(x1 , z)(27)

By Nanc4, PT, MP,⊢g 0 ⌈c1/x1 ⌉ (dsep(x1 , y, z) ∧ nanc(x1 , z))→ (nanc(x1 , y) ∧ nanc(x1 , z))(28)

By (28), DGEI , MP,⊢g0 ⌈c1/x1 ⌉((dsep(x1 , y, z) ∧ nanc(x1 , z))→ (nanc(x1 , y) ∧ nanc(x1 , z)))
→

(29)

∧

By (29), DistrEI , DistrEI , MP,⊢g0 ((⌈c1/x1 ⌉dsep(x1 , y, z) ∧ ⌈c1/x1 ⌉nanc(x1 , z)))→ (⌈c1/x1 ⌉nanc(x1 , y) ∧ ⌈c1/x1 ⌉nanc(x1 , z))(30)

By (30), Nanc2, PT, MP,⊢g0 ((⌈c1/x1 ⌉dsep(x1 , y, z) ∧ ⌈c1/x1 ⌉nanc(x1 , z)))→ (nanc(x1 , y) ∧ nanc(x1 , z))(31)Formalizing Statistical Causality via Modal Logic

43

By (31), Nanc1, PT, MP,⊢g0 ((⌈c1/x1 ⌉dsep(x1 , y, z) ∧ ⌈c1/x1 ⌉nanc(x1 , z)))→ ((f1 = y|z ) ↔ ⌈c1/x1 ⌉(f1 = y|z ))(32)

By (32), (20), PT, MP,⊢g0 ((⌈c1/x1 ⌉ψdp ) ∧ ⌈c1/x1 ⌉nanc(x1 , z))→ ((f1 = y|z ) ↔ ⌈c1/x1 ⌉(f1 = y|z ))(33)

By (33), (27), (19), PT, MP,⊢g0 ψpre → ((f1 = y|z ) ↔ ⌈c1/x1 ⌉(f1 = y|z ))(34)

By (34), (24), Eq2, PT, MP,⊢g0 ψpre → ((f0 = y|z ) ↔ ⌈c1/x1 ⌉(f0 = y|z ))(35)

By Do2, PT,MP,⊢g 0 ⌈c1/x1 ⌉ ψdo2 → (f2 = y|z,x2 =c2 ↔ ⌈c2/x2 ⌉f2 = y|z )(36)

By (36), (25), PT, MP,⊢g 0 ⌈c1/x1 ⌉ ψdp → (f2 = y|z,x2 =c2 ↔ ⌈c2/x2 ⌉f2 = y|z )(37)

By (37), (23), Eq2, PT, MP⊢g 0 ⌈c1/x1 ⌉ ψdp → (f0 = y|z ↔ ⌈c2/x2 ⌉f0 = y|z )
→

(38)

∧

By (38), DGEI , DistrEI , DistrEI , PT, MP,⊢g0 ⌈c1/x1 ⌉ψdp → ((⌈c1/x1 ⌉f0 = y|z ) ↔ ⌈c1/x1 ⌉⌈c2/x2 ⌉f0 = y|z )(39)

By (39), (19), PT, MP,⊢g0 ψpre → ((⌈c1/x1 ⌉f0 = y|z ) ↔ ⌈c1/x1 ⌉⌈c2/x2 ⌉f0 = y|z )(40)

By (35), (40), Eq2, PT, MP,⊢g0 ψpre → ((f0 = y|z ) ↔ ⌈c1/x1 ⌉⌈c2/x2 ⌉f0 = y|z )(41)

By (41), DGEI , PT, MP,⊢g (⌈c0/v⌉ψpre )→ ((⌈c0/v⌉f0 = y|z ) ↔ ⌈c0/v⌉⌈c1/x1 ⌉⌈c2/x2 ⌉f0 = y|z )(42)

By (42), SimulEI , MP,⊢g (⌈c0/v⌉ψpre )→ ((⌈c0/v⌉f0 = y|z ) ↔ ⌈c0/v, c1/x1 , c2/x2 ⌉f0 = y|z )(43)

By (43), Eq2, PT, MP,⊢g (⌈c0/v⌉ψpre )→ ((⌈c0/v⌉φ) ↔ ⌈c0/v, c1/x1 , c2/x2 ⌉φ)Therefore, Claim (3) follows.

□