Axiomatizations of causal reasoning under indeterministic causal laws

Fausto Barbero; Fausto Barbero

doi:10.48130/ker-0026-0005

We investigate the generalization of causal models to the case of indeterministic causal laws that was suggested in Halpern (2000). We give an overview of what differences in modeling are enforced by this more general perspective, and propose an implementation of generalized models in the style of the causal team semantics of Barbero & Sandu (2021). In these models, the laws are not represented by functions (as in the deterministic case), but more generally by relations. We point out significant differences in the indeterministic vs. the deterministic case, both for what concerns the axiomatization of counterfactuals and the definability of causal notions in terms of them. We notice, for instance, that the notions of parenthood and direct cause, differently from the deterministic case, come apart.We provide two main strongly complete axiomatizations, one for the class of indeterministic causal models and one for their team generalizations, which can also represent uncertainty about the state of the system. Then, we also identify axioms that allow specializing the axiomatizations to a number of significant subclasses, characterized by properties such as acyclicity, totality and determinism of the causal laws.We also see that a minor change in the notion of signature of the models has a dramatic impact; in particular, it makes so that the deterministic subclass of models become undefinable in the usual Halpern-style counterfactual language. We see that the definability of determinism can be recovered either by a restriction of the class of models, by allowing right-nested counterfactuals, or by introducing an operator for information update.

HTML

1. Introduction

When the existence of causal laws is considered at all, the discussion of causality in the philosophy of science tends to focus on deterministic causal mechanisms, which uniquely determine an effect given full knowledge of the causes. The restriction to deterministic laws is, in some cases, a deliberate choice to avoid technical complications (see, e.g., Paul et al.^[1], section 4.3), as many important and sometimes puzzling aspects of causation already emerge at this level. However, often, the laws considered in applied sciences are not of this kind. A physical law may allow us to predict, for example, that

A cannonball shot at a certain angle will fall within a certain range.

In contrast to more idealized laws of mechanics, this kind of law tells us that, even without taking into account some factor that is not mentioned by the law (such as the direction or intensity of the wind), we can predict that the effect will (quite literally) fall within a certain range of possible values. These kinds of causal dependencies are discussed at length, e.g., in Bohm's book Causality and chance in modern physics^[2], chapter I.7, under the name of one-to-many causal relationships.

Note that in the cannonball example, the law is indeterministic due to the impossibility of taking into account all factors, i.e., it accounts for epistemic limitations; the indeterministic law might, e.g., just be a rough approximation of an underlying deterministic law. On the other hand, many physicists would think that the following statement expresses an irreducibly indeterministic law about the behaviour of a particle:

If an atom of silver passes through a Stern-Gerlach apparatus, it will be detected in either of two specific areas of the screen.

In other words, a physical law may tell us that the specifics of the outcome of a certain experiment are unpredictable in principle, even if we had a complete knowledge of the initial conditions of a physical system. In this case, an indeterministic law tells us that the particle will be detected somewhere within two areas, but nothing more. Indeterministic laws do not just arise within scientific theories, but also justify everyday statements such as

If I toss the coin, it will land on heads or tails.

Far from being a platitude, such a statement implicitly assumes an indeterministic causal law, which allows two values for the future state of the coin, while excluding other alternatives (such as "the coin staying in my pocket" or "the coin breaking into pieces"). Notice also that all these examples do not require probabilities for their formulation and justification. We might not know what probabilistic distributions are involved, or, in some context, it might even be mathematically impossible to associate a probability distribution to a given phenomenon (see e.g., Wysocki's work^[3] for some examples of this kind). Thus, probabilistic laws are only a special case of indeterministic laws.

In the last decades, causal reasoning has been mathematically formalized in the fields of statistics and computer science known as causal discovery^[4] and causal inference^[5], which have found applications, e.g., in machine learning^[6,7], epidemiology^[8], econometrics^[9], and social sciences^[10]. Do indeterministic laws feature in these approaches? There are two main types of models considered in this context. The first are the Bayesian networks; these consist of probabilistic distributions paired with graphs, and are intrinsically indeterministic models; but laws or mechanisms are not specified in any way by such models. Instead, structural equation models (or causal models), use systems of equations to encode the causal laws that link together the relevant variables of the scenario under examination. The equations take the form:

$ Y:=f(X_1,\dots,X_n) $

where the term $ f(X_1, \dots, X_n) $ stands for a function of the variables $ X_1, \dots, X_n $. The equations, together with some information about the state of the variables, allow one to formulate and often answer queries about the deterministic and probabilistic behaviour of the variables. A significant example of such a query is establishing the truth or falsity of an interventionist counterfactual^[11]:

If variables $Z_1, \dots Z_m $ were set to values $z_1, \dots z_m $, then condition $\psi $ would hold.

These kinds of expressions can be studied with the methods of logic. The classic work of Halpern^[12,13] provided a wealth of complete deduction systems for classes of causal models, and the idea has since been extended in various directions^[14–24]. Now, the very fact that causal laws are represented by functions amounts to a restriction to deterministic laws. The natural way to extend these kinds of models to the indeterministic case is to replace these functional constraints with relational constraints. If we write $ R_Y $ for the causal law describing the behaviour of variable $ Y $, we shall interpret the statement that $ (x_1, \dots, x_n, y)\in R_Y $ as expressing the fact that, if variables $ X_1, \dots, X_n $ are set to values $ x_1, \dots, x_n $, then $ Y $ might take the value $ y $ (but it might also take any other value $ y' $ such that $ (x_1, \dots, x_n, y')\in R_Y $). Equivalently, we can recover the equational form by encoding the causal law as a multivalued function $ \mathcal{F}_Y $ that associates to each tuple of values for $ X_1, \dots X_n $ a set of possible values for $ Y $.

The possibility of such an extension is hinted at by Halpern in the conclusions of his paper on the axiomatization of interventionist counterfactuals:

(...) a more general approach to modeling causality would allow there to be more than one value of $ X $ once we have set all other variables. This would be appropriate if we model things at a somewhat coarser level of granularity, where the values of all the variables other than $ X $ do not suffice to completely determine the value of $ X $. I believe the results of this paper can be extended in a straightforward way to deal with this generalization, although I have not checked the details^[12].

Perhaps stating that this generalization is "straightforward" discouraged researchers from pursuing this direction: or was it the discovery that, after all, the details are not so straightforward? To the best of our knowledge, the idea has been taken up again only in 2021, when Peters and Halpern^[17,25] introduced the more complex framework of generalized structural equation models (GSEMs). In that context, causal laws are not mentioned at all, but it is evident that indeterministic causal laws can be modeled in a GSEM as a special case. More recently, a simpler framework, closer to Halpern's original idea for extending causal models, was considered by Wysocki^[3], who provided a cursory examination of the differences between deterministic and indeterministic counterfactuals^①. The purpose of the present paper is to sharpen the understanding of the logic of interventionist counterfactuals in the indeterministic (but not probabilistic) context and ultimately provide complete axiomatizations for significant classes of indeterministic causal models. The models we use (relational causal teams) are a generalization of the causal teams proposed in Barbero & Sandu^[28] and are somewhat more general than those of Wysocki (one key difference being that our models—like structural equation models—do not necessarily obey the Markov condition^②). In section 2, we will describe, in general terms, some key differences between deterministic and indeterministic frameworks, and how they will affect our modeling choices. We then use the insights just gained to provide (section 3.1) a precise definition of indeterministic models. We then introduce (section 3.2) a language $ \mathcal{H} $ similar to those considered in Halpern's work^[12], and its extension $ \mathcal{H}^+ $ that also allows right-nesting of counterfactuals. In section 4, we provide a strongly complete axiomatization of language $ \mathcal{H} $ over the class of all singleton models (of a given signature); this allows us to make a direct comparison with the usual case of deterministic causal models. Later, section 6 provides an axiomatization of $ \mathcal{H}^+ $ over the class of all models; section 5 lays down some necessary technical tools for the proof, by clarifying which models are indistinguishable using $ \mathcal{H} $ or $ \mathcal{H}^+ $, and explaining to what extent the causal laws can be described in these languages. In section 7, we analyze notions such as parenthood, direct cause, and (non-) dummy arguments, we see that (differently from the deterministic case) they come apart, and investigate their mutual relationships. Some of these insights help us produce complete axiomatizations for models where cyclic causal relationships are forbidden (section 8); more precisely, we axiomatize two classes of models that we call, respectively, strictly recursive and visibly recursive. In section 9, we axiomatize two other interesting subclasses, that of deterministic models (those in which the causal laws associate at most one output to each input value for the parents) and that of total models (where the causal laws associate at least one possible effect to each input value for the parents). We also see that the recursive class of models, which forbids cycles of direct causation, can be axiomatized relatively to the class of total models. Combining all these results, we obtain an alternative axiomatization for the (usual, deterministic) recursive causal models. In section 10, we consider a slight variation of the framework, which adopts a notion of signature closer to that which is often used in the philosophical literature. Such simplified signatures only fix a variable domain and the allowed value ranges for the variables; they do not decide which variables are going to be associated with a causal law. While the use of such signatures is tempting, as it can potentially lead to more general completeness results, we see (section 10.1) that, in the indeterministic context, it leads to a barrage of undefinability results (which, among other things, prevent us from extending the axiomatization strategies used in the rest of the paper). Some of these results—e.g., the undefinability of direct cause—extend to full signatures. Others, like the undefinability of the deterministic class of models, affect $ \mathcal{H} $ only if simplified signatures are adopted. We show three different strategies for recovering the definability of determinism while keeping the simplified signatures: First, we see it is again definable if we restrict attention to singleton models (section 10.2). Second, we see the definability is regained if one allows for right-nested counterfactuals (section 10.3). Third, the same is achieved by extending $ \mathcal{H} $ with a second conditional operator which describes learning or information updates (section 10.4); we analyze the potential axioms and rules for this language extension. Lastly, in section 11, we compare our approach and results to the recent literature on indeterministic counterfactuals.

The reader who is interested in the conceptual aspects of indeterministic causation and counterfactuals but not in the technicalities of proving the completeness results can pick the following shorter route: reading sections 2, 3, the first two pages of 4, sections 7, 8, 10, and 11.

2. Differences with the deterministic case

4. An axiomatization for singleton models

5. Definability of law components

Toward the formulation of a complete proof system for $ \mathcal{H}^+ $ over the general class of models, we need some additional concepts and terminology, which we introduce here.

Note that any fixed signature $ \sigma $ allows finitely many possible law components $ \mathcal{F} $; we will denote as $ \mathbb{F}_\sigma $ the set of these objects. The subtleties of formalization described in section 2 suggest that it might be difficult to talk about the law components within language $ \mathcal{H^+ }$; in particular, it might be difficult to tell apart law components that only disagree about the parent sets of some variables. We introduce a notion of equivalence of law components to take this obstacle into account. When discussing several function components, say $ \mathcal{F}, \mathcal{G} $, we will differentiate between their parent sets by using indexed notation such as $ PA_V^ \mathcal{F} $, resp. $ PA_V^ \mathcal{G} $.

Definition 5.1. Let $ \mathcal{F}, \mathcal{G} $ be two law components of signature $ \sigma = (\mathcal E, \mathcal I, \mathrm{Ran}) $. We say that $ \mathcal{F} $ and $ \mathcal{G} $ are equivalent, $ \mathcal{F} \equiv \mathcal{G} $ if, for all $ V \in \mathcal I $ and all $ pa \in \mathrm{Ran}(PA^ \mathcal{F}_V \cup PA^ \mathcal{G}_V) $, $ \mathcal{F}_V(pa_{\upharpoonright PA^ \mathcal{F}_V}) = \mathcal{G}_V(pa_{\upharpoonright PA^ \mathcal{G}_V}) $.

Two models $ S=(S^-, \mathcal{F}) $ and $ T = (T^-, \mathcal{G}) $ of signature $ \sigma $ are equivalent, $ S\equiv T $, if $ S^- = T^- $ and $ \mathcal{F} \equiv \mathcal{G} $.

The next theorem shows that this notion of equivalence does indeed characterize all that can be said about law components in language $ \mathcal{H}^+ $ (as well as in $ \mathcal{H} $).

Theorem 5.1. Let $ S=(S^-, \mathcal{F}), T =(T^-, \mathcal{G}) $ be two models of signature $ \sigma = (\mathcal E, \mathcal I, \mathrm{Ran}) $. Then, $ S \equiv T $ iff for all $ \varphi\in \mathcal{H}^+_\sigma $, $ S\models \varphi \iff T \models \varphi $ iff for all $ \varphi\in \mathcal{H}_\sigma $, $ S\models \varphi \iff T \models \varphi $.

Proof. 1) First, we prove that $ S \equiv T $ implies that $ S $ and $ T $ agree over all $ \mathcal{H}^+_\sigma $ formulas. We proceed by induction on $ \varphi $; we prove the statement simultaneously for all pairs of equivalent teams of arbitrary signatures. The atomic case ($ \varphi $ is $ Y=y $) immediately follows from the fact that $ S $ and $ T $ have the same team component. The cases for $ \varphi $ of the forms $ {\sim}\psi $ and $ \psi {\& }\chi $ are straightforward.

If $ S\models \varphi = [\mathbf{X} = \mathbf{x}]\psi $, then, for all $ s\in S_{\mathbf{X} = \mathbf{x}}^- $, $ (\{s\}, \mathcal{F}_{\mathbf{X} = \mathbf{x}})\models \psi $. Since $ \mathcal{F}\equiv \mathcal{G} $, we have $ \mathcal{F}_V(pa_{\upharpoonright PA^ \mathcal{F}_V}) = \mathcal{G}_V(pa_{\upharpoonright PA^ \mathcal{G}_V}) $ for all $ V\in \mathcal I\setminus \mathbf{X} $. Since $ V\in \mathcal I\setminus \mathbf{X} $ is the set of internal variables of $ \mathcal{F}_{\mathbf{X} = \mathbf{x}} $ and $ \mathcal{G}_{\mathbf{X} = \mathbf{x}} $, and for all such variables $ (\mathcal{F}_{\mathbf{X} = \mathbf{x}})_V = \mathcal{F}_V $ and $ (\mathcal{G}_{\mathbf{X} = \mathbf{x}})_V = \mathcal{G}_V $, then, $ \mathcal{F}_{\mathbf{X} = \mathbf{x}} \equiv \mathcal{G}_{\mathbf{X} = \mathbf{x}} $. Thus, for each $ s\in S_{\mathbf{X} = \mathbf{x}}^- $, $ (\{s\}, \mathcal{F}_{\mathbf{X} = \mathbf{x}}) \equiv (\{s\}, \mathcal{G}_{\mathbf{X} = \mathbf{x}}) $. By the inductive hypothesis, then, for all $ s\in (S_{\mathbf{X} = \mathbf{x}})^- $ we have $ (\{s\}, \mathcal{G}_{\mathbf{X} = \mathbf{x}})\models \psi $. If we manage to prove that $ S_{\mathbf{X} = \mathbf{x}}^- = T_{\mathbf{X} = \mathbf{x}}^- $, then, we are done.

It suffices to show that $ S_{\mathbf{X} = \mathbf{x}}^- \subseteq T_{\mathbf{X} = \mathbf{x}}^- $; the converse proof is symmetric. Suppose $ s\in S_{\mathbf{X} = \mathbf{x}}^- $; by definition of intervention, this means that $ s(\mathbf{N}_{\mathbf{X}})\in S^-(\mathbf{N}_{\mathbf{X}}), s(\mathbf{X}) = \mathbf{x} $ and $ s $ satisfies the constraints given by $ \mathcal{F}_{\mathbf{X} = \mathbf{x}} $. The latter means that, for all $ V\in \mathcal{I}\setminus \mathbf{X} $, $ (s(PA^ \mathcal{F}_V), s(V))\in \mathcal{F}_V $. In other words, $ s(V) \in \mathcal{F}_V(s(PA^ \mathcal{F}_V)) = \mathcal{G}_V(s(PA_V^ \mathcal{G})) $, where the equality is given by $ \mathcal{F} \equiv \mathcal{G} $. Thus $ (s(PA^ \mathcal{G}_V), s(V))\in \mathcal{G}_V $ for all $ V\in \mathcal{I}\setminus \mathbf{X} $; together with $ s(\mathbf{N}_{\mathbf{X}})\in S^-(\mathbf{N}_{\mathbf{X}}) = T^-(\mathbf{N}_{\mathbf{X}}) $ and $ s(\mathbf{X}) = \mathbf{x} $, this yields $ s\in T_{\mathbf{X} = \mathbf{x}}^- $.

2) We now deduce $ S \equiv T $ from the assumption that $ S $ and $ T $ agree on the truth values of $ \mathcal{H}_\sigma $ formulas. Since $ S $ and $ T $ satisfy the same formulas of the form $ \Diamond \mathbf{W} = \mathbf{w} $, we immediately obtain $ S^- = T^- $. Now let $ pa \in \mathrm{Ran}(PA^ \mathcal{F}_Y \cup PA^ \mathcal{G}_Y) $. Suppose $ y\in \mathcal{F}_Y(pa_{\upharpoonright PA^ \mathcal{F}_Y}) $. By definition of intervention, for any $ \mathbf{w}\in \mathrm{Ran}(\mathbf{W}_Y) $ with $ \mathbf{w}_{\upharpoonright PA^ \mathcal{F}_Y \cup PA^ \mathcal{G}_Y} = pa $ we have $ S\models \langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y $. But then, by the assumption, $ T\models \langle \mathbf{W}_Y = \mathbf{w}\rangle Y= y $. Thus, by the same reasoning, $ y\in \mathcal{G}_Y(pa_{\upharpoonright PA^ \mathcal{G}_Y}) $. The converse is analogous. Thus, we conclude that $ \mathcal{F} \equiv \mathcal{G} $. □

We can improve on this result by showing that each equivalence class of law components can be characterized by a single $ \mathcal{H} $ formula. For each signature $ \sigma = (\mathcal E, \mathcal I, \mathrm{Ran}) $ and each $ \mathcal{F} \in \mathbb{F}_\sigma $, we define a formula

$ \Phi^ \mathcal{F} := \bigwedge\limits_{\substack{Y\in\mathcal I \\ \mathbf{w} \in \mathrm{Ran}(\mathbf{W}_Y) \\y\in \mathcal{F}_Y(\mathbf{w}_{\upharpoonright PA_Y^ \mathcal{F}})}} \langle \mathbf{W}_Y=\mathbf{w}\rangle Y=y \ {\&}\ \bigwedge\limits_{\substack{Y\in\mathcal I \\ \mathbf{w} \in \mathrm{Ran}(\mathbf{W}_Y) \\ y\notin \mathcal{F}_Y(\mathbf{w}_{\upharpoonright PA_Y^ \mathcal{F}})}} {\sim} \langle \mathbf{W}_Y=\mathbf{w}\rangle Y=y. $

The $ \Phi^ \mathcal{F} $ formulas will be crucial in the formulation of two axioms; the next result shows that they indeed characterize law components up to equivalence.

Theorem 5.2. Let $ T= (T^-, \mathcal{G}) $ be a model. Then, $ T\models \Phi^ \mathcal{F} $ $ \iff $ $ \mathcal{G}\equiv \mathcal{F} $.

Proof. $ \Rightarrow $) Suppose $ T\models \Phi^ \mathcal{F} $. Let $ Y\in \mathcal I $, $ pa\in \mathrm{Ran}(PA_Y^ \mathcal{F} \cup PA_Y^ \mathcal{G}) $. Pick a $ \mathbf{w} \in \mathrm{Ran}(\mathbf{W}_Y) $ such that $ \mathbf{w}_{\upharpoonright PA_Y^ \mathcal{F} \cup PA_Y^ \mathcal{G}} = pa $.

