# On Probabilistic and Causal Reasoning with Summation Operators

Duligur Ibeling∗, Thomas Icard∗, and Milan Mossé†
∗ Stanford University
† University of California, Berkeley

(May 2024)

###### Abstract

Ibeling et al., (2023) axiomatize increasingly expressive languages of
causation and probability, and Mossé et al., (2024) show that reasoning
(specifically the satisfiability problem) in each causal language is as
difficult, from a computational complexity perspective, as reasoning in its
merely probabilistic or “correlational” counterpart. Introducing a summation
operator to capture common devices that appear in applications—such as the
$do$-calculus of Pearl, (2009) for causal inference, which makes ample use of
marginalization—van der Zander et al., (2023) partially extend these earlier
complexity results to causal and probabilistic languages with marginalization.
We complete this extension, fully characterizing the complexity of
probabilistic and causal reasoning with summation, demonstrating that these
again remain equally difficult. Surprisingly, allowing free variables for
random variable values results in a system that is undecidable, so long as the
ranges of these random variables are unrestricted. We finally axiomatize these
languages featuring marginalization (or more generally summation), resolving
open questions posed by Ibeling et al., (2023).

##  1 Introduction and Motivation

One important research program in probability logic is to design, analyze, and
compare alternative formal language fragments designed to reason about
probability distributions. The usual logical tradeoff between expressive
power—how much one can say—and (both formal and intuitive) complexity is very
much on display in this subject. At one extreme are very simple languages that
admit only of “qualitative” likelihood comparisons between events, which are
often no more complex than propositional logic (Fagin et al.,, 1990; Ibeling
et al.,, 2023). Toward the other extreme are first-order probability logical
languages whose validity problems are often highly undecidable, not even
arithmetical (Abadi and Halpern,, 1994).

Summing over the values of a random variable is ubiquitous in the theory and
application of probability. Marginalizing out a variable, or taking an
expectation of a (discrete) variable, for example, involves summing an
expression over all possible values of that variable. Summation operators,
however, rarely appear in studies of probability logic. In the finite
setting—for instance, where all random variables come with a fixed, finite
range of possible values—this is immaterial when it comes to the expressive
power of the language. Any such sum can simply be replaced be an explicit
application of binary addition over all the summands. There are several
limitations to this strategy, however. The first is obviously that it does not
extend to the infinitary setting. Indeed, it does not even work in the setting
of finite ranged variables but where those ranges (and perhaps their sizes)
are unknown. That is, the variable values may not all be named by a constant
in the language. A second, more subtle limitation is that summation operators
may affect the complexity of the language, since they may facilitate succinct
encodings of statements that would otherwise require very long expressions. As
recently shown by van der Zander et al., (2023), adding a marginalization
operator to a polynomial language results in a substantial complexity
increase.

The present contribution aims at a thorough analysis of probability logics
with summation operators, building on previous work, and focusing on questions
of axiomatization and computational complexity. Part of our motivation comes
not from ordinary probabilistic reasoning, but from problems in causal
reasoning. In addition to the well-known logical problem of induction—the fact
that any pattern of observations is logically compatible with any continuation
of it—there is also a deep logical problem of causation: roughly, the fact
that any pattern of observations logically underdetermines what would happen
to a system when some agent acts upon the system. By capturing what is meant
by “data,” “causal assumptions,” and “causal conclusions” with formal
languages, these types of result can be construed as (everywhere or _almost_
everywhere) logical undefinability results (Bareinboim et al.,, 2022; Ibeling
and Icard,, 2021). The relevant formalisms commonly build on an appropriate
choice of probability logical language.

In addition to facilitating such negative results, logical formalization of
causal reasoning also facilitates the analysis and verification of positive
results. Seminal observations across many fields—from econometrics to
artificial intelligence to epidemiology—can be cast in a rigorous manner,
sometimes highlighting and clarifying hidden assumptions that might otherwise
go unnoticed. Here are two well-known _identifiability_ results that help
motivate the kinds of languages we study in this paper:

######  Example 1 (Local average treatment effect).

Imagine a clinical trial that involves assignment ($Z$) to a control condition
(value $z^{-}$) or a treatment condition (value $z^{+}$), with some outcome
$Y$ of interest. The trial cannot guarantee full compliance, so there is an
additional variable ($X$) for whether the treatment is in fact administered
(has value $x^{+}$, as opposed to $x^{-}$).

A quantity of interest is the causal effect of the treatment ($X$) on the
outcome ($Y$), among those who comply with their assignment. This is the
conditional expectation $\mathbf{E}(Y_{x^{+}}-Y_{x^{-}}\mid x^{+}_{z^{+}}\land
x^{-}_{z^{-}})$,111Note that $x^{+}_{z^{+}}$, etc. abbreviates the potential
outcome $X_{Z=z^{+}}=x^{+}$, etc. which in general is given by the sum,

$\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{y,y^{\prime}}\,(\mathsf{y}-\mathsf{y}^{\prime})\cdot\mathsf{P}(y_{x^{+}}\land
y^{\prime}_{x^{-}}\mid x^{+}_{z^{+}}\land x^{-}_{z^{-}}),$ (1)

and thus when $Y$ is also binary (with range $\\{y^{-}=0,y^{+}=1\\}$), simply
by the difference $\mathsf{P}(y^{+}_{x^{+}}\mid x^{+}_{z^{+}}\land
x^{-}_{z^{-}})-\mathsf{P}(y^{+}_{x^{-}}\mid x^{+}_{z^{+}}\land
x^{-}_{z^{-}})$.

For various reasons researchers may not be able to track which individuals
comply with their assignments. This is a typical “Level 3” counterfactual
claim, a class that is in general difficult to ascertain empirically (see
Bareinboim et al., 2022; Ibeling and Icard, 2021). It was observed by Angrist
et al., (1996) that (1) can nonetheless be determined from typically available
experimental data, provided two assumptions are made. First, it must be that
$Z$ (assignment) affects $Y$ (the outcome) only through the variable $X$.
Second, there should be no _defiers_ , that is, individuals who would take the
treatment if and only if they are assigned to the control condition.
Symbolically, using notation to be introduced in the sequel, this positive
result can be viewed as a fact about entailment in suitable causal-probability
logical languages:

$\big{[}y\not\equiv y^{\prime}\rightarrow\mathsf{P}(y_{x,z^{+}}\wedge
y^{\prime}_{x,z^{-}})\approx\underline{0}\big{]},\quad\mathsf{P}(x^{-}_{z^{+}}\wedge
x^{+}_{z^{-}})\approx\underline{0}\\\ \vDash\mathbf{E}(Y_{x^{+}}-Y_{x^{-}}\mid
x^{+}_{z^{+}}\land
x^{-}_{z^{-}})\approx\frac{\mathbf{E}\big{(}Y_{z^{+},X_{z^{+}}}-Y_{z^{-},X_{z^{-}}}\big{)}}{\mathbf{E}(X_{z^{+}}-X_{z^{-}})}.$
(2)

Any situation in which the claims appearing before the turnstile symbol
$\vDash$ are all true will guarantee that the conditional expectation after
the symbol is equal to this ratio. In the setting where $Y$ is binary, this
can be derived in a relatively simple logical calculus for (probabilistic)
causal reasoning (Ibeling and Icard,, 2023), and it can also be shown that
both numerator and denominator of the ratio are identifiable.

######  Example 2 (Front-door criterion).

For a second example, suppose one is interested in the probability of $Y$
taking on some value $y$ given an intervention setting variable $X$ to $x$,
notated by $\mathsf{P}(y_{x})$. Imagine, however, that one has only passive
observational access to the $X$ and $Y$. In general, it is impossible to infer
$\mathsf{P}(y_{x})$, even given perfect access to the full joint distribution
$\mathsf{P}(X,Y)$ (see again Bareinboim et al., 2022).

Nevertheless, as shown in Pearl, (1995), it is possible to determine such
probabilities exactly from interventional data, provided one can make certain
independence assumptions involving one more “intermediate mechanism” $Z$. The
crucial fact is the following causal-probabilistic logical entailment:

$\mathsf{P}(z_{x})\approx\mathsf{P}(z\mid
x),\quad\mathsf{P}(x_{z})\approx\mathsf{P}(x),\quad\mathsf{P}(y_{x}\mid
z_{x})\approx\mathsf{P}(y_{x,z}),\quad\mathsf{P}(y_{x,z})\approx\mathsf{P}(y_{z}),\quad\mathsf{P}(y_{z}\mid
x_{z})\approx\mathsf{P}(y\mid x,z)\\\
\vDash\mathsf{P}(y_{x})\approx\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{z}\mathsf{P}(z\mid
x)\cdot\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x^{\prime}}\mathsf{P}(y\mid
x^{\prime},z)\cdot\mathsf{P}(x^{\prime}).$

So long as the equalities before the turnstile all hold, the final identity is
guaranteed. Pearl’s (1995; 2009) _$do$ -calculus_ presents a correspondence
between graphical properties and independencies. For instance, all of the
equalities before the turnstile will hold on the graph depicted in Figure 1.

$X$$Z$$Y$$U$ Figure 1: Front-door graph.

In other words, if a practitioner happens to know that a domain is one in
which $X$ causes $Y$ only through an intermediate mechanism $Z$, and any
further confounding ($U$) exerts influence on only $X$ and $Y$ (and in
particular, not on $Z$), then the identification is valid. That is, one can
determine the interventional probability knowing only the relevant
observational probabilities.

Both of these examples illustrate cases where some constraints on a causal
setup—i.e., the expressions on the left-hand side of the turnstile—are
sufficient to entail that some causal quantity of interest on the right-hand
side can be identified with another expression that may be more empirically
tractable. Notably, these conclusions follow as a matter of logical
entailment.

A natural starting point for formalizing these styles of reasoning is to
employ some form of probability logic. This is precisely the strategy pursued
in recent work by Ibeling and Icard, (2020, 2021, 2023); Mossé et al., (2024);
Bareinboim et al., (2022). As a typical example language, we might have
Boolean combinations of real polynomials over probability terms, where those
probability terms include interventional probabilities like
$\mathsf{P}(y_{x})$, as well as so-called counterfactual probabilities like
$\mathsf{P}(y^{+}_{x^{+}}\wedge y^{-}_{x^{-}})$, and so on. Provided the
variable ranges are all finite, examples like those in Exs. 1 and 2 can be
easily formalized. The works cited above investigate standard logical issues
for such languages, viz. complexity, definability, axiomatization, etc. In
particular, Mossé et al., (2024) characterize the complexity of (suitably
formalized) causal reasoning, thereby circumscribing the complexity of common
tools for causal reasoning.

While such formalization is possible in principle, it does risk distorting
some of the logical and computational issues at play. The aforementioned point
about succinctness in particular may be relevant. As van der Zander et al.,
(2023) point out, supposing that sums are always expanded out to an
exponentially-large explicit sum threatens to belie important complexity
considerations. Indeed, it may inflate the run-time of some algorithms, e.g.
for estimating conditional interventional distributions (Shpitser and Pearl,,
2006), from linear to exponential. Such considerations motivate the study of
probability logics (with and without causal primitives) that explicitly
include some kind of summation or marginalization operator.

Another motivation for the setting considered here comes from the observation
that much of this style of reasoning does not depend on the specific
assumption that the range of each random variable is finite and fixed in
advance by the signature. Indeed, the entailment facts listed above are more
general, in that they hold even if we do not make any upfront assumptions
about variable ranges. Thus, in addition to the points about succinctness and
complexity, there are also broader logical reasons for exploring such
constructions.

Summation operators introduce a further feature into probability logic that is
not typically included in many presentations, namely free and bound (range)
variables. Summation is essentially a variable-binding operator, so we need to
build up expressions that include free (range) variables. The presence of such
variables also suggests possible uses in which they are left free. In fact,
both Examples 1 and 2 involve free variables both in the “premises” (before
the turnstile) and in the “conclusion” (after the turnstile). The intended
interpretation of these free variables is universal. Roughly speaking (cf.
Def. 9 below for a precise statement), when we write $\varphi\vDash\psi$, if
$\varphi$ has free variables $\mathbf{x}$ and $\psi$ has free variables
$\mathbf{y}$, then this is to be interpreted as
$\forall\mathbf{x}\varphi\Rightarrow\forall\mathbf{y}\psi$. Thus, for
instance, in Example 2 the entailment is to be read: if for all values $x$ in
the range of $X$, $y$ of $Y$, and $z$ of $Z$, the equalities all hold—viz.
$\mathsf{P}(z_{x})\approx\mathsf{P}(z\mid x)$, and so on—then for all $x$ and
$y$ the conclusion holds. (Note that $z$ does not appear free in the
conclusion.)

A first contribution of the present paper is to observe that this move alone
is actually sufficient to render the resulting probability-logical system
undecidable. Li, (2023) recently proved the following fact:

######  Theorem 1 (Li, 2023, Thm. 3).

The following problem is undecidable: Where
$\mathbf{U}_{i},\mathbf{V}_{i},\mathbf{W}_{i}$ denote three pairwise disjoint
subsets of the random variables $X_{1},...,X_{k}$ for each $i=0,...,\ell$,
determine whether the implication

$\bigwedge_{i=1}^{\ell}\mathbf{U}_{i}\perp\mathbf{V}_{i}\mid\mathbf{W}_{i}\rightarrow\mathbf{U}_{0}\perp\mathbf{V}_{0}\mid\mathbf{W}_{0}$
(3)

holds for all jointly distributed $X_{1},\dots,X_{k}$ with finite support.
(The same also holds if stated for all discrete $X_{1},\dots,X_{k}$—i.e., for
all those each of which has finite or countably infinite support.)

In other words, if we do not impose any restriction on the (finite) ranges of
random variables, then the problem of deciding whether a set of conditional
independence statements implies another is undecidable. Of course, such
statements can be easily encoded in a system like the one we have been
describing. For example the conditional independence

