Theorem 3.5 TM,w ∈ Trec *and, for all formulas* ϕ ∈ Luniq(S) and all contexts ~u*, we have* (**M, w**) |= ϕ iff (TM,w**, ~u**) |= ϕ.

Proof: It is easy to see that TM,w ∈ Trec; the definition of F guarantees that ≺TM,w =≺M. The definition of FX is independent of the context; it easily follows that for all contexts ~u and ~u′, we have (TM,w**, ~u**) |= ϕ iff (TM,w**, ~u**′) |= ϕ. Again, an easy induction on the structure of ϕ shows that, for all contexts ~u,
(**M, w**) |= ϕ iff (TM,w**, ~u**) |= ϕ.

It is easy to modify the construction slightly so that each context ~u corresponds to a different world w ∈ Ω. Thus, if the number of contexts is at least |Ω|, then we can get a closer analogue to Theorem 3.4, where we can associate with each world w ∈ Ω a context ~uw and show that (**M, w**) |= ϕ iff (**T, ~u**w) |=
ϕ. However, Theorem 3.5 suffices for the following corollary.

Corollary 3.6 *The same formulas in* Luniq(ΦS) *are valid in both* Trec(S) and Mrec(S). Proof: If ϕ is not valid in Trec, then there is some causal model T ∈ Trec and context ~u such that (**T, ~u**) |= ¬ϕ. By Theorem 3.4, (MT , w~u) |= ¬ϕ, so ϕ is not valid in Mrec. For the converse, if ϕ is not valid in Mrec, then there is some counterfactual structure M ∈ Mrec and world w such that
(**M, w**) |= ¬ϕ. By Theorem 3.5, (TM,w**, ~u**) |= ¬ϕ. Thus, the same formulas are satisfiable in both Trec and Mrec, and hence the same formulas are valid.

What happens if we consider Tuniq rather than Trec? Now causal models and counterfactual structures are incomparable. Consider the formula

$$\begin{array}{r l}{\varphi=_{\mathrm{def}}}&{{}[X_{1}=1](X_{2}=1\wedge X_{3}=0)\land}\\ {}&{{}[X_{2}=1](X_{3}=1\wedge X_{1}=0)\land}\\ {}&{{}[X_{3}=1](X_{1}=1\wedge X_{2}=0).}\end{array}$$

Theorem 3.7 ¬ϕ *is valid in* Trec and Mf *(and hence* M+
f
), but ϕ *is satisfiable in* Tuniq.

Proof: The validity of ¬ϕ in Trec follows from its validity in Mf , in light of Corollary 3.6 and the fact that Mrec ⊆ Mf . Nevertheless, I prove the validity of ¬ϕ in Trec first, since the proof is short and gives some insight. Consider a causal model T ∈ Trec, and suppose, by way of contradiction, that (**M, w**) |= ϕ. Let ≺T be the total ordering on the variables in V in T. One of X1, X2, and X3 must be minimal with respect to ≺T . Suppose it is X1 and that (**T, ~u**) |= X1 = i. Then we must have
(T, ~u) |= [X2 **= 1](**X1 = i) and (T, ~u) |= [X3 **= 1](**X1 = i). But since (**T, ~u**) |= ϕ, it follows that
(T, ~u) |= [X2 = 1](X1 **= 0)** and (T, ~u) |= [X3 = 1](X1 **= 1)**. Thus, X1 cannot be minimal with respect to ≺T . An analogous argument shows that X2 and X3 also cannot be minimal with respect to
≺T . Thus, we have a contradiction.

I next show that ¬ϕ is valid in Mf . Suppose by way of contradiction that M ∈ Mf and (**M, w**) |=
ϕ. Consider a world w
′closest to w that satisfies X1 = 1 ∨ X2 = 1 ∨ X3 = 1. (Since M ∈ Mf ,
there is guaranteed to be such a world.) Suppose that (M, w′) |= X1 = 1. Note that w
′ must be one of the worlds closest to w that satisfies X1 = 1. Since (M, w) |= [X1 = 1](X2 **= 1)**, we must have
(M, w′) |= X2 = 1. Thus, w
′ must also be one of the worlds closest to w that satisfies X2 = 1.

Since (M, w) |= [X2 = 1](X3 **= 1)**, we must have that (M, w′) |= X3 = 1. On the other hand,