Suppose first that $ y\in \mathcal{F}_Y(pa_{\upharpoonright PA_Y^ \mathcal{F}}) $. Thus, we may also write $ y\in \mathcal{F}_Y(\mathbf{w}_{\upharpoonright PA_Y^ \mathcal{F}}) $. Since $ T\models \Phi^ \mathcal{F} $, then, in particular $ T\models \langle \mathbf{W}_Y=\mathbf{w}\rangle Y=y $. By definition of intervention, then, $ y\in \mathcal{G}(\mathbf{w}_{\upharpoonright PA_Y^ \mathcal{G}}) = \mathcal{G}(pa_{\upharpoonright PA_Y^ \mathcal{G}}) $, as needed.

Vice versa, suppose $ y\in \mathcal{G}(pa_{\upharpoonright PA_Y^ \mathcal{G}}) $. Then, by definition of intervention, $ T\models \langle \mathbf{W}_Y=\mathbf{w}\rangle Y=y $. Suppose for the sake of contradiction that $ y\notin \mathcal{F}_Y(pa_{\upharpoonright PA_Y^ \mathcal{F}}) $. Then, $ y\notin \mathcal{F}_Y(\mathbf{w}_{\upharpoonright PA_Y^ \mathcal{F}}) $. So, since $ T\models \Phi^ \mathcal{F} $, we obtain that $ T\models {\sim} \langle \mathbf{W}_Y=\mathbf{w}\rangle Y=y $, contradicting our earlier statement.

Thus, $ \mathcal{G} \equiv \mathcal{F} $.

$ \Leftarrow $) Suppose $ \mathcal{G} \equiv \mathcal{F} $. Let $ Y\in \mathcal I $, $ pa\in \mathrm{Ran}(PA_Y^ \mathcal{F} \cup PA_Y^ \mathcal{G}) $. Pick a $ \mathbf{w} \in \mathrm{Ran}(\mathbf{W}_Y) $ such that $ \mathbf{w}_{\upharpoonright PA_Y^ \mathcal{F} \cup PA_Y^ \mathcal{G}} = pa $.

Assume first that $ y\in \mathcal{F}_Y(\mathbf{w}_{\upharpoonright PA_Y^ \mathcal{F}}) $. Since $ \mathcal{G} \equiv \mathcal{F} $, we have $ y\in \mathcal{G}_Y(\mathbf{w}_{\upharpoonright PA_Y^ \mathcal{G}}) $. Thus, by definition of intervention, $ T\models \langle \mathbf{W}_Y=\mathbf{w}\rangle Y=y $, as needed.

If we assume instead that $ y\notin \mathcal{F}_Y(\mathbf{w}_{\upharpoonright PA_Y^ \mathcal{F}}) $, since $ \mathcal{G} \equiv \mathcal{F} $ we obtain $ y\notin \mathcal{G}_Y(\mathbf{w}_{\upharpoonright PA_Y^ \mathcal{G}}) $. By definition of intervention, then, $ T\not\models \langle \mathbf{W}_Y=\mathbf{w}\rangle Y= y $, and thus $ T\models {\sim}\langle \mathbf{W}_Y=\mathbf{w}\rangle Y=y $. □

6. A general axiomatization

In the following, we prove the soundness and completeness of the following system $ \textsf{B}_\sigma $ for language $ \mathcal{H}^+ $ over the class of all models (again, $ \textsf{B}_\sigma $ will often just denote the set of axioms of this system).

$ \quad \text{Rule MP}. {\dfrac{\psi \quad \psi \rightarrow \chi}{\chi}} \quad \text{Rule NEC}. \dfrac{\vdash\psi}{\vdash[\mathbf{X} = \mathbf{x}]\psi}$

J0. $ \mathcal{H}^+_\sigma $ instances of a classical tautologies in $ {\sim}, {\& } $.

I1. $ [\mathbf{X} = \mathbf{x}] Y=y \rightarrow [\mathbf{X} = \mathbf{x}] Y \neq y' $ (when $ y\neq y' $) [Uniqueness]

I2. $ [\mathbf{X} = \mathbf{x}] \bigsqcup_{y\in \mathrm{Ran}(Y)} Y=y $ [Definiteness]

I3. $ \langle\mathbf{X} = \mathbf{x}\rangle (Z = z \ {\&} \ \mathbf{Y} = \mathbf{y}) \rightarrow \langle\mathbf{X} = \mathbf{x}, Z =z \rangle \mathbf{Y} = \mathbf{y} $ [Weak composition]

I4. $ [\mathbf{X} = \mathbf{x}, Y=y] Y=y $ [Effectiveness]

I5. $ ([\mathbf{X} = \mathbf{x}]\psi \ {\&}\ [\mathbf{X} = \mathbf{x}](\psi\rightarrow \chi)) \rightarrow [\mathbf{X} = \mathbf{x}]\chi $ [K-axiom]

J6. $ \mathbf{W} = \mathbf{w} \rightarrow $ I6. [Reversibility for small teams]

I7. $ \mathbf{Y} = \mathbf{y} \leftrightarrow \Box \mathbf{Y} = \mathbf{y} $. [Flatness]

I8. $ \langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y \leftrightarrow \Diamond Y=y $ (if $ Y\in \mathcal E $) [External variables]

I9. $ \langle \mathbf{W} = \mathbf{w}\rangle\top $ [Full intervention]

J10. $ \langle \mathbf{X} = \mathbf{x} \rangle \langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y \leftrightarrow \langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y $ (if $ Y\in \mathcal I $ and $ Y\notin \mathbf{X} $) [Diamond screen-off]

J11. $ [\mathbf{X} = \mathbf{x}]\langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y \leftrightarrow \langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y $ (if $ Y\in \mathcal I $ and $ Y\notin \mathbf{X} $) [Box screen-off]

J12. $ [\mathbf{X} = \mathbf{x}]\Diamond\psi \leftrightarrow [\mathbf{X} = \mathbf{x}]\psi $ [Conditional diamond]

J13. $ \langle\mathbf{X} = \mathbf{x} \rangle\Diamond \psi \leftrightarrow \langle\mathbf{X} = \mathbf{x} \rangle\psi $ [Mighty diamond]

J14. $ \Diamond \langle\mathbf{X} = \mathbf{x} \rangle\psi \leftrightarrow \langle\mathbf{X} = \mathbf{x} \rangle\psi $ [Double diamond]

J15. $ \langle\mathbf{X} = \mathbf{x} \rangle \psi \rightarrow \langle\mathbf{X} = \mathbf{x} \rangle(\psi {\& } \Diamond \top) $ [Persistency of diamond]

J16. $ \bigsqcup_{ \mathcal{F}\in \mathbb{F}_\sigma} \Phi^ \mathcal{F} $ [Certainty of laws]

J17. $ \Phi^ \mathcal{F} \rightarrow ([\mathbf{X} = \mathbf{x}]\psi \leftrightarrow [\mathbf{X} = \mathbf{x}]\bigsqcup_{\substack{t \text{ such that} \\ (\{t\}, \mathcal{F}_{\mathbf{X} = \mathbf{x}})\models \psi}} \mathbf{W}=t(\mathbf{W})) $ [Modal collapse]

As in system $ \textsf{A} $, we allow $ \mathbf{X} $ and $ \mathbf{Y} $ to be empty tuples, as a special case.

Eight of the axioms (those marked with a letter I) are shared with system $ \textsf{A}_\sigma $. Note the absence of I10 and I1b (which only hold in nonempty models) and I2b (which holds iff there is at most one assignment). Axiom J6 says that Weak reversibility holds for singleton and empty models (under the same restrictions as for axiom I6, which have not been repeated here). The remaining axioms deal with the nesting of modal operators. Axioms J10−J11 say that an intervention on all variables except an internal $ Y $ trumps any previous intervention on variables different from $ Y $. Axioms J12−13−14−15 are various consequences of the fact that the semantics of the modal operators only involves looking at certain singleton submodels. We note that the "empty intervention" versions of these axioms imply that any sequence of $ \Diamond $ and $ \Box $ modalities can always be reduced to the leftmost modality occurring in it (contrarily, e.g., to what happens in modal logic S5). J16 says that any model has a fixed set of causal laws. Together with J17, it will be used to show that, when reasoning with maximal consistent sets of formulas, the $ \mathcal{H}^+ $ formulas can always be "reduced" to $ \mathcal{H} $ formulas (note that, differently from $ [\mathbf{X} = \mathbf{x}]\psi $, the rightmost member of J17 is always an unnested formula). We have to admit that axiom scheme J17 is rather unsatisfying due to its complexity and semantic flavour; however, note that membership in this scheme is decidable due to the finiteness of the models. Furthermore, the problem of deciding which formulas are instances of J17 reduces to the proof-theoretic problem of finding proofs of consequences of the forms $ \mathbf{W} = s(\mathbf{W}), \Phi^{ \mathcal{F}_{\mathbf{X} = \mathbf{x}}} \vdash \psi $ and $ \mathbf{W} = s(\mathbf{W}), \Phi^{ \mathcal{F}_{\mathbf{X} = \mathbf{x}}} \vdash {\sim}\psi $ in system $ \textsf{A} $, which we already know to be complete.

Theorem 6.1. System $ \textsf{B}_\sigma $ is sound over the class of all models of signature $ \sigma $.

Proof. See the proof of Theorem 4.2 for the soundness of axioms J0, I1−I5, and I7−I9.

Concerning axiom J6, suppose $ T\models \mathbf{W} = \mathbf{w} $. Then, $ T $ is either a singleton model or empty. If it a singleton model, then it satisfies I6 (see Theorem 4.2 for a proof). Suppose now that $ T $ is empty, and that it safisfies $ \psi: \langle \mathbf{X} = \mathbf{x}, V=v \rangle (Y=y \ {\&} \ \mathbf{Z} = \mathbf{z}) $ and $ \chi: \langle \mathbf{X} = \mathbf{x}, Y=y \rangle (V=v \ {\&} \ \mathbf{Z} = \mathbf{z}) $. By $ \psi $, there is an $ s \in T_{\mathbf{X} = \mathbf{x}, V=v}^- $ such that $ s(Y)=y $ and $ s(\mathbf{Z})=\mathbf{z} $. But (since $ \mathbf{X} \cup \mathbf{Z} \cup \{Y\}\cup \{V\} = \mathrm{Dom} $) $ \chi $ tells us that $ s $ is also in $ T_{\mathbf{X} = \mathbf{x}, Y=y}^- $. In particular, if $ V $ is internal, $ s $ is compatible also with the law $ \mathcal{F}_V $; if we prove that (*): $ s(\mathbf{N}_{\mathbf{X}}) \in T^-(\mathbf{N}_{\mathbf{X}}) $, then we can conclude that $ s\in T_{\mathbf{X} = \mathbf{x}}^- $. But, since $ s \in T_{\mathbf{X} = \mathbf{x}, V=v}^- $ and $ T^- $ is empty, by definition of intervention, we must have $ \mathbf{N}_{\mathbf{X}V} = \emptyset $; and similarly, we obtain $ \mathbf{N}_{\mathbf{X}Y} = \emptyset $. But then $ \mathbf{N}_{\mathbf{X}} = \mathbf{N}_{\mathbf{X}Y} \cup \mathbf{N}_{\mathbf{X}V} = \emptyset $, so that condition (*) is trivially satisfied.

For axiom J10, note that $ T\models \langle \mathbf{X} = \mathbf{x} \rangle \langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y $ iff, for some $ s\in T_{\mathbf{X} = \mathbf{x}}^- $, $ (\{s\}, \mathcal{F}_{\mathbf{X} = \mathbf{x}})\models \langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y $. The latter holds iff there is a $ t\in (\{s\}, \mathcal{F}_{\mathbf{X} = \mathbf{x}})_{ \mathbf{W}_Y = \mathbf{w}}^- $ such that $ (\{t\}, (\mathcal{F}_{\mathbf{X} = \mathbf{x}})_{\mathbf{W}_Y = \mathbf{w}})\models Y=y $. But $ (\mathcal{F}_{\mathbf{X} = \mathbf{x}})_{\mathbf{W}_Y = \mathbf{w}} = \mathcal{F}_{\mathbf{W}_Y = \mathbf{w}} $ (since $ \mathbf{X} \subseteq \mathbf{W}_Y $). Let us show that $ t\in T_{\mathbf{W}_Y = \mathbf{w}}^- $. Since $ t\in (\{s\},\ \mathcal{F}_{\mathbf{X} = \mathbf{x}})_{ \mathbf{W}_Y = \mathbf{w}}^- $, by definition of intervention, $ t(\mathbf{W}_Y) = \mathbf{w} $, and, since $ Y\in \mathcal I $, $ t(Y)\in \mathcal{F}_Y(\mathbf{w}_{\upharpoonright PA_Y}) $, as needed. Thus, $ t\in T_{\mathbf{W}_Y = \mathbf{w}}^- $, and therefore $ T\models \langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y $.

Vice versa, if $ T\models \langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y $, there is a $ t\in T_{\mathbf{W}_Y = \mathbf{w}}^- $ such that $ (\{t\}, \mathcal{F}_{\mathbf{W}_Y = \mathbf{w}})\models Y=y $. As before $ (\mathcal{F}_{\mathbf{X} = \mathbf{x}})_{\mathbf{W}_Y = \mathbf{w}} = \mathcal{F}_{\mathbf{W}_Y = \mathbf{w}} $. It suffices then to show that $ t\in (T_{\mathbf{X} = \mathbf{x}})_{\mathbf{W}_Y = \mathbf{w}}^- $. Since $ t\in T_{\mathbf{W}_Y = \mathbf{w}}^- $, we have $ t(\mathbf{W}_Y) = \mathbf{w} $, as needed. Since $ Y $ is internal (in all the involved causal teams, since $ Y\notin \mathbf{X} $), then $ t(Y)=y \in (\mathcal{F}_{\mathbf{W}_Y = \mathbf{w}})_Y(\mathbf{w}_{\upharpoonright PA_Y}) = ((\mathcal{F}_{\mathbf{X} = \mathbf{x}})_{\mathbf{W}_Y = \mathbf{w}})_Y(\mathbf{w}_{\upharpoonright PA_Y}) $; thus, $ t\in (T_{\mathbf{X} = \mathbf{x}})_{\mathbf{W}_Y = \mathbf{w}}^- $, as needed. The soundness of axiom J11 is proved analogously.

The soundness of axioms J12, J13, and J14 is a straightforward consequence of the semantic clause for the modal operators, which just requires checking whether the consequent is satisfied in singleton models. For example, for axiom J12, note that $ T\models [\mathbf{X} = \mathbf{x}]\Diamond\psi $ iff all singleton submodels of $ T_{\mathbf{X\mathit{=\mathbf{x}}}} $ satisfy $ \Diamond\psi $ iff (being singleton) they satisfy $ \psi $, iff $ T\models [\mathbf{X} = \mathbf{x}]\psi $.

For axiom J15, suppose $ T\models \langle \mathbf{X} = \mathbf{x} \rangle \psi $. Then, there is an $ s\in T_{\mathbf{X} = \mathbf{x}}^- $ such that $ (\{s\}, \mathcal{F}_{\mathbf{X} = \mathbf{x}})\models \psi $. Obviously $ (\{s\}, \mathcal{F}_{\mathbf{X} = \mathbf{x}}) \models \Diamond\top $. Thus, $ (\{s\}, \mathcal{F}_{\mathbf{X} = \mathbf{x}})\models \psi\ {\&}\ \Diamond \top $. But $ s\in T_{\mathbf{X} = \mathbf{x}}^- $; thus, $ T\models \langle\mathbf{X} = \mathbf{x} \rangle(\psi\ {\&}\ \Diamond \top) $.

For axiom J16, note that $ T = (T^-, \mathcal{F})\models \Phi^ \mathcal{F} $ by Theorem 5.2. Thus, $ T\models \bigsqcup_{ \mathcal{F}\in \mathbb{F}_\sigma} \Phi^ \mathcal{F} $.

For axiom J17, suppose $ T\models \Phi^ \mathcal{F} $.

$ \Rightarrow $) Assume $ T\models [\mathbf{X} = \mathbf{x}]\psi $. Then, for all $ s\in (T_{\mathbf{X} = \mathbf{x}})^- $, (*): $ (\{s\}, \mathcal{F}_{\mathbf{X} = \mathbf{x}})\models \psi $. But we also have that $ (\{s\}, \mathcal{F}_{\mathbf{X} = \mathbf{x}})\models \mathbf{W} = s(\mathbf{W}) $; thus, by (*), $ (\{s\}, \mathcal{F}_{\mathbf{X} = \mathbf{x}})\models \bigsqcup_{\substack{t \text{ such that} \\ (\{t\}, \mathcal{F}_{\mathbf{X} = \mathbf{x}})\models \psi}} \mathbf{W}=t(\mathbf{W}) $. Since this holds for all $ s\in T_{\mathbf{X} = \mathbf{x}}^- $, $ T\models [\mathbf{X} = \mathbf{x}]\bigsqcup_{\substack{t \text{ such that} \\ (\{t\}, \mathcal{F}_{\mathbf{X} = \mathbf{x}})\models \psi}} \mathbf{W}=t(\mathbf{W}) $.

$ \Leftarrow $) Assume $ T\models [\mathbf{X} = \mathbf{x}]\bigsqcup_{\substack{t \text{ such that} \\ (\{t\}, \mathcal{F}_{\mathbf{X} = \mathbf{x}})\models \psi}} \mathbf{W}=t(\mathbf{W}) $. Then, for all $ s\in (T_{\mathbf{X} = \mathbf{x}})^- $, $ (\{s\}, \mathcal{F}_{\mathbf{X} = \mathbf{x}})\models \bigsqcup_{\substack{t \text{ such that} \\ (\{t\}, \mathcal{F}_{\mathbf{X} = \mathbf{x}})\models \psi}} \mathbf{W}=t(\mathbf{W}) $. Thus, by the semantic clauses, $ s=t $ for some $ t $ such that $ (\{t\}, \mathcal{F})\models \psi $. In other words, $ (\{s\}, \mathcal{F})\models \psi $. Thus, $ T\models [\mathbf{X} = \mathbf{x}]\psi $. □

Since this system includes modal logic K (MP, NEC, axioms J0 and I5), we automatically obtain the same theorems as in Lemma 4.4. But note that points 2., 3. and 5. have more relaxed statements.

Lemma 6.2. The following hold in $ \textsf{B}_{ } $.

1. (Deduction theorem) If $ \Gamma, \psi \vdash \chi $, then $ \Gamma \vdash \psi\rightarrow \chi $.

2. ($ \Box $-Monotonicity) If $ \Gamma\vdash[\mathbf{X} = \mathbf{x}]\psi $ and, $ \vdash \psi \rightarrow \psi' $, then $ \Gamma\vdash [\mathbf{X} = \mathbf{x}]\psi' $.

3. ($ \Diamond $-Monotonicity) If $ \Gamma\vdash \langle\mathbf{X} = \mathbf{x}\rangle\psi $ and $ \vdash \psi \rightarrow \psi' $, then $ \Gamma\vdash \langle\mathbf{X} = \mathbf{x} \rangle\psi' $.

4. $ \vdash([\mathbf{X} = \mathbf{x}]\psi \ {\&}\ [\mathbf{X} = \mathbf{x}]\chi) \leftrightarrow [\mathbf{X} = \mathbf{x}](\psi \ {\&}\ \chi) $.