$\\{X_{1},\dots,X_{j}\\}\perp\\{Y_{1},\dots,Y_{m}\\}\mid\\{Z_{1},\dots,Z_{n}\\}$

can be expressed straightforwardly as the formula

$\mathsf{P}(\mathbf{x}\land\mathbf{y}\mid\mathbf{z})\approx\mathsf{P}(\mathbf{x}\mid\mathbf{z})\cdot\mathsf{P}(\mathbf{y}\mid\mathbf{z})$
(4)

where $\mathbf{x}=x_{1}\land\dots\land x_{j}$,
$\mathbf{y}=y_{1}\land\dots\land y_{m}$, and $\mathbf{z}=z_{1}\land\dots\land
z_{n}$, with all these variables $x_{1},y_{1},z_{1},\dots,x_{j},y_{m},z_{n}$
left free. Let $p_{i}$ for $i=0,...,\ell$ denote such a statement for each
triple of sets of random variables
$(\mathbf{U}_{i},\mathbf{V}_{i},\mathbf{W}_{i})$. Then the implication (3) is
easily expressed as $\bigwedge_{i=1}^{\ell}p_{i}\vDash p_{0}.$ From Li’s
result, Thm. 1, it immediately follows that any language expressive enough to
encode statements like (4) will possess an undecidable validity (or
satisfiability) problem under this universal interpretation of free variables.
Note that this is importantly different from simply adding (e.g., universal)
quantifiers to the language explicitly. See Schaefer and Štefankovič, (2023)
for a recent study of quantifier depth in the first-order theory of real
numbers; it of course follows from Tarski’s theorem that all such fragments
remain decidable. Entailment facts like those above, in effect, involve
several different types of universal quantification: they quantify over all
possible values, for all possible ranges of their variables simultaneously.

This result means in particular that the natural logical habitat for
$do$-calculus—a logical language that generalizes the reasoning exhibited in
Ex. 2, for instance—will be generally undecidable. At the same time, van der
Zander et al., (2023) have recently shown that probability-logical systems
which assume a _fixed_ finite range for random variables remain decidable.
Assuming there are no free variables at all, they were able to show that
relatively expressive probability and “Level 2” causal-probability logics with
summation operators are complete for the class $\text{succ}\exists\mathbb{R}$,
whose prototypical problem is to decide whether a given Boolean circuit
computes a satisfiable formula in the (first-order) existential theory of the
real numbers. Another contribution of the present work (Theorem 3 below) is to
show that this characterization extends to the full “Level 3” fragment
encompassing all possible statements over probabilities of counterfactuals,
thereby resolving a problem left open by van der Zander et al., (2023) and
Mossé et al., (2024). The same theorem further extends these results to
formulas with free variables.

Finally, in the last part of the paper we consider axiomatic questions for
pure probabilistic (i.e., non-causal) logical languages with summation
operators. Both the presence of free variables (with universal interpretation)
and the use of summation present interesting logical challenges. A first
observation is that the usual statement of the deduction theorem fails in this
setting, due to the interpretation of free variables.

######  Remark 1.

It does not generally hold that if $\varphi\vDash\psi$ then
$\vDash\varphi\rightarrow\psi$. For instance, while $\mathsf{P}(x\land
y)\approx\mathsf{P}(x)\cdot\mathsf{P}(y)\vDash\mathsf{P}(x^{\prime}\land
y^{\prime})\approx\mathsf{P}(x^{\prime})\cdot\mathsf{P}(y^{\prime})$ since the
“conclusion” merely relabels the free $x,y\mapsto x^{\prime},y^{\prime}$, it
does not follow that $\vDash\mathsf{P}(x\land
y)\approx\mathsf{P}(x)\cdot\mathsf{P}(y)\rightarrow\mathsf{P}(x^{\prime}\land
y^{\prime})\approx\mathsf{P}(x^{\prime})\cdot\mathsf{P}(y^{\prime})$ for every
$x,y,x^{\prime},y^{\prime}$.

The laws governing summation can also be subtle, particularly when value
ranges are allowed to be arbitrarily large, or even infinite. For instance,
infinite sums over a probability term can be approximate from below by finite
sums over increasing substitutions with constants. As is typical for
probability logics, the systems we study here are not compact, so we cannot
hope to obtain a strong completeness theorem with only finitary axioms.
Instead, we provide strong axiomatizations with infinitary rules, building on
previous work in probability logic. Enforcing the “closed-world” assumption
that every element of the range is named by a constant, we prove strong
completeness for several systems, including those with and without allowance
for free variables. We close with further limitative results, as well as
additional open questions.

##  2 Preliminaries

This section lays out the syntax, semantics, and relevant notions from
complexity for the probabilistic language $\mathcal{L}_{\text{prob}}$ and the
probabilistic causal counterfactual language $\mathcal{L}_{\text{causal}}$.

###  2.1 Syntax

####  2.1.1 Signatures

Let $\mathbf{V}$ be a countable set of _random variables_. For each
$V\in\mathbf{V}$, let $\mathcal{C}_{V}$ be a countable set of _constant
symbols_ (or constants) and let $\mathcal{V}_{V}$ be a countably infinite set
of _range variables_. All these sets must be disjoint for distinct random
variables $V\neq V^{\prime}\in\mathbf{V}$, and we will often enumerate their
elements explicitly. For range variables we write
$\mathcal{V}_{V}=\\{v_{1},v_{2},v_{3},\dots\\}$ and often denote generic range
variables $v,v^{\prime}$, etc. with such standing for distinct elements of
$\mathcal{V}_{V}$. As for constants, we write
$\mathcal{C}_{V}=\\{c^{V}_{1},c^{V}_{2},\dots\\}$ in the case of infinitely
many constants and $\mathcal{C}_{V}=\\{c^{V}_{1},\dots,c^{V}_{N}\\}$
otherwise. Thus, for constant symbols, superscripts indicate the random
variable, but we often write $c,c^{\prime},$ etc. for elements of
$\mathcal{C}_{V}$ when context makes it clear which $V$. Let
$\mathcal{D}_{V}=\mathcal{C}_{V}\cup\mathcal{V}_{V}$, for each
$V\in\mathbf{V}$. Elements of $\mathcal{D}_{V}$ are naturally denoted
$d,d^{\prime},$ etc.

####  2.1.2 Languages

In this section, we build up our two languages, $\mathcal{L}_{\mathrm{prob}}$
and $\mathcal{L}_{\mathrm{causal}}$, comparing polynomials in probabilities of
events, as well as some fragments thereof. We start with base atoms $V=v$,
where $V$ ranges over random variables $\mathbf{V}$ and $v$ over variable
symbols $\mathcal{V}_{V}$, as well as atoms $V=c^{V}_{i}$, for each
$c^{V}_{i}\in\mathcal{C}_{V}$. For the remainder of this section, we assume
there are infinitely many constant symbols in each $\mathcal{C}_{V}$. Then
some base (deterministic) languages are:

$\displaystyle\mathcal{L}_{\mathrm{base}}^{\mathrm{prob}}$
$\displaystyle:=V=v\;|\;V=c^{V}_{i}\;|\;\lnot\mathcal{L}_{\mathrm{base}}^{\mathrm{prob}}\;|\;\mathcal{L}_{\mathrm{base}}^{\mathrm{prob}}\land\mathcal{L}_{\mathrm{base}}^{\mathrm{prob}},$
$\displaystyle\mathcal{L}_{\mathrm{int}}$
$\displaystyle:=\top\;|\;V=v\;|\;V=c^{V}_{i}\;|\;\mathcal{L}_{\mathrm{int}}\land\mathcal{L}_{\mathrm{int}}.$

Define the base causal conditional language as follows:

$\displaystyle\mathcal{L}_{\mathrm{base}}^{\mathrm{causal}}$
$\displaystyle:=[\mathcal{L}_{\mathrm{int}}]\mathcal{L}_{\mathrm{base}}^{\mathrm{prob}}\;|\;\neg\mathcal{L}_{\mathrm{base}}^{\mathrm{causal}}\;|\;\mathcal{L}_{\mathrm{base}}^{\mathrm{causal}}\land\mathcal{L}_{\mathrm{base}}^{\mathrm{causal}}.$

Thus, instead of writing, e.g., $Y_{X=x}=y$ or its abbreviation $y_{x}$ for
the interventional conditional, as in Examples 1 and 2, we will adopt dynamic
logical notation and write $[X=x]Y=y$, or abbreviatedly, $[x]y$.

Probability terms are defined as follows for
$*\in\\{\text{prob},\text{causal}\\}$ and any $c^{V}_{i}\in\mathcal{C}_{V}$,
$v_{i}\in\mathcal{V}_{V}$:

$\displaystyle\mathsf{t}^{*}_{\circ}$
$\displaystyle:=\mathsf{P}\big{(}\mathcal{L}_{\mathrm{base}}^{*}\;|\;\mathcal{L}_{\mathrm{base}}^{*}\big{)}\;|\;\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{v_{i}}\mathsf{t}^{*}_{\circ}\;|\;\mathsf{t}^{*}_{\circ}+\mathsf{t}^{*}_{\circ}\;|\;\mathsf{t}^{*}_{\circ}\cdot\mathsf{t}^{*}_{\circ}$
(5) $\displaystyle\mathsf{t}^{*}$
$\displaystyle:=\mathsf{P}\big{(}\mathcal{L}_{\mathrm{base}}^{*}\;|\;\mathcal{L}_{\mathrm{base}}^{*}\big{)}\;|\;\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{v_{i}}\mathsf{t}^{*}\;|\;\mathsf{t}^{*}+\mathsf{t}^{*}\;|\;\mathsf{t}^{*}\cdot\mathsf{t}^{*}\;|\;-\mathsf{t}^{*}\;|\;\mathsf{c}^{V}_{i}\;|\;\mathsf{v}_{i}\;$
(6)

The probability primitives are thus the conditional probabilities of base
expressions. Now, define languages comparing probability terms and equality of
symbols for $*\in\\{\text{prob},\text{causal}\\}$:

$\displaystyle\mathcal{L}_{*}$
$\displaystyle:=\mathcal{D}_{V}\equiv\mathcal{D}_{V}\;|\;\mathsf{t}^{*}\succsim\mathsf{t}^{*}\;|\;\lnot\mathcal{L}\;|\;\mathcal{L}\land\mathcal{L}.$
(7)

Thus, e.g., (2) is in $\mathcal{L}_{\text{causal}}$, with $y\not\equiv
y^{\prime}$ representing disequality of $y,y^{\prime}\in\mathcal{V}_{Y}$. We
specify some fragments of these languages for
$*\in\\{\text{prob},\text{causal}\\}$:

  * •

$\mathcal{L}_{*}^{\text{closed}}$ is the closed fragment of $\mathcal{L}_{*}$
containing no free variables, i.e. in which every range variable $v$ is bound
by a summation operator
$\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{v}$.

  * •

$\mathcal{L}_{*}^{\circ}$ is the fragment of $\mathcal{L}_{*}$ with restricted
coefficients, formed by restricting the terms $\mathsf{t}^{*}$ in the second
case of (7) to the $\mathsf{t}_{\circ}^{*}$ defined by (5), i.e. those in
which all coefficients are $1$ and not $-1$, $\mathsf{c}_{i}^{V}$, or
$\mathsf{v}_{i}$.

  * •

$\mathcal{L}_{*}^{\circ+\text{closed}}$ is their intersection.

In sum, the targets of our analysis are the eight languages
$\mathcal{L}^{\dagger}_{*}$ formed for each
$*\in\\{\text{prob},\text{causal}\\}$ and
$\dagger\in\\{\varepsilon,\text{closed},\circ,\circ+\text{closed}\\}$.222Here
$\varepsilon$ is the empty string.

####  2.1.3 Bounded Languages

As we alluded to above, we also consider languages whose signatures have
finitely many constants, in which for some $N\geq 1$ we have
$\mathcal{C}_{V}=\\{c_{1}^{V},\dots,c_{N}^{V}\\}$ for each $V$ (note here that
$N$ is uniform over all $V$). Where $\mathcal{L}=\mathcal{L}^{\dagger}_{*}$
represents any of the eight languages defined in §2.1.2, let $\mathcal{L}(N)$
be that constructed analogously to $\mathcal{L}$ but over a signature built
from this bounded constant set. We can equivalently consider $\mathcal{L}(N)$
to be a fragment of $\mathcal{L}$ containing all and only those $\varphi$ such
that an atom $V=c^{V}_{i}$ appears in $\varphi$ only when $i\leq N$.

####  2.1.4 Abbreviations and expressibility

Given some $\delta\in\mathcal{L}_{\mathrm{base}}^{*}$ we use
$\mathsf{P}(\delta)$ as shorthand for $\mathsf{P}(\delta\;|\;\top)$. Given a
term $\mathsf{t}$, $V\in\mathbf{V}$, $v\in\mathcal{V}_{V}$, and
$\epsilon\in\mathcal{L}_{\mathrm{base}}^{\mathrm{prob}}$ we use the notation
$\mathsf{t}[V=v/\epsilon]$ to denote $\mathsf{t}$ but with the base formula
$\epsilon$ substituted in place of every free occurrence of $V=v$ (as an atom
within a probability operator $\mathsf{P}$); given a formula
$\varphi\in\mathcal{L}_{*}$ we write $\varphi[v/d]$, to denote $\varphi$
except with every free occurrence of $v$ (both across equalities $\equiv$ and
as atoms $V=v$ in probability terms) replaced by $d\in\mathcal{D}_{V}$.
Informal sums with serifs $\sum$ (as opposed to formal sans-serif sums
$\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@$) are used along with dummy variables as “macros”
to abbreviate polynomial terms, e.g. $\sum_{i=1}^{2}\mathsf{P}(V=c^{V}_{i})$
is shorthand for $\mathsf{P}(V=c^{V}_{1})+\mathsf{P}(V=c^{V}_{2})$.

