Counterfactual identities under the front-door conditions

Let $I_A={\mathrm{An}}_G(A)$, including $A$. By recursive substitution, $A$ is measurable with respect to $U_{I_A}$; under $do(A=a)$, the equation at $A$ is replaced, so $M^a$ is measurable with respect to $U_{I_M}$. Under $do(M=m)$, the equation at $M$ is replaced, so $Y^m$ is measurable with respect to $U_{I_Y}$. These claims follow by induction in the finite topological order: an endogenous value depends only on the exogenous coordinates at vertices with directed paths to it in the relevant mutilated graph.

Suppose $v\in I_M\cap I_A$. Since $v\mathrm{\ne }A$, there are directed paths $v\to \cdots \to A$ in $G$ and $v\to \cdots \to M$ in $G_{\bar{A}}$; the latter avoids $A$. Take the last common vertex $w$ of these paths in a topological ordering. Their suffixes are disjoint, so they form a simple fork path $A\leftarrow \cdots \leftarrow w\to \cdots \to M$ with no internal collider. It is retained in $G_{\underset{‾}{A}}$, because the path uses no arrow out of its endpoint $A$, and is active given the empty set. This contradicts (ii), so $I_M\cap I_A=\mathrm{\varnothing }$.

Suppose $v\in I_M\cap I_Y$. There are directed paths $v\to \cdots \to M$ in $G_{\bar{A}}$ and $v\to \cdots \to Y$ in $G_{\bar{M}}$. The first path avoids $A$. The second avoids $M$; it also avoids $A$, since otherwise its segment $A\to \cdots \to Y$ would be a directed $A$-to-$Y$ path avoiding $M$, contrary to (i). Take the last common vertex $w$ of the paths. Their suffixes form a simple fork path $M\leftarrow \cdots \leftarrow w\to \cdots \to Y$ with no internal collider and no internal $A$. It lies in $G_{\underset{‾}{M}}$ and is active given $\{A\}$, contradicting (iii). Thus $I_M\cap I_Y=\mathrm{\varnothing }$.

Fix $v\in I_Y$. There is a directed path $q$ from $v$ to $Y$ in $G_{\bar{M}}$. It avoids $M$ by definition and avoids $A$, because an occurrence of $A$ would leave a directed $A$-to-$Y$ suffix avoiding $M$, contrary to (i). Thus $q$ is retained in $G_{\underset{‾}{M}}$. If an active path $p$ from $M$ to $v$ given $\{A\}$ existed there, choose the last vertex $w$ of $p$ that also lies on $q$ when $q$ is traversed from $v$ to $Y$. Keep the prefix of $p$ from $M$ to $w$ and append the directed suffix of $q$ from $w$ to $Y$. The suffix after $w$ is disjoint from the prefix by the choice of $w$, so this is a path. Its old internal vertices remain active; $w\mathrm{\notin }A$ and the outgoing directed edge makes it a noncollider; all new internal vertices are noncolliders outside $A$. This would be an active path from $M$ to $Y$ given $A$, contradicting (iii). Hence $A$ d-separates $M$ and $v$ in $G_{\underset{‾}{M}}$. In the expanded graph each added root has only one skeleton neighbor, its own equation vertex, so a simple path cannot contain a root internally. An active path ending at $U_v$ would therefore have penultimate vertex $v$; deleting its last edge leaves an active path from $M$ to $v$ (or $v=M$). The latter case is excluded by $M\mathrm{\notin }{I}_Y$, and the former was just excluded. Adding roots does not create new directed descendants of endogenous vertices, so the remaining collider-activity tests are unchanged. Thus $A$ also d-separates $M$ and the whole root set $U_{I_Y}$ in the expanded graph with arrows out of $M$ deleted.

By [F3], the disjoint exogenous vectors $U_{I_M}$ and $U_{I_A}$ are independent. Step 1.1 makes $M^a$ and factual $A$ measurable functions of these respective vectors, so $M^a\perp A$.

The finite vectors $U_{I_M}$ and $U_{I_Y}$ are independent by [F3]. By step 1.1, $M^a$ and the response family $(Y^m{)}_{m\in S_M}$ are measurable functions of these disjoint vectors; in particular $M^a\perp U_{I_Y}$.

Adjoin all exogenous coordinates as independent root vertices. In the factual law, no strict descendant of $M$ is an ancestor of $(M,A,U_{I_Y})$: it cannot be an ancestor of an exogenous root, and if it were an ancestor of $A$, the directed path from $M$ to $A$ would remain in $G_{\underset{‾}{A}}$ and contradict (ii). Reverse-topological integration therefore marginalizes all other vertices and leaves the joint law of $(M,A,U_{I_Y})$ factored on its ancestral subgraph, which has no outgoing edge from $M$. This is a subgraph of the expanded mutilated graph in step 1.4, so the separation there still holds. The global Markov implication [F2], interpreted by the conditional-independence definition [F4], gives $M\perp U_{I_Y}\mid A$.

In $G_{\bar{M}}$ there is no directed path from $A$ to $Y$, since every directed $A$-to-$Y$ path in $G$ contains $M$ and arrows into $M$ were deleted. With $M$ fixed, changing the equation at $A$ therefore cannot change $Y$ by recursive substitution: any directed route by which $A$ could affect $Y$ would have to reach the fixed node $M$. Under $do(A=a)$, the mediator equals $M^a$. Replacing the mediator equation by that same realized value leaves every other equation unchanged; the no-directed-path argument shows that leaving $A$ factual has no further effect on $Y$. Thus $Y^a=Y^{M^a}$.