5. (Replacement) Suppose $ \Gamma\vdash \theta \leftrightarrow \theta' $. Then, $ \Gamma\vdash \varphi \leftrightarrow \varphi[\theta'/\theta] $.

6. $ \vdash{\sim}[\mathbf{X} = \mathbf{x}]\psi \leftrightarrow \langle\mathbf{X} = \mathbf{x}\rangle{\sim}\psi $

7. $ \vdash{\sim}\langle\mathbf{X} = \mathbf{x}\rangle\psi \leftrightarrow [\mathbf{X} = \mathbf{x}]{\sim}\psi $

8. $ \vdash(\langle\mathbf{X} = \mathbf{x}\rangle \psi \sqcup \langle\mathbf{X} = \mathbf{x}\rangle \chi) \leftrightarrow \langle\mathbf{X} = \mathbf{x}\rangle(\psi\sqcup\chi) $.

9. $ \vdash([\mathbf{X} = \mathbf{x}]\psi\ {\&}\ \langle\mathbf{X} = \mathbf{x}\rangle \top)\rightarrow \langle\mathbf{X} = \mathbf{x}\rangle\psi $.

10. $ \vdash([\mathbf{X} = \mathbf{x}]\psi\ {\&}\ \langle \mathbf{X} = \mathbf{x} \rangle \chi) \rightarrow \langle \mathbf{X} = \mathbf{x} \rangle (\psi\ {\&}\ \chi) $.

11. $ \vdash\langle\mathbf{X} = \mathbf{x}\rangle(\psi\ {\&}\ \chi) \rightarrow (\langle\mathbf{X} = \mathbf{x}\rangle\psi \ {\&} \ \langle\mathbf{X} = \mathbf{x}\rangle\chi) $.

Let us clarify the relationship between systems $ \textsf{A}_\sigma $ and $ \textsf{B}_\sigma $. The intuitive picture is that system $ \textsf{B}_\sigma $ is conservative over $ \textsf{A}_\sigma $ when restricting our attention to singleton models. Formally, this means:

Theorem 6.3. Let $ \Gamma\cup \{\varphi\}\subseteq \mathcal{H}_\sigma $. Then, $ \Gamma\vdash_{ \textsf{A}_\sigma} \varphi $ iff $ \Diamond \top, \ \bigsqcup_{\mathbf{w} \in \mathrm{Ran}(\mathbf{W})} \mathbf{W} = \mathbf{w},\ \Gamma\vdash_{ \textsf{B}_\sigma} \varphi $.

Proof. For brevity, let us write $ \Delta $ for the set of assumptions $ \{\Diamond \top\} \cup \{\bigsqcup_{\mathbf{w} \in \mathrm{Ran}(\mathbf{W})} \mathbf{W} = \mathbf{w}\} \cup \Gamma $. Let us first observe that, if $ \theta $ is an axiom of $ \textsf{A}_\sigma $, then $ \Delta\vdash_{ \textsf{B}_\sigma} \theta $. Indeed, most of the axioms of $ \textsf{A}_\sigma $ are included in $ \textsf{B}_\sigma $. For axiom I10, obviously $ \Delta\vdash_{ \textsf{B}_\sigma} \Diamond\top $. For I2b, note first that $ \Delta\vdash_{ \textsf{B}_\sigma} \bigsqcup_{\mathbf{w} \in \mathrm{Ran}(\mathbf{W})} \mathbf{W} = \mathbf{w} $ trivially. But then $ \Delta \vdash_{ \textsf{B}_\sigma} \bigsqcup_{y\in \mathrm{Ran}(Y)} Y=y $ follows by J0 and MP.

For axiom I1b, write $ \Xi $ for $ \Delta \cup \{Y=y\} \cup\{Y=y'\} $. By axiom I7, $ \Xi \vdash_{ \textsf{B}_\sigma} \Box Y=y $ and $ \Xi \vdash_{ \textsf{B}_\sigma} \Box Y=y' $. On the other hand, by I1, $ \Box Y=y \rightarrow \Box Y \neq y' $; thus, by MP, $ \Xi \vdash_{ \textsf{B}_\sigma} \Box Y\neq y' $. By J0 and Lemma 6.2, 4., $ \Xi \vdash_{ \textsf{B}_\sigma} \Box (Y=y' \ {\&}\ Y\neq y') $. Thus, by J0 and replacement, $ \Xi \vdash_{ \textsf{B}_\sigma} \Box\bot $. Since $ \Diamond \top\in \Delta $, by Lemma 6.2, 9., $ \Xi \vdash_{ \textsf{B}_\sigma} \Diamond\bot $, i.e., $ \Xi \vdash_{ \textsf{B}_\sigma}{\sim}\Box \top $. On the other hand, $ \Xi \vdash_{ \textsf{B}_\sigma} \Box \top $ by J0 and NEC. So, by J0, $ \Xi \vdash_{ \textsf{B}_\sigma}\bot $. By the deduction theorem, then, $ \Delta \vdash_{ \textsf{B}_\sigma} (Y=y {\& } Y=y')\rightarrow \bot $. By J0, then, $ \Delta \vdash_{ \textsf{B}_\sigma} Y=y \rightarrow Y \neq y' $.

Finally, for axiom I6, just note that, by J6, J0 and MP, $ \Delta \vdash_{ \textsf{B}_\sigma} \bigsqcup_{\mathbf{w}\in \mathrm{Ran}(\mathbf{W})} $I6. Thus, by J0 again, $ \Delta \vdash_{ \textsf{B}_\sigma} $I6.

Since all axioms of $ \textsf{A}_\sigma $ are $ \vdash_{ \textsf{B}_\sigma} $-derivable from $ \Delta $, and $ \textsf{B} $ includes all the rule instances of $ \textsf{A} $, it is straightforward to transform any proof of the form $ \Gamma\vdash_{ \textsf{A}_\sigma} \varphi $ into a proof of $ \Delta\vdash_{ \textsf{B}_\sigma} \varphi $.

Vice versa, if $ \Delta\vdash_{ \textsf{B}_\sigma} \varphi $, by the soundness of $ \textsf{B} $ (Theorem 6.1), $ \Delta\models \varphi $. But this (by Lemma 4.1) means that every singleton model that satisfies $ \Gamma $ also satisfies $ \varphi $; i.e., $ \Gamma \models^1 \varphi $. But then $ \Gamma\vdash_{ \textsf{A}_\sigma} \varphi $ by the completeness theorem for $ \textsf{A}_\sigma $ (Theorem 4.13). □

We will now consider maximally $ \textsf{B}_\sigma $-consistent sets and their relationships to canonical teams. Note that, for sets $ \Gamma $ of $ \mathcal{H}^+_\sigma $ formulas that are maximally consistent according to $ \textsf{B}_\sigma $, we can define their associate canonical causal team $ \mathbb{T}^\Gamma $ exactly as in section 4; we may write $ \mathbb{T}^\Gamma_ \textsf{B} $ where there is the risk of confusion. As before, we can prove:

Lemma 6.4. Let $ \Gamma\supseteq\textsf{B}_{\sigma} $ be a maximal consistent set of $ \mathcal{H}^+_\sigma $ formulas. Then $ \mathbb{T}^\Gamma $ is a model, i.e.,

1. For all $ Y\in \mathrm{Int}(\mathbb{T}^\Gamma) $, $ \mathcal{F}_Y^\Gamma $ is well-defined.

2. For all $ Y\in \mathrm{Int}(\mathbb{T}^\Gamma) $ and $ s\in (\mathbb{T}^\Gamma)^- $, $ (s(PA_Y), s(Y))\in \mathcal{F}^\Gamma_Y $.

The proof is as for $ \textsf{A} $, since it only uses axiom I3 and classical logic.

The following corollary of Theorem 6.3 shows that the notational abuse of writing $ \mathbb{T}^\Gamma $ for $ \mathbb{T}^\Gamma_ \textsf{B} $ is not too dangerous, at least when $ \mathbb{T}^\Gamma_ \textsf{B} $ is a singleton model.

Corollary 6.5. Let $ \Gamma\supseteq \textsf{B}_\sigma $ be a maximal $ \textsf{B}_\sigma $-consistent set of $ \mathcal{H}^+_\sigma $-formulas such that $ \mathbb{T}_ \textsf{B}^\Gamma $ is a singleton model, and let $ \Gamma_0 $ be the set of $ \mathcal{H}_\sigma $ formulas in $ \Gamma $. Then, $ \Gamma_0 $ is maximally $ \textsf{A}_\sigma $-consistent, and $ \mathbb{T}^{\Gamma_0} = \mathbb{T}_ \textsf{B}^\Gamma $.

Proof. First, we show that $ \Diamond \top, \bigsqcup_{\mathbf{w}\in \mathrm{Ran}(\mathbf{W})} \mathbf{W} = \mathbf{w} \in \Gamma $.

For the former, note that since $ \mathbb{T}^\Gamma_ \textsf{B} $ is a singleton model, by its definition there is a $ \mathbf{w}\in \mathrm{Ran}(\mathbf{W}) $ such that $ \Diamond \mathbf{W} = \mathbf{w} \in \Gamma $. But $ \vdash_{ \textsf{B}_\sigma} \mathbf{W} = \mathbf{w} \rightarrow \top $ by J0, so $ \Diamond \top \in \Gamma $ by monotonicity.

For the latter, note that, by the definition of $ \mathbb{T}^\Gamma_ \textsf{B} $ and the fact that it is a singleton model, we also have that, for all $ \mathbf{w}'\neq \mathbf{w} $, $ \Diamond \mathbf{W} = \mathbf{w}' \notin\Gamma $. Since $ \Gamma $ is maximal, $ {\sim}\Diamond \mathbf{W} = \mathbf{w}' \in\Gamma $. By Lemmas 6.2, 7. and Lemma 4.5, 3., we obtain $ \bigwedge_{\mathbf{w}' \neq \mathbf{w}} \Box{\sim} \mathbf{W} = \mathbf{w}' \in\Gamma $. By Lemma 6.2, 4., $ \Box\bigwedge_{\mathbf{w}' \neq \mathbf{w}} {\sim} \mathbf{W} = \mathbf{w}' \in\Gamma $. Thus, since we have $ \Box \bigsqcup_{\mathbf{w}\in \mathrm{Ran}(\mathbf{W})} \mathbf{W} = \mathbf{w}\in \Gamma $ based on I2, from Lemma 4.5, 3. and Lemma 6.2, 4. we obtain $ \Box(\bigwedge_{\mathbf{w} \neq \mathbf{w}} {\sim} \mathbf{W} = \mathbf{w}' \ {\&}\ \bigsqcup_{\mathbf{w}\in \mathrm{Ran}(\mathbf{W})} \mathbf{W} = \mathbf{w})\in\Gamma $. Thus, based on J0 and replacement, $ \Box\mathbf{W} = \mathbf{w} \in \Gamma $. By I7, $ \mathbf{W} = \mathbf{w} \in \Gamma $. Thus, by I0, $ \bigsqcup_{\mathbf{w}\in \mathrm{Ran}(\mathbf{W})} \mathbf{W} = \mathbf{w} \in \Gamma $.

We use these facts to prove that $ \Gamma_0 $ is closed under $ \textsf{A} $-derivations. Suppose $ \Gamma_0 \vdash_ \textsf{A} \varphi $. Then, from Theorem 6.3, $ \Diamond \top, \ \bigsqcup_{\mathbf{w}\in \mathrm{Ran}(\mathbf{W})} \mathbf{W} = \mathbf{w}, $ $ \Gamma_0 \vdash_ \textsf{B} \varphi $; but then, based on what we proved above, $ \Gamma \vdash_ \textsf{B} \varphi $. Since $ \Gamma $ is maximal, then, $ \varphi\in\Gamma $; since $ \varphi \in \mathcal{H} $, we conclude $ \varphi\in\Gamma_0 $.

Now suppose for the sake of contradiction that $ \Gamma_0 $ is $ \textsf{A} $-inconsistent; then $ \Gamma_0\vdash_{ \textsf{A}_\sigma} \bot $, but since $ \Gamma_0 $ is closed under $ \textsf{A} $-derivations, $ \bot \in\Gamma_0\subseteq\Gamma $, contradicting the $ \textsf{B} $-consistency of $ \Gamma $.

Finally, suppose for the sake of contradiction that $ \Gamma_1\supset \Gamma_0 $ is an $ \textsf{A}_\sigma $-consistent set of $ \mathcal{H}_\sigma $ formulas; say, $ \varphi\in\Gamma_1\setminus \Gamma_0 $. Then, $ \varphi\notin\Gamma $, so, by the maximality of $ \Gamma $, $ {\sim}\varphi \in \Gamma $. But $ {\sim}\varphi $ is an $ \mathcal{H} $ formula, so $ {\sim}\varphi \in \Gamma_0 \subseteq \Gamma_1 $. Thus, after all, $ \Gamma_1 $ is inconsistent.

Now, since $ \Gamma_0 $ is maximally $ \textsf{A}_\sigma $-consistent, it defines the canonical team $ \mathbb{T}^{\Gamma_0} $, which by definition is the same as $ \mathbb{T}_ \textsf{B}^\Gamma $. □

Theorem 6.3 also ensures that the truth lemma will work correctly at least for the $ \mathcal{H} $ formulas in $ \Gamma $, provided $ \mathbb{T}^\Gamma $ is a singleton model.

Corollary 6.6. Let $ \Gamma\supseteq \textsf{B}_\sigma $ be a set of $ \mathcal{H}^+_\sigma $ formulas that is maximally consistent, and $ \varphi $ be an $ \mathcal{H}_\sigma $ formula.

1. If $ \varphi $ is an atomic formula, then $ \varphi\in \Gamma \iff \mathbb{T}^\Gamma \models \varphi $.

2. If $ \mathbb{T}^\Gamma $ is a singleton model, then $ \varphi \in \Gamma \iff \mathbb{T}^\Gamma \models \varphi $.

Proof. 1) Suppose $ Y=y \in \Gamma $. Then, $ \Box Y=y \in \Gamma $ by I7. Suppose for the sake of contradiction that there is a $ t\in (\mathbb{T}^\Gamma)^- $ such that $ t(Y)= y' \neq y $. Then, by definition of $ \mathbb{T}^\Gamma $, $ \Diamond\mathbf{W} = t(\mathbf{W}) \in \Gamma $. Thus, $ \Diamond Y=y'\in\Gamma $ by Lemma 6.2, 11. Thus, by Lemma 6.2, 10., $ \Diamond (Y=y\ {\&}\ Y=y')\in\Gamma $. On the other hand, by I1 and MP we have $ \Box Y\neq y' \in \Gamma $. Again, by Lemma 6.2, 10., we obtain $ \Diamond (Y=y\ {\&}\ Y=y'\ {\&}\ Y\neq y')\in \Gamma $, so, by I0 and monotonicity, $ \Diamond \bot \in \Gamma $. This contradicts Lemma 4.5, 5. Thus, all assignments in $ (\mathbb{T}^\Gamma)^- $ satisfy $ Y=y $, and so $ \mathbb{T}^\Gamma \models Y=y $.

Vice versa, suppose $ \mathbb{T}^\Gamma \models Y=y $. Suppose for the sake of contradiction that $ Y=y \notin \Gamma $. By axiom I7, $ \Box Y=y \notin \Gamma $. By maximality, $ {\sim} \Box Y=y\in \Gamma $, and by Lemma 6.2, 6., $ \Diamond {\sim}Y=y \in \Gamma $. On the other hand, by axioms I2, $ \Box \bigsqcup_{\mathbf{w} \in \mathrm{Ran}(\mathbf{W})} \mathbf{W} = \mathbf{w}\in\Gamma $. Thus, by Lemma 6.2, 10., $ \Diamond ({\sim}Y=y \ {\&}\ \bigsqcup_{\mathbf{w} \in \mathrm{Ran}(\mathbf{W})} \mathbf{W} = \mathbf{w})\in\Gamma $. By I0 and monotonicity, $ \Diamond \bigsqcup_{\mathbf{w} \in \mathrm{Ran}(\mathbf{W}), \mathbf{w}_{\upharpoonright Y}\neq y} \mathbf{W} = \mathbf{w} \in \Gamma $. By Lemma 6.2, 8., $ \bigsqcup_{\mathbf{w} \in \mathrm{Ran}(\mathbf{W}), \mathbf{w}_{\upharpoonright Y}\neq y}\Diamond \mathbf{W} = \mathbf{w} \in \Gamma $. Thus, by primality of $ \Gamma $, there is a $ \mathbf{w} \in \mathrm{Ran}(\mathbf{W}) $ such that $ \mathbf{w}_{\upharpoonright Y}\neq y $ and $ \Diamond \mathbf{W} = \mathbf{w} \in \Gamma $. Thus, the assignment $ s(\mathbf{W}) = \mathbf{w} $ is in $ (\mathbb{T}^\Gamma)^- $. But $ s(Y)\neq y $; thus, $ \mathbb{T}^\Gamma \not\models Y=y $, contradicting our initial assumption.

2) Let $ \Gamma_0 $ be the set of all $ \mathcal{H} $ formulas in $ \Gamma $. From right to left, suppose $ \mathbb{T}^\Gamma\models \varphi $; by corollary 6.5, this gives $ \mathbb{T}^{\Gamma_0} \models\varphi $. But then, since $ \varphi\in \mathcal{H} $, by the truth lemma 4.12 for $ \Gamma_0 $, $ \varphi\in\Gamma_0 \subseteq \Gamma $.

From left to right, note that, since $ \mathbb{T}^{\Gamma_0}= \mathbb{T}^\Gamma $ is a singleton model, $ \mathbb{T}^{\Gamma_0}\models \Diamond \top, \bigsqcup_{\mathbf{w} \in \mathrm{Ran}(\mathbf{W})} \mathbf{W} = \mathbf{w} $. Now, if $ \varphi\in \Gamma $, then $ \varphi\in \Gamma_0 $ (since it is an $ \mathcal{H} $ formula). Then, by the maximality of $ \Gamma_0 $, $ \Gamma_0 \vdash_{ \textsf{A}_\sigma} \varphi $. Thus, by Theorem 6.3, we have $ \Diamond \top, \bigsqcup_{\mathbf{w} \in \mathrm{Ran}(\mathbf{W})} \mathbf{W} = \mathbf{w}, \Gamma_0\vdash_{ \textsf{B}_\sigma} \varphi $. Furthermore, $ \mathbb{T}^{\Gamma_0} \models \Gamma_0 $ by the truth lemma for $ \mathbb{T}^{\Gamma_0} $. Thus, by the soundness of $ \textsf{B}_\sigma $, $ \mathbb{T}^\Gamma = \mathbb{T}^{\Gamma_0}\models \varphi $.□

This corollary gives us some control on the $ \mathcal{H}_\sigma $-formulas that are $ \textsf{B} $-provable for singleton models. To extend our grasp to $ \mathcal{H}^+ $ formulas, we aim to show that the $ \mathcal{H}_\sigma $ formulas that hold in a singleton model completely determine the truth or falsity of $ \mathcal{H}^+_\sigma $ formulas. We already know that this holds semantically (even for non-singleton models) by Theorem 5.1; we seek here a proof-theoretic counterpart of this result. We need a couple of intermediate lemmas; the first one shows that, if $ \Gamma\supseteq \textsf{B}_\sigma $ is a maximal consistent set of formulas, then there is exactly one $ \mathcal{F} $ (up to equivalence) such that $ \Phi^ \mathcal{F} \in \Gamma $.

Lemma 6.7. If $ \Gamma\supseteq \textsf{B}_\sigma $ is a maximal consistent set of $ \mathcal{H}^+ $ formulas, then there is an $ \mathcal{F}\in \mathbb{F}_\sigma $ such that $ \Phi^ \mathcal{F} \in \Gamma $; if $ \Phi^ \mathcal{F}, \Phi^ \mathcal{G} \in \Gamma $, then $ \mathcal{F}\equiv \mathcal{G} $.