Other comparisons of terms are readily expressible in terms of our one, e.g.,
$\mathsf{t}_{1}\precsim\mathsf{t}_{2}\Leftrightarrow\mathsf{t}_{2}\succsim\mathsf{t}_{1}$
or
$\mathsf{t}_{1}\prec\mathsf{t}_{2}\Leftrightarrow\mathsf{t}_{2}\succsim\mathsf{t}_{1}\land\lnot(\mathsf{t}_{1}\succsim\mathsf{t}_{2})$.
We write $\mathsf{t}_{1}\approx\mathsf{t}_{2}$ for
$\mathsf{t}_{1}\succsim\mathsf{t}_{2}\land\mathsf{t}_{1}\precsim\mathsf{t}_{2}$.
Subtraction is expressible: we write $\mathbf{t}_{1}-\mathbf{t}_{2}$ for
$\mathbf{t}_{1}+(-\mathbf{t}_{2})$. Ratios are also expressible:
$\mathsf{t}_{1}/\mathsf{t}_{2}\succsim\mathsf{t}_{3}\Leftrightarrow\mathsf{t}_{1}\succsim\mathsf{t}_{2}\cdot\mathsf{t}_{3}$.
In sums of ratios, etc., the latter pattern generalizes via clearing common
denominators. The only case in which it fails is when the bound variable of a
sum occurs in a denominator, as in
$\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{v}\mathsf{t}_{1}/\mathsf{P}(V=v)\succsim\mathsf{t}_{2}$,
since the range of a formal summation is unbounded in our semantics below.
Thus—being careful to eschew syntactically this single exception—we may avail
ourselves of division as well.

Finally, although the above language does not include numerical constants, it
is natural to define a term $\underline{1}$ for $\mathsf{P}(\top)$ and
$\underline{0}$ for $\mathsf{P}(\bot)$. For any $q\in\mathbb{Q}$ we can use
$\underline{q}$ as a term freely, unpacking it by applying the rules above to
$\underline{1}$s. For example, $\mathsf{t}\succsim\underline{1/2}$ is short
for
$\mathsf{t}\cdot\big{[}\mathsf{P}(\top)+\mathsf{P}(\top)\big{]}\succsim\mathsf{P}(\top)$.

###  2.2 Semantics

####  2.2.1 Structural causal models

The semantics for all of these languages will be defined relative to
_structural causal models_ , which can be understood as a very general
framework for encoding _data-generating processes_. In addition to the
endogenous variables $\mathbf{V}$, structural causal models also employ
_exogenous variables_ $\mathbf{U}$ as a source of random variation among
endogenous settings. For extended introductions, see, e.g., Pearl, (2009);
Bareinboim et al., (2022).

######  Definition 1.

A structural causal model (SCM) $\mathfrak{M}$ is a tuple
$\mathfrak{M}=(\mathcal{F},\mathbb{P},\mathbf{U},\mathbf{V})$, with:

  1. (a)

$\mathbf{V}$ a set of endogenous variables, with each $V\in\mathbf{V}$ taking
on possible values from a range $\text{Val}(V)$,

  2. (b)

$\mathbf{U}$ a set of exogenous variables, with each $U\in\mathbf{U}$ taking
on possible values $\text{Val}(U)$,

  3. (c)

$\mathcal{F}=\\{f_{V}\\}_{V\in\textbf{V}}$ a family of _structural functions_
, such that $f_{V}$ determines the value of $V$ given the values of the
exogenous variables $\mathbf{U}$ and those of the other endogenous variables
$V^{\prime}\in\mathbf{V}\setminus\\{V\\}$, and

  4. (d)

$\mathbb{P}$ a probability measure on a $\sigma$-algebra $\sigma(\mathbf{U})$
on $\mathbf{U}$.

In addition, we adopt the common assumption that our SCMs are _recursive_ or
acyclic. Where $\mathbf{S}$ is a set of variables let
$\mathrm{Val}(\mathbf{S})=\bigtimes_{S\in\mathbf{S}}\mathrm{Val}(S)$ be their
joint range.

######  Definition 2.

A SCM $\mathfrak{M}$ is recursive if there is a well-order $\prec$ on
$\mathbf{V}$ such that $\mathcal{F}$ respects $\prec$ in the following sense:
for any $V\in\mathbf{V}$, whenever the joint ranges
$\mathbf{v}_{1},\mathbf{v}_{2}\in\mathrm{Val}(\mathbf{V})$ have the property
that
$\pi_{V^{\prime}}(\mathbf{v}_{1})=\pi_{V^{\prime}}(\mathbf{v}_{2})$333Here
$\pi_{V^{\prime}}:\mathrm{Val}(\mathbf{V})\to\mathrm{Val}(V^{\prime})$ is the
projection map from joint to single ranges, taking
$\\{v_{V}\\}_{V\in\mathbf{V}}\mapsto v_{V^{\prime}}$. for all $V^{\prime}\prec
V$, we are guaranteed that
$f_{V}(\mathbf{v}_{1},\mathbf{u})=f_{V}(\mathbf{v}_{2},\mathbf{u})$ for every
$\mathbf{u}\in\mathrm{Val}(\mathbf{U})$.

Causal interventions represent the result of a _manipulation_ to the causal
system, and are defined in the standard way (e.g., Spirtes et al., 2000;
Pearl, 2009):

######  Definition 3.

An intervention X=x assigns a set of random variables
$\textbf{X}\subset\mathbf{V}$ to a set of values
$\textbf{x}\in\mathrm{Val}(\mathbf{X})$. An intervention induces a mapping of
a system of functions $\mathcal{F}=\\{f_{V}\\}_{V\in\textbf{V}}$ to another
system $\mathcal{F}_{\textbf{X=x}}$, which is identical to $\mathcal{F}$, but
with $f_{V}$ replaced by the constant function
$f_{X}(\cdot)=\pi_{X}(\mathbf{x})$ for each $X\in\textbf{X}$. Similarly, where
$\mathfrak{M}$ is a model with equations $\mathcal{F}$, we write
$\mathfrak{M}_{\textbf{X={x}}}$ for the model which is identical to
$\mathfrak{M}$ but with the equations $\mathcal{F}_{\textbf{X}=\textbf{x}}$ in
place of $\mathcal{F}$.

In order to guarantee that interventions lead to a well-defined semantics, we
work with structural causal models which are measurable:

######  Definition 4.

A SCM $\mathfrak{M}$ is measurable if under every finite intervention
$\mathbf{X}=\mathbf{x}$, the joint distribution $\mathbb{P}(\mathbf{V})$
associated with the model $\mathfrak{M}_{\mathbf{X}=\mathbf{x}}$ is well-
defined. This, in turn, defines a probability
$\mathbb{P}_{\mathfrak{M}}(\delta)$ for
$\delta\in\mathcal{L}^{*}_{\text{base}}$. (For details, see §2.2.2 of Mossé et
al., 2024.)

Lastly, we restrict attention to models in which variables take values in the
natural numbers:

######  Definition 5.

A SCM is countable if the range $\mathrm{Val}(V)$ of any variable $V$ is a
subset of $\mathbb{Z}^{+}=\\{1,2,3,\dots\\}$.

####  2.2.2 Interpretation of terms and truth definitions

######  Definition 6.

A _model_ $\mathfrak{M}$ is a recursive, measurable, countable SCM together
with an assignment $c^{\mathfrak{M}}\in\mathrm{Val}(V)$ for each constant
symbol $c\in\mathcal{C}_{V}$. We restrict attention to models $\mathfrak{M}$
that are closed-world or “Herbrand,” such that for every $V\in\mathbf{V}$, the
map $\mathcal{C}_{V}\to\mathrm{Val}(V)$ taking $c\mapsto c^{\mathfrak{M}}$ is
surjective.

######  Definition 7.

A (range) variable assignment for $V\in\mathbf{V}$ is a partial mapping
$\iota:\mathbf{V}\times\mathbb{Z}^{+}\to\mathrm{Val}(V)$, neither surjective
nor injective in general. The value $\iota(V,i)$ is the interpretation of the
range variable $v_{i}$.

######  Definition 8.

The relation $\mathfrak{M},\iota\vDash\varphi$ for
$\varphi\in\mathcal{L}_{\text{causal}}$ is defined as follows. Numerical
denotations for terms (6) are elements of
$\mathbb{R}\cup\\{\infty,-\infty,\bot\\}$. We define
$[\\![\mbox{\em$\mathsf{P}(\delta\mid\delta^{\prime})$\/}]\\!]^{\mathfrak{M}}_{\iota}=\mathbb{P}_{\mathfrak{M}}(\delta\land\delta^{\prime})/\mathbb{P}_{\mathfrak{M}}(\delta^{\prime})$
provided $\mathbb{P}_{\mathfrak{M}}(\delta^{\prime})\neq 0$, and
$[\\![\mbox{\em$\mathsf{P}(\delta\mid\delta^{\prime})$\/}]\\!]^{\mathfrak{M}}_{\iota}=\bot$
otherwise. We also define
$[\\![\mbox{\em$\mathsf{c}^{V}_{i}$\/}]\\!]^{\mathfrak{M}}_{\iota}=({c}^{V}_{i})^{\mathfrak{M}}$
and
$[\\![\mbox{\em$\mathsf{v}_{i}$\/}]\\!]^{\mathfrak{M}}_{\iota}=\iota(V,i)$;
this works since these are values in
$\mathrm{Val}(V)\subset\mathbb{Z}^{+}\subset\mathbb{R}$. As expected, we
define
$[\\![\mbox{\em$\mathsf{t}\oplus\mathsf{t}^{\prime}$\/}]\\!]^{\mathfrak{M}}_{\iota}=[\\![\mbox{\em$\mathsf{t}$\/}]\\!]^{\mathfrak{M}}_{\iota}\oplus[\\![\mbox{\em$\mathsf{t}^{\prime}$\/}]\\!]^{\mathfrak{M}}_{\iota}$
for each $\oplus\in\\{\cdot,+\\}$ and
$[\\![\mbox{\em$-\mathsf{t}$\/}]\\!]^{\mathfrak{M}}_{\iota}=-[\\![\mbox{\em$\mathsf{t}$\/}]\\!]^{\mathfrak{M}}_{\iota}$.
Binary operations on our doubly-extended line are defined as expected; also

$\displaystyle 0\cdot\infty=\infty\cdot 0=0\cdot(-\infty)=(-\infty)\cdot
0=0,\quad\infty+(-\infty)=(-\infty)+\infty=0$

and any operation with $\bot$ as one of the operands yields $\bot$. Now we
define444In this definition, $\iota[V,i\mapsto n]$, for $V\in\mathbf{V}$,
$i\in\mathbb{Z}^{+}$, $n\in\mathrm{Val}(V)$, denotes the map $\iota^{\prime}$
such that $\mathrm{dom}(\iota^{\prime})=\mathrm{dom}(\iota)\cup\\{(V,i)\\}$
and $\iota^{\prime}(V,i)=n$ but
$\iota^{\prime}(V^{\prime},j)=\iota(V^{\prime},j)$ for any
$(V^{\prime},j)\in\mathrm{dom}(\iota)$ such that $(V^{\prime},j)\neq(V,i)$.

$\displaystyle[\\![\mbox{\em$\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{v_{i}}\mathsf{t}$\/}]\\!]^{\mathfrak{M}}_{\iota}=\sum_{n\in\mathrm{Val}(V)}[\\![\mbox{\em$\mathsf{t}$\/}]\\!]^{\mathfrak{M}}_{\iota[V,i\mapsto
n]}$

with this sum taking the expected extended value if divergent (and $\bot$ if
any summand is $\bot$). Note that the syntax of terms $\mathsf{t}$ guarantees
that any divergent sum will tend toward $\infty$ or $-\infty$.

Now we define the semantics of formulas (7) as follows. First,
$\mathfrak{M},\iota\vDash d\equiv d^{\prime}$ for
$d,d^{\prime}\in\mathcal{D}_{V}$ iff
$[\\![\mbox{\em$d$\/}]\\!]^{\mathfrak{M}}_{\iota}=[\\![\mbox{\em$d^{\prime}$\/}]\\!]^{\mathfrak{M}}_{\iota}$,
where the denotation in ranges $\mathrm{Val}(V)$ of elements of
$\mathcal{D}_{V}$ for each $V\in\mathbf{V}$ are given in the obvious way:
$[\\![\mbox{\em$c^{V}_{i}$\/}]\\!]^{\mathfrak{M}}_{\iota}=(c^{V}_{i})^{\mathfrak{M}}$
and $[\\![\mbox{\em$v_{i}$\/}]\\!]^{\mathfrak{M}}_{\iota}=\iota(V,i)$. Then,
$\mathfrak{M},\iota\vDash\mathsf{t}\succsim\mathsf{t}^{\prime}$ iff
$[\\![\mbox{\em$\mathsf{t}$\/}]\\!]^{\mathfrak{M}}_{\iota}\geq[\\![\mbox{\em$\mathsf{t}^{\prime}$\/}]\\!]^{\mathfrak{M}}_{\iota}$,
with neither $[\\![\mbox{\em$\mathsf{t}$\/}]\\!]^{\mathfrak{M}}_{\iota}$ nor
$[\\![\mbox{\em$\mathsf{t}^{\prime}$\/}]\\!]^{\mathfrak{M}}_{\iota}$ being
$\bot$, and the order on the doubly-extended real line being defined as
expected. Next, $\mathfrak{M},\iota\vDash\neg\varphi$ iff
$\mathfrak{M},\iota\not\vDash\varphi$.555Thus, we have
$\mathfrak{M},\iota\vDash\neg\varphi$ if $\varphi$ contains any term
evaluating to $\bot$, i.e., any probability conditional on a measure zero.
Finally, $\mathfrak{M},\iota\vDash\varphi\land\psi$ iff
$\mathfrak{M},\iota\vDash\varphi$ and $\mathfrak{M},\iota\vDash\psi$.

