value x". This formula is true in a causal model T in a context ~u if in all solutions to the equations in TY~ =~y in context ~u, the random variable X has value x. Note that this formula is trivially true if there are no solutions to the structural equations.

A formula in L
+(S) is true or false in a causal model in T (S), given a context ~u. As usual, we write (**T, ~u**) |= ϕ if the causal formula ϕ is true in causal model T given context ~u.

3 For a basic causal formula [Y~ = ~y]ϕ, we define (T, ~u) |= [Y~ = ~y]ϕ if ϕ holds in all solutions to the equations F
Y~ =~y with the values of the variables in U set to ~u. Thus, for example, if ϕ has the form X1 = x1 ∨ X2 = x2, then
(**T, ~u**) |= ϕ iff every vector of values for the endogenous variables that simultaneously satisfies all the equations in F has either X1 = x1 or X2 = x2.

4 We define the truth value of arbitrary causal formulas, which are just Boolean combinations of basic causal formulas, in the obvious way:

$$\bullet\ (T,{\vec{u}})\models\varphi_{1}\land\varphi_{2}{\mathrm{~if~}}(T,{\vec{u}})\models\varphi_{1}{\mathrm{~and~}}(T,{\vec{u}})\models\varphi_{2}$$
$$\bullet\ (T,{\vec{u}})\models\lnot\varphi\ \mathrm{if}\ (T,{\vec{u}})\not\vDash\varphi.$$

As usual, a formula ϕ is said to be *valid* with respect to a class T
′ of causal models if (**T, ~u**) |= ϕ for all T ∈ T ′and contexts ~u in T.

L
+ is the most general language that I consider in [Halpern 2000]. To compare my results to those of GP, who use a more restricted language, I also consider some restrictions of L
+. Specifically, let Luniq be the sublanguage of L
+ that consists of Boolean combinations of formulas of the form [Y~ =
~y](X = x). Thus, the difference between Luniq and L
+ is that in Luniq, only X = x is allowed after
[Y~ = ~y], while in L
+, arbitrary Boolean combinations of formulas of the form X = x are allowed.

As the following lemma, proved in [Halpern 2000], shows, for reasoning about causality in Tuniq, the language Luniq is adequate, since it is equivalent in expressive power to L
+.

Lemma 2.1 [Halpern 2000] In Tuniq and Trec*, the language* L
+ and Luniq *are expressively equivalent;*
for every formula ϕ ∈ L+*, we can effectively find a formula* ϕ
′ ∈ Luniq *such that* Tuniq |= ϕ ⇔ ϕ
′.

The equivalence described in Lemma 2.1 no longer holds when reasoning about causality in the more general class T of structures. However, since I focus in this paper on Trec and Tuniq, in the rest of the paper I consider the language Luniq; this suffices to make my points.