Proof. Existence: Since $ \Gamma\supseteq \textsf{B}_\sigma $, by axiom J16 we have $ \bigsqcup_{ \mathcal{F}\in \mathbb{F}_\sigma} \Phi^ \mathcal{F}\in \Gamma $. Thus, by the primality of $ \Gamma $, there is an $ \mathcal{F} $ such that $ \Phi^ \mathcal{F}\in \Gamma $.

Uniqueness: Suppose for the sake of contradiction that $ \Phi^ \mathcal{F}, \Phi^ \mathcal{G} \in \Gamma $, where $ \mathcal{F}\not\equiv \mathcal{G} $. The statement $ \mathcal{F}\not\equiv \mathcal{G} $ implies that there is a $ Y \in \mathcal I $ and a tuple $ pa\in \mathrm{Ran}(PA_Y^ \mathcal{F} \cup PA_Y^ \mathcal{G}) $ such that $ \mathcal{F}_Y(pa_{\upharpoonright PA_Y^ \mathcal{F}}) \neq \mathcal{G}_Y(pa_{\upharpoonright PA_Y^ \mathcal{G}}) $. Suppose wlog that there is a $ y \in \mathcal{F}_Y(pa_{\upharpoonright PA_Y^ \mathcal{F}}) \setminus \mathcal{G}_Y(pa_{\upharpoonright PA_Y^ \mathcal{G}}) $. Then, by J0, $ \Phi^ \mathcal{F} \in \Gamma $ implies $ \langle \mathbf{W}_Y = \mathbf{w} \rangle Y=y\in\Gamma $ and $ \Phi^ \mathcal{G} \in \Gamma $ implies $ {\sim}\langle \mathbf{W}_Y = \mathbf{w} \rangle Y=y\in\Gamma $ for some $ \mathbf{w} $ such that $ \mathbf{w}_{\upharpoonright PA_Y^ \mathcal{F} \cup PA_Y^ \mathcal{G}} = pa $, contradicting the consistency of $ \Gamma $. □

Lemma 6.8. Let $ \Gamma\supseteq \textsf{B}_\sigma $ be a maximal consistent set of $ \mathcal{H}^+_\sigma $ formulas. Then, for each $ \varphi\in \mathcal{H}^+_\sigma $ there is a $ \varphi^*_\Gamma\in \mathcal{H}_\sigma $ such that $ \Gamma \vdash_{ \textsf{B}_\sigma} \varphi \leftrightarrow \varphi^*_\Gamma $.

Furthermore, $ \varphi^*_\Gamma $ is determined just by the causal laws encoded in $ \Gamma $, i.e., if $ \Phi^ \mathcal{F}\in\Gamma $ and $ \Phi^ \mathcal{F}\in\Gamma' $, then $ \varphi^*_\Gamma = \varphi^*_{\Gamma'} $.

Proof. We define $ \varphi^*_\Gamma $ and prove $ \Gamma \vdash \varphi \leftrightarrow \varphi^*_\Gamma $ by induction on $ \varphi $.

If $ \varphi $ is atomic, we let $ \varphi^*_\Gamma:= \varphi $; then, $ \Gamma \vdash \varphi \leftrightarrow \varphi^*_\Gamma $ follows from J0 (since $ \textsf{B}_\sigma \subseteq \Gamma $).

If $ \varphi $ is $ \psi\ {\&}\ \chi $, then we let $ \varphi^*_\Gamma := \psi^*_\Gamma \ {\&}\ \chi^*_\Gamma $. By the i.h., $ \Gamma \vdash \psi \leftrightarrow \psi^*_\Gamma $ and $ \Gamma \vdash \chi \leftrightarrow \chi^*_\Gamma $; thus, $ \Gamma \vdash \varphi \leftrightarrow \varphi^*_\Gamma $ follows by I0 and MP. The case for $ \varphi $ of the form $ {\sim}\psi $ is similar (letting $ \varphi^*_\Gamma := {\sim}\psi^*_\Gamma $).

If $ \varphi $ is $ [\mathbf{X} = \mathbf{x}]\psi $, then observe that by Lemma 6.7, there is one function component $ \mathcal{F} $ (up to equivalence) such that $ \Phi^ \mathcal{F}\in \Gamma $. We let $ \varphi^*_\Gamma:= [\mathbf{X} = \mathbf{x}] \bigsqcup_{\substack{t \text{ such that} \\ (\{t\}, \mathcal{F}_{\mathbf{X} = \mathbf{x}})\models \psi}} \mathbf{W}=t(\mathbf{W}) $. We note that, by Theorem 5.1, if $ \mathcal{F} \equiv \mathcal{G} $ then this formula is the same as $ [\mathbf{X} = \mathbf{x}]\bigsqcup_{\substack{t \text{ such that} \\ (\{t\}, \mathcal{G}_{\mathbf{X} = \mathbf{x}})\models \psi}} \mathbf{W}=t(\mathbf{W}) $ (as obviously $ \mathcal{F} \equiv \mathcal{G} $ implies $ \mathcal{F}_{\mathbf{X} = \mathbf{x}} \equiv \mathcal{G}_{\mathbf{X} = \mathbf{x}} $); thus, the definition of $ \varphi^*_\Gamma $ is determined by the equivalence class of $ \mathcal{F} $. Now, since $ \Phi^ \mathcal{F}\in \Gamma $, by axiom J17 $ \Gamma\vdash \varphi \leftrightarrow \varphi^*_\Gamma $. □

Upon closer inspection, this lemma also proves that, if an $ \mathcal{H}^+ $ formula completely determines the causal laws (i.e., it entails $ \Phi^ \mathcal{F} $ for some $ \mathcal{F} $) then it is equivalent to an $ \mathcal{H} $ formula. We will not need this fact in the following.

Theorem 6.9. For every $ \Gamma_0\supseteq \textsf{A}_\sigma $ maximal $ \textsf{A}_\sigma $-consistent set of $ \mathcal{H}_\sigma $ formulas there is a unique maximal $ \textsf{B}_\sigma $-consistent set $ \Gamma \supseteq \Gamma_0 \cup \textsf{B}_\sigma $ of $ \mathcal{H}^+ $ formulas.

Proof. Existence. Since $ \Gamma_0 $ includes $ \textsf{A}_\sigma $ and is maximally $ \textsf{A}_\sigma $-consistent, by Lemma 4.12 $ \Gamma_0 $ has a (singleton) model $ T $. Let $ \Gamma:= \{\varphi\in \mathcal{H}^+_\sigma \mid T\models \varphi\} $. Since $ T\models \Gamma $, by the soundness of $ \textsf{B}_\sigma $ (Lemma 6.1), we have $ \textsf{B}_\sigma \subseteq \Gamma $. And since it is the set of $ \mathcal{H}^+_\sigma $ formulas satisfied by a model, $ \Gamma $ is maximally consistent.

Uniqueness. Suppose for the sake of contradiction that there are two distinct $ \Gamma, \Gamma' $ satisfying the statement. Say, wlog, that there is a $ \varphi\in \Gamma \setminus \Gamma' $. Thus, by maximality of $ \Gamma' $, $ {\sim}\varphi\in\Gamma' $. By Lemma 6.8, there is a $ \varphi^*_\Gamma \in \mathcal{H}_\sigma $ such that $ \Gamma\vdash \varphi \leftrightarrow \varphi^*_\Gamma $; thus, by MP, (*): $ \varphi^*_\Gamma\in \Gamma_0\subseteq \Gamma $. By the same lemma, we also have $ \Gamma'\vdash {\sim}\varphi \leftrightarrow ({\sim}\varphi)^*_{\Gamma'} $. But the proof of the lemma shows that $ ({\sim}\varphi)^*_{\Gamma'} = {\sim}\varphi^*_{\Gamma'} $. Furthermore, note that, since $ \Phi^ \mathcal{F} \in \mathcal{H} $, we have $ \Phi^ \mathcal{F}\in\Gamma \iff \Phi^ \mathcal{F} \in \Gamma_0 \iff \Phi^ \mathcal{F} \in \Gamma' $. Since the $ \varphi^*_\Gamma $ are determined by the $ \mathcal{F} $ such that $ \Phi^ \mathcal{F} \in\Gamma $, we conclude that $ \varphi^*_\Gamma = \varphi^*_{\Gamma'} $. Therefore, $ \Gamma'\vdash {\sim}\varphi \leftrightarrow {\sim}\varphi^*_\Gamma $. So, $ {\sim}\varphi^*_\Gamma \in\Gamma_0\subseteq\Gamma' $. This, together with (*), contradicts the consistency of $ \Gamma_0 $. □

We now move toward a completeness proof. The failure of Weak reversibility over general models (and the apparent lack of an adequate substitute axiom) prevents us from applying the typical proof strategy used for logics of causal reasoning; weak reversibility seems essential for the usual proof of the truth lemma (cp. Lemma 4.12). Our strategy will be to introduce an (artificial) modal semantics for $ \mathcal{H}^+ $, so that we can use the standard techniques for proving completeness in modal logics, see e.g. Blackburn et al.^[32]㉘; this was also the reason for switching from $ \mathcal{H} $ to $ \mathcal{H}^+ $. In particular, we will build a canonical modal model whose worlds can be identified (modulo equivalence) with our canonical teams, and prove a truth lemma for it.

Let us fix some notation. We assume that there is a fixed alphabetical order of the variables. For a given signature $ \sigma $, we write $ I_\sigma $ for the set of all conjunctions of the form $ \mathbf{X} = \mathbf{x} $, where the variables in $ \mathbf{X} $ are listed alphabetically and without repetitions.

Definition 6.1. An unintended model (umodel) for $ \sigma $ is a tuple $ M=(W,\ R_{\top},\ (R_{\mathbf{X} = \mathbf{x}})_{\mathbf{X} = \mathbf{x} \in I_\sigma},\ V) $, where $ W $ is an arbitrary set (of "worlds"), $ R_{\top} $ and the $ R_{\mathbf{X} = \mathbf{x}} $ are binary relations on $ W $, and $ V $ is a function $ W\times \mathrm{Atom}_\sigma\rightarrow \{0, 1\} $.

We can then define the notion of truth at a world. Given a umodel $ M $, a world $ u $ of $ M $ and an $ \mathcal{H}^+ $ formula $ \varphi $, the relation $ M,\ u\Vdash \varphi $ is given by the following inductive clauses:

● $ M,\ u \Vdash Y=y $ iff $ V(u, Y=y)=1 $.

● $ M,\ u \Vdash \psi\ {\&}\ \chi $ iff $ M, u \Vdash \psi $ and $ M,\ u \Vdash \chi $.

● $ M,\ u \Vdash {\sim}\psi $ iff $ M, u \not\Vdash \psi $.

● $ M,\ u \Vdash \Box \psi $ iff for all $ v $ such that $ u R_{\top} v $, $ M, v\Vdash \psi $.

● $ M,\ u \Vdash [\mathbf{X} = \mathbf{x}]\psi $ iff for all $ v $ such that $ u R_{\mathbf{X} = \mathbf{x}} v $, $ M,\ v\Vdash \psi $.

Umodel–world pairs $ M, w $ might in general not be equivalent to any causal team (in the sense that they might not satisfy the same set of $ \mathcal{H}^+ $ formulas as a causal team). However, we introduce a canonical umodel whose worlds are maximal consistent sets^㉙, and they do behave like causal teams. We need to introduce a bit of extra notation. If $ \sigma = (\mathcal E, \mathcal I, \mathrm{Ran}) $ is a signature and $ \mathbf{X} \subseteq \mathcal E \cup \mathcal I $, we denote as $ \sigma_\mathbf{X} $ the signature $ (\mathcal E\cup \mathbf{X}, \mathcal I\setminus \mathbf{X}, \mathrm{Ran}) $ and call it a derived signature of $ \sigma $. Note that, conveniently, $ \mathcal{H}^+_{\sigma_\mathbf{X}} = \mathcal{H}^+_\sigma $ and $ \mathcal{H}_{\sigma_\mathbf{X}} = \mathcal{H}_\sigma $; on the other hand, $ \textsf{B}_{\sigma_\mathbf{X}} $ may differ from $ \textsf{B}_\sigma $ (they may contain different instances of axioms I8, J10, J11, J16, and J17). Thus, in general, $ \mathbb{T}^\Gamma_{\sigma_\mathbf{X}} $ might differ from $ \mathbb{T}^\Gamma_\sigma $, even if $ \Gamma $ is both a set of $ \mathcal{H}^+_{\sigma_\mathbf{X}} $ and $ \mathcal{H}^+_\sigma $ formulas. We denote by $ \hat\sigma $ the set of all derived signatures of $ \sigma $; note that $ \sigma \in \hat\sigma $.

The canonical umodel $ \mathbb{M}_\sigma $ has the following components:

● $ W $ is the set of all maximal consistent sets $ \Gamma \supseteq \textsf{B}_\tau $ of $ \mathcal{H}^+_\tau $ formulas, where $ \tau\in \hat\sigma $.

● $ \Gamma R_\top \Delta $ iff, for some $ \tau\in\hat\sigma $, $ \Gamma, \Delta\supseteq \textsf{B}_\tau $ and:

1. for some $ \mathbf{w}\in \mathrm{Ran}(\mathbf{W}) $, $ \Diamond\top, \Box \mathbf{W} = \mathbf{w} \in \Delta $

2. for all $ Y\in \mathcal I, y\in \mathrm{Ran}(Y) $ and $ \mathbf{w} \in \mathrm{Ran}(\mathbf{W}_Y) $, if $ \langle \mathbf{W}_Y = \mathbf{w}\rangle Y= y \in \Gamma $, then it is also in $ \Delta $

3. for all $ \chi \in \mathcal{H}^+_\sigma $, if $ \chi\in\Delta $, then $ \Diamond \chi \in \Gamma $.

● $ \Gamma R_{\mathbf{X} = \mathbf{x}} \Delta $ iff for some $ \tau\in\hat\sigma $, we have $ \Gamma\supseteq \textsf{B}_\tau $, $ \Delta\supseteq \textsf{B}_{\tau_\mathbf{X}} $ and:

1. for some $ \mathbf{w}\in \mathrm{Ran}(\mathbf{W}_\mathbf{X}) $, $ \Diamond\top, \Box (\mathbf{X}\mathbf{W}_\mathbf{X} = \mathbf{x} \mathbf{w}) \in \Delta $

2. for all $ Y\in \mathcal I\setminus \mathbf{X}, y\in \mathrm{Ran}(Y) $ and $ \mathbf{w} \in \mathrm{Ran}(\mathbf{W_Y}) $, if $ \langle \mathbf{W}_Y = \mathbf{w}\rangle Y= y \in \Gamma $, then it is also in $ \Delta $

3. for all $ \chi \in \mathcal{H}^+_\sigma $, if $ \chi\in\Delta $, then $ \langle \mathbf{X} = \mathbf{x} \rangle \chi \in \Gamma $.

● $ V(\Gamma, Y=y)=1 $ iff $ Y=y \in \Gamma $

We will simply write $ \mathbb{M} $ when the intended signature is not ambiguous. In the definition of the accessibility relations for $ \mathbb{M} $, clause 3 is the standard one used in the definition of canonical models in modal logic. The purpose of the additional clause 1 is to guarantee that, if a world $ \Delta $ is accessible from some other world, then it behaves analogously as a singleton causal model. This is to mimic the fact that the evaluation of a formula $ [\mathbf{X} = \mathbf{x}]\psi $ on a causal model amounts to checking whether $ \psi $ holds on singleton submodels of the intervened model. Finally, clause 2 (together with 3) guarantees that such singleton models have the same causal laws as the initial causal model—except for the variables $ \mathbf{X} $ that have been intervened upon. Concerning these variables, the fact that $ \Delta $ has signature $ \tau_\mathbf{X} $ guarantees that they behave as external variables.

Lemma 6.10. With notations as above:

1. In the definition of $ \Gamma R_\top \Delta $, clause 3 can be replaced with: for all $ \varphi \in \mathcal{H}^+_\sigma $, $ \Box \varphi \in \Gamma $ implies $ \varphi \in \Delta $.

2. In the definition of $ \Gamma R_{\mathbf{X} = \mathbf{x}} \Delta $, clause 3 can be replaced with: for all $ \varphi \in \mathcal{H}^+_\sigma $, $ [\mathbf{X} = \mathbf{x}] \varphi \in \Gamma $ implies $ \varphi \in \Delta $.

Proof. We only prove point 2., as the proof of point 1 is analogous.

From left to right, suppose $ \Gamma R_{\mathbf{X} = \mathbf{x}} \Delta $ and $ \varphi \notin \Delta $. By Lemma 4.5, 2., $ {\sim}\varphi \in \Delta $. By clause 3 of the definition of $ \mathbb{M} $, then, $ \langle\mathbf{X} = \mathbf{x}\rangle {\sim}\varphi \in \Gamma $. By Lemma 6.2, 6. $ {\sim} [\mathbf{X} = \mathbf{x}] \varphi \in \Gamma $. Thus, by the consistency of $ \Gamma $, $ [\mathbf{X} = \mathbf{x}] \varphi \notin \Gamma $.

From right to left, suppose $ [\mathbf{X} = \mathbf{x}]\varphi \in \Gamma $ implies $ \varphi \in \Delta $ for all formulas $ \varphi \in \mathcal{H}^+_\sigma $. By contraposition, $ \varphi \notin \Delta $ (which is equivalent to $ {\sim}\varphi \in \Delta $ by Lemma 4.5, 2.) implies $ [\mathbf{X} = \mathbf{x}] \varphi \notin \Gamma $, thus $ {\sim}[\mathbf{X} = \mathbf{x}] \varphi \in \Gamma $ by Lemma 4.5, 2., and finally $ \langle \mathbf{X} = \mathbf{x}\rangle {\sim}\varphi \in \Gamma $ by Lemma 6.2, 6. Since every formula $ \chi $ is equivalent to a negated formula (say, $ \chi \equiv {\sim}{\sim}\chi $), this is just a reformulation of clause 3 in the definition of $ \mathbb{M} $. □

Lemma 6.11. Let $ \psi $ be an $ \mathcal{H}^+_\sigma $ formula and $ \Gamma \supseteq \textsf{B}_\sigma $ be a maximal consistent set of $ \mathcal{H}^+_\sigma $ formulas.

1. Suppose $ \Diamond \psi \in \Gamma $. Then, there is a $ \mathbf{w} \in \mathrm{Ran}(\mathbf{W}) $ such that $ \Diamond(\psi {\& } \Box\mathbf{W} = \mathbf{w})\in\Gamma $.

2. Suppose $ \langle\mathbf{X} = \mathbf{x}\rangle \psi \in \Gamma $. Then, there is a $ \mathbf{w} \in \mathrm{Ran}(\mathbf{W}_\mathbf{X}) $ such that $ \langle\mathbf{X} = \mathbf{x}\rangle(\psi\ {\&}\ \Box \mathbf{X}\mathbf{W}_{\mathbf{X}} = \mathbf{x} \mathbf{w})\in\Gamma $.

Proof. We prove only statement 2., as the proof of statement 1. is analogous.