######  Definition 9 (Entailment).

We say that $\varphi$ is valid in a model $\mathfrak{M}$, and write
$\mathfrak{M}\vDash\varphi$, if $\mathfrak{M},\iota\vDash\varphi$ for every
$\iota$. A model $\mathfrak{M}$ satisfies a _sequent_
$\Gamma\Rightarrow\varphi$ if either $\mathfrak{M}\not\vDash\gamma$ for some
$\gamma\in\Gamma$, or $\mathfrak{M}\vDash\varphi$. We say that a set $\Gamma$
of formulas entails a formula $\varphi$, and write $\Gamma\vDash\varphi$, when
$\mathfrak{M}$ satisfies $\Gamma\Rightarrow\varphi$ for every $\mathfrak{M}$
(in some class $\mathcal{M}^{\prime}$).

######  Definition 10.

Let $\mathcal{M}$ be the class of (recursive, measurable, countable, closed-
world) models. Let $\mathcal{M}_{N}\subset\mathcal{M}$ be the subclass in
which each variable $V$ has a range of cardinality $N$. Let
$\mathcal{M}_{\text{fin}}=\bigcup_{N=1}^{\infty}\mathcal{M}_{N}$ be the
subclass of those in which all variables have a finite range.

######  Definition 11 (Satisfiability).

$\mathsf{SAT}_{\mathcal{L}_{*}^{\dagger}}$ is the problem of deciding whether
a given sequent $\Gamma\Rightarrow\varphi$, where
$\varphi\in\mathcal{L}_{*}^{\dagger}$ and
$\Gamma\subset\mathcal{L}_{*}^{\dagger}$ is finite, has a model satisfying it
within a fixed class $\mathcal{M}^{\prime}$.

van der Zander et al., (2023) restrict attention to
$\mathsf{SAT}_{\mathcal{L}_{*}^{\text{closed}}(N)}$666Strictly speaking, they
consider satisfiability for the fragment of
$\mathcal{L}_{*}^{\text{closed}}(N)$ in which the primitives
$\mathsf{c}^{V}_{i}$ and $\mathsf{v}_{i}$ in (6) are disallowed, but this of
course only means our complexity results in §3 are stronger. over
$\mathcal{M}_{N}$.

####  2.2.3 Examples for separation in expressive power

In this section, we show that the distinctions among languages and classes of
models just introduced track gaps in expressive power.

##### Free and bound range variables.

Consider the following formula with a free range variable:

$\displaystyle\mathsf{P}(V=v_{i})\succ\underline{0}.$

This formula $\varphi$ is satisfied only by models which assign positive
probability to $V=n$ for every value $n\in\text{Val}(V)$. However, no formula
$\psi$ with only bound range variables picks out precisely such models.

##### Coefficients.

Unlike $\mathcal{L}_{\text{prob}}^{\circ+\text{closed}}$, the language
$\mathcal{L}_{\text{prob}}^{\text{closed}}$ allows the use of constants, as in
the following formula, where $i$ is shorthand for the $i$-term sum
$\mathsf{P}(\top)+\dots+\mathsf{P}(\top)$:

$\bigwedge_{1\leq i\leq n}c^{V}_{i}\approx
i\land\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{v_{i}}\mathsf{P}(\top)\approx n$

Indeed, this formula $\varphi$ is satisfied only by models which assign
$\text{Val}(V)=\\{1,\dots,n\\}$. But no formula
$\psi\in\mathcal{L}_{\text{prob}}^{\text{closed}}$ is true of the same models
as $\varphi$, since for any model $\mathfrak{M}$ of $\psi$, we can create
another model $\mathfrak{M}^{\prime}$ where
$\mathrm{Val}(V)=\\{2,\dots,n+1\\}$, associating the event $V=i$ in
$\mathfrak{M}$ with $V=i+1$ in $\mathfrak{M}^{\prime}$, without sacrificing
the satisfaction of $\psi$.

##### Probabilistic and causal languages.

To illustrate the expressivity of causal as opposed to purely probabilistic
languages, we recall a variation by Bareinboim et al., (2022) on an example
due to Pearl, (2009):

######  Example 3 (Causation without correlation).

Let $\mathfrak{M}_{1}=(\mathcal{F},\mathbb{P},\mathbf{U},\mathbf{V})$, where U
contains two binary variables $U_{1},U_{2}$ such that
$\mathbb{P}(U_{1})=\mathbb{P}(U_{2})=\nicefrac{{1}}{{2}}$, and V contains two
variables $V_{1},V_{2}$ such that $f_{V_{1}}=U_{1}$ and $f_{V_{2}}=U_{2}$.
Then $V_{1}$ and $V_{2}$ are independent. But having observed this, one could
not conclude that $V_{1}$ has no causal effect on $V_{2}$; consider the model
$\mathfrak{M}^{\prime}$, which is like $\mathfrak{M}$, except with the
mechanisms:

$\displaystyle f_{V_{1}}$ $\displaystyle=\mathbf{1}_{U_{1}=U_{2}}$
$\displaystyle f_{V_{2}}$
$\displaystyle=U_{1}+\mathbf{1}_{V_{1}=1,U_{1}=0,U_{2}=1}.$

In this case
$\mathbb{P}_{\mathfrak{M}}(V_{1},V_{2})=\mathbb{P}_{\mathfrak{M}^{\prime}}(V_{1},V_{2})$,
so that the models are indistinguishable in $\mathcal{L}_{\mathrm{prob}}$.
However, the models are distinguishable in $\mathcal{L}_{\mathrm{causal}}$
(given appropriate constant interpretations), via the statement

$\displaystyle\mathbb{P}\big{(}[V_{1}=1]V_{2}=1\big{)}=\mathbb{P}\big{(}[V_{1}=1]V_{2}=0\big{)}$

As shown in Bareinboim et al., (2022) (cf. also Suppes and Zanotti, 1981;
Ibeling and Icard, 2021), the pattern in Example 3 is universal: for any model
$\mathfrak{M}$ it is _always_ possible to find some $\mathfrak{M}^{\prime}$
that agrees with $\mathfrak{M}$ on all of $\mathcal{L}_{\mathrm{prob}}$ but
disagrees on $\mathcal{L}_{\mathrm{causal}}$.

###  2.3 Complexity

In this section, we introduce the target complexity class for our completeness
result, namely $\text{succ}\exists\mathbb{R}$ (van der Zander et al.,, 2023).
Recall that ETR is the existential fragment of first-order logic, that is, the
set of first-order expressions of the form $\exists
x_{1},\dots,x_{n}\;\alpha$, such that $\alpha$ is a quantifier-free. The class
$\text{succ}\exists\mathbb{R}$ is defined by the problem of determining
whether a circuit computes an encoding of a satisfiable ETR instance:

######  Definition 12 (Trees for ETR formulas).

Represent an ETR formula $\varphi$ as a tree, where the leaf nodes are labeled
with the variables of $\varphi$ and the non-leaf nodes are labeled with the
operations of $\varphi$, whose children are their operands; we will call this
an ETR tree. Fix some encoding on the locations of nodes in the tree, such
that the binary string for a node $v$ specifies its location in the tree. We
will abuse notation, using $v$ to refer to the encoding of $v$’s location, and
using $\varphi$ to refer to the associated ETR tree.

######  Definition 13.

A Boolean circuit is a directed acyclic graph $G=(V,E)$ such that

  * •

$N$ vertices, the inputs, have no predecesors, and $M$ vertices, the outputs,
have no successors;

  * •

each non-input node is labeled with $\land$, $\lor$, or $\neg$, and has the
correct number of predecessors in $G$; and

  * •

the edges $E$ are ordered, to distinguish different arguments to the same
Boolean expression.

######  Definition 14.

A Boolean circuit $C:\\{0,1\\}^{N}\rightarrow\\{0,1\\}^{M}$ computes $\varphi$
if $C(v)=(\ell_{v},\text{parent}_{v},\text{children}_{v})$ contains the label
for $v$ as well as the locations of its parent and children.

######  Definition 15.

succETR is the problem of deciding whether a circuit
$C:\\{0,1\\}^{N}\rightarrow\\{0,1\\}^{M}$ computes a satisfiable ETR instance.

######  Definition 16.

$\text{succ}\exists\mathbb{R}$ is the class of problems that are reducible in
polynomial time to succETR.

##  3 Complexity of Satisfiability

The introduction observed a negative result:

######  Theorem 2.

$\mathsf{SAT}_{\mathcal{L}_{\text{prob}}}$ and
$\mathsf{SAT}_{\mathcal{L}_{\text{causal}}}$ over either
$\mathcal{M}_{\text{fin}}$ or $\mathcal{M}$ are undecidable.

This section shows the following positive results:

######  Theorem 3.

$\mathsf{SAT}_{\mathcal{L}_{\text{causal}}(N)}$ over $\mathcal{M}_{N}$ is
complete for $\text{succ}\exists\mathbb{R}$.

######  Theorem 4.

$\mathsf{SAT}_{\mathcal{L}_{\text{prob}}}$ and
$\mathsf{SAT}_{\mathcal{L}_{\text{causal}}}$ over $\mathcal{M}_{\text{fin}}$
are recursively enumerable.

To show Theorem 3, we use a characterization of $\text{succ}\exists\mathbb{R}$
by Bläser et al., 2024, which allows us to lift the results of Mossé et al.,
(2024) to the setting with summation operators:

######  Definition 17.

A real RAM is a tuple $(P,T,R)$, where $P$ is a program, $T$ is an infinite
memory tape, and $R$ is a set of registers. There are two kinds of registers:
real registers and word registers, which respectively store real numbers and
binary strings. The program $P$ can move values between memory and registers,
as well as add, subtract, multiply, and divide values stored in registers; $P$
can also perform bitwise Boolean operations on binary registers. A
nondeterministic real RAM $M$ receives a binary string as input $I$, together
with a certificate $C=(x,s)$, where $x$ is a sequence of real numbers and $s$
is a binary string. Then $M$ accepts $I$ if there exists a certificate $C$
such that $M(I,C)=1$. (For details, see Erickson et al., 2022.)

######  Theorem 5 (Bläser et al., 2024).

$\text{succ}\exists\mathbb{R}$ is the precisely the sets of languages decided
by nondeterministic real RAMs in exponential time.

We include a sketch of the proof by Bläser et al., (2024):

###### Proof.

One direction is trivial: an exponential-time nondeterministic real RAM can
simply use a circuit to write out the ETR instance it computes and solve this
instance. For the other direction, it suffices to show that given a real RAM
$M$, an input $I$, and $w,t\in\mathbb{N}$, one can construct a circuit $C$ of
size $\text{poly}(|M|\cdot|I|\cdot w)\cdot\text{polylog}(t)$ in time
$\text{poly}(|M|\cdot|I|\cdot w)$ encoding an ETR formula $\varphi$ which is
satisfiable iff $M$ accepts $I$ within $t$ steps.

We begin with the special case where $M$ is polynomial-time (Lemma 11 of
Erickson et al., 2022). In this case, let $\varphi$ be the formula

$\exists
x_{0},...,x_{n}\;\texttt{PowersOf2}(x_{0},..,x_{n})\land\texttt{WordsAreWords}(x_{0},..,x_{n})\land\texttt{FixInput}(x_{0},..,x_{n})\\\
\land\texttt{ProgramCounter}(x_{0},...,x_{n})\land\texttt{Execute}(x_{0},..,x_{n}).$

The subformulas are defined as follows:

  * •

PowersOf2 ensures that the first $w$ variables $x_{0},...,x_{w-1}$ are equal
to the first $w$ powers of $2$.

  * •

$\texttt{IsWord}(X)$ for $X=x_{i},...,x_{j}$ ensures that $X$ describes a
number in binary between $x_{0}=1$ and $x_{w-1}=2^{w-1}$. The sub-formula
WordsAreWords selects a subset $X_{1},..,X_{k}$ of the variables
$x_{w},...,x_{n}$, ensuring that $\texttt{IsWord}(X_{i})$ for $i\in[k]$. These
variables represent the word registers of $M$.

  * •

FixInput ensures that some of the word variables encode the input $I$ provided
to $M$.

  * •

$\texttt{ProgramCounter}(x_{0},...,x_{n})$ designates a single variable
$x_{t}$ to indicate the time-step of computation.

  * •

Using the standard reduction provided by the Cook-Levin Theorem,
$\texttt{Execute}(x_{0},..,x_{n})$ simulates $M$, using and updating the
program counter at each time step.

Since $\varphi$ precisely simulates runs of $M$, there exist a certificate and
input on which $M$ accepts iff there exist variables $x_{0},...,x_{n}$
satisfying $\varphi$. Bläser et al., (2024) show that in the general case, one
can construct a succinct circuit computing this formula in polynomial-time;
correctness for the construction follows immediately from correctness in the
special case. ∎

The completeness results of Mossé et al., (2024) relied on small model
property. This is no longer guaranteed, but given the above characterization,
an exponential model property will suffice:

######  Definition 18.

Fix a formula $\varphi\in\mathcal{L}_{\mathrm{causal}}$. Let
$\mathbf{V}_{\varphi}$ denote all variables appearing in $\varphi$, and let
$\mathcal{I}$ contain all interventions over all values of variables appearing
in $\varphi$. Let $\Delta_{\varphi}$ contain all interventions
$\alpha\in\mathcal{I}$ paired with all possible assignments resulting from
those interventions:

