Provability Counterfactuals vs Three Axioms of Galles and Pearl

Summary: A translation of the provability counterfactual $\square(x\rightarrow y)$ into the language of (Galles and Pearl, 1998 [1]) satisfies the axioms of Compositionality and Effectiveness, but only satisfies the axiom of Reversibility under specific conditions $(\ref{eq:RProvabilityCondition})$, which we derive below.

(I proposed using the axioms of Galles and Pearl as a sanity check for logical counterfactuals at MIRI's May 2015 workshop on decision theory. This post is based on the subsequent discussion and my own follow-up work.)

This is the first of what will hopefully become a series of posts exploring logical counterfactuals. I'll be looking directly at properties of counterfactuals, and trying to close the gap between how they actually behave and how we want them to behave. My hope here is that formalizing what exactly goes wrong with our current logical counterfactuals will point towards a way of fixing them.

In contrast to logical counterfactuals, which we don't yet have a good model for, counterfactuals in Pearlean causality are well-defined and meet many criteria for our intuitive notions of how counterfactuals should behave (Galles and Pearl, 1998 [1]). Specifically, three axioms of counterfactuals proposed in that paper are supposed to be sufficient to get these nice properties. These axioms are potentially a useful baseline of comparison for any alternative counterfactual we might want to consider. Hence, in this post I will be investigating whether they hold for a particular way of doing logical counterfactuals.

The original context involves a system of equations assigning values to a set of endogenous variables $V_i$ given a set of exogenous variables $U_i$. We have for each endogenous variable $V_i$ a parent set $PA_{i}\subseteq U\cup (V\setminus \{V_{i}\})$, and an associated function $f_{i}(PA_{i})$ that computes a value for $V_i$ given the values of its parents. This collection defines a system of equations, which is assumed to have a unique solution for every possible assignment of exogenous variables.

In this setting, an action is represented by modifying some subset of equations $f_i$ into constant functions. Letting $X$ and $Y$ stand for subsets of endogenous variables, the notation $Y_{x}$ is shorthand for the functions defining the solutions for variables in $Y$ after setting the functions for each $X_i$  to the corresponding constant function $x_i$. Below, let $X,$ $Y,$ and $W$ stand for three disjoint sets of endogenous variables. The three axioms of causal counterfactuals are then defined as (leaving implicit that the specific functions implied by lower-case letters are actually functions of exogenous variables $u$):

$\begin{align}
\text{Compositionality: }&\ \ \ \ \left(W_{x}=w\right)\rightarrow\left(\left(Y_{x\wedge w}=y\right)\leftrightarrow\left(Y_{x}=y\right)\right)\label{eq:Compositionality}\\
\text{Effectiveness: }&\ \ \ \ \ X_{x}=x\label{eq:Effectiveness}\\
\text{Reversibility: }&\ \ \ \ \ \left(\left(Y_{x\wedge w}=y\right)\wedge\left(W_{x\wedge y}=w\right)\right)\rightarrow\left(Y_{x}=y\right).\label{eq:Reversibility}
\end{align}$

Provability counterfactuals

One working definition of counterfactuals we talked about at the workshop is based on what I will call provability of implication. Intuitively, if we can prove that $x\rightarrow y$, then it seems reasonable to say that $y$ is a counterfactual consequence of $x.$ We will adopt the language of GL[2][3], in which the symbol “$\square$” stands for “is provable” (for concreteness, we can assume that the underlying proof system is Peano Arithmetic (PA)).

We'll have to bend (1)–(3) a bit to port them into a logical setting. In particular, we will replace the equality statements with arbitrary sentences of logic. In the following, let $x$, $y,$ and $w$ stand for arbitrary sentences in PA. A straightforward and very general translation of the Pearlean counterfactual $Y_{x}=y$ is then the GL statement $$\square \left(x\rightarrow y\right).$$ There might well be better ways to craft the analogy (something I plan on looking into!) Notably, we have done away with the connection between “sets of variables” and their values. This is obviously more general, and in line with the intuition in the previous paragraph, but is a potential weak point in the analogy.

Translating each of the axioms (1)–(3) into the language of provability counterfactuals, we show below that Compositionality and Effectiveness always hold in this interpretation, but that Reversibility requires an additional condition.

Compositionality

Translating the components of (1) into this language, we get
$$\begin{align}
W_{x}=w&:\square\left(x\rightarrow w\right)\\
Y_{x\wedge w}=y&:\square\left(\left(x\wedge w\right)\rightarrow y\right)\\
Y_{x}=y&:\square\left(x\rightarrow y\right).
\end{align}$$
The full translation of (1) is then given by
$$\begin{equation}\label{eq:CompositionTarget}\left(\square\left( x\rightarrow w\right)\right)\rightarrow \left(\square\left(\left(x\wedge w\right)\rightarrow y\right)\leftrightarrow\square\left(x\rightarrow y\right)\right).\end{equation}$$ This statement is a theorem of GL. To see this, we first note that the equivalent statement with all boxes removed,
$$\begin{equation} \label{eq:CompositionUnboxed} \left(x\rightarrow w\right)\rightarrow\left(\left(\left(x\wedge w\right)\rightarrow y\right)\leftrightarrow\left(x\rightarrow y\right)\right) \end{equation}$$ is a tautology. (The proof is straightforward, or it can be verified by writing out the truth table.) Since all logical tautologies are provable, GL allows us to add a box in front of equation ($\ref{eq:CompositionUnboxed}$), which, with repeated application of GL's distribution rule, yields
$$\begin{align*}
1.\ &\square \left( \left(x\rightarrow w\right)\rightarrow\left(\left(\left(x\wedge w\right)\rightarrow y\right)\leftrightarrow\left(x\rightarrow y\right)\right)\right)\\
2.\ &\left(\square\left( x\rightarrow w\right)\right)\rightarrow \square\left(\left(\left(x\wedge w\right)\rightarrow y\right)\leftrightarrow\left(x\rightarrow y\right)\right)\\
3.\ &\left(\square\left( x\rightarrow w\right)\right)\rightarrow \left(\square\left(\left(x\wedge w\right)\rightarrow y\right)\leftrightarrow\square\left(x\rightarrow y\right)\right).
\end{align*}$$ Since this matches equation ($\ref{eq:CompositionTarget}$), we have proven that (1) holds in this model of counterfactuals.

Effectiveness

Translating (2) into our logical counterfactual model yields the statement $$\square\left(x\rightarrow x\right),$$ which is obviously a theorem of GL since $x\rightarrow x$ is a tautology. So (2) clearly holds.

Reversibility

The components of (3) translate as $$\begin{align}Y_{x\wedge w}=y&:\square\left(\left(x\wedge w\right)\rightarrow y\right)\\W_{x\wedge y}=w&:\square\left(\left(x\wedge y\right)\rightarrow w\right)\\Y_{x}=y&:\square\left(x\rightarrow y\right).\end{align}$$

This gives for the full translation of (3)
$$\begin{equation}\label{eq:RProvability}\left(\square\left(\left(x\wedge w\right)\rightarrow y\right)\wedge\square\left(\left(x\wedge y\right)\rightarrow w\right)\right)\rightarrow\square\left(x\rightarrow y\right).\end{equation}$$
Note that the corresponding sentence with boxes removed, $$\begin{equation}\label{ReversibilityBoxless}\left(\left(\left(x\wedge w\right)\rightarrow y\right)\right)\wedge\left(\left(\left(x\wedge y\right)\rightarrow w\right)\right)\rightarrow\left(\left(x\rightarrow y\right)\right)\end{equation}$$ is valid iff $$\neg\left(x\wedge\neg y\wedge \neg w \right),$$which can be seen in the truth table for the expression: $$
\begin{array}{|c|c|c|c|c|c|c|}
\hline
x & y & w & (x\wedge w)\rightarrow y & (x\wedge y)\rightarrow w & x\rightarrow y & \textbf{(\ref{ReversibilityBoxless})}\\
\hline
\hline
0 & 0 & 0 & 1 & 1 & 1 & \textbf{1}\\
\hline
0 & 0 & 1 & 1 & 1 & 1 & \textbf{1}\\
\hline
0 & 1 & 0 & 1 & 1 & 1 & \textbf{1}\\
\hline
0 & 1 & 1 & 1 & 1 & 1 & \textbf{1}\\
\hline
\color{red}{1} & \color{red}{0} & \color{red}{0} & \color{red}{1} & \color{red}{1} & \color{red}{0} & \color{red}{\textbf{0}}\\
\hline
1 & 0 & 1 & 0 & 1 & 0 & \textbf{1}\\
\hline
1 & 1 & 0 & 1 & 0 & 1 & \textbf{1}\\
\hline
1 & 1 & 1 & 1 & 1 & 1 & \textbf{1}\\
\hline

\end{array}
$$
Rewriting $\neg\left(x\wedge\neg y\wedge \neg w \right)$ as $\left(\left(x\rightarrow y \right)\vee \left(x\rightarrow w \right)\right),$ we then have that $$\begin{align*}1.\  & \begin{gathered}\square\left(\left(\left(\left(\left(x\wedge w\right)\rightarrow y\right)\wedge\left(\left(x\wedge y\right)\rightarrow w\right)\right)\rightarrow\left(x\rightarrow y\right)\right)\right.\\
\left.\leftrightarrow\left(\left(x\rightarrow y\right)\vee\left(x\rightarrow w\right)\right)\right)
\end{gathered}
\\
2.\  & \begin{gathered}\square\left(\left(\left(\left(x\wedge w\right)\rightarrow y\right)\wedge\left(\left(x\wedge y\right)\rightarrow w\right)\right)\rightarrow\left(x\rightarrow y\right)\right)\\
\leftrightarrow\square\left(\left(x\rightarrow y\right)\vee\left(x\rightarrow w\right)\right)
\end{gathered}
\\
3.\  & \begin{gathered}\left(\square\left(\left(\left(x\wedge w\right)\rightarrow y\right)\wedge\left(\left(x\wedge y\right)\rightarrow w\right)\right)\rightarrow\square\left(x\rightarrow y\right)\right)\\
\leftrightarrow\square\left(\left(x\rightarrow y\right)\vee\left(x\rightarrow w\right)\right)
\end{gathered}
\\
4.\  & \begin{gathered}\left(\left(\square\left(\left(x\wedge w\right)\rightarrow y\right)\wedge\square\left(\left(x\wedge y\right)\rightarrow w\right)\right)\rightarrow\square\left(x\rightarrow y\right)\right)\\
\leftrightarrow\square\left(\left(x\rightarrow y\right)\vee\left(x\rightarrow w\right)\right)
\end{gathered}
\end{align*}
$$ (To get from step 1 to 3 we repeatedly applied GL's distribution rule. To get to step 4 we used Theorem 3 of Chapter 1 of Boolos, which says that for all sentences A and B, $\square\left(A\wedge B\right)\leftrightarrow\left(\square A\wedge \square B\right).$)

Note that the left hand side of the biconditional in step 4 above is exactly equivalent to equation ($\ref{eq:RProvability}$), which implies that the Reversibility Axiom holds iff $$\begin{equation}\label{eq:RProvabilityCondition}\square\left(\left(x\rightarrow y\right)\vee\left(x\rightarrow w\right)\right).\end{equation}$$ I claimed at the workshop that Reversibility simply didn't hold, but doing the modal logic more carefully yielded this condition, which is probably a lot more interesting! It seems that in this setting, reversibility is a local property that may or may not hold for each triple of sentences $x,y,w.$

Further questions

We derived an additional dependence among sentences that must hold to recover the Reversibility Axiom, but what does it mean? Is this even a property we would want a logical counterfactual to have? Is there a better way to map modal logic to Pearlean counterfactuals than the one presented here? What other properties of counterfactuals can we use as sanity checks? (I have a few ideas on these last points that I aim to explore in subsequent posts).

References

---

1. Galles, D., & Pearl, J. (1998). An Axiomatic Characterization of Causal Counterfactuals. Foundations of Science, 3(1), 151–182.^↩
2. Boolos, G. (1995). The logic of provability. Cambridge university press.^↩
3. Verbrugge, R. (2010). Provability Logic. http://plato.stanford.edu/entries/logic-provability/ ↩