Suppose $ \langle \mathbf{X} = \mathbf{x} \rangle \psi \in \Gamma $. By axiom J2, $ [\mathbf{X} = \mathbf{x}]\bigsqcup_{\mathbf{x}\mathbf{w} \in \mathrm{Ran}(\mathbf{X}\mathbf{W}_{\mathbf{X}})}\mathbf{X}\mathbf{W}_{\mathbf{X}} = \mathbf{x}\mathbf{w} \in \Gamma $. By axiom I7 and replacement, $ [\mathbf{X} = \mathbf{x}]\bigsqcup_{\mathbf{x}\mathbf{w} \in \mathrm{Ran}(\mathbf{X}\mathbf{W}_{\mathbf{X}})}\Box\mathbf{X}\mathbf{W}_{\mathbf{X}} = \mathbf{x}\mathbf{w} \in \Gamma $. Thus, by Lemma 6.2, 10., $ \langle \mathbf{X} = \mathbf{x} \rangle (\psi\ {\&}\ \bigsqcup_{\mathbf{x}\mathbf{w} \in \mathrm{Ran}(\mathbf{X}\mathbf{W}_{\mathbf{X}})}\Box\mathbf{X}\mathbf{W}_{\mathbf{X}} = \mathbf{x}\mathbf{w})\in \Gamma $. By J0 and replacement, $ \langle \mathbf{X} = \mathbf{x} \rangle \bigsqcup_{\mathbf{x}\mathbf{w} \in \mathrm{Ran}(\mathbf{X}\mathbf{W}_{\mathbf{X}})}(\psi\ {\&}\ \Box\mathbf{X}\mathbf{W}_{\mathbf{X}} = \mathbf{x}\mathbf{w}) \in \Gamma $. By Lemma 6.2, 8., $ \bigsqcup_{\mathbf{x}\mathbf{w} \in \mathrm{Ran}(\mathbf{X}\mathbf{W}_{\mathbf{X}})}\langle \mathbf{X} = \mathbf{x} \rangle(\psi\ {\&}\ \Box\mathbf{X}\mathbf{W}_{\mathbf{X}} = \mathbf{x}\mathbf{w}) \in \Gamma $. By primality of $ \Gamma $ (Lemma 4.5, 4.), there is an $ \mathbf{x}'\mathbf{w} \in \mathrm{Ran}(\mathbf{X}\mathbf{W}_{\mathbf{X}}) $ such that $ \langle \mathbf{X} = \mathbf{x} \rangle(\psi\ {\&}\ \Box\mathbf{X}\mathbf{W}_{\mathbf{X}} = \mathbf{x}'\mathbf{w})\in \Gamma $. Now, suppose for the sake of contradiction that $ \mathbf{x}' \neq \mathbf{x} $. Note that, from the previous statement, by Lemma 6.2, 11., and J0 we obtain $ \langle\mathbf{X} = \mathbf{x}\rangle\Box\mathbf{X}\mathbf{W}_{\mathbf{X}} = \mathbf{x}'\mathbf{w}\in \Gamma $. By I7 and replacement, $ \langle\mathbf{X} = \mathbf{x}\rangle\mathbf{X}\mathbf{W}_{\mathbf{X}} = \mathbf{x}'\mathbf{w}\in \Gamma $. Thus, $ \langle\mathbf{X} = \mathbf{x}\rangle\mathbf{X} = \mathbf{x}'\in \Gamma $ by I0 and monotonicity. But $ [\mathbf{X} = \mathbf{x}]\mathbf{X} = \mathbf{x}\in \Gamma $ by axiom I4; thus, by Lemma 6.2, 10., $ \langle\mathbf{X} = \mathbf{x}\rangle(\mathbf{X} = \mathbf{x} {\& } \mathbf{X} = \mathbf{x}')\in \Gamma $. By the same lemma, J1 and J0, we obtain $ \langle\mathbf{X} = \mathbf{x}\rangle \bot \in \Gamma $, i.e. $ {\sim}[\mathbf{X} = \mathbf{x}]{\sim} \bot \in \Gamma $. On the other hand, $ [\mathbf{X} = \mathbf{x}]{\sim} \bot \in \Gamma $ by J0 and NEC, contradicting the consistency of $ \Gamma $. Thus, $ \mathbf{x}' = \mathbf{x} $. □

Lemma 6.12 (Existence lemma). Let $ \Gamma \supseteq \textsf{B}_\sigma $ be a maximal consistent set of $ \mathcal{H}^+_\sigma $ formulas, $ \varphi $ an $ \mathcal{H}^+_\sigma $ formula. Then:

1. if $ \Diamond \varphi \in \Gamma $, then there is a maximal $ \textsf{B}_\sigma $-consistent set $ \Delta $ of $ \mathcal{H}^+_\sigma $ formulas such that $ \Gamma R_\top \Delta $ and $ \varphi \in \Delta $.

2. if $ \langle \mathbf{X} = \mathbf{x} \rangle \varphi \in \Gamma $, then there is a maximal consistent $ \textsf{B}_{\sigma_\mathbf{X}} $ set $ \Delta $ of $ \mathcal{H}^+_\sigma $ formulas such that $ \Gamma R_{\mathbf{X} = \mathbf{x}} \Delta $ and $ \varphi \in \Delta $.

Proof. We only prove point 2., as the proof of point 1. is analogous.

Suppose $ \langle \mathbf{X} = \mathbf{x} \rangle \varphi \in \Gamma $. We first observe that, since $ \langle \mathbf{X} = \mathbf{x} \rangle \varphi\in\Gamma $, by Lemma 6.11 there is a $ \mathbf{w}\in \mathrm{Ran}(\mathbf{W}) $ such that $ \langle \mathbf{X} = \mathbf{x} \rangle (\varphi\ {\&}\ \Box \mathbf{W} = \mathbf{w}) \in\Gamma $ and $ \mathbf{w}_{\upharpoonright \mathbf{X}} = \mathbf{x} $. Let $ \Delta_1 = \{ \psi \mid [\mathbf{X} = \mathbf{x}] \psi \in \Gamma\} $, $ \Delta_2 = \{\langle \mathbf{W}_Y = \mathbf{w}\rangle Y= y \in \Gamma \mid Y\in \mathcal I \setminus \mathbf{X}, \mathbf{w}y \in \mathrm{Ran}(\mathbf{W}_YY)\} $ and $ \Delta_0 = \Delta_1 \cup \Delta_2 \cup \{\varphi, \Diamond \top, \Box \mathbf{W} = \mathbf{w}\} $. Suppose for the sake of contradiction that $ \Delta_0 $ is not consistent in $ \textsf{B}_{\sigma_\mathbf{X}} $. Since $ \textsf{B}_{\sigma_\mathbf{X}} $ is finitary, this means that there are formulas $ \psi_1, \dots, \psi_n\in \Delta_1 $ and $ \chi_1:\langle\mathbf{W}_{Y_1}=\mathbf{w_{\mathrm{1}}}\rangle Y_1=y_1,\ \dots\ ,\ \chi_m:\langle\mathbf{W_{\mathit{Y_m}}=\mathbf{w_{\mathit{m}}}}\rangle Y_m=y_m \in\Delta_2 $ such that $ \psi_1,\ \dots,\ \psi_n,\ \chi_1,\ \dots,\ \chi_m,\ \varphi,\ \Diamond \top,\ \Box \mathbf{W} = \mathbf{w} \vdash \bot $. By some applications of the deduction theorem and J0, we obtain $ \vdash (\psi_1\ {\&}\ \dots\ {\&}\ \psi_n\ {\&}\ \chi_1\ {\&}\ \dots\ {\&}\ \chi_m\ {\&}\ \Diamond \top) \rightarrow {\sim}(\varphi\ {\&}\ \Box \mathbf{W} = \mathbf{w}) $. By NEC, I5, Lemma 6.2, 4. and replacement, $ \vdash ([\mathbf{X} = \mathbf{x}]\psi_1\ {\&}\ \dots\ {\&}\ $ $ [\mathbf{X} = \mathbf{x}]\psi_n\ {\&}\ [\mathbf{X} = \mathbf{x}]\chi_1\ {\&}\ \dots\ {\&}\ [\mathbf{X} = \mathbf{x}]\chi_m\ {\&}\ [\mathbf{X} = \mathbf{x}]\Diamond \top) \rightarrow [\mathbf{X} = \mathbf{x}] $ $ {\sim}(\varphi\ {\&}\ \Box \mathbf{W} = \mathbf{w}) $. We can remove the diamond using axiom J12 and replacement, and then by $ m $ applications of J11, we obtain $ \vdash ([\mathbf{X} = \mathbf{x}]\psi_1 {\& } \dots\ {\&}\ [\mathbf{X} = \mathbf{x}]\psi_n {\& } \chi_1\ {\&}\ \dots {\&}\ \chi_m\ {\&}\ [\mathbf{X} = \mathbf{x}]\top) \rightarrow [\mathbf{X} = \mathbf{x}] {\sim}(\varphi\ {\&}\ \Box \mathbf{W} = \mathbf{w}) $ (applying J11 is correct because $ Y_1, \dots, Y_m $ are internal and not in $ \mathbf{X} $). But now, $ [\mathbf{X} = \mathbf{x}] \psi_1,\ \dots,\ [\mathbf{X} = \mathbf{x}]\psi_n\in \Gamma $ (by definition of $ \Delta_1 $), $ \chi_1, \dots, \chi_m\in \Gamma $ (by definition of $ \Delta_2 $) and $ [\mathbf{X} = \mathbf{x}]\top \in\Gamma $ (by J0 and NEC). Thus, by MP, $ [\mathbf{X} = \mathbf{x}]{\sim}(\varphi\ {\&}\ \Box \mathbf{W} = \mathbf{w})\in\Gamma $. Then, by Lemma 6.2, 7., $ {\sim}\langle \mathbf{X} = \mathbf{x} \rangle (\varphi\ {\&}\ \Box \mathbf{W} = \mathbf{w})\in\Gamma $. But we already know that $ \langle \mathbf{X} = \mathbf{x} \rangle (\varphi\ {\&}\ \Box\mathbf{W} = \mathbf{w})\in\Gamma $, so we contradict the consistency of $ \Gamma $.

Thus, $ \Delta_0 $ is consistent. By the Lindenbaum lemma, there is a maximal $ \textsf{B}_{\sigma_\mathbf{X}} $-consistent set $ \Delta \supseteq \Delta_0 $. Note that $ [\mathbf{X} = \mathbf{x}] \psi\in \Gamma $ implies $ \psi \in \Delta $ for all $ \psi $. By Lemma 6.10, then, we obtain clause 3 of the definition of $ R_{\mathbf{X} = \mathbf{x}} $. Furthermore, we have that $ \Diamond \top\in\Delta $ and $ \Box \mathbf{W} = \mathbf{w} \in \Delta $ with $ \mathbf{w}_{\upharpoonright \mathbf{X}} = \mathbf{x} $; this is clause 1 of the definition of $ R_{\mathbf{X} = \mathbf{x}} $. Finally, $ \Delta_2 \subseteq\Delta $; this is clause 2. Thus, $ \Gamma R_{\mathbf{X} = \mathbf{x}} \Delta $. Finally, we observe that $ \varphi\in\Delta $, as needed. □

Lemma 6.13 (Truth lemma for $ \mathbb{M} $). Let $ \Gamma\supseteq\textsf{B}_{\sigma} $ be a maximally consistent set of $ \mathcal{H}^+_\sigma $ formulas, and $ \varphi $ an $ \mathcal{H}^+_\sigma $ formula. Then, $ \mathbb{M}, \Gamma\Vdash \varphi $ iff $ \varphi\in\Gamma $.

Proof. By some applications of I0 and replacement, we can assume up to equivalence that all modal operators $ [\mathbf{X} =\mathbf{x}] $ occurring in $ \varphi $ are replaced with $ {\sim}{\sim}[\mathbf{X} =\mathbf{x}]{\sim}{\sim} $, i.e., $ {\sim} \langle\mathbf{X} =\mathbf{x} \rangle{\sim} $. We can then proceed by induction on the subformulas $ \psi $ of $ \varphi $, thought as combinations of atoms, $ {\sim} $, $ {\& } $ and $ \langle \mathbf{X} =\mathbf{x}\rangle $ operators; we prove the statement simultaneously for all $ \Gamma $.

If $ \psi $ is an atom $ Y=y $, then $ \mathbb{M}, \Gamma \Vdash Y=y $ iff (by definition of $ \Vdash $) $ V(\Gamma, Y=y)=1 $ iff (by definition of $ \mathbb{M} $) $ Y=y\in\Gamma $. The cases for $ \psi= \chi_1\ {\&}\ \chi_2 $ or $ \psi = {\sim}\chi $ are also straightforward.

If $ \psi $ is of the form $ \langle\mathbf{X} =\mathbf{x}\rangle\chi $, then $ \mathbb{M}, \Gamma \Vdash \langle\mathbf{X} =\mathbf{x}\rangle\chi $ iff (by definition of $ \Vdash $) there is a $ \Delta $ such that $ \Gamma R_{\mathbf{X} = \mathbf{x}} \Delta $ and $ \mathbb{M}, \Delta\Vdash \chi $, iff (induction hypothesis) there is a $ \Delta $ such that $ \Gamma R_{\mathbf{X} = \mathbf{x}} \Delta $ and $ \chi \in \Delta $. By clause 3 of the definition of $ R_{\mathbf{X} = \mathbf{x}} $, then, the latter implies $ \langle\mathbf{X} =\mathbf{x}\rangle\chi \in \Gamma $. Vice versa, if $ \langle\mathbf{X} =\mathbf{x}\rangle\chi \in \Gamma $, by the existence Lemma 6.12 there is a $ \Delta $ such that $ \Gamma R_{\mathbf{X} = \mathbf{x}} \Delta $ and $ \chi \in \Delta $. □

Corollary 6.14. If $ \Gamma $ is a world of $ \mathbb{M}_\sigma $ of signature $ \sigma_\mathbf{X} $, then it satisfies the axioms of $ \textsf{B}_{\sigma_{\mathbf{X}}} $.

Lemma 6.15 (Canonical singletons). Let $ \Delta\supseteq\textsf{B}_{\sigma} $ be a maximally consistent set of $ \mathcal{H}^+_\sigma $ formulas, and let $ \Delta_0 $ be the set of $ \mathcal{H} $ formulas in $ \Delta $. If $ \Diamond \top, \Box \mathbf{W} = s(\mathbf{W}) \in \Delta $, then $ \Delta_0 = \{\chi \in \mathcal{H}_\sigma \mid (\{s\}, \mathcal{F}^\Delta) \models \chi \} $.^㉚

Proof. By Lemma 6.2, 9., $ \Diamond \top, \Box \mathbf{W} = s(\mathbf{W}) \in \Delta_0\subseteq\Delta $ implies that $ \Diamond \mathbf{W} = s(\mathbf{W}) \in\Delta_0 $. Furthermore, by axiom I1, $ \vdash\Box \mathbf{W} = s(\mathbf{W}) \rightarrow \Box \mathbf{W} \neq t(\mathbf{W}) $ if $ s\neq t $; thus, $ \Box \mathbf{W} \neq t(\mathbf{W})\in\Delta $. If we had $ \Diamond \mathbf{W} = t(\mathbf{W})\in \Delta_0 $ for some $ t\neq s $, then, by Lemma 6.2, 10., we would obtain $ \Diamond (\mathbf{W} = t(\mathbf{W})\ {\&}\ \mathbf{W} \neq t(\mathbf{W})) $; thus, by J0 and replacement, $ \Diamond\bot\in \Delta_0\subseteq \Delta $; this contradicts Lemma 4.5, 5. Thus, $ s $ is the unique assignment such that $ \Diamond \mathbf{W} = s(\mathbf{W}) \in\Delta $. By definition of $ (\mathbb{T}^\Delta_ \textsf{B})^- $, then, we have $ (\mathbb{T}^\Delta_ \textsf{B})^- = \{s\} $. Thus, $ (\{s\}, \mathcal{F}^{\Delta_0}) = (\{s\}, \mathcal{F}^\Delta) = \mathbb{T}^\Delta $. By corollary 6.6, then, $ \Delta = \{\chi \in \mathcal{H}^+_\sigma \mid \mathbb{T}^\Delta \models \chi \} $; thus, $ \Delta_0 = \{\chi \in \mathcal{H}_\sigma \mid \mathbb{T}^{\Delta}\models \chi \} = \{\chi \in \mathcal{H}_\sigma \mid (\{s\}, \mathcal{F}^\Delta) \models \chi \} $. □

As we said early on, the canonical model $ \mathbb{M} $ is designed so that each of its worlds $ \Gamma $ would behave as the canonical causal team $ \mathbb{T}^\Gamma $, and each world $ \Delta $ with $ \Gamma R_{\mathbf{X} = \mathbf{x}} \Delta $ would behave as one of the singleton models that are produced by the intervention $ do(\mathbf{X} = \mathbf{x}) $ applied to $ \mathbb{T}^\Gamma $. The second of these claims, unfortunately, will not in general be correct; the law component $ \mathcal{F}^\Delta $ of $ \mathbb{T}^\Delta $ might disagree with the law component $ \mathcal{F}^\Gamma_{\mathbf{X} = \mathbf{x}} $ of $ \mathbb{T}^\Gamma_{\mathbf{X} = \mathbf{x}} $ about the parent sets of some variables.^㉛ We will see that, nonetheless, $ \mathbb{T}^\Delta $ is $ \equiv $-equivalent to a corresponding singleton submodel of $ \mathbb{T}^\Gamma_{\mathbf{X} = \mathbf{x}} $, and thus it satisfies the same $ \mathcal{H}^+ $ formulas.

Lemma 6.16. Let $ \tau\in \hat\sigma $. Let $ \Gamma\supseteq\textsf{B}_{\tau} $ and $ \Delta\supseteq\textsf{B}_{\tau_{\mathbf{X}}} $ be maximal consistent sets of $ \mathcal{H}^+_\sigma $ formulas. If $ \Gamma R_{\mathbf{X} = \mathbf{x}} \Delta $, then $ \mathcal{F}^\Delta \equiv \mathcal{F}^\Gamma_{\mathbf{X} = \mathbf{x}} $.

Proof. The causal laws for an internal variable $ Y $ do not necessarily have the same parent set in $ \mathcal{F}^\Delta $ as in $ \mathcal{F}^\Gamma_{\mathbf{X} = \mathbf{x}} $; so, we shall write $ PA^\Delta_Y $, resp. $ PA^\Gamma_Y $, to differentiate them. Note that $ \Gamma R_{\mathbf{X} = \mathbf{x}} \Delta $ entails that $ \mathcal{F}^\Delta $ and $ \mathcal{F}^\Gamma_{\mathbf{X} = \mathbf{x}} $ have the same signature (namely, $ \tau_\mathbf{X} $), so that the definition of $ \equiv $ may apply. Let us consider a tuple of values $ pa \in \mathrm{Ran}(PA^\Delta_Y \cup PA^\Gamma_Y) $; to conclude that $ \mathcal{F}^\Delta \equiv \mathcal{F}^\Gamma_{\mathbf{X} = \mathbf{x}} $ we need to prove that $ \mathcal{F}^\Delta_Y(pa_{\upharpoonright PA^\Delta_Y}) = \mathcal{F}^\Gamma_Y(pa_{\upharpoonright PA^\Gamma_Y}) $ when $ Y\in \mathcal I\setminus \mathbf{X} $.^㉜

Suppose $ y\in \mathcal{F}^\Delta_Y(pa_{\upharpoonright PA^\Delta_Y}) $. By definition of $ \mathcal{F}^\Delta $, this means that, for any $ \mathbf{w} \in \mathrm{Ran}(\mathbf{W}_Y) $ with $ \mathbf{w}_{\upharpoonright PA^\Delta_Y} = pa_{\upharpoonright PA^\Delta_Y} $, $ \langle \mathbf{W}_Y = \mathbf{w}\rangle Y = y \in \Delta $. In particular, this holds for any $ \mathbf{w} \in \mathrm{Ran}(\mathbf{W}_Y) $ with $ \mathbf{w}_{\upharpoonright PA^\Delta_Y \cup PA^\Gamma_Y} =pa $; fix one such tuple $ \mathbf{w} $. By clause 3 of the definition of $ R_{\mathbf{X} = \mathbf{x}} $, then, $ \langle \mathbf{X} = \mathbf{x} \rangle\langle \mathbf{W}_Y = \mathbf{w}\rangle Y = y \in \Gamma $. Since $ Y\notin \mathbf{X} $, by axiom J10 we have $ \langle \mathbf{W}_Y = \mathbf{w}\rangle Y = y \in \Gamma $. Thus, by definition of $ \mathcal{F}^\Gamma_Y $, $ y \in \mathcal{F}^\Gamma_Y(pa_{\upharpoonright PA^\Gamma_Y}) $.

Vice versa, suppose $ y \in \mathcal{F}^\Gamma_Y(pa_{\upharpoonright PA^\Gamma_Y}) $. Reasoning as before, there is a $ \mathbf{w} \in \mathrm{Ran}(\mathbf{W}_Y) $ with $ \mathbf{w}_{\upharpoonright PA^\Delta_Y \cup PA^\Gamma_Y} =pa $ such that $ \langle \mathbf{W}_Y = \mathbf{w}\rangle Y = y \in \Gamma $. But then, $ \langle \mathbf{W}_Y = \mathbf{w}\rangle Y = y \in \Delta $ by clause 2 of the definition of $ R_{\mathbf{X} = \mathbf{x}} $. □

The following two lemmas show that the singleton subteams of a canonical model $ \mathbb{T}^\Gamma $, resp. those of $ \mathbb{T}^\Gamma_{\mathbf{X} = \mathbf{x}} $, can be identified (up to $ \equiv $-equivalence) with well-chosen canonical teams.

Lemma 6.17. Let $ \Gamma\supseteq {\textsf{B}}_\sigma $ be a maximal consistent set of $ \mathcal{H}^+_\sigma $ formulas. If $ s\in (\mathbb{T}^\Gamma)^- $, then $ (\{s\}, \mathcal{F}^\Gamma) \equiv \mathbb{T}^\Delta $, where $ \Delta = \{\varphi\in \mathcal{H}^+_\sigma \mid \Diamond(\mathbf{W}= s(\mathbf{W})\ {\&}\ \varphi)\in\Gamma \} $. Furthermore, $ \Gamma R_\top \Delta $.

Proof. First of all, note that it is easy to show that, for any formula $ \varphi $, $ (\{s\}, \mathcal{F}^\Gamma)\models \varphi $ iff $ \mathbb{T}^\Gamma \models \Diamond(\mathbf{W}=s(\mathbf{W})\ {\&}\ \varphi) $. Therefore, $ (\{s\}, \mathcal{F}^\Gamma)\models \Delta $ and it satisfies no $ \mathcal{H}^+_\sigma $ formula outside of $ \Delta $. Thus, $ \Delta $ is a maximal $ \textsf{B}_\sigma $-consistent set of $ \mathcal{H}^+_\sigma $ formulas.

Thus, $ \mathbb{T}^\Delta $ is well-defined. Since $ \Delta $ is the set of all formulas satisfied by $ (\{s\}, \mathcal{F}^\Gamma) $, and $ (\{s\}, \mathcal{F}^\Gamma) $ is a model of signature $ \sigma $, by the soundness of $ \textsf{B}_\sigma $ we have $ \Delta \supseteq \textsf{B}_\sigma $. Let $ \Delta_0 $ be the set of all $ \mathcal{H} $ formulas in $ \Delta $. If we can prove that $ \mathbb{T}^\Delta $ is a singleton model, then by corollary 6.6 $ \mathbb{T}^\Delta \models \Delta_0 $, i.e., $ \mathbb{T}^\Delta $ and $ (\{s\}, \mathcal{F}^\Gamma) $ satisfy the same $ \mathcal{H}_\sigma $ formulas; thus, by Theorem 5.1, $ \mathbb{T}^\Delta \equiv (\{s\}, \mathcal{F}^\Gamma) $.

Let us then prove that $ \mathbb{T}^\Delta $ is a singleton model. Since $ s\in (\mathbb{T}^\Gamma)^- $, by definition of $ \mathbb{T}^\Gamma $ we have $ \Diamond \mathbf{W} = s(\mathbf{W})\in \Gamma $. Thus, $ \Diamond (\mathbf{W} = s(\mathbf{W})\ {\&}\ \mathbf{W} = s(\mathbf{W}))\in \Gamma $ by I0 and replacement; so, by the definition of $ \Delta $, $ \mathbf{W} = s(\mathbf{W}) \in \Delta $. By axiom I7, (*): $ \Box\mathbf{W} = s(\mathbf{W}) \in \Delta $.

On the other hand, since $ \Diamond \mathbf{W} = s(\mathbf{W})\in \Gamma $, by axiom J15 $ \Diamond (\mathbf{W} = s(\mathbf{W})\ {\&}\ \Diamond \top)\in \Gamma $. Thus, $ \Diamond \top \in \Delta $. Together with (*), this gives (by Lemma 6.2, 10.) $ \Diamond\mathbf{W} = s(\mathbf{W}) \in \Delta $. Thus, by definition of $ \mathbb{T}^\Delta $, $ s\in (\mathbb{T}^\Delta)^- $.

If $ t\neq s $, then $ \Diamond\mathbf{W} = t(\mathbf{W}) \in \Delta $, together with (*), would imply (Lemma 6.2, 10.) that $ \Diamond (\mathbf{W} = s(\mathbf{W})\ {\&}\ \mathbf{W} = t(\mathbf{W}))\in \Delta $. Together with I1 and J0, this yields $ \Diamond \bot $, contradicting Lemma 4.5, 5. Thus, for each $ t\neq s $, $ \Diamond\mathbf{W} = t(\mathbf{W}) \notin \Delta $. So, by definition of $ \mathbb{T}^\Delta $, $ (\mathbb{T}^\Delta)^- $ is the singleton $ \{s\} $.

Lastly, let us prove that $ \Gamma R_\top \Delta $. We already know that $ \Gamma, \Delta \supseteq \textsf{B}_\sigma $. We need to verify the three clauses of the definition of $ R_\top $.

Clause 1. Since obviously $ (\{s\}, \mathcal{F}^\Gamma)\models \Diamond\top,\ \Box \mathbf{W} = s(\mathbf{W}) $ and we have shown $ (\{s\}, \mathcal{F}^\Gamma) \equiv \mathbb{T}^\Delta $, we have $ T^\Delta\models \Diamond\top,\ \Box \mathbf{W} = s(\mathbf{W}) $. Since $ \Diamond\top,\ \Box \mathbf{W} = s(\mathbf{W}) $ are $ \mathcal{H} $ formulas, and furthermore $ \mathbb{T}^{\Delta_0} = \mathbb{T}^\Delta $ is a singleton, by corollary 6.6 we obtain $ \Diamond\top,\ \Box \mathbf{W} = s(\mathbf{W}) \in \Delta_0 \subseteq \Delta $, as needed.

Clause 2. Let $ Y\in \mathcal I $ (where $ \sigma = (\mathcal E, \mathcal I, \mathrm{Ran}) $), and suppose $ \left\langle\mathbf{W_{\mathit{Y}}}=\mathbf{w}\right\rangle Y=y\in\Gamma $. Since we have $ \Diamond \mathbf{W} = s(\mathbf{W}) \in \Delta $, by definition of $ \Delta $, $ \Diamond (\mathbf{W} = s(\mathbf{W})\ {\&}\ \mathbf{W} = s(\mathbf{W})) \in \Gamma $. By J0 and replacement, $ \Diamond \mathbf{W} = s(\mathbf{W}) \in \Gamma $. On the other hand, by axiom J11, from the initial assumption we get $ \Box\langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y \in \Gamma $. So, by Lemma 6.2, 10., we obtain $ \Diamond (\mathbf{W} = s(\mathbf{W})\ {\&}\ \langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y)\in \Gamma $. Thus, by definition of $ \Delta $, $ \left\langle\mathbf{W_{\mathit{Y}}}=\mathbf{w}\right\rangle Y=y\in\Delta $.

Clause 3. Suppose $ \chi\in\Delta $. By definition of $ \Delta $, then, $ \Diamond (\mathbf{W} = s(\mathbf{W})\ {\&}\ \chi) \in\Gamma $. Thus, $ \Diamond \chi \in \Gamma $ by Lemma 6.2, 11. □

Lemma 6.18. Let $ \tau\in\hat\sigma $, and $ \mathbf{X} $ be a tuple of variables in the domain of $ \sigma $. Let $ \Gamma\supseteq\textsf{B}_{\tau} $ be a maximal $ \textsf{B} $-consistent set of $ \mathcal{H}^+_\sigma $ formulas. If $ s\in (\mathbb{T}^\Gamma_{\mathbf{X} = \mathbf{x}})^- $, then there is a a maximal consistent set $ \Delta\supseteq\textsf{B}_{\tau_{\mathbf{X}}} $ of $ \mathcal{H}^+_\sigma $ formulas such that 1) $ \Gamma R_{\mathbf{X} = \mathbf{x}} \Delta $ and 2) $ \mathbb{T}^\Delta_{\tau_{\mathbf{X}}} \equiv (\{s\}, \mathcal{F}^\Gamma_{\mathbf{X} = \mathbf{x}}) $.