$\displaystyle\Delta_{\varphi}=\Big{\\{}\bigwedge_{\alpha\in\mathcal{I}}\;\Big{(}[\alpha]\bigwedge_{V\in\mathbf{V}_{\varphi}}\beta_{V}^{\alpha}\Big{)}\;:\;\beta_{V}^{\alpha}\in\text{Val}(V)\text{
for }V\in\textbf{V}_{\varphi}\Big{\\}}$

We note that interventions and values are not restricted to those appearing in
$\varphi$; this is a departure from the definition of $\Delta_{\varphi}$ in
Mossé et al., (2024).

######  Lemma 1 (Exponential model property).

Fix a formula $\varphi$ in $\mathcal{L}_{\text{causal}}^{\text{closed}}(N)$.
If $\varphi$ is satisfiable, then it is satisfied by a model $\mathfrak{M}$
which assigns positive probability to at most $2^{\text{poly}(|\varphi|)}$
complete state descriptions $\delta\in\Delta_{\varphi}$.

###### Proof.

Transform $\varphi$ into a formula $\varphi^{\prime}$ by writing out each sum
and range variable or coefficient explicitly. For example,
$\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x_{i}}x_{i}\cdot\mathsf{P}(X=x_{i})$ is replaced
with
$1\cdot\mathsf{P}\big{(}X=c_{1}^{X}\big{)}+2\cdot\mathsf{P}\big{(}X=c_{2}^{X}\big{)}+\dots+n\cdot\mathsf{P}\big{(}X=c_{n}^{X}\big{)}$,
where the natural number $n$ is shorthand for
$\mathsf{P}(\top)+\dots+\mathsf{P}(\top)$, the $n$-term sum of
$\mathsf{P}(\top)$. (Note that this formulation of $\varphi^{\prime}$ requires
the closed-world and finite range assumptions: each value in the finite range
of $X$ is named by a constant.)

Then $\varphi^{\prime}$ contains no summation operators and no unbound
assignments; it belongs to the fragment $\mathcal{L}$ of
$\mathcal{L}_{\text{causal}}$ without summation or free variables. Let
$\Delta_{\varphi^{\prime}}$ contain all interventions appearing in
$\varphi^{\prime}$ paired with all possible assignments. Note that
$\Delta_{\varphi^{\prime}}\subseteq\Delta_{\varphi}$. By the small model
property for $\mathcal{L}$ (Lemma 4.7 of Mossé et al., 2024),
$\varphi^{\prime}$ has a model which assigns positive probability to at most
$|\varphi^{\prime}|\leq 2^{\text{poly}(|\varphi|)}$ complete state
descriptions $\delta\in\Delta_{\varphi^{\prime}}$. This is also a model of
$\varphi$, given that $\Delta_{\varphi^{\prime}}\subseteq\Delta_{\varphi}$ and
the construction of $\varphi^{\prime}$ from $\varphi$. ∎

We now show completeness, using the following hardness result:

######  Theorem 6 (van der Zander et al., 2023).

The satisfiability problem for $\mathcal{L}_{\text{prob}}^{\text{closed}}(N)$
is succETR-hard.

###### Proof of Theorem 3.

By Theorem 6, satisfiability for
$\mathcal{L}_{\text{prob}}^{\text{closed}}(N)$, and thus for
$\mathcal{L}_{\text{causal}}(N)$, is succETR-hard. It then suffices to show
that satisfiability for $\mathcal{L}_{\text{causal}}(N)$ is in succETR.
Consider any sequent $\varphi\Rightarrow\psi$ in
$\mathcal{L}_{\text{causal}}$. By Theorem 5, it suffices to construct a
nondeterministic exponential time real RAM $M$ which decides whether
$\varphi\Rightarrow\psi$ is satisfiable:

  1. 1.

For a possible assignment $\iota$ of free range variables appearing in
$\varphi$, let $\varphi_{\iota}$ denote the result of replacing all free
variables with constants denoting their assignments, e.g. replacing
$\mathsf{P}(V=v_{i})$ with $\mathsf{P}(V=c_{j}^{V})$, where $j=\iota(V,i)$.
Let $\overline{\varphi}=\bigwedge_{\iota}\varphi_{\iota}$, and similarly for
$\overline{\psi}$. Then
$\overline{\varphi},\overline{\psi}\in\mathcal{L}_{\text{causal}}^{\text{closed}}$,
and $\varphi\Rightarrow\psi$ iff
$\overline{\varphi}\Rightarrow\overline{\psi}$. Let $M$ construct
$\overline{\varphi}\Rightarrow\overline{\psi}$, which is exponential in the
size of the input formula. Since this sequent has no free variables, it is
equisatisfiable with $\overline{\varphi}\rightarrow\overline{\psi}$ and may be
considered a single formula $\varphi^{\prime}$.

  2. 2.

Using Lemma 1, let $M$ receive as a certificate the support $\Delta^{\prime}$
of an exponential model for $\varphi^{\prime}$ and an ordering $\prec$ on the
variables $\textbf{V}_{\varphi^{\prime}}$. Note that
$|\Delta^{\prime}|\leq|\Delta_{\varphi^{\prime}}|\leq
2^{\text{poly}(|\varphi|)}$.

  3. 3.

$M$ will then check that $\Delta^{\prime}\subseteq\Delta_{\varphi^{\prime}}$
and that the $\delta\in\Delta^{\prime}$ do not induce influence relations
which are incompatible with the ordering $\prec$ (Lemma 4.5 of Mossé et al.,
2024).777A model $\mathfrak{M}$ induces the influence relation
$V_{i}\rightsquigarrow V_{j}$ when there exist values
$v,v^{\prime}\in\text{Val}(V_{j})$ and interventions $\alpha,\alpha^{\prime}$
differing only in the value they impose upon $V_{i}$ for which
$\mathfrak{M}\vDash\mathsf{P}\big{(}[\alpha]V_{j}=v\land[\alpha^{\prime}]V_{j}=v^{\prime}\big{)}>0.$
Given an enumeration of variables $V_{1},...,V_{n}$ compatible with a well-
order $\prec$, the model $\mathfrak{M}$ is compatible with $\prec$ when it
induces no instance $V_{i}\rightsquigarrow V_{j}$ with $i>j$.

  4. 4.

$M$ will form a formula $\varphi_{\text{prob}}$ from $\varphi^{\prime}$ by
replacing each $\mathsf{P}(\epsilon)$ in $\varphi$ with

$\mathsf{P}\bigg{(}\bigvee_{\begin{subarray}{c}\delta\in\Delta^{\prime}\\\
\delta\vDash\epsilon\end{subarray}}f(\delta)\bigg{)},$

where $f$ is a bijection between $\Delta^{\prime}$ and an arbitrary set of
mutually unsatisfiable propositional statements built from the atoms
$X=c^{X}_{3},Y=c^{Y}_{1}$, and so on.

  5. 5.

Now $\varphi_{\text{prob}}\in\mathcal{L}_{\text{prob}}^{\text{closed}}(N)$ and
contains no marginalization. Satisfiability for
$\mathcal{L}_{\text{prob}}^{\text{closed}}(N)$ without marginalization is ETR-
complete (Mossé et al.,, 2024). Any problem in ETR is decidable by a
nondeterministic, polynomial-time real RAM $M^{\prime}$ (Erickson et al.,,
2022), so $M^{\prime}$ solves the satisfiability problem for $\psi$ in
polynomial time. Let $M$ run $M^{\prime}$ on $\varphi_{\text{prob}}$ and
return the result.

If $\varphi\Rightarrow\psi$ is satisfiable, then there is some probability
assignment to the $\delta\in\Delta^{\prime}$ which satisfies it (by Lemma 1);
this assignment is also a model of $\varphi_{\text{prob}}$. Conversely, if
there is a model of $\varphi_{\text{prob}}$, then the mutual unsatisfiability
of the $f(\delta)$ ensures the existence of a causal model for
$\varphi^{\prime}=\varphi\rightarrow\psi$, and thus for
$\varphi\Rightarrow\psi$ (Lemma 4.6 of Mossé et al., 2024). Thus the map
$\varphi\Rightarrow\psi\mapsto\varphi_{\text{prob}}$ preserves and reflects
satisfiability, and $M$ decides the satisfiability of the latter. ∎

In addition to resolving an open question about the complexity of
$\mathsf{SAT}_{\mathcal{L}_{\text{causal}}(N)}$, the above immediately gives
an independent proof of the completeness results van der Zander et al., (2023)
obtained for languages intermediate between $\mathcal{L}_{\text{causal}}(N)$
and $\mathcal{L}_{\text{prob}}^{\text{closed}}(N)$. We note that Dörfler et
al., (2024) independently obtained the above result, by the same argument, for
the fragment of $\mathcal{L}_{\text{causal}}$ without coefficients or free
variables.

The above result can also be used to show recursive enumerability for
$\mathsf{SAT}_{\mathcal{L}_{\text{causal}}}$ over merely finite models:

###### Proof of Theorem 4.

We show that $\mathsf{SAT}_{\mathcal{L}_{\text{causal}}}$ over
$\mathcal{M}_{\text{fin}}$ is recursively enumerable. Fix a satisfiability
problem $\Gamma\Rightarrow\psi$; with $\Gamma$ assumed finite, we may replace
it with a single formula $\varphi$. Enumerate over all possible finite ranges
of all variables appearing in $\varphi,\psi$.

For each such finite range, by Theorem 3, the satisfiability problem for
$\varphi\Rightarrow\psi$ is computable by some Turing machine $M$. Run $M$ and
declare $\varphi\Rightarrow\psi$ satisfiable if $M$ returns yes. If
$\varphi\Rightarrow\psi$ is satisfiable over $\mathcal{M}_{\text{fin}}$, then
it is satisfiable for some choice of finite ranges, and this procedure will
correctly declare it satisfiable.∎

##  4 Axiomatization

We now work toward an axiomatization of the entailment relation
$\Gamma\vDash\varphi$ for probabilistic languages. We will make the
coefficient restriction of (5), focusing on the languages
$\mathcal{L}^{\ddagger}_{\text{prob}}$ and
$\mathcal{L}^{\ddagger}_{\text{prob}}(N)$, where
$\ddagger\in\\{\circ,\circ+\text{closed}\\}$. Note that our semantics have
possibly unintuitive outcomes when it comes to conditional probability. For
example, even the formula $\mathsf{P}(Y=y\mid X=x)\succsim\underline{0}$ or
$\mathsf{P}(Y=y\mid X=x)\succ\underline{0}\lor\lnot\mathsf{P}(Y=y\mid
X=x)\succ\underline{0}$ is invalid, as witnessed by any model assigning zero
measure to some $X=x$, and just as in Kleene’s 3-valued logic there are no
Boolean tautologies. One solution is to “guard” each formula with an
antecedent saying that all its conditions occur with positive probability.
However, in order to simplify the results, we will instead assume every SCM
$\mathfrak{M}$ to be _positive_ , meaning that the observational joint
distribution $\mathbb{P}_{\mathfrak{M}}(\mathbf{V})$ is strictly positive,
i.e., such that the measure of any clopen cylinder set is nonzero. (Recall a
cylinder set is any $S=\bigtimes_{V\in\mathbf{V}}S_{V}$ where
$S_{V}=\mathrm{Val}(V)$ for all except finitely many $V$.) Although this
assumption is stronger, it is ubiquitous in causal inference (see, e.g.,
Shpitser and Pearl, 2008; Pearl, 2009 for typical examples).

######  Definition 19.

Let $\mathcal{M}^{+},\mathcal{M}_{\text{fin}}^{+},\mathcal{M}_{N}^{+}$ be the
positive subclasses of $\mathcal{M},\mathcal{M}_{\text{fin}},\mathcal{M}_{N}$
respectively.

The assumption of positivity ensures that conditional probabilities are well-
defined, provided we never condition on events equivalent to $\bot$. We will
therefore restrict conditions to the fragment
$\mathcal{L}_{\text{cond}}\subset\mathcal{L}_{\text{base}}^{\mathrm{prob}}$
consisting of $\top$ and pure conjunctions of literals ($V=d$ or $\lnot V=d$)
such that for any $V\in\mathbf{V}$, a literal involving $V$ appears at most
once in $\varphi$. It is straightforward to see that any
$\varphi\in\mathcal{L}_{\text{cond}}$ receives a positive probability under
any positive $\mathfrak{M}$ and assignment $\iota$.

######  Definition 20.

Let $\mathcal{L}_{\text{prob}^{+}}^{\ddagger}$ for
$\ddagger\in\\{\circ,\circ+\text{closed}\\}$ be the fragment of
$\mathcal{L}_{\text{prob}}^{\ddagger}$ where in any primitive term
$\mathsf{P}(\delta\;|\>\delta^{\prime})$ from (5) we require
$\delta^{\prime}\in\mathcal{L}_{\text{cond}}$. Let
$\mathcal{L}_{\text{prob}^{+}}^{\ddagger}(N)$ be the same over signatures of
uniform cardinality $N$ (cf. §2.1.3). With $\mathcal{L}$ standing for
$\mathcal{L}_{\text{prob}^{+}}^{\circ}$, we abbreviate these four as
$\mathcal{L}_{**}^{*}$ for
$*\in\\{\varepsilon,\text{closed}\\},**\in\\{\varepsilon,N\\}$.

###  4.1 Axioms

We start with the system $\mathsf{AX}_{\text{poly}}$ from Ibeling et al.,
(2023). This includes Boolean tautologies across probability comparisons as
well as equalities between variable symbols. As for new axioms, first, we
include properties of $\equiv$; for any $c,c^{\prime}\in\mathcal{C}_{V}$ and
$V\in\mathbf{V}$:

$\displaystyle\mathsf{EqReflex}.$ $\displaystyle c\equiv c$
$\displaystyle\mathsf{EqReplace}.$ $\displaystyle c\equiv
c^{\prime}\rightarrow(\varphi[v/c]\rightarrow\varphi[v/c^{\prime}]).$

