1: \begin{definition}

2: Let $X$ be a set of atoms $\{X_1, X_2, X_3, \dots\}$ representing the values of the memory tape variables

3: and let $\mathcal{L}_{\mathrm{prop}}$ be the propositional language formed by closing $X$

4: off under conjunction, disjunction, and negation.

5: 

6: 	Let the intervention specification language $\mathcal{L}_{\mathrm{int}} \subset \mathcal{L}_{\mathrm{prop}}$

7: be the language of

8: purely conjunctive, ordered formulas of unique literals,\footnote{

9: The point being that such formulas are in one-to-one correspondence with specifications of interventions,

10: i.e., finite lists of variables along with the values each is to be held fixed to.

11: } i.e., formulas of the form $l_{i_1} \land \dots \land l_{i_n}$ for some $n \ge 0$, where $i_j < i_{j+1}$ and each $l_{i_j}$ is either $X_{i_j}$ or $\lnot X_{i_j}$.

12: $\top$ abbreviates the ``empty intervention'' formula with $n = 0$.

13: 	Let $\mathcal{L}_{\mathrm{cond}}$ be the conditional language of formulas

14: of the form $\langle\alpha\rangle \beta$ for $\alpha \in \mathcal{L}_{\mathrm{int}}, \beta \in \mathcal{L}_{\mathrm{prop}}$. 

15: 	

16: 	The overall basic language $\mathcal{L}_{\nonprob}$ is the language 

17: 	formed by closing off the formulas of $\mathcal{L}_{\mathrm{cond}}$

18: \footnote{Unlike \cite{ibeling}, we do not

19: admit the basic atoms $X$ as atoms of $\mathcal{L}$. There is no difficulty extending the semantics

20: to such atoms, but allowing them would needlessly complicate the proof of Theorem \ref{soundcomplete}.

21: }

22: under conjunction, disjunction, and negation.

23: \end{definition}