Proof. In case $ \mathbf{X} = \emptyset $, this is just Lemma 6.17. Let us assume henceforth that $ \mathbf{X} \neq \emptyset $.

We let $ \Delta := \{\varphi \in \mathcal{H}^+_\sigma \mid \langle \mathbf{X} = \mathbf{x} \rangle (\mathbf{W} = s(\mathbf{W})\ {\&}\ \varphi) \in \Gamma\} $. Let us verify that $ \Delta $ is maximally consistent and $ \textsf{B}_{\tau_{\mathbf{X}}} \subseteq \Delta $ (so that $ \mathbb{T}^\Delta $ is well-defined), and that it satisfies 1) and 2).

Observe first that, for any formula $ \varphi $, $ (\{s\}, \mathcal{F}^\Gamma_{\mathbf{X} = \mathbf{x}})\models \varphi $ iff $ \mathbb{T}^\Gamma_{\tau} \models \langle \mathbf{X} = \mathbf{x} \rangle(\mathbf{W}=s(\mathbf{W})\ {\&}\ \varphi) $. Therefore, $ (\{s\}, \mathcal{F}^\Gamma_{\mathbf{X} = \mathbf{x}}) $ is a model for $ \Delta $, and it satisfies no $ \mathcal{H}^+ _\sigma $ formulas outside $ \Delta $. From this we obtain, exactly as in the proof of Lemma 6.17, that $ \Delta $ is maximally consistent and (since $ (\{s\}, \mathcal{F}^\Gamma_{\mathbf{X} = \mathbf{x}}) $ is a model of signature $ \tau_{\mathbf{X}} $) $ \textsf{B}_{\tau_{\mathbf{X}}} \subseteq \Delta $.

1) We need to show that clauses 1.–3. of the definition of $ R_{\mathbf{X} = \mathbf{x}} $ are satisfied.

Clause 1. Since $ s\in (\mathbb{T}^\Gamma_{\mathbf{X} = \mathbf{x}})^- $, we have $ \mathbb{T}^\Gamma \models \langle \mathbf{X} = \mathbf{x} \rangle \mathbf{W} = s(\mathbf{W}) $. But then, there is a $ t\in (\mathbb{T}^\Gamma)^- $ such that $ (\{t\}, \mathcal{F}^\Gamma) \models \langle \mathbf{X} = \mathbf{x} \rangle \mathbf{W} = s(\mathbf{W}) $. Now, by Lemma 6.17, $ (\{t\}, \mathcal{F}^\Gamma)\equiv \mathbb{T}^\Lambda $ for the maximal consistent set $ \Lambda:= \{\varphi\in \mathcal{H}^+_\sigma \mid \Diamond(\mathbf{W}=t(\mathbf{W})\ {\&}\ \varphi)\in\Gamma \} $; thus, by Theorem 5.1, $ \mathbb{T}^\Lambda \models \langle \mathbf{X} = \mathbf{x} \rangle \mathbf{W} = s(\mathbf{W}) $. Since this is an $ \mathcal{H} $ formula, and $ \mathbb{T}^\Lambda $ is a singleton model, by corollary 6.6 we have $ \langle \mathbf{X} = \mathbf{x} \rangle \mathbf{W} = s(\mathbf{W}) \in \Lambda $. Therefore, $ \Diamond (\mathbf{W} = t(\mathbf{W})\ {\&}\ \langle \mathbf{X} = \mathbf{x} \rangle \mathbf{W} = s(\mathbf{W})) \in \Gamma $. By Lemma 6.2, 11., $ \Diamond\langle \mathbf{X} = \mathbf{x} \rangle \mathbf{W} = s(\mathbf{W}) \in \Gamma $. Thus, by axiom J14, $ \langle \mathbf{X} = \mathbf{x} \rangle \mathbf{W} = s(\mathbf{W}) \in \Gamma $. By axiom J15, $ \langle \mathbf{X} = \mathbf{x} \rangle (\mathbf{W} = s(\mathbf{W})\ {\&}\ \Diamond \top) \in \Gamma $. Thus, by definition of $ \Delta $, we have $ \Diamond\top\in \Delta $, as needed.

Note also that, from $ \langle \mathbf{X} = \mathbf{x} \rangle (\mathbf{W} = s(\mathbf{W})) \in \Gamma $, by J0 and replacement we obtain $ \langle \mathbf{X} = \mathbf{x} \rangle (\mathbf{W} = s(\mathbf{W})\ {\&}\ \mathbf{W} = s(\mathbf{W})) \in \Gamma $. Thus, by definition of $ \Delta $, $ \mathbf{W} = s(\mathbf{W}) \in \Delta $. Since we have already shown $ \textsf{B}_{\tau_{\mathbf{X}}} \subseteq \Delta $, and $ \Delta $, being maximally consistent, is closed under $ \vdash_{ \textsf{B}_{\tau_{\mathbf{X}}}} $ (Lemma 4.5, 1.) by axiom I7, we conclude $ \Box\mathbf{W} = s(\mathbf{W}) \in \Delta $. If we can prove that $ s(\mathbf{X})= \mathbf{x} $, then, we are done. But that immediately follows from the assumption $ s\in (\mathbb{T}^\Gamma_{\mathbf{X} = \mathbf{x}})^- $.

Clause 2. Suppose $ \langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y \in \Gamma $ for an internal $ Y\notin\mathbf{X} $. From this we obtain, by axiom J11, that (*): $ [\mathbf{X} = \mathbf{x}]\langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y \in \Gamma $. On the other hand, note that, since $ \Diamond\top, \Box\mathbf{W} = s(\mathbf{W})\in \Delta $, by Lemma 6.2, 10, we have $ \Diamond\mathbf{W} = s(\mathbf{W})\in\Delta $. By definition of $ \Delta $, then, $ \langle \mathbf{X} = \mathbf{x} \rangle (\mathbf{W} = s(\mathbf{W})\ {\&}\ \Diamond\mathbf{W} = s(\mathbf{W})) \in \Gamma $. By Lemma 6.2, 11., $ \langle \mathbf{X} = \mathbf{x} \rangle\Diamond\mathbf{W} = s(\mathbf{W}) \in \Gamma $. By axiom J13, then, $ \langle \mathbf{X} = \mathbf{x} \rangle \mathbf{W} = s(\mathbf{W}) \in \Gamma $. This, together with (*), yields $ \langle\mathbf{X} = \mathbf{x}\rangle (\mathbf{W} = s(\mathbf{W})\ {\&}\ \langle \mathbf{W}_Y = \mathbf{w}\rangle Y= y) \in \Gamma $ by Lemma 6.2, 10. Thus, by definition of $ \Delta $, $ \langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y \in \Delta $.

Clause 3. Suppose $ \chi\in \Delta $. By definition of $ \Delta $, $ \langle\mathbf{X} = \mathbf{x}\rangle (\mathbf{W} = s(\mathbf{W})\ {\&}\ \chi)\in \Gamma $. By Lemma 6.2, 11., then, $ \langle\mathbf{X} = \mathbf{x}\rangle \chi\in \Gamma $.

2) Let $ \Delta_0 $ be the set of $ \mathcal{H} $ formulas in $ \Delta $. Since $ \mathbb{T}^\Delta $ is a singleton, by corollary 6.6, we have $ \mathbb{T}^\Delta\models \Delta_0 $. Thus, $ \mathbb{T}^\Delta $ and $ (\{s\}, \mathcal{F}^\Gamma_{\mathbf{X} = \mathbf{x}}) $ satisfy the same $ \mathcal{H}_\sigma $ formulas. By Theorem 5.1, then, $ \mathbb{T}^\Delta \equiv (\{s\}, \mathcal{F}^\Gamma_{\mathbf{X} = \mathbf{x}}) $. □

Lemma 6.19 (Representation lemma). Let $ \tau\in\hat\sigma $, and let $ \Gamma \supseteq \textsf{B}_\tau $ be a maximally consistent set of $ \mathcal{H}^+_\sigma $ formulas, $ \varphi $ an $ \mathcal{H}^+_\sigma $ formula. Then, $ \mathbb{M}, \Gamma \Vdash \varphi $ iff $ \mathbb{T}^\Gamma \models \varphi $.

Proof. By induction on $ \varphi $: The cases for $ {\& } $ and $ {\sim} $ are straightforward.

Atomic case: $ \varphi $ is $ Y=y $. Since $ Y=y $ is atomic, corollary 6.6 tells us that $ \mathbb{T}^\Gamma\models Y=y $ iff $ Y=y \in \Gamma $, iff (by definition of $ \mathbb{M} $) $ V(\Gamma, Y=y)=1 $ iff (by definition of $ \Vdash $) $ M, \Gamma \Vdash Y=y $.

Case $ \varphi $ is $ [\mathbf{X}=\mathbf{x}]\psi $.

$ \Rightarrow $) Suppose $ \mathbb{M}, \Gamma \Vdash [\mathbf{X}=\mathbf{x}]\psi $. Since $ \mathbb{M}, \Gamma \Vdash [\mathbf{X}=\mathbf{x}]\psi $, we have that, for all $ \Delta $ such that $ \Gamma R_{\mathbf{X}=\mathbf{x}}\Delta $, $ \mathbb{M}, \Delta \Vdash \psi $. By the i.h., $ \mathbb{T}^\Delta \models \psi $. Therefore, if we show that 1) $ \mathbb{T}^\Delta $ is a singleton model, 2) every singleton submodel of $ \mathbb{T}^\Gamma_{\mathbf{X}=\mathbf{x}} $ is $ \equiv \mathbb{T}^\Delta $ for some $ \Delta $ with $ \Gamma R_{\mathbf{X}=\mathbf{x}}\Delta $, we will have $ \mathbb{T}^\Gamma\models [\mathbf{X}=\mathbf{x}]\psi $ by the semantic clauses for $ \models $.

2) This point is given by Lemma 6.18 (or Lemma 6.17 in the special case for $ \mathbf{X} = \emptyset $).