Another principle states that unequal constants cannot occur simultaneously:

$\displaystyle\mathsf{EqDist}.$ $\displaystyle c\not\equiv
c^{\prime}\rightarrow\mathsf{P}(V=c\land V=c^{\prime})\approx\underline{0}.$

Then, a single axiom schema allows us to reduce conditional to unconditional
probability:

$\displaystyle\mathsf{Cond}.$
$\displaystyle\mathsf{P}(\delta\;|\;\delta^{\prime})\succsim\mathsf{t}\leftrightarrow\mathsf{P}(\delta\land\delta^{\prime})\succsim\mathsf{t}\cdot\mathsf{P}(\delta^{\prime}).$

Next, we have a lower bound on sums. Where $S\subset\mathcal{C}_{V}$ is any
finite subset of constants:

$\displaystyle\mathsf{SumLower}.$
$\displaystyle\bigwedge_{\begin{subarray}{c}i\neq j\\\ c^{V}_{i},c^{V}_{j}\in
S\end{subarray}}c^{V}_{i}\not\equiv
c^{V}_{j}\rightarrow\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{v_{i}}\mathsf{t}\succsim\sum_{c^{V}_{i}\in
S}\mathsf{t}[V={v_{i}}/V=c^{V}_{i}]$

After that, an axiom captures the strict positivity assumed in our model
classes. Where $\alpha$ ranges over $\mathcal{L}_{\mathrm{cond}}$:

$\displaystyle\mathsf{Pos}.$
$\displaystyle\mathsf{P}(\alpha)\succ\underline{0}.$

Finally, for the case of finite signatures only, to capture the distinctness
requirement in $\mathcal{M}_{N}$ we introduce the axiom schema

$\displaystyle\mathsf{Fin}_{N}.$
$\displaystyle\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{v_{i}}\mathsf{P}(\top)\approx\underline{N}.$

###  4.2 Rules

The system $\mathsf{AX}_{\text{poly}}$ we adopted from prior work has only one
rule, _modus ponens_ , i.e., $\\{\varphi,\varphi\rightarrow\psi\\}\vdash\psi$
or

$\displaystyle\psi\varphi,\varphi\rightarrow\psi$

As we will illustrate by several different examples, all our languages are
incompact over their respective model classes, necessitating the use of rules
with infinitely many premises in order to obtain strongly complete
axiomatizations. We first introduce a variant of the infinitary rule R3 of
Perović et al., (2008):

$\displaystyle\varphi\rightarrow\mathsf{t}\precsim\underline{0}\varphi\rightarrow\mathsf{t}\precsim\underline{1/n}\text{
for every }n=1,2,3,\dots$

which allows eliciting a contradiction from finitely-satisfiable,
unsatisfiable sets, such as

$\\{\mathsf{P}(V=c_{1}^{V})\precsim\underline{1/n}:n=1,2,3,\dots\\}\cup\\{\mathsf{P}(V=c_{1}^{V})\succ\underline{0}\\}.$

Next, we add the following rule (or collection thereof), for every finite
$\mathbf{X}\subset\mathbf{V}$ and rational $q>0$:

$\displaystyle\varphi\rightarrow\underline{1}-\mathsf{P}\Big{(}\bigwedge_{X\in\mathbf{X}}X=c_{X}^{1}\lor\lnot
X=c_{X}^{1}\Big{)}\succ\underline{q}\varphi\rightarrow\underline{1}-\mathsf{P}\Big{(}\bigwedge_{X\in\mathbf{X}}\bigvee_{\begin{subarray}{c}1\leq
i\leq n\\\
c^{X}_{i}\in\mathcal{C}_{X}\end{subarray}}X=c_{X}^{i}\Big{)}\succ\underline{q}\text{
for every }n=1,2,3,\dots$

Note that from its conclusion we can deduce $\varphi\rightarrow\bot$;
nevertheless, it will be important for our proof strategy that it have the
specific form above. Also observe that the rule above is infinitary iff we
have infinitely many constant symbols; the set of formulas
$\big{\\{}\mathsf{P}(V=c_{V}^{n})\approx\underline{1/3^{n}}:n=1,2,3,\dots\big{\\}}$
in such a signature is finitely satisfiable but unsatisfiable, and
$\mathsf{Unity}$ derives a contradiction from it.

After that, the following rule provides upper bounds on sums. Where $\varphi$
is a formula and $\mathsf{t}$ is some term, $n\geq 1$ and
$\Pi=\\{\Pi_{\upsilon}\\}_{\upsilon\in\Upsilon}$ is a partition of
$\mathcal{C}_{X}(n)=\\{c^{X}_{i}\in\mathcal{C}_{X}:1\leq i\leq n\\}$, let
$\varphi_{n,\Pi}$ denote the formula

$\displaystyle\varphi_{n,\Pi}\quad:=\quad\varphi\rightarrow\Big{[}\Big{(}\bigwedge_{\begin{subarray}{c}\upsilon\in\Upsilon\\\
c^{X}_{i},c^{X}_{j}\in\Pi_{\upsilon}\end{subarray}}c^{X}_{i}=c^{X}_{j}\land\bigwedge_{\begin{subarray}{c}\upsilon\neq\upsilon^{\prime}\in\Upsilon\\\
c^{X}_{i}\in\Pi_{\upsilon}\\\
c^{X}_{j}\in\Pi_{\upsilon^{\prime}}\end{subarray}}c^{X}_{i}\neq
c^{X}_{j}\Big{)}\rightarrow\sum_{\upsilon\in\Upsilon}\mathsf{t}\big{[}X=x_{i}/\bigvee_{c^{X}_{i}\in\Pi_{\upsilon}}X=c^{X}_{i}\big{]}\precsim\mathsf{t}^{\prime}\Big{]}.$
(8)

Letting $\mathbf{B}_{n}$ be the set of partitions of $\mathcal{C}_{X}(n)$, we
have a rule:

$\displaystyle\varphi\rightarrow\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x_{i}}\mathsf{t}\precsim\mathsf{t}^{\prime}\varphi_{n,\Pi}\text{
for each }n\in\mathbb{Z}^{+},\Pi\in\mathbf{B}_{n}$

As with $\mathsf{Unity}$, the rule $\mathsf{SumUpper}$ becomes infinitary with
infinite signatures. A finitely satisfiable set it proves inconsistent is
$\big{\\{}\bigwedge_{1\leq i\neq j\leq n}c^{X}_{i}\neq
c^{X}_{j}\land\sum_{i=1}^{n}\mathsf{P}(X=c^{X}_{i})\precsim\underline{1/2}:n=1,2,3,\dots\big{\\}}$.

Finally, consider the set
$\\{\mathsf{P}(X=c_{X}^{n})\approx\underline{1/2^{n}}:n=1,2,3,\dots\\}$,
satisfiable in $\mathcal{M}$. In $\mathcal{M}_{\text{fin}}$, this set is
finitely satisfiable but unsatisfiable. The next rule addresses the
distinction; as with $\mathsf{Unity}$, its conclusion proves
$\varphi\rightarrow\bot$:

$\displaystyle\varphi\rightarrow\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x_{i}}\mathsf{P}(\top)\prec\underline{0}\varphi\rightarrow\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x_{i}}\mathsf{P}(\top)\succsim\underline{n}\text{
for every }n=1,2,3,\dots$

Although $\mathsf{Fin}$ is still an infinitary rule if we have finitely many
constants, we will not need it in this case.

Having completed our description of the axioms and rules, we can now define
the systems for the closed fragments:

######  Definition 21.

Let
$\mathsf{AX}^{\text{closed}}=\mathsf{AX}_{\text{poly}}+\mathsf{EqReflex}+\mathsf{EqReplace}+\mathsf{EqDist}+\mathsf{Cond}+\mathsf{SumLower}+\mathsf{Pos}+\mathsf{Conv}+\mathsf{Unity}+\mathsf{SumUpper}$,
$\mathsf{AX}^{\text{closed}}_{N}=\mathsf{AX}^{\text{closed}}+\mathsf{Fin}_{N}$,
and
$\mathsf{AX}^{\text{closed}}_{\text{fin}}=\mathsf{AX}^{\text{closed}}+\mathsf{Fin}$.

###  4.3 Deduction with free variables

Finally add two rules toward axiomatizing the languages with free variables
(implicitly universally quantified):

$\displaystyle\varphi[v/c]\varphi\qquad\qquad\varphi\varphi[v/c]\text{ for
each }c\in\mathcal{C}_{V}$

where $v\in\mathcal{V}_{V}$ is any range variable for $V$ and in the
conclusion of $\mathsf{FreeElim}$, $c\in\mathcal{C}_{V}$ is any $V$-constant.
As the deduction theorem fails in this setting (see Rmk. 1), unlike with the
previous infinitary rules we have no intuitive example of incompactness
associated with $\mathsf{FreeIntro}$.

######  Definition 22.

Let
$\mathsf{AX}_{*}=\mathsf{AX}_{*}^{\text{closed}}+\mathsf{FreeElim}+\mathsf{FreeIntro}$
for each $*\in\\{\varepsilon,N,\text{fin}\\}$.

Although these systems just amount to handling free variables via (infinitely
many) constant substitutions, note that those of §4.1–4.2 at least generally
remain sound when schemata range over free variables.

###  4.4 Examples

Before proving completeness, we give a few examples to illustrate reasoning
with the systems above. First, it is straightforward to see that the deduction
theorem _does_ hold in the closed systems of Definition 21:

######  Lemma 2 (Deduction Theorem).

Let $T\subset\mathcal{L}_{*}^{\text{closed}}$ and
$\varphi,\psi\in\mathcal{L}_{*}^{\text{closed}}$. Then
$T\vdash\varphi\rightarrow\psi$ iff $T\cup\\{\varphi\\}\vdash\psi$, where
$\vdash$ is derivability in ${\mathsf{AX}^{\text{closed}}_{*}}$. ∎

####  4.4.1 The bounded case

Consider the following axioms:

$\displaystyle\mathsf{Distinct}_{N}.$ $\displaystyle\bigwedge_{1\leq i\neq
j\leq N}c^{V}_{i}\not\equiv c^{V}_{j},$ (9)
$\displaystyle\mathsf{SumEquals}_{N}.$
$\displaystyle\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
<EMAIL_ADDRESS>(10)

######  Proposition 1.

These are interderivable: (1) $\mathsf{AX}_{N}$; (2)
$\mathsf{AX}+\mathsf{Distinct}_{N}$; (3) $\mathsf{AX}+\mathsf{SumEquals}_{N}$.

###### Proof.

$(1)\vdash(2)$: if $c_{i}^{V}\equiv c_{j}^{V}$ for some $i,j$, then
$\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x}\mathsf{P}(\top)\precsim\underline{N-1}$ by
$\mathsf{SumUpper}$, contradicting $\mathsf{Fin}_{N}$; $(2)\vdash(3)$: derive
$\mathsf{SumEquals}_{N}$ using $\mathsf{SumLower}$ and $\mathsf{SumUpper}$
together; $(3)\vdash(1)$: trivial by taking $\mathsf{t}=\mathsf{P}(\top)$. ∎

####  4.4.2 Sums of sums

We derive the following principle:

$\displaystyle\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{v_{i}}(\mathsf{t}_{1}+\mathsf{t}_{2})\approx\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{v_{i}}\mathsf{t}_{1}+\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
<EMAIL_ADDRESS>
Casing on the different possibilities of whether $c^{X}_{i}\equiv c^{X}_{j}$
for each $X$ and $i,j\leq n$, using $\mathsf{SumUpper}$ and
$\mathsf{SumLower}$, along with $\mathsf{EqReflex}$ and $\mathsf{EqReplace}$
for reasoning about equalities, we can derive for any $\mathsf{t}^{\prime}$
that $\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{v_{i}}(\mathsf{t}_{1}+\mathsf{t}_{2})\precsim\mathsf{t}^{\prime}\leftrightarrow\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{v_{i}}\mathsf{t}_{1}+\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{v_{i}}\mathsf{t}_{2}\precsim\mathsf{t}^{\prime}$.
Thus it suffices to show the following rule admissible:

$\displaystyle\mathsf{t}\approx\mathsf{t}^{\prime\prime}\mathsf{t}\precsim\mathsf{t}^{\prime}\leftrightarrow\mathsf{t}^{\prime\prime}\precsim\mathsf{t}^{\prime}\text{
for any term }\mathsf{t}^{\prime}.$

To see this, use Lemma 2. If $\Gamma$ contains all the premises but
$\Gamma\cup\\{\mathsf{t}\not\approx\mathsf{t}^{\prime\prime}\\}$ is
consistent, then supposing without loss that
$\mathsf{t}\prec\mathsf{t}^{\prime\prime}$, we can prove
$\mathsf{t}\prec\frac{\mathsf{t}+\mathsf{t}^{\prime\prime}}{\underline{2}}\prec\mathsf{t}^{\prime\prime}$,
a contradiction.

####  4.4.3 Conditional independence implication

Suppose we have some conditional independence implication (3) that is true
over finite ranges, encoded with free variables as
$\\{\varphi_{1},\dots,\varphi_{\ell}\\}\vDash\varphi_{0}$, where without loss
we take those free ones to be $x_{1},\dots,x_{k}$; we want to show
$\\{\varphi_{1},\dots,\varphi_{\ell}\\}\vdash\varphi_{0}$ over
$\mathsf{AX}_{\text{fin}}$. Letting $\mathbf{X}=\\{X_{1},\dots,X_{k}\\}$, note
that, by the completeness of $\mathsf{AX}_{\text{poly}}$ for semi-algebraic
reasoning (Ibeling et al.,, 2023), we can show for each $n$ that
$\\{\varphi^{n}_{1},\dots,\varphi^{n}_{\ell}\\}\cup\big{\\{}\mathsf{P}\big{(}\bigwedge_{X\in\mathbf{X}}\bigvee_{i=1}^{n}X=c^{X}_{i}\big{)}\approx\underline{1}\big{\\}}\vdash\varphi^{n}_{0}$
where $\varphi^{n}_{i}=\bigwedge_{1\leq i_{1},\dots,i_{k}\leq
n}\varphi_{i}\big{[}x_{1}/c_{i_{1}}^{X_{1}}\big{]}\dots\big{[}x_{k}/c_{i_{k}}^{X_{k}}\big{]}$.
By Lemma 2 for $\mathcal{L}^{\text{closed}}$ and $\mathsf{FreeElim}$ this
means
$\\{\varphi_{1},\dots,\varphi_{\ell}\\}\vdash\mathsf{P}\big{(}\bigwedge_{X\in\mathbf{X}}\bigvee_{i=1}^{n}X=c^{X}_{i}\big{)}\approx\underline{1}\rightarrow\varphi^{m}_{0}$,
for each $n$ and $m\leq n$.

Since $\\{\varphi^{n}_{0}:n\geq 1\\}\vdash\varphi_{0}$ by
$\mathsf{FreeIntro}$, to complete the argument, it suffices to show the
following rule is admissible:

$\displaystyle\varphi\mathsf{P}\big{(}\bigwedge_{X\in\mathbf{X}}\bigvee_{i=1}^{n}X=c^{X}_{i}\big{)}\approx\underline{1}\rightarrow\varphi\text{
for each }n\in\mathbb{Z}^{+}.$

To see this, if $\lnot\varphi$ is consistent with the premises, then conclude
$\mathsf{P}\big{(}\bigwedge_{X\in\mathbf{X}}\bigvee_{i=1}^{n}X=c^{X}_{i}\big{)}\prec\underline{1}$
for all $n$. Casing on whether $c^{X}_{i}\equiv c^{X}_{j}$ for each $X$ and
$i,j\leq n$, as $n\to\infty$ by consistency with $\mathsf{Unity}$ there must
be infinitely many equivalence classes of constants under this relation, for
at least some $X$. But this implies inconsistency with $\mathsf{Fin}$ via
$\mathsf{SumUpper}$.

###  4.5 Completeness

######  Theorem 7.

The six systems above are sound and strongly complete in the respective
settings (Table 1).

Axiomatic System | Language | Model Class
---|---|---
$\mathsf{AX}^{\text{closed}}$ | $\mathcal{L}^{\text{closed}}$ | $\mathcal{M}^{+}$
$\mathsf{AX}^{\text{closed}}_{\text{fin}}$ | $\mathcal{L}^{\text{closed}}$ | $\mathcal{M}^{+}_{\text{fin}}$
$\mathsf{AX}^{\text{closed}}_{N}$ | $\mathcal{L}_{N}^{\text{closed}}$ | $\mathcal{M}^{+}_{N}$
$\mathsf{AX}$ | $\mathcal{L}$ | $\mathcal{M}^{+}$
$\mathsf{AX}_{\text{fin}}$ | $\mathcal{L}$ | $\mathcal{M}^{+}_{\text{fin}}$
$\mathsf{AX}_{N}$ | $\mathcal{L}_{N}$ | $\mathcal{M}^{+}_{N}$
Table 1: Deductive systems (Definitions 21, 22), languages (Definition 20),
and model classes (Definition 19) with respect to which we show soundness and
completeness.

###### Proof.

Soundness is straightforward. As for completeness, it suffices to prove only
the closed cases:

######  Lemma 3.

Suppose $\mathsf{AX}^{\text{closed}}_{*}$ is complete for
$\mathcal{L}^{\text{closed}}_{*}$ over $\mathcal{M}^{+}_{*}$, where $*$ ranges
over the cases in Table 1. Then $\mathsf{AX}_{*}$ is complete for
$\mathcal{L}_{*}$ over $\mathcal{M}^{+}_{*}$.

###### Proof.

Suppose $\Gamma\vDash\varphi$ over $\mathcal{M}^{+}_{*}$, where
$\varphi\in\mathcal{L}_{*}$. Write $\varphi/\psi$ for
$\psi\in\mathcal{L}^{\text{closed}}_{*}$ if
$\psi=\varphi[x_{1}/c^{X_{1}}_{i_{1}}]\dots[x_{n}/c^{X_{n}}_{i_{n}}]$ for some
random variables $X_{1},\dots,X_{n}\in\mathbf{V}$, corresponding free
variables $x_{1},\dots,x_{n}$, and indices
$i_{1},\dots,i_{n}\in\mathbb{Z}^{+}$. Define
$\Delta=\\{\delta\in\mathcal{L}^{\text{closed}}_{*}:\gamma/\delta\text{ for
some }\gamma\in\Gamma\\}$ and
$\Psi=\\{\psi\in\mathcal{L}_{*}^{\text{closed}}:\varphi/\psi\\}$. Then
$\Gamma\vDash\varphi$ implies that $\Delta\vDash\psi$ for any $\psi\in\Psi$.
Note that $\Gamma\vdash\delta$ for every $\delta\in\Delta$ using
$\mathsf{FreeElim}$, while $\Delta\vdash\psi$ for every $\psi\in\Psi$ by
completeness of $\mathsf{AX}_{*}^{\text{closed}}$ for
$\mathcal{L}_{*}^{\text{closed}}$; finally $\Psi\vdash\varphi$ using
$\mathsf{FreeIntro}$. Thus $\Gamma\vdash\varphi$. ∎

As for $\mathsf{AX}^{\text{closed}}_{N}$, the axiom (10) is derivable and
allows the elimination of all primitive sum operators, thereby reducing the
problem essentially to the setting of Perović et al., (2008) where the result
has already been shown. Thus we prove only $\mathsf{AX}^{\text{closed}}$ and
the finite case $\mathsf{AX}^{\text{closed}}_{\text{fin}}$. By Lemma 2 we can
prove completeness in the usual way by showing that any consistent set
$\Gamma$ is satisfiable, toward which we will now show $\Gamma$ can be
extended to some maximal consistent $\Gamma^{*}$. The preliminary results
below are variations of Perović et al., (2008, Lemma 1, Definition 6, Theorem
2); we omit their completely analogous proofs.

######  Lemma 4.

Consider any (instance of) one of our infinitary rules, with premises
$\varphi\rightarrow\psi_{i}$ indexed $i\in\mathbb{Z}^{+}$ and conclusion
$\varphi\rightarrow\psi$. Suppose $T\subset\mathcal{L}$ is consistent but
$T\cup\\{\varphi\rightarrow\psi\\}$ is inconsistent. Then there is some
$n\in\mathbb{Z}^{+}$ such that $T\cup\\{\varphi\rightarrow\lnot\psi_{n}\\}$ is
consistent.

######  Definition 23.

Enumerate the formulas of $\mathcal{L}$ as
$\\{\varphi_{1},\varphi_{2},\varphi_{3},\dots\\}$. Let $T\subset\mathcal{L}$
be consistent, and define for each $i$ a set $T_{i}$ as follows:

  1. 1.

$T_{0}=T$.

  2. 2.

If $T_{i}\cup\\{\varphi_{i}\\}$ is consistent then
$T_{i+1}=T_{i}\cup\\{\varphi_{i}\\}$.

  3. 3.

If $T_{i}\cup\\{\varphi_{i}\\}$ is inconsistent then:

    1. (a)

If $\varphi_{i}$ is $\varphi\rightarrow\mathsf{t}\precsim\underline{0}$ then
let $T_{i+1}=T_{i}\cup\\{\varphi\rightarrow\mathsf{t}\succ\underline{1/n}\\}$
where $n$ is that guaranteed by Lemma 4, applied to $\mathsf{Conv}$, such that
$T_{i+1}$ is consistent.

    2. (b)

If $\varphi_{i}$ is
$\varphi\rightarrow\Big{[}\underline{1}-\mathsf{P}\Big{(}\bigwedge_{X\in\mathbf{X}}X=c_{X}^{1}\lor\lnot
X=c_{X}^{1}\Big{)}\succ\underline{q}\Big{]}$ then let
$T_{i+1}=T_{i}\cup\\{\varphi\rightarrow\Big{[}\underline{1}-\mathsf{P}\Big{(}\bigwedge_{X\in\mathbf{X}}\bigvee_{1\leq
i\leq n}X=c_{X}^{i}\Big{)}\precsim\underline{q}\Big{]}\\}$ where $n$ is that
guaranteed by Lemma 4, applied to $\mathsf{Unity}$, such that $T_{i+1}$ is
consistent.

    3. (c)

If $\varphi_{i}$ is
$\varphi\rightarrow\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x}\mathsf{t}\precsim\mathsf{t}^{\prime}$ then let
$T_{i+1}=T_{i}\cup\\{\varphi\rightarrow\lnot\varphi_{n,\Pi}\\}$ where
$\varphi_{n,\Pi}$ is the formula (8) and $n,\Pi$ are guaranteed by Lemma 4,
applied to $\mathsf{SumUpper}$, to make $T_{i+1}$ consistent.

    4. (d)

In the finite case: if $\varphi_{i}$ is
$\varphi\rightarrow\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x}\mathsf{P}(\top)\prec\underline{0}$ then let
$T_{i+1}=T_{i}\cup\\{\varphi\rightarrow\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x}\mathsf{P}(\top)\prec\underline{n}\\}$ where $n$
is guaranteed by Lemma 4, applied to $\mathsf{Fin}$, to make $T_{i+1}$
consistent.

    5. (e)

Otherwise let $T_{i+1}=T_{i}$.

Then let $T^{*}=\bigcup_{i=1}^{\infty}T_{i}$. The above are disjoint and
exhaustive since the structural form of $\varphi_{i}$ is distinct for all
cases 3a–3d and any possible instances of rules therein.

######  Lemma 5 (Lindenbaum’s).

Suppose $T$ is consistent with $T^{*}$ that defined by Definition 23. Then (1)
$T^{*}\vdash\varphi$ implies $\varphi\in T^{*}$, (2) not every formula is in
$T^{*}$, and (3) for each $\varphi$ either $\varphi\in T^{*}$ or
$\lnot\varphi\in T^{*}$. ∎

Thus we extend $\Gamma$ to $\Gamma^{*}$; we will now define a model
$\mathfrak{M}^{*}$ satisfying $\Gamma^{*}$. We first work toward defining the
constant interpretations and ranges. We have:

######  Lemma 6.

Define a relation $\sim$ on $\mathcal{C}_{V}$ by $c_{i}^{V}\sim c_{j}^{V}$ iff
$c_{i}^{V}\equiv c_{j}^{V}\in\Gamma^{*}$. Then $\sim$ is an equivalence
relation.

###### Proof.

By $\mathsf{EqReplace}$ with $\varphi=v\equiv c$ we have $c\equiv
c^{\prime}\rightarrow(c\equiv c\rightarrow c^{\prime}\equiv c)$ so we can
derive $c\equiv c^{\prime}\rightarrow c^{\prime}\equiv c$ since
$\mathsf{EqReflex}$ is an axiom. Transitivity is clear as well, since we have
$c^{\prime}\equiv c^{\prime\prime}\rightarrow(c\equiv c^{\prime}\rightarrow
c\equiv c^{\prime\prime})$. ∎

For each $V\in\mathbf{V}$ the set of equivalence classes under $\sim$ is
countable; if finite of cardinality $M$, define
$\mathrm{Val}(V)=\\{1,\dots,M\\}$ and if infinite, define
$\mathrm{Val}(V)=\mathbb{Z}^{+}$, with
$g_{V}:\mathrm{Val}(V)\to\mathcal{C}_{V}$ a map defining an association of
elements $v$ of $\mathrm{Val}(V)$ to equivalence classes $[g_{V}(v)]$
represented by $g_{V}(v)$, i.e. such that $[g_{V}(v)]\neq[g_{V}(v^{\prime})]$
for $v\neq v^{\prime}\in\mathrm{Val}(V)$. In particular $g_{V}$ is injective
and we define the constant interpretations
$(c^{V}_{i})^{\mathfrak{M}^{*}}=g_{V}^{-1}(c^{V}_{i})$. In the finite cases,
consistency with $\mathsf{Fin}$ implies that each $\mathrm{Val}(V)$ is finite,
since otherwise by $\mathsf{SumLower}$ we can show
$\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{v}\mathsf{P}(\top)\succsim\underline{n}$ for each
$n$. We now define a measure $\mu$ on a basis of cylinder sets to obtain the
model $\mathfrak{M}^{*}$. That is, we define the measure $\mu(S)$ on sets
$S=\bigtimes_{V\in\mathbf{V}}S_{V}$ where $S_{V}=\mathrm{Val}(V)$ for all
except finitely many $V$. Equivalently, assuming $S$ is nonempty, we have
$S=\pi^{-1}_{\mathbf{X}}\big{(}(i_{X})_{X\in\mathbf{X}}\big{)}$ for some
finite $\mathbf{X}\subset\mathbf{V}$ and values $i_{X}\in\mathrm{Val}(X)$ for
each $X\in\mathbf{X}$, where
$\pi_{\mathbf{X}}:\bigtimes_{V\in\mathbf{V}}\mathrm{Val}(V)\to\bigtimes_{X\in\mathbf{X}}\mathrm{Val}(X)$
is the projection map. We define:

$\displaystyle\mu\big{[}\pi^{-1}_{\mathbf{X}}\big{(}(i_{X})_{X\in\mathbf{X}}\big{)}\big{]}=\mathrm{sup}\Big{\\{}s\in[0,1]\cap\mathbb{Q}:\Gamma^{*}\vdash\mathsf{P}\Big{(}\bigwedge_{X\in\mathbf{X}}X=g_{X}(i_{X})\Big{)}\succsim\underline{s}\Big{\\}}.$
(11)