1) Since $ \Gamma R_{\mathbf{X}=\mathbf{x}}\Delta $, by definition, $ \Diamond \top\in\Delta $ and $ \Box \mathbf{W} = \mathbf{w} \in \Delta $ for some $ \mathbf{w} $ such that $ \mathbf{w}_{\upharpoonright \mathbf{X}} = \mathbf{x} $. By Lemma 6.2, 9., $ \Diamond \mathbf{W} = \mathbf{w} \in \Delta $; thus, $ s\in (\mathbb{T}^\Delta)^- $, where $ s $ is the assignment $ s(\mathbf{W}) = \mathbf{w} $. Suppose, for the sake of contradiction, that $ t\in (\mathbb{T}^\Delta)^- $, where $ t(\mathbf{W}) = \mathbf{w}' \neq \mathbf{w}\in \Delta $. By definition of $ \mathbb{T}^\Delta $, then, $ \Diamond \mathbf{W} = \mathbf{w}'\in \Delta $. On the other hand, $ \Box \mathbf{W} = \mathbf{w} \in \Delta $ together with axiom I1 yields $ \Box \mathbf{W} \neq \mathbf{w}' $. Thus, by Lemma 6.2, 10., $ \Diamond (\mathbf{W} = \mathbf{w}'\ {\&}\ \mathbf{W} \neq \mathbf{w}') \in \Delta $. By I0 and monotonicity, then, $ \Diamond \bot\in\Delta $. Since $ \Delta $ is consistent, we contradict Lemma 4.5, 5.

$ \Leftarrow $) Assume $ \mathbb{T}^\Gamma \models [\mathbf{X}=\mathbf{x}]\psi $. Then, for all $ s\in (\mathbb{T}^\Gamma_{\mathbf{X} =\mathbf{x}})^- $, $ (\{s\}, \mathcal{F}^\Gamma_{\mathbf{X} =\mathbf{x}}) \models \psi $. Suppose we manage to prove the following, for all maximally consistent sets of $ \mathcal{H}_\sigma^+ $ formulas $ \Delta \supseteq \textsf{B}_{\tau_{\mathbf{X}}} $:

$ (*): \text{if}~~ \Gamma R_{\mathbf{X}=\mathbf{x}}\Delta, \text{then for some}~~ s\in (\mathbb{T}^\Gamma_{\mathbf{X} =\mathbf{x}})^-, \Delta = \{\chi \in \mathcal{H}^+_\sigma \mid (\{s\}, \mathcal{F}^\Gamma_{\mathbf{X} =\mathbf{x}})\models \chi \}.$

If so, then by the above $ \psi \in \Delta $ if $ \Gamma R_{\mathbf{X}=\mathbf{x}}\Delta $. But then, by the truth lemma for $ \mathbb{M} $ (Lemma 6.13), $ \mathbb{M}, \Delta \Vdash \psi $ if $ \Gamma R_{\mathbf{X}=\mathbf{x}}\Delta $. Thus, $ \mathbb{M}, \Gamma \Vdash [\mathbf{X}=\mathbf{x}]\psi $, as needed.

Let us then prove (*). If $ \Gamma R_{\mathbf{X}=\mathbf{x}}\Delta $, then by definition of $ R_{\mathbf{X}=\mathbf{x}} $ we have $ \Diamond \top, \Box \mathbf{W} = \mathbf{w}^* \in \Delta $ for some $ \mathbf{w}^* $; let $ s $ be the assignment such that $ s(\mathbf{W})= \mathbf{w}^* $. Let $ \Delta_0 $ be the set of $ \mathcal{H} $ formulas in $ \Delta $. By Lemma 6.15, we have that $ \Delta_0 = \{\chi \in \mathcal{H}_\sigma \mid (\{s\}, \mathcal{F}^\Delta) \models \chi \} $. By Lemma 6.16$, \mathcal{F}^\Delta \equiv \mathcal{F}^\Gamma_{\mathbf{X} = \mathbf{x}} $; but then, by Theorem 5.1, $ (\{s\}, \mathcal{F}^\Delta) $ and $ (\{s\}, \mathcal{F}^\Gamma_{\mathbf{X} = \mathbf{x}}) $ satisfy the same $ \mathcal{H}^+_\sigma $ formulas. Thus, $ \Delta_0 = \{\chi \in \mathcal{H}_\sigma \mid (\{s\}, \mathcal{F}^\Gamma_{\mathbf{X} = \mathbf{x}}) \models \chi \} $. Since $ \Delta_0 $ has a singleton model of signature $ \tau_\mathbf{X} $, by the soundness of $ \textsf{A} $ we have $ \textsf{A}_{\tau_{\mathbf{X}}} \subseteq \Delta_0 $, and $ \Delta_0 $ is maximally $ \textsf{A}_{\tau_{\mathbf{X}}} $-consistent. Thus, by Theorem 6.9, $ \Delta $ is the only maximal consistent set of $ \mathcal{H}^+ $ formulas that extends both $ \Delta_0 $ and $ \textsf{B}_{\tau_{\mathbf{X}}} $. Now, $ \Delta':= \{\chi \in \mathcal{H}^+_\sigma \mid (\{s\}, \mathcal{F}^\Gamma_{\mathbf{X} = \mathbf{x}}) \models \chi \} $ also extends $ \Delta_0 $. Since $ (\{s\}, \mathcal{F}^\Gamma_{\mathbf{X} = \mathbf{x}}) $ is a model of $ \Delta' $, we also have $ \textsf{B}_{\tau_\mathbf{X}}\subseteq \Delta' $. Thus, $ \Delta=\Delta' $, as needed. □

Theorem 6.20 (Strong completeness of $ \textsf{B} $). For $ \Gamma \cup \{\varphi\} \subseteq \mathcal H^+_\sigma $,

$ \Gamma \models_\sigma \varphi \iff \Gamma \vdash_{ \textsf{B}_\sigma} \varphi. $

Proof. The right-to-left direction is given by the soundness theorem 6.1. In the other direction, suppose $ \Gamma \not\vdash_{ \textsf{B}_\sigma} \varphi $. By the usual reasoning, then, $ \Gamma \cup \textsf{B}_\sigma \cup \{{\sim}\varphi\} $ is $ \textsf{B}_\sigma $-consistent. By the Lindenbaum lemma, there is a maximal consistent set of $ \mathcal{H}^+_\sigma $ formulas $ \Delta \supseteq \Gamma \cup \textsf{B}_\sigma \cup \{{\sim}\varphi\} $. By the truth lemma for $ \mathbb{M} $ (Lemma 6.13), $ \mathbb{M}, \Delta \Vdash \Gamma, {\sim}\varphi $. But then, by the representation lemma (Lemma 6.19), $ \mathbb{T}^\Delta \models \Gamma, {\sim}\varphi $. Since $ \mathbb{T}^\Delta $ is a model (by Lemma 6.4), we conclude that $ \Gamma \not \models \varphi $. □

As a final remark, we note that now we may obtain an axiomatization of the $ \mathcal{H}^+_\sigma $ languages over singleton models as an extension of $ \textsf{B}_\sigma $. Consider the following axiom:

Sing. $ \Diamond\top {\& } \bigsqcup_{\mathbf{w} \in \mathrm{Ran}(\mathbf{W})} \mathbf{W} = \mathbf{w} $.

Theorem 6.21. For $ \Gamma \cup \{\varphi\} \subseteq \mathcal H^+_\sigma $, we have $ \Gamma \models_\sigma^1 \varphi \iff \Gamma$, Sing $ \vdash_{ \textsf{B}_\sigma} \varphi $.

Proof. This is an immediate consequence of Theorem 6.3 and Theorem 4.13. □

We are left instead with the open issue of axiomatizing language $ \mathcal{H}_\sigma $ over the class of all models (of signature $ \sigma $). We might conjecture that system $ \textsf{B}_\sigma $ could be conservative over the subsystem of axioms involving only unnested formulas (axioms J0, I1-I5, J6, I7-I9, and J16); the completeness for $ \mathcal{H}_\sigma $ formulas of this smaller set of axioms would immediately follow. But nothing of what has been done here supports this conjecture.

7. Parents, direct causes, and dummy arguments

9. Further axiomatizations

9.1. The deterministic case

We now consider the issues of definability and axiomatizability for the subclass of deterministic models. Remember that $ T = (T^-, \mathcal{F}) $ is deterministic if, for each internal variable $ Y $, $ \mathcal{F}_Y $ assigns at most one value to each tuple of values for the parents of $ Y $ ($ |\mathcal{F}_Y(pa)|\le1 $ for each such tuple $ pa $). We characterize this property by the following axiom:

$ \text{Det}.\ \langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y \rightarrow {\sim} \langle\mathbf{W}_Y = \mathbf{w}\rangle Y=y' \quad \text{(when}~~ y\neq y'~~\text{ and }~~ Y\in \mathcal I) $

We remark that this axiom scheme (like axiom schemes I8, J10, J11, J16, and J17) depends, for its formulation, on having the internal/external distinction in the signature; the formulas in this scheme are not sound in deterministic models when $ Y $ is an external variable. We will show in section 10.1 that this dependency is ineliminable.

Lemma 9.1. Let $ T $ be a model. Then, $ T\models \mathrm{Det} $ iff $ T $ is deterministic.

Proof. $ \Rightarrow $) Suppose, for the sake of contradiction, that $ T $ is not deterministic. Then, there is a variable $ Y\in \mathrm{Int}(T) $, a value $ pa \in \mathrm{Ran}(PA_Y) $, and two values $ y \neq y' \in \mathrm{Ran}(Y) $ such that $ y, y' \in \mathcal{F}_Y(pa) $. Pick a $ \mathbf{w} \in \mathrm{Ran}(\mathbf{W}_Y) $ such that $ \mathbf{w}_{\upharpoonright PA_Y} = pa $. By the definition of intervention, $ T\models \langle\mathbf{W}_Y = \mathbf{w}\rangle Y=y $ and $ T\models \langle\mathbf{W}_Y = \mathbf{w}\rangle Y=y' $. From the latter, we obtain $ T\not\models {\sim}\langle\mathbf{W}_Y = \mathbf{w}\rangle Y=y' $. But then, $ T $ falsifies an instance of Det.

$ \Leftarrow $) Suppose $ T $ is deterministic, and assume that $ T\models \langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y $ for some $ Y,\ y,\ \mathbf{w} $, with $ Y\in \mathrm{Int}(T) $.

Since $ T\models \langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y $ {and $ Y $ is internal}, then, by the semantic clause and the assumption of determinism, $ T\not\models \langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y' $ when $ y'\neq y $. Thus, $ T\models \langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y \rightarrow {\sim} \langle\mathbf{W}_Y = \mathbf{w}\rangle Y=y' $ whenever $ y\neq y' $ and $ Y $ is internal, i.e., $ T\models \operatorname{Det} $. □

Lemma 9.2. Let $ \Gamma \supseteq \textsf{A} \cup \{\mathrm{Det}\} $ (resp. $ \Gamma \supseteq \textsf{B} \cup \{\mathrm{Det}\} $) be a maximal consistent set of $ \mathcal{H}_\sigma $ (resp. $ \mathcal{H}^+_\sigma $) formulas. Then, $ \mathbb{T}^\Gamma $ is deterministic.

Proof. Suppose for the sake of contradiction that there is an internal variable $ Y $, values $ y\neq y'\in \mathrm{Ran}(Y) $, and a tuple $ pa \in \mathrm{Ran}(PA_Y) $ such that $ \{y, y'\}\subseteq \mathcal{F}^\Gamma_Y(pa) $. Then, by the definition of canonical model, there is a $ \mathbf{w} \in \mathrm{Ran}(\mathbf{W}_Y) $ such that $ \mathbf{w}_{\upharpoonright PA_Y} = pa $ and $ \langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y \in \Gamma, \langle \mathbf{W}_Y = \mathbf{w}\rangle Y=y'\in\Gamma $. However, $ \{\operatorname{Det}\}\subseteq \Gamma $, so in particular $ {\sim} \langle\mathbf{W}_Y = \mathbf{w}\rangle Y=y'\in \Gamma $. Thus $ \Gamma $ is inconsistent, contradicting the assumption. □

By the usual argument, then, we obtain the following completeness result. Write $ \models^{\operatorname D} $ for semantic entailment in the class of deterministic models, and $ \models^{\operatorname D}_1 $ for entailment in the class deterministic singleton models.

Theorem 9.3. $ \Gamma \models^{\operatorname D}_1 \varphi $ iff $ \Gamma, \mathrm{Det} \vdash_ \textsf{A} \varphi $, and $ \Gamma \models^{\operatorname D} \varphi $ iff $ \Gamma, \mathrm{Det} \vdash_ \textsf{B} \varphi $.

9.2. The total and recursive cases

We consider here the axiomatization of total causal teams (of a given fixed signature). Remember that a causal team $ T = (T^-, \mathcal{F}) $ is total if, for each of its internal variables $ Y $, $ \mathcal{F}_Y $ is a total multivalued function; i.e, for each tuple $ pa \in PA_Y $, $ \mathcal{F}_Y(pa) \neq \emptyset $. We claim that a complete axiomatization for the class of total models is obtained by adding to $ \textsf{B} $ the following axiom scheme:^㊲

Tot. $ \langle \mathbf{W}_Y = \mathbf{w}\rangle \top $ (when $ Y\in \mathcal I $),

where $ \mathbf{W}_Y $ denotes a list of all variables in the domain, except $ Y $. In the following two lemmas, we will see that axiom Tot captures the notion of totality from a semantic point of view.

Proposition 9.4. Let $ T $ be a model. $ T\models \mathrm{Tot} $ iff $ T $ is total.

Proof. $ \Leftarrow $) Let $ T = (T^-, \mathcal{F}) $ be total. Since $ Y $ is internal, then, we may pick a $ y\in \mathcal{F}_Y(\mathbf{w}_{\upharpoonright PA_Y}) $. We note then that the assignment $ s(\mathbf{W}_Y) = \mathbf{w} $, $ s(Y) = y $ is in $ T_{\mathbf{W}_Y = \mathbf{w}}^- $. Thus, $ T \models \langle \mathbf{W}_Y = \mathbf{w}\rangle \top $.

$ \Rightarrow $) Suppose $ T $ satisfies all instances of Tot. Let $ Y\in \mathrm{Int}(T) $, $ pa\in \mathrm{Ran}(PA_Y) $, and $ \mathbf{w}\in\mathrm{Ran}(\mathbf{W_{\mathit{Y}}}) $ such that $ \mathbf{w}_{\upharpoonright PA_Y} = pa $. Then, $ T\models \langle \mathbf{W}_Y = \mathbf{w}\rangle \top $. Thus, there is an $ s\in T_{\mathbf{W}_Y = \mathbf{w}}^- $, and $ s(PA_Y)=pa $. Then, by the definition of intervention, $ (pa, s(Y))\in \mathcal{F}_Y $. Since the choice of $ pa\in \mathrm{Ran}(PA_Y) $ was arbitrary, $ \mathcal{F}_Y $ is a total function. Since the choice of $ Y $ among internal variables was arbitrary, $ T $ is total. □

Lemma 9.5. Let $ \Gamma $ be a maximal consistent set of $ \mathcal{H} $ (resp. $ \mathcal{H}^+ $) formulas containing all instances of $ \textsf{A} $ (resp. $ \textsf{B} $) and $\textrm{Tot}$. Then, $ \mathbb{T}^\Gamma $ is total.

Proof. In the $ \textsf{A} $ case, since axiom Tot is an $ \mathcal{H} $ formula, by the truth lemma 4.12, $ \mathbb{T}^\Gamma\models \operatorname{Tot} $. Thus, $ \mathbb{T}^\Gamma $ is total by Proposition 9.4.

In the $ \textsf{B} $ case, we use Lemmas 6.13 and 6.19 instead of Lemma 4.12. □

Let us fix a signature $ \sigma $. We write $ \Gamma\models^{\operatorname T}\varphi $ if, for all total causal teams $ T $ of signature $ \sigma $, $ T\models \Gamma $ implies $ T\models \varphi $. Similarly, we write $ \Gamma\models_1^T\varphi $ if this holds for all singleton total causal teams of signature $ \sigma $.

Theorem 9.6.

1. $ \Gamma\models^{\operatorname T}_1\varphi $ iff $ \Gamma,\ \mathrm{Tot} \vdash_ \textsf{A} \varphi $.

2. $ \Gamma\models^{\operatorname T}\varphi $ iff $ \Gamma,\ \mathrm{Tot} \vdash_ \textsf{B} \varphi $.

Proof. We prove the left-to-right directions. Suppose $ \Gamma,\ \mathrm{Tot} \not\vdash \varphi $. Then, by the usual argument, $ \Gamma \cup\mathrm{Tot} \cup \{{\sim}\varphi\}\cup \textsf{A} $ (resp. $ \Gamma \cup\mathrm{Tot} \cup \{{\sim}\varphi\}\cup \textsf{B} $) is consistent, and by the Lindenbaum lemma, it is included in a maximally consistent set $ \Delta $. By Lemma 9.5, $ \mathbb{T}^\Delta $ is total. Furthermore, $ \mathbb{T}^\Delta\models\Delta $ (by the truth lemma 4.12, in the $ \textsf{A} $ case; by Lemmas 6.13 and 6.19 in the $ \textsf{B} $ case). In particular, $ \mathbb{T}^\Delta\models \Gamma $ but $ \mathbb{T}^\Delta\not\models \varphi $, and thus $ \Gamma \not\models^{\operatorname{T}}_{(1)}\varphi $. □

Moreover, we can see that the class of total recursive models can be axiomatized by further adding axiom R (it turns out that, within the class of total models, the logic of recursivity coincides with that of strict/visible recursivity).

Lemma 9.7. Let $ \Gamma \supseteq { \textsf{A} } \cup \{ \mathit{\text{Tot, R}}\} $ be a maximally consistent set of $ \mathcal{H}_\sigma $ formulas. Then, $ \mathbb{T}^\Gamma $ is total and recursive.

Proof. Totality is given by Lemma 9.5. Let us prove recursivity. Suppose for the sake of contradiction that there is a cycle $ X_1, \dots, X_n $ in the causal graph of $ \mathbb{T}^\Gamma $. Since $ \mathbb{T}^\Gamma $ is total, then, we may apply Theorem 7.4 and conclude that $ X_1, \dots, X_n $ is also a cycle in the parenthood graph. By Proposition 8.1, it is a cycle in the visible causal graph. The proof then proceeds as for Lemma 8.2. □

Then, the usual line of reasoning tells us that $ \textsf{B} \cup \{ \text{Tot, R}\} $ is a sound and complete axiomatization for the class of total recursive models, while $ \textsf{A} \cup \{ \text{Tot, R}\} $ is a sound and complete axiomatization for the class of total recursive singleton models.

Finally, a moment of thought shows that the singleton causal teams that are total, deterministic, and recursive essentially describe the same semantics as the recursive causal models of Galles & Pearl^[11] and Halpern^[12–13].^㊳ Indeed, first of all, while Halpern's causal settings only include an assignment $ u $ over the exogenous variables, the recursivity and determinism constraints make so that $ u $ determines a unique assignment $ s $ over all variables that complies with the causal laws. Second, even though our definition of intervention in the general case differs from that of Halpern, it was shown in Barbero & Galliani^[30] that in the (deterministic and) recursive case the two notions of interventions coincide. On the side of the of syntax, we note that our axioms are sound in Halpern's models if we follow him in interpreting the formulas $ \psi $ without modal operators as abbreviations for $ \Box\psi $. We can thus conclude that:

● The axiom systems $ \textsf{A} $ + Rec + Tot + Det and $ \textsf{B} $ + Rec + Tot + Det + Sing are alternative axiomatizations for the class of Halpern's recursive causal models.