######  Lemma 7 (cf. Perović et al., 2008, Lemma 2).

$\mu$ extends uniquely to a positive probability measure. ∎

###### Proof.

From standard extension theorems, with normalization guaranteed by consistency
with $\mathsf{Unity}$ and positivity by consistency with $\mathsf{Pos}$. ∎

######  Lemma 8.

We have that $\mathfrak{M}^{*}\vDash\varphi$ iff $\varphi\in\Gamma^{*}$.

###### Proof.

The axiom $\mathsf{EqReplace}$ guarantees that our definition (11) in terms of
a single representative constant $g_{X}(i_{X})\in\mathcal{C}_{X}$ is
consistent in $\Gamma^{*}$. Otherwise, comparing to Perović et al., (2008,
Theorem 3), we have two features to address. First, $\mathsf{EqDist}$
guarantees the result for formulas that include primitive probabilities
$\mathsf{P}(\delta)$ where literals involving the same variable $V$ occur more
than once in $\delta$.

Second is the presence of sums here, for which it suffices to show that
$\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x_{i}}\mathsf{t}\succsim\underline{q}\in\Gamma^{*}$
iff
$q\leq[\\![\mbox{\em$\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x_{i}}\mathsf{t}$\/}]\\!]^{\mathfrak{M}^{*}}$, and
$\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x_{i}}\mathsf{t}\precsim\underline{q}\in\Gamma^{*}$
iff
$q\geq[\\![\mbox{\em$\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x_{i}}\mathsf{t}$\/}]\\!]^{\mathfrak{M}^{*}}$, for
any term $\mathsf{t}$ and $q\in\mathbb{Q}$. Suppose
$\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x_{i}}\mathsf{t}\succsim\underline{q}\in\Gamma^{*}$.
If $q>[\\![\mbox{\em$\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x_{i}}\mathsf{t}$\/}]\\!]^{\mathfrak{M}^{*}}$ then
there is some rational $\varepsilon>0$ such that

$\displaystyle[\\![\mbox{\em$\mathsf{t}$\/}]\\!]^{\mathfrak{M}^{*}}_{\iota[X,i\mapsto
1]}+\dots+[\\![\mbox{\em$\mathsf{t}$\/}]\\!]^{\mathfrak{M}^{*}}_{\iota[X,i\mapsto
n]}\leq q-\varepsilon$

for any $n\in\mathrm{Val}(X)$. By consistency with $\mathsf{SumUpper}$, this
means
$\underline{q-\varepsilon}\succsim\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x_{i}}\mathsf{t}\in\Gamma^{*}$, so
$\underline{q-\varepsilon}\succsim\underline{q}\in\Gamma^{*}$, a
contradiction. Conversely suppose
$q\leq[\\![\mbox{\em$\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x_{i}}\mathsf{t}$\/}]\\!]^{\mathfrak{M}^{*}}$. If
$\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x_{i}}\mathsf{t}\prec\underline{q}\in\Gamma^{*}$
then by consistency with $\mathsf{Conv}$ there is some $\varepsilon>0$ such
that $\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x_{i}}\mathsf{t}\prec\underline{q-\varepsilon}\in\Gamma^{*}$
and by $\mathsf{SumLower}$ we have that
$[\\![\mbox{\em$\mathsf{t}$\/}]\\!]^{\mathfrak{M}^{*}}_{\iota[X,i\mapsto
1]}+\dots+[\\![\mbox{\em$\mathsf{t}$\/}]\\!]^{\mathfrak{M}^{*}}_{\iota[X,i\mapsto
n]}<q-\varepsilon$ for any $n\in\mathrm{Val}(X)$. This implies
$[\\![\mbox{\em$\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x_{i}}\mathsf{t}$\/}]\\!]^{\mathfrak{M}^{*}}\leq
q-\varepsilon$, a contradiction.

Now suppose $\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x_{i}}\mathsf{t}\precsim\underline{q}\in\Gamma^{*}$.
If $q<[\\![\mbox{\em$\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x_{i}}\mathsf{t}$\/}]\\!]^{\mathfrak{M}^{*}}$ then
there is some $n\in\mathrm{Val}(X)$ such that
$q<[\\![\mbox{\em$\mathsf{t}$\/}]\\!]^{\mathfrak{M}^{*}}_{\iota[X,i\mapsto
1]}+\dots+[\\![\mbox{\em$\mathsf{t}$\/}]\\!]^{\mathfrak{M}^{*}}_{\iota[X,i\mapsto
n]}$, and by $\mathsf{SumLower}$, we have
$\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x_{i}}\mathsf{t}\succ\underline{q}\in\Gamma^{*}$,
a contradiction. Conversely if
$q\geq[\\![\mbox{\em$\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x_{i}}\mathsf{t}$\/}]\\!]^{\mathfrak{M}^{*}}$,
then
$q\geq[\\![\mbox{\em$\mathsf{t}$\/}]\\!]^{\mathfrak{M}^{*}}_{\iota[X,i\mapsto
1]}+\dots+[\\![\mbox{\em$\mathsf{t}$\/}]\\!]^{\mathfrak{M}^{*}}_{\iota[X,i\mapsto
n]}$ for any $n\in\mathrm{Val}(X)$, so that
$\underline{q}\succsim\mathop{\mathchoice{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}{\vbox{\hbox{\begin{picture}(0.9,1.0)
\roundcap\roundjoin\polyline(0.83,0.07)(0.08,0.07)(0.45,0.5)(0.08,0.93)(0.83,0.93)
\end{picture}}}}}\slimits@_{x_{i}}\mathsf{t}\in\Gamma^{*}$ by
$\mathsf{SumUpper}$. ∎

This completes the proof of Theorem 7, showing $\mathfrak{M}^{*}$ satisfies
$\Gamma^{*}\supset\Gamma$. Note that $\mathsf{Cond}$ has been used implicitly
in working with plain probabilities throughout rather than conditional
probabilities. ∎

##  5 Conclusion

Although the present contribution has settled some of the most basic questions
about probability logics with summation, many open questions remain. As a
first example, although we have been able to show strong completeness for
infinitary proof systems, questions of weak completeness may also be of
interest.

In that direction, consider a language $\mathcal{L}_{\star}$, which is just
like $\mathcal{L}_{\textnormal{causal}}$, except that we allow no constants at
all, and also disallow equalities between free variables. In other words, this
language has only (free and bound) variables occurring in atomic expressions
$V=v$; it is of interest since Ex. 2 and other uses of $do$-calculus fall
within this natural fragment. We noted in Theorem 2 that this language (or any
other language sufficient for encoding conditional independence statements
with unbounded variables ranges) will be undecidable. Meanwhile, the proof of
Theorem 4 can be readily adapted to show the set of satisfiable
$\mathcal{L}_{\star}$-expressions is recursively enumerable. It follows that
validity cannot also be recursively enumerable, which in turn implies the
following:

######  Corollary 1.

There is no weakly complete, recursive axiomatization of $\mathcal{L}_{\star}$
over models with unbounded finite variable ranges.

Whether any other settings we have investigated here can be given (finitary)
weak axiomatizations we leave as a worthy open question. Another natural
question about axiomatization concerns the full causal language. As we have
seen, the principles that encode reasoning about pure probability are already
rather complex. Causal reasoning—especially about recursive models—introduces
another source of compactness failure. So strong axiomatization would again
demand infinitary schemes. We leave this work also for a future occasion.

Several natural open questions also remain concerning complexity. For example,
while we know that the satisfiability problem for the general, “open universe”
setting is undecidable (Theorem 2), we do not know how undecidable it is,
e.g., when variable ranges can be infinite. A reasonable conjecture is that it
is complete for $\Sigma^{0}_{1}$, but this remains to be shown.

Finally, moving beyond the systems we have investigated here, natural
extensions suggest themselves for investigation. The continuous setting, with
integration operators replacing summation operators, would be of particular
interest. Languages for integration have been explored by model theorists
(see, e.g., Bagheri and Pourmahdian, 2009), though axiomatic questions appear
not to have received much attention. Marginalization (both through summation
and through integration) is also closely related to issues of _abstraction_ of
models, a topic that has been of particular interest in the recent causality
literature (see Bongers et al., 2021; Geiger et al., 2024 for connections
between marginalization and causal abstraction). A causal-probability logical
system capable of reasoning explicitly about abstraction would also be worth
investigating.

## References

  * Abadi and Halpern, (1994) Abadi, M. and Halpern, J. Y. (1994).  Decidability and expressiveness for first-order logics of probability.  Information and computation, 112(1):1–36.
  * Angrist et al., (1996) Angrist, J. D., Imbens, G. W., and Rubin, D. B. (1996).  Identification of causal effects using instrumental variables.  Journal of the American Statistical Association, 91(434):444–455.
  * Bagheri and Pourmahdian, (2009) Bagheri, S.-M. and Pourmahdian, M. (2009).  The logic of integration.  Archive for Mathematical Logic, 48:465–492.
  * Bareinboim et al., (2022) Bareinboim, E., Correa, J., Ibeling, D., and Icard, T. (2022).  On Pearl’s hierarchy and the foundations of causal inference.  In Geffner, H., Dechter, R., and Halpern, J. Y., editors, Probabilistic and Causal Inference: The Works of Judea Pearl, pages 509–556. ACM Books.
  * Bläser et al., (2024) Bläser, M., Dörfler, J., Liśkiewicz, M., and van der Zander, B. (2024).  The existential theory of the reals with summation operators.  In Manuscript.
  * Bongers et al., (2021) Bongers, S., Forré, P., Peters, J., and Mooij, J. M. (2021).  Foundations of structural causal models with cycles and latent variables.  The Annals of Statistics, 49(5):2885–2915.
  * Dörfler et al., (2024) Dörfler, J., van der Zander, B., Bläser, M., and Liskiewicz, M. (2024).  Probabilistic and causal satisfiability: the impact of marginalization.  arXiv preprint arXiv:2405.07373.
  * Erickson et al., (2022) Erickson, J., Van Der Hoog, I., and Miltzow, T. (2022).  Smoothing the gap between np and er.  SIAM Journal on Computing, (0):FOCS20–102.
  * Fagin et al., (1990) Fagin, R., Halpern, J. Y., and Megiddo, N. (1990).  A logic for reasoning about probabilities.  Information and Computation, 87(1-2):78–128.
  * Geiger et al., (2024) Geiger, A., Ibeling, D., Zur, A., Chaudhary, M., Chauhan, S., Huang, J., Arora, A., Wu, Z., D’Oosterlink, K., Goodman, N. D., Potts, C., and Icard, T. (2024).  Causal abstraction: A theoretical foundation for faithful interpretability.  Manuscript, Pr(AI)2r Group and Stanford University.
  * Ibeling and Icard, (2020) Ibeling, D. and Icard, T. (2020).  Probabilistic reasoning across the causal hierarchy.  In Proceedings of AAAI.
  * Ibeling and Icard, (2021) Ibeling, D. and Icard, T. (2021).  A topological perspective on causal inference.  Advances in Neural Information Processing Systems, 34:5608–5619.
  * Ibeling and Icard, (2023) Ibeling, D. and Icard, T. (2023).  Comparing causal frameworks: Potential outcomes, structural models, graphs, and abstractions.  In Advances in Neural Information Processing Systems 36 (NeurIPS 2023), pages 1–12.
  * Ibeling et al., (2023) Ibeling, D., Icard, T., Mierzewski, K., and Mossé, M. (2023).  Probing the quantitative–qualitative divide in probabilistic reasoning.  Annals of Pure and Applied Logic, page 103339.
  * Li, (2023) Li, C. T. (2023).  Undecidability of network coding, conditional information inequalities, and conditional independence implication.  IEEE Transactions on Information Theory, 69(6).
  * Mossé et al., (2024) Mossé, M., Ibeling, D., and Icard, T. (2024).  Is causal reasoning harder than probabilistic reasoning?  The Review of Symbolic Logic, 17(1):106–131.
  * Pearl, (1995) Pearl, J. (1995).  Causal diagrams for empirical research.  Biometrika, 82(4):669–710.
  * Pearl, (2009) Pearl, J. (2009).  Causality.  Cambridge University Press.
  * Perović et al., (2008) Perović, A., Ognjanović, Z., Rašković, M., and Marković, Z. (2008).  A probabilistic logic with polynomial weight formulas.  In International Symposium on Foundations of Information and Knowledge Systems, pages 239–252.
  * Schaefer and Štefankovič, (2023) Schaefer, M. and Štefankovič, D. (2023).  Beyond the existential theory of the reals.  Theory of Computing Systems, pages 1–32.
  * Shpitser and Pearl, (2006) Shpitser, I. and Pearl, J. (2006).  Identification of conditional interventional distributions.  In Proceedings of the Twenty-Second Conference on Uncertainty in Artificial Intelligence, UAI’06, page 437–444, Arlington, Virginia, USA. AUAI Press.
  * Shpitser and Pearl, (2008) Shpitser, I. and Pearl, J. (2008).  Complete identification methods for the causal hierarchy.  Journal of Machine Learning Research, 9:1941–1979.
  * Spirtes et al., (2000) Spirtes, P., Glymour, C. N., and Scheines, R. (2000).  Causation, Prediction, and Search.  The MIT Press.
  * Suppes and Zanotti, (1981) Suppes, P. and Zanotti, M. (1981).  When are probabilistic explanations possible?  Synthese, 48:191–199.
  * van der Zander et al., (2023) van der Zander, B., Bläser, M., and Liśkiewicz, M. (2023).  The hardness of reasoning about probabilities and causality.  In Elkind, E., editor, Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI-23, pages 5730–5738. International Joint Conferences on Artificial Intelligence Organization.  Main Track.