One might be tempted to surmise that the axiom systems $ \textsf{A} $ + Tot + Det and $ \textsf{B} $ + Tot + Det + Sing are then axiomatizations of Halpern's general causal models, but that is incorrect. One reason, already hinted above, is that without the restriction of recursivity, our notion of intervention produces distinct results from both the ref.^[12] and ref.^[13] versions of Halpern's definition. For example, Halpern's empty interventions can produce new assignments, so that axiom I7 ($ \mathbf{Y} = \mathbf{y} \leftrightarrow \Box \mathbf{Y} = \mathbf{y} $) can be falsified. Note furthermore that, in our framework, if we apply the same intervention to two assignments $ s, s' $ that agree on the values of the external variables, we might still get two distinct sets of post-intervention assignments, in case $ s $ and $ s' $ disagree on the values of some variables that are not descendants of the intervened variables. Thus, it is not even clear, in the nonrecursive case, to what singleton causal team should a causal setting $ (M,\ u) $ of Halpern's^[12] semantics correspond to.^㊴ Most likely, such a causal setting should correspond to the maximal causal team containing all the assignments that assign $ u $ to the exogenous variables and respect the constraint of compatibility with the causal laws (this shows that, implicitly, causal team semantics was already used in Halpern^[12]). Interestingly, it can be shown that this class of model satisfies axiom I6 (Weak reversibility), and thus plausibly it can be axiomatized by some appropriate extension of system $ \textsf{A} \setminus \{ \rm{I}10\} $. We will not pursue this line of thought any further in this paper, as in any case the language from Halpern^[12] requires further complications in the semantics.^㊵

11. Comparisons with related work

As mentioned in the introduction, the idea of extending the Galles-Pearl framework of causal models with one-to-many causal laws is already suggested as a final remark in Halpern's original axiomatization work^[12]; on the other hand, we are not aware of any further development in this direction in the following two decades.

In 2021, Peters & Halpern^[17,25] developed a vast generalization of causal models (the generalized structural equation models, GSEM). Their generalizations go into two directions: on one hand, they remove the restriction to finite variable domains and finite value ranges, seemingly with the aim of modeling physical phenomena; and on the other hand, they allow for highly arbitrary interventions, which do not require causal laws for their computation. Such interventions associate a set of possible outcomes for the endogenous variables to each setting for the exogenous variables, and the only constraint that the interventions are enforced to abide to is that, say, an intervention $ do(\mathbf{X} = \mathbf{x}) $ should only produce sets of assignments that set the variables $ \mathbf{X} $ to $ \mathbf{x} $. It is clear that a causal model with indeterministic causal laws can be seen as a rather special case of a GSEM, although this is not remarked upon in these works; no talk of laws at all seems to be made in these papers. Given the large increase in generality—well beyond the simple addition of indeterministic laws—the GSEM framework seems quite unsuitable for obtaining a clear comparison between the usual causal models and their indeterministic generalization. And indeed, even when restricting attention to finite signatures, some of the usual axioms like Weak composition (our I3) and Weak reversibility (our I6) fail.

In 2023, Wysocki^[3] focused explicitly on indeterministic causal laws (there called "underdeterministic") as an addition to the usual recursive causal models (although, not having to deal with the problem of axiomatization, he does not bother restricting value ranges to the finite case). The paper is mainly a philosophical defense of qualitative indeterministic laws as opposed to probabilistic laws, and provides, e.g., several examples where indeterministic laws may be available (either as a representation of real indeterminism or of lack of exact knowledge) while a probabilistic law is unavailable due to pragmatic or mathematical constraints. Its most interesting technical contributions are, arguably, 1) the idea of redefining direct causation in terms of variation in the range of possible values of $ Y $ when intervening on $ X $ having fixed all other variables (which we tried to formalize in section 7.1); and 2) the observation that the $ d $-separation criterion is correct also for qualitative independence statements. For the rest, the presentation and some details of the framework—e.g., the definition of intervention, the semantics, and the syntax—are unusual and a bit vague, which makes it rather difficult to say to what extent Wysocki's framework agrees or differs with that which is considered in the present paper. It would look like formulas of the form $ \Diamond\psi $ or $ \Box\psi $ are evaluated over teams that are maximal, in the sense we mentioned in section 9.2, but allowing, rather than a single tuple of values for the exogenous variables, a cartesian product of value ranges for each exogenous variable (so as to ensure a qualitative form of independence among the exogenous variables). We have not considered this class of causal teams in the present paper.

In 2024, the proceedings version of the present paper^[38] appeared in print. Our work on the subject of indeterministic causal models began as early as 2020, and was influenced only in the later stages by the publication of Wysocki^[3] (from which we essentially only borrowed the generalized idea of direct causation that is discussed here in section 7.1). The paper introduced a formal definition of relational causal team (with simplified signatures) and sketched a description of the formalization obstacles that are presented more sharply here (sections 2 and 8). The paper also made some claims about axiomatization; regrettably, it was later discovered that the system therein introduced (as a purported axiomatization of the general class of models) is unsound. Indeed, the system in question includes axiom I6 (Weak reversibility), which, as we have seen, can be falsified by teams with more than one assignment. Secondly, its version of axiom I8 (which, differently from ours, does not rely on having the external/internal distinction in the signature) relies on the definability, in $ \mathcal{H} $, of what we call here visible direct cause in order to enforce syntactically the assumption that this axiom only applies to external variables; unfortunately, doing so amounts to evaluating externality by looking at the incorrect graph (the visible causal graph instead of the parenthood graph). Lastly, there is an axiom $ \Diamond\top \leftrightarrow\langle \mathbf{W} = \mathbf{w}\rangle\top $. Its right-to-left direction is in general false, since, as we have seen, the semantics allows for the possibility that intervening on an empty model may produce a nonempty team (this is actually always the case when intervening on the set $ \mathbf{W} $ of all variables). Our system $ \textsf{A} $ replaces this incorrect principle with axioms I9 and I10. We also remark that, while I6 is at least sound on singleton models, the other two axioms we discussed here are not.

In Beckers^[26], Beckers contributed his own theory of indeterministic counterfactuals, which was then used in Beckers^[27] to formulate a new definition of actual causality. The indeterministic causal models used by Beckers (at least, in what he calls swc semantics) are essentially identical to our total recursive singleton models. The paper is directly inspired by our work^[38], but Beckers proposes a different definition of counterfactual. Roughly, the truth value of his counterfactuals is assessed after a phase of observation (of values actually taken by the variables), followed by an intervention in the sense of Halpern. The observation phase is used (to the best of our understanding) to exclude interventions that would modify the actual value of a variable $ Y $ even though they do not change the values of the parents of $ Y $ (thus, in practice, enforcing the validity of the Strong composition axiom we discussed in section 8.2). So, for example, in a coin-tossing scenario where the coin has been tossed and it came heads, the counterfactual "had the coin been tossed, it would have come heads" is taken to be true (while it is false in our framework). Our impression is that Beckers' counterfactuals might be closer to Lewisian counterfactuals; their consequents are evaluated in (some of the) worlds that differ from the actual one only for making the antecedent true. The counterfactuals considered in our paper seem to be closer to the spirit of interventionist counterfactuals; their consequents are evaluated in worlds where not only is the antecedent true but it is also enforced by external intervention. Note also that it is only our paper's version of the counterfactual that preserves the predictive power of causal statements. Suppose, for example, that the Federal Council of Switzerland decides to declare war on Luxembourg upon the outcome of a coin toss (war shall be declared if a tails is tossed). Heads is tossed, thus preventing a suicidal war declaration. If we made the mistake of using Beckers' notion of counterfactual for policy-making, we would reach the obviously mistaken conclusion that it will be a good policy to use coin-tossing as a device to decide on the future diplomatic relations between Switzerland and Luxembourg. Using the counterfactuals from our paper, one will instead conclude that further coin-tossing might lead to a counterproductive war.^㊺ It would seem, then, that we have a distinction between a philosophical and a practical notion of counterfactual; the differences between the two approaches are certainly worth future investigation. As for what concerns axiomatization, Beckers provides deduction systems for two rather special classes of models. First, he axiomatizes total recursive singleton models (what he calls swc semantics); his system differs from our $ \textsf{A}+\operatorname{Tot}+\operatorname{R} $ (see section 8) in that it features both Strong composition (which is unsound in our context) and Weak composition (our I3), it lacks Nonemptyness (I10) and has axiom $ \Diamond \varphi \rightarrow \Box \varphi $ in place of our I12b. Furthermore, axioms I7 and I8 are absent due to differences in the syntax.^㊻ The recursivity axiom is formulated in terms of an indeterministic version of "causally affecting" instead of our choice of direct cause. Second, Beckers provides an axiomatization for what he calls scc semantics, i.e., essentially for the (total, recursive) maximal causal teams that we briefly mentioned in section 9.2.

There is a different line of inquiry connecting counterfactuals and (qualitative) indeterminism, and that is the study of (using Bohm's terminology) many-to-one causation, i.e., cases where "many different kinds of causes can produce essentially the same effect"^[2]. We are aware of only three papers attempting to develop the technicalities behind this idea. The first one, from 2022, is Barbero & Yang^[19], in whose conclusion section, an idea is described of indeterminate interventions, i.e., interventions that are in some ways underspecified (e.g., "pressing any button on the remote", "picking one direction", "switching to the third or fifth gear"). Such interventions admit a natural definition in the generalized causal teams studied in that paper.^㊼ These interventions are introduced with the purpose of giving an intervention-based semantics for interventionist counterfactuals with disjunctive antecedents. While several semantic frameworks for such counterfactuals had been proposed elsewhere, e.g., studies^[14,39,40], all these earlier proposals seemed rather ad hoc and ungrounded in interventionist ideas. In 2023, Wysocki^[41] makes a similar proposal under the curious name of semaphore interventions.^㊽ Since he does not cite our paper^[19], we can only assume that the idea was developed independently. This paper makes the interesting observation that for a simple enough language (say, $ \mathcal{H} $ extended with the possibility of having disjunctive counterfactual antecedents), the semantics returns the same judgments of truth and falsity as Briggs's theory. Thus, the indeterministic interventions provide a clear interventionist motivation for Briggs's seemingly ad hoc truth-maker semantics.

[1]	Paul LA, Hall EJ. 2013. Causation: a user’s guide. UK: Oxford University Press. doi: 10.1093/acprof:oso/9780199673445.001.0001
[2]	Bohm D. 1957. Causality and chance in modern physics. Princeton, NJ: Van Nostrand Company, Inc.
[3]	Wysocki T. 2026. The underdeterministic framework. The British Journal for the Philosophy of Science 77:245−270 doi: 10.1086/724450 CrossRef Google Scholar
[4]	Spirtes P, Glymour C, Scheines RN. 1993. Causation, prediction, and search. Vol. 81. New York: Springer. doi: 10.1007/978-1-4612-2748-9
[5]	Pearl J. 2000. Causality: models, reasoning, and inference. New York, NY, USA: Cambridge University Press.
[6]	Peters J, Janzing D, Scholkopf B. 2017. Elements of Causal Inference: Foundations and Learning Algorithms. US: The MIT Press.
[7]	Schölkopf B. 2022. Causality for machine learning. In Probabilistic and causal inference: the works of Judea Pearl. New York, USA: Association for Computing Machinery. pp. 765–804 doi: 10.1145/3501714.3501755
[8]	Hernan MA, Robins J. 2020. Causal inference: what if. Boca Raton: Chapman & Hill/CRC.
[9]	Heckman JJ, Vytlacil EJ. 2007. Econometric evaluation of social programs, part I: causal models, structural models and econometric policy evaluation. Handbook of Econometrics 6:4779−4874 doi: 10.1016/s1573-4412(07)06070-9 CrossRef Google Scholar
[10]	Morgan SL, Winship C. 2015. Counterfactuals and causal inference. New York, UK: Cambridge University Press. doi: 10.1017/CBO9781107587991
[11]	Galles D, Pearl J. 1998. An axiomatic characterization of causal counterfactuals. Foundations of Science 3(1):151−182 doi: 10.1023/A:1009602825894 CrossRef Google Scholar
[12]	Halpern JY. 2000. Axiomatizing causal reasoning. Journal of Artificial Intelligence Research 12(1):317−337 doi: 10.1613/jair.648 CrossRef Google Scholar
[13]	Halpern JY. 2016. Actual Causality. Cambridge, Massachussetts: The MIT Press.
[14]	Briggs R. 2012. Interventionist counterfactuals. Philosophical Studies 160(1):139−166 doi: 10.1007/s11098-012-9908-5 CrossRef Google Scholar
[15]	Zhang J. 2013. A Lewisian logic of causal counterfactuals. Minds and Machines 23(1):77−93 doi: 10.1007/s11023-011-9261-z CrossRef Google Scholar
[16]	Ibeling D, Icard T. 2020. Probabilistic reasoning across the causal hierarchy. Proceedings of the AAAI Conference on Artificial Intelligence 34:10170−10177 doi: 10.1609/aaai.v34i06.6577 CrossRef Google Scholar
[17]	Halpern JY, Peters S. 2022. Reasoning about causal models with infinitely many variables. Proceedings of the AAAI Conference on Artificial Intelligence 36:5668−5675 doi: 10.1609/aaai.v36i5.20508 CrossRef Google Scholar
[18]	Barbero F, Schulz K, Velazquez-Quesada FR, Xie K. 2022. Observing interventions: a logic for thinking about experiments. Journal of Logic and Computation 33:1152−1185 doi: 10.1093/logcom/exac011 CrossRef Google Scholar
[19]	Barbero F, Yang F. 2022. Characterizing counterfactuals and dependencies over (generalized) causal teams. Notre Dame Journal of Formal Logic 63(3):301−341 doi: 10.1215/00294527-2022-0017 CrossRef Google Scholar
[20]	Beckers S, Halpern J, Hitchcock C. 2023. Causal models with constraints. Proceedings of the Second Conference on Causal Learning and Reasoning, Tubingen, Germany, 2023. PMLR. pp. 866–879. https://proceedings.mlr.press/v213/beckers23a/beckers23a.pdf (accessed on 30 April 2026)
[21]	Barbero F, Virtema J. 2023. Strongly complete axiomatization for a logic with probabilistic interventionist counterfactuals. Logics in artificial intelligence, eds. Gaggl S, Martinez MV, Ortiz M. Cham: Springer. pp. 649–664 doi: 10.1007/978-3-031-43619-2_44
[22]	Fang J, Zhang J. 2023. A characterization of Lewisian causal models. International Workshop on Logic, Rationality and Interaction. LORI 2023. Lecture Notes in Computer Science. Cham: Springer. pp. 94–108 doi: 10.1007/978-3-031-45558-2_8
[23]	Kawamoto Y, Sato T, Suenaga K. 2023. Formalizing statistical causality via modal logic. European Conference on Logics in Artificial Intelligence, JELIA 2023. Lecture Notes in Computer Science. Cham: Springer. pp. 681–696 doi: 10.1007/978-3-031-43619-2_46
[24]	Ding Y, Manoorkar K, Tzimoulis A, Wang R, Wang X. 2023. Causal kripke models. Electronic Proceedings in Theoretical Computer Science 379:185−200 doi: 10.4204/EPTCS.379.16 CrossRef Google Scholar
[25]	Peters S, Halpern JY. 2021. Causal modeling with infinitely many variables. arXiv Preprint doi: 10.48550/arXiv.2112.09171 CrossRef Google Scholar
[26]	Beckers S. 2025. Nondeterministic causal models. Proceedings of the Fourth Conference on Causal Learning and Reasoning. Proceedings of Machine Learning Research, Lausanne, Switzerland, 2025, eds. Huang B, Drton M. Vol. 275. PMLR. pp. 1532–1554 https://proceedings.mlr.press/v275/beckers25b.html
[27]	Beckers S. 2025. Actual causation and nondeterministic causal models. arXiv Preprint doi: 10.48550/arXiv.2503.07849 CrossRef Google Scholar
[28]	Barbero F, Sandu G. 2021. Team semantics for interventionist counterfactuals: observations vs. interventions. Journal of Philosophical Logic 50:471−521 doi: 10.1007/s10992-020-09573-6 CrossRef Google Scholar
[29]	Strasser C, Antonelli GA. 2024. Non-monotonic Logic. In The Stanford Encyclopedia of Philosophy (Winter 2024 Edition), eds. Zalta EN, Nodelman U. https://plato.stanford.edu/entries/logic-nonmonotonic/index.html
[30]	Barbero F, Galliani P. 2022. Embedding causal team languages into predicate logic. Annals of Pure and Applied Logic 173:103159 doi: 10.1016/j.apal.2022.103159 CrossRef Google Scholar
[31]	Pearl J. 2017. Physical and metaphysical counterfactuals: evaluating disjunctive actions. Journal of Causal Inference 5(2):20170018 doi: 10.1515/jci-2017-0018 CrossRef Google Scholar
[32]	Blackburn P, De Rijke M, Venema Y. 2001. Modal Logic. Vol. 53. Cambridge, England: Cambridge University Press.
[33]	Wang Y, Cao Q. 2013. On axiomatizations of public announcement logic. Synthese 190:103−134 doi: 10.1007/s11229-012-0233-5 CrossRef Google Scholar
[34]	Woodward J. 2003. Making things happen: a theory of causal explanation. Vol. 114. Oxford Studies in the Philosophy of Science. Oxford University Press.
[35]	Zhang J, Lam WY, De Clercq R. 2013. A peculiarity in Pearl's logic of interventionist counterfactuals. Journal of Philosophical Logic 42:783−794 doi: 10.1007/s10992-012-9249-z CrossRef Google Scholar
[36]	Barbero F, Virtema J. 2024. Expressivity landscape for logics with probabilistic interventionist counterfactuals. 32^nd EACSL Annual Conference on Computer Science Logic, CSL 2024. Vol. 288. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. pp. 15:1−15:19 doi: 10.4230/LIPIcs.CSL.2024.15
[37]	Barbero F, Sandu G. 2024. Multiteam semantics for interventionist counterfactuals: probabilities and causation. Journal of Philosophical Logic 53(6):1537−1577 doi: 10.1007/s10992-024-09777-0 CrossRef Google Scholar
[38]	Barbero F. 2024. On the logic of interventionist counterfactuals under indeterministic causal laws. International Symposium on Foundations of Information and Knowledge Systems. Cham: Springer. pp. 203–221 doi: 10.1007/978-3-031-56940-1_11
[39]	Ciardelli I, Zhang L, Champollion L. 2018. Two switches in the theory of counterfactuals: a study of truth conditionality and minimal change. Linguistics and Philosophy 41(6):577−621 doi: 10.1007/s10988-018-9232-4 CrossRef Google Scholar
[40]	Santorio P. 2019. Interventions in premise semantics. Philosophers’ Imprint 19(1):1−27 Google Scholar
[41]	Wysocki T. 2023. An event algebra for causal counterfactuals. Philosophical Studies 180(12):3533−3565 doi: 10.1007/s11098-023-02015-4 CrossRef Google Scholar
[42]	Lewis D. 1973. Counterfactuals. Oxford: Blackwell Publishers. https://perso.uclouvain.be/peter.verdee/counterfactuals/lewis.pdf
[43]	Halpern JY. 2013. From causal models to counterfactual structures. The Review of Symbolic Logic 6(2):305−322 doi: 10.1017/S1755020312000305 CrossRef Google Scholar
[44]	Mossé M, Ibeling D, Icard T. 2024. Is causal reasoning harder than probabilistic reasoning? The Review of Symbolic Logic 17:106−131 doi: 10.1017/S1755020322000211 CrossRef Google Scholar

{{lists.name}}

Axiomatizations of causal reasoning under indeterministic causal laws

Abstract

Supplementary information

Rights and permissions

References

About this article

Cite this article

Article Metrics

Access History

Other Articles By Authors