Proof. By Fact 2.1, the events $[\![ \varphi (f,\vec g)]\!] $ approximate $[\![ \exists x\varphi (x,\vec g)]\!] $ arbitrarily well from within; the result now follows from the assumption that $\varphi (x,\vec y)$ is $\mathbf {d}$ -computable with respect to $(\mathcal {M}^{[0,1)})^\#$ .

Proof. Suppose $\vec x=(x_1,\ldots ,x_n)$ and consider a tuple $\vec f=(f_1,\ldots ,f_n)$ of special points of $(\mathcal {M}^{[0,1)})^\#$ . Write $f_i=\sum _j a_{ij}\chi _{I_{ij}}$ . Set

$$ \begin{align*}X:=\{(j(1),\ldots,j(n)) \ : \ \mathcal M\models \varphi(a_{1j(1)},\ldots,a_{nj(n)}\};\end{align*} $$

since $\mathcal M^\#$ is computable, we see that X can be computed from $\varphi $ and $\vec f$ ; it then follows that $\mu [\![ \varphi (\vec f)]\!] =\sum _{(j(1),\ldots ,j(n))\in X}\mu (I_{1j(1)}\cap \cdots \cap I_{nj(n)})$ , which can then be effectively approximated.

Proof. This follows immediately from Propositions 3.1 and 3.2.

Proof. If $\mathcal M$ has a decidable presentation, then the induced presentation on $\mathcal {M}^{[0,1)}$ is aware by Lemma 2.5 and computable by Corollary 3.4.

Conversely, suppose that $(\mathcal {M}^{[0,1)})^\#$ is a computable aware presentation of $\mathcal {M}^{[0,1)}$ . By Proposition 2.10, we may assume that $(\mathcal {M}^{[0,1)})^\#$ is the presentation induced by a presentation $\mathcal {M}^\#$ of $\mathcal {M}$ . In order to show that $\mathcal {M}^\#$ is decidable, fix an arbitrary formula $\varphi (\vec x)$ and tuple $\vec a$ of generated points of $\mathcal {M}^\#$ . Since $\vec a$ can also be construed as a tuple of generated points of $(\mathcal {M}^{[0,1)})^\#$ (and whose $(\mathcal {M}^{[0,1)})^\#$ -indices can be computed from their $\mathcal {M}^\#$ -indices), we can approximate $\mu [\![ \varphi (\vec a)]\!] $ to within $1/2$ ; since the value of $\mu [\![ \varphi (\vec a)]\!] $ is either $1$ or $0$ , depending on whether or not $\mathcal {M}\models \varphi (\vec a)$ , this allows us to decide the latter statement.

Question 3.6. Can one drop the “awareness” assumption in the previous theorem?

Proof. Suppose that $B(f;\epsilon )$ is a rational open ball and a is a generated point of $\mathcal {M}$ with corresponding formula $\varphi _a(x)$ . One then proceeds to approximate $\mu [\![ \varphi _a(\vec f)]\!] $ ; if one finds that this measure exceeds $1-\epsilon $ , this implies that $f(\omega )=a$ for a set of $\omega $ ’s of measure at least $1-\epsilon $ , that is, $d(f,a)<\epsilon $ , whence one returns this ball $B(f;\epsilon )$ as intersecting $\mathcal {M}$ .

Proof. Suppose that $\psi _p(B, \vec A)<\dfrac {\epsilon }{n}$ . For each $i=1,\dots ,n$ , do the following:

1. i) If $\mu (B\cap A_1^{i(1)}\cap \dots \cap A_m^{i(m)})-r_i>0$ , set

   $$ \begin{align*}B_i'=(B\cap A_1^{i(1)}\cap\dots\cap A_m^{i(m)})\backslash D_i,\end{align*} $$

   where $D_i\kern1.3pt{\subseteq}\kern1.3pt B\cap A_1^{i(1)}\cap \dots \cap A_m^{i(m)}$ and $\mu (D_i)\kern1.3pt{=}\kern1.3pt\mu (B\kern1.3pt{\cap}\kern1.3pt A_1^{i(1)}\cap \dots \cap A_m^{i(m)}) \kern1.3pt{-}\kern1.3pt r_i.$

2. ii) If $\mu (B\cap A_1^{k_1(i)}\cap \dots \cap A_m^{k_m(i)})-r_i<0$ , set

   $$ \begin{align*}B_i'=(B\cap A_1^{i(1)}\cap\dots\cap A_m^{i(m)})\cup D_i,\end{align*} $$

   where $D_i\subseteq A_1^{i(1)}\cap \dots \cap A_m^{i(m)}$ , $D_i\cap (B\cap A_1^{i(1)}\cap \dots \cap A_m^{i(m)})=\emptyset $ , and $\mu (D_i)=r_i-\mu (B\cap A_1^{i(1)}\cap \dots \cap A_m^{i(m)}).$

3. iii) If $\mu (B\cap A_1^{i(1)}\cap \dots \cap A_m^{i(m)})-r_i=0$ , set

   $$ \begin{align*}B_i'=B\cap A_1^{i(1)}\cap\dots\cap A_m^{i(m)}.\end{align*} $$

Set $B'=\displaystyle \bigcup _{i=1}^nB_i'\in \mathcal {B}([0,1))$ . By construction, $B'$ realizes p. Furthermore, note that

$$ \begin{align*}d(B,B')=\sum_{i=1}^nd\left(B\cap A_1^{i(1)}\cap\dots\cap A_m^{i(m)}, B_i'\right)<\epsilon.\end{align*} $$

Proof. Let $\mathcal {G}$ denote the set of generated points of $\mathcal {B}([0,1))^\#$ . Let $\Omega $ denote the set of realizations of p, so $\Omega =\{E\in \mathcal {B}([0,1))\ : \ \psi _p(E,\vec A)=0\}.$ We now describe an algorithm which enumerates all pairs $(C,\epsilon )$ , where $C\in \mathcal G$ and $\epsilon>0$ is rational, for which $B(C,\epsilon )\cap \Omega \neq \emptyset $ .

We first note that, since $\vec A$ is computable, given rational $\delta>0$ , one can compute a tuple of generated points $\vec A_\delta $ such that $d(\vec A,\vec A_\delta )<\Delta _{\psi _p}(\delta )$ Footnote ⁵ , and thus, for every $C\in \mathcal G$ , we have $|\psi _p(C,\vec A)-\psi _p(C,\vec A_\delta )|<\delta .$

Here is the desired algorithm: for each pair $(C,\epsilon )$ as above, we infinitely often return to considering this pair by searching for $D\in \mathcal G$ and rational $\delta>0$ such that $d(C,D)<\epsilon $ and $\psi _p(D,\vec A_\delta )+\delta <(\epsilon -d(C,D))/2^{|\vec A|}.$ Note that we can indeed effectively approximate $\psi _p(D,\vec A_\delta )$ since the presentation is computable.

First suppose we find such D and $\delta $ ; we need to know that $B(C,\epsilon )\cap \Omega \not =\emptyset $ . We know that $\psi _p(D,\vec A)<(\epsilon -d(C,D))/2^{|\vec A|}$ and thus, by Lemma 4.1, there is $D'\in \Omega $ such that $d(D,D')<\epsilon -d(C,D)$ ; it follows that

$$ \begin{align*}d(C,D')\leq d(C,D)+d(D,D')<\epsilon\end{align*} $$

and so $D'\in B(C,\epsilon )\cap \Omega $ .

We now need to verify that if $B(C,\epsilon )\cap \Omega \not =\emptyset $ , then this algorithm will eventually let us know this fact. Take $E\in B(C,\epsilon )\cap \Omega $ . Since $\psi _p(E,\vec A)=0$ , there is $D\in \mathcal G$ such that $d(C,D)<\epsilon $ and $\psi _p(D,\vec A)<\eta /2^{|\vec A|}$ for rational $\eta <\epsilon -d(C,D)$ ; it follows that, for sufficiently small $\delta $ , that $\psi _p(D,\vec A_\delta )+\delta <\epsilon -d(C,D)$ and our search will succeed.

Note finally that the uniformity statement holds by the description of the algorithm.

Fact 4.3. Suppose that ${\mathcal {N}}^\#$ is a computable presentation of a metric structure ${\mathcal {N}}$ . Then every nonempty c.e. closed subset X of ${\mathcal {N}}^\#$ contains a computable point; moreover, an index for the computable point can be computed from an index for X.

Proof. Fix computable presentations $\mathcal {B}([0,1))^\#$ and $\mathcal {B}([0,1))^\dagger $ of $\mathcal {B}([0,1))$ . Let $(A_n)$ and $(B_n)$ be effective enumerations of the generated points of $\mathcal {B}([0,1))^\#$ and $\mathcal {B}([0,1))^\dagger $ , respectively. We effectively build a sequence $(\phi _n)$ of partial elementary maps from $\mathcal {B}([0,1))$ to $\mathcal {B}([0,1))$ , where each domain is finite and such that:

• • For each n, $\phi _n\subseteq \phi _{n+1}$ .

• • If $n=2s$ , then $A_s$ is in the domain of $\phi _n$ .

• • If $n=2s+1$ , then $B_s$ is in the range of $\phi _n$ .

• • The domain of $\phi _n$ is a finite tuple of $\mathcal {B}([0,1))^\#$ -computable points, and the codes of these points can be computed from n.

• • The range of $\phi _n$ is a finite tuple of $\mathcal {B}([0,1))^\dagger $ -computable points, and the indices of these points can be computed from n.

Suppose that $\phi _{n-1}$ has been defined. We treat only the case $n=2s$ , the other case being handled similarly. Let $\{C_1,\ldots ,C_{n-1}\}$ denote the domain of $\phi _{n-1}$ . Let $p_0(x)=\operatorname {tp}(A_s/\vec C)$ and let $p(x):=\phi _{n-1}(p_0)$ ; in other words, $p\in S_1(\phi _{n-1}(\vec C))$ is the type determined by the formula $\psi _p(x)$ obtained by replacing each occurrence of $C_i$ with $\phi _{n-1}(C_i)$ ; since $\phi _{n-1}$ is partial elementary, p is indeed a consistent type. Note also that the real numbers in $\psi _p$ are computable, and their indices can be computed from n and indices for $C_1,\ldots ,C_{n-1}$ , which, by induction, are computable from $n-1$ . By countable saturation, p is realized in $\mathcal {B}([0,1))$ . By Lemma 4.2 and Fact 4.3, we can compute the index of a $\mathcal {B}([0,1))^\dagger $ -computable point D that realizes p, and we define $\phi _n:=\phi _{n-1}\cup \{(A_s,D)\}$ .

Set $\Phi _0:=\bigcup _n \phi _n$ . Then $\Phi _0$ is a partial elementary map from $\mathcal {B}([0,1))$ to $\mathcal {B}([0,1))$ with dense domain and range. It follows that $\Phi _0$ extends to an automorphism $\Phi $ of $\mathcal {B}([0,1))$ . Moreover, by construction, the $\Phi $ -image of each $\mathcal {B}([0,1))^\#$ -rational point is uniformly $\mathcal {B}([0,1))^\dagger $ -computable, whence $\Phi $ is a computable isomorphism.

Proof. Suppose a restricted formula $\varphi (\vec x)$ and rational $\epsilon>0$ are given. First note that the procedure for converting a restricted formula into an equivalent restricted formula in prenex normal form is effective (see [Reference Ben Yaacov, Berenstein, Henson and Usvyatsov3, Proposition 6.9]), whence we may assume that $\varphi $ is itself in prenex normal form. Write

$$ \begin{align*}\varphi(\vec x)=Q_1y_1\cdots Q_my_m \psi(\vec x,\vec y)\end{align*} $$

with $\psi (\vec x,\vec y)$ a quantifier-free restricted formula. By assumption, we may find a quantifier-free restricted formula $\psi _1(\vec x,y_1,\ldots ,y_{m-1})$ such that

$$ \begin{align*}\|Q_my_m\psi(\vec x,y_1,\ldots,y_{m-1},y_m)-\psi_1(\vec x,y_1,\ldots,y_{m-1})\|_T<\frac{\epsilon}{m}.\end{align*} $$

Similarly, one can find a quantifier-free restricted formula $\psi _2(\vec x,y_1,\ldots ,y_{m-2})$ such that

$$ \begin{align*}\|Q_{m-1}y_{m-1}\psi_1(\vec x,y_1,\ldots,y_{m-2},y_{m-1})-\psi_2(\vec x,y_1,\ldots,y_{m-2})\|_T<\frac{\epsilon}{m}.\end{align*} $$

Continuing in this way, we obtain a sequence of quantifier-free restricted formula $\psi _1(\vec x,y_1,\ldots ,y_{m-1}),\ldots ,\psi _m(\vec x)$ . It follows that $\|\varphi (\vec x)-\psi _m(\vec x)\|_T<\epsilon $ .

Proof. Given a restricted function v, find $n\in \mathbb N$ such that

$$ \begin{align*}2^{-n}<\min(\Delta_u(\epsilon/6),\Delta_v(\epsilon/6)).^8\end{align*} $$

For each $k=1,\ldots ,2^n$ , find open intervals $I_k,J_k\subseteq [0,1]$ with rational endpoints of length at most $\epsilon /6$ such that $u(k/2^n)\in I_k$ and $v(k/2^n)\in J_k$ . The algorithm then checks if

$$ \begin{align*}\max\{|s-s'| \ : \ s\in I_k,s'\in J_k\}<\epsilon/2; \quad (\dagger)\end{align*} $$

if the answer is yes, then the algorithm returns $\nu $ as the desired restricted function. To see that $\nu $ is as claimed, note that, for any $x\in [k/2^n,(k+1)/2^n)$ , we have

$$ \begin{align*}|u(x)-v(x)|&\leq |u(x)-u(k/2^n)|+|u(k/2^n)-v(k/2^n)|+|v(k/2^n)-v(x)|\\ &\leq 5\epsilon/6<\epsilon.\end{align*} $$

Also note that, if $\nu $ is such that $\|u-v\|_\infty <\epsilon /6$ , then indeed $(\dagger )$ above holds, so the algorithm always terminates.

Proof. Let T denote the theory of atomless probability algebras. We apply the test described in Lemma 5.3. Suppose that $\varphi (x,\vec y)$ and $\epsilon>0$ are given. Write $\vec y=(y_1,\ldots ,y_n)$ . Without loss of generality, we may write

$$ \begin{align*}\varphi(x,\vec y)=u((\mu(x\cap \vec y^k)_{k\in 2^n})),\end{align*} $$

where $u:[0,1]^{2^n}\to [0,1]$ is a restricted function and $\vec y^k:=y_1^{k(1)}\cap \cdots \cap y_n^{k(n)}$ . We then have that $\inf _x\varphi (x,\vec y)$ is equivalent to $\min (u)((\mu (\vec y^k)_{k\in 2^n}))$ . By Lemma 5.6, we can compute a code for $\min (u)$ from a code for u; by Lemma 5.5, we can then compute a restricted function v such that $\|\min (u)-v\|_\infty <\epsilon $ . It follows that $\|\inf _x\varphi (x,\vec y)-v((\mu (\vec y^k))_{k\in 2^n})\|_T<\epsilon $ .

Proof. We follow the proofs of [Reference Ben Yaacov, Berenstein, Henson and Usvyatsov3, Theorem 9.17 and Proposition 9.19], just noting that they hold in this more general setting and that they hold effectively. Take a continuous, non-decreasing function $\alpha :[0,1]\to [0,1]$ with $\alpha (0)=0$ such that $|\psi (\vec a,\vec b)-\psi (\vec a',\vec b)|\leq \alpha (d(\vec a,\vec a'))$ for all $\vec a,\vec a',\vec b\in {\mathcal {N}}$ . Note that if $\psi $ is restricted, then $\alpha $ is computable and a code for $\alpha $ can be computed from a code for the modulus of uniform continuity of $\psi $ (see [Reference Goldbring and Hart8, Section 2]), which in turn can be computed from a code for $\psi $ by Lemma 5.4 above. Since $\varphi $ defines a definable family of definable subsets of ${\mathcal {N}}$ , there is a continuous, non-decreasing function $\beta :[0,1]\to [0,1]$ such that $\beta (0)=0$ and such that, for all $\vec a,\vec b\in {\mathcal {N}}$ , one has $d(\vec a,Z(\varphi (\vec x, \vec b)))\leq \beta (\varphi (\vec a,\vec b))$ . As in the previous sentence, if $\Delta $ is computable, then a code for $\beta $ can be computed from a code for $\Delta $ .

Consider the formula $\Phi (\vec x,\vec y)=\inf _{\vec x'}\min (\beta (\varphi (\vec x',\vec y))+d(\vec x,\vec x'),1)$ . Then for any $\vec b\in {\mathcal {N}}$ , one has $\Phi (\vec a,\vec b)=d(\vec a,Z(\varphi (\vec x,\vec b)))$ . Finally, set

$$ \begin{align*}\zeta(\vec y,\vec z)=\inf_{\vec x}\left(\psi(\vec x,\vec y,\vec z)+\alpha(\Phi(\vec x,\vec y))\right).\end{align*} $$

One checks as in [Reference Ben Yaacov, Berenstein, Henson and Usvyatsov3, Theorem 9.17] that $P(\vec b,\vec c)=\zeta (\vec b,\vec c)^{\mathcal {N}}$ for all $\vec b,\vec c\in {\mathcal {N}}$ .

Setting $\Lambda (\vec x,\vec x',\vec y)$ to be the quantifier-free portion of $\Phi $ , we have that $\Phi (\vec x,\vec y)$ is equivalent to the formula

$$ \begin{align*}\inf_{\vec x}\inf_{\vec x'}(\psi(\vec x,\vec y,\vec z)+\alpha(\Lambda(\vec x,\vec x',\vec y)).\end{align*} $$

As a result, if $\varphi $ and $\psi $ are quantifier-free, then $\zeta $ is an existential formulae with $2|\vec x|$ many existential quantifiers. If $\beta $ is computable and $\varphi $ is quantifier-free, then by Lemma 5.5, one can effectively approximate $\Lambda $ by restricted quantifier-free formulae. Another application of Lemma 5.5 shows that if $\psi $ is also quantifier-free and $\alpha $ is computable, then $\zeta $ can be effectively approximated by restricted quantifier-free formulae, uniformly in codes for $\alpha $ and $\psi $ , completing the proof of the proposition.

Fact 5.10. Let $\theta _i(x,\vec {y})$ , $i=1,\dots ,n$ be a sequence of L-formulas such that

$$ \begin{align*}\models(\theta_1\vee\dots\vee\theta_n)\text{ and }\models\neg(\theta_i\wedge\theta_j)\text{ for }1\leq i<j\leq n.\end{align*} $$

Consider a Borel randomization $\mathcal {M}^{[0,1)}$ of an L-structure $\mathcal M$ . Fix $B_1,\dots ,B_n\in \mathcal {B}$ and random variables $\vec {f}\in \mathcal {K}$ . Then the following are equivalent:

1. i) There exists a random variable $g\in \mathcal K$ such that, for each $i=1,\ldots n$ , we have

   $$ \begin{align*}B_i=[\![\theta_i(g,\vec{f})]\!].\end{align*} $$

2. ii) The events $B_1,\ldots ,B_n$ form a partition of $\top $ and, for each $i=1,\ldots ,n$ , we have

   $$ \begin{align*}B_i\subseteq[\![\exists x\theta_i(x,\vec{f})]\!].\end{align*} $$

Proof. Given $\epsilon>0$ , we will show that, for any tuple of events $\vec E$ and tuple $\vec f$ from sort $\mathcal K$ , if

$$ \begin{align*}\Phi(\vec E,\vec f)<n\epsilon/4(n+1)^2,\end{align*} $$

then $d\left (\vec E,Z(\Phi (\cdot ,\vec f))\right )<\epsilon .$ We leave it to the reader to check that, in what follows, we may assume, without loss of generality, that $\vec f$ is a tuple of random variables; indeed, this follows from a simple continuity argument.

Step 1: Fix $\delta>0$ and take $\eta <(n/(n+1))\delta $ . For any $\eta $ -partition $\vec E$ , that is, a tuple $\vec E$ such that

$$ \begin{align*}\max\left(\sum_{i=1}^m\mu(E_i)\dot-\mu(\bigcup_{i=1}^m E_i),1\dot-\mu(\bigcup_{i=1}^m E_i)\right)<\eta,\end{align*} $$

there is a partition $\vec V$ such that $d(\vec E,\vec V)<\delta $ .

To establish step 1, let $N=2^n$ and for each $k=1,\dots ,N$ , consider all the possible events given by

$$ \begin{align*}E_1^{k(1)}\cap\dots\cap E_n^{k(n)},\end{align*} $$

where each $k:\{1,\dots ,n\}\to \{0,1\}$ , $E_i^0=\neg E_i$ , and $E_i^1=E_i$ . For each $k=1,\dots ,N,$ set

$$ \begin{align*}\Gamma(k)=\{i\in\{1,\dots,n\}\ : \ k(i)=1\}.\end{align*} $$

If $\Gamma (k)\neq \emptyset $ , let $\{V_i^k\}_{i\in \Gamma (k)}$ be a “fair” (measurable) partition of $E_1^{k(1)}\cap \dots \cap E_n^{k(n)}$ , that is, for each $i\in \Gamma (k)$ , we have

$$ \begin{align*}\mu(V_i^k)=\dfrac{\mu(E_1^{k(1)}\cap\dots\cap E_n^{k(n)})}{|\Gamma(k)|}.\end{align*} $$

If $\Gamma (k)=\emptyset $ , let $W_1,\dots ,W_n$ be a fair partition of $E_1^0\cap \dots \cap E_n^0$ . For each $i=1,\ldots , n$ , define

$$ \begin{align*}V_i=\left(\bigcup_{\{k\ \ : \ i\in \Gamma(k)\}}V_i^k\right)\cup W_i.\end{align*} $$

By construction, $\vec V$ form a partition of $\top $ . We now show that $d(\vec E,\vec V)<\delta .$ First note that, by construction, for each $i=1,\dots ,n$ , we have $V_i\backslash W_i\subset E_i$ and $E_i\cap W_i=\emptyset $ , and thus

$$ \begin{align*}d(E_i,V_i)&=\mu(E_i\backslash(V_i\backslash W_i))+\mu(W_i)\\&=\mu\left(E_i\backslash\bigcup_{\{k\ |\ i\in \Gamma(k)\}}V_i^k\right)+\mu(W_i).\end{align*} $$

Since $1-\mu (\bigcup _{i=1}^n E_i)<\eta $ , then $\mu (W_i)<\eta /n$ . In the same way, since

$$ \begin{align*}E_i\backslash\bigcup_{\{k\ |\ i\in \Gamma(k)\}}V_i^k\subset\bigcup_{\ell=1,\ell\neq i}^n(E_i\cap E_\ell)\subset\bigcup_{i\neq j}(E_i\cap E_j)\end{align*} $$

and

$$ \begin{align*}\mu\left(\bigcup_{i=1}^n E_i\right)+\mu\left(\bigcup_{i\neq j}(E_i\cap E_j)\right)\leq \sum_{i=1}^n\mu(E_i),\end{align*} $$

we have $\mu \left (\bigcup _{i\neq j}^n(E_i\cap E_j)\right )<\eta $ and so

$$ \begin{align*}\mu\left(E_i\backslash\bigcup_{\{k\ |\ i\in \Gamma(k)\}}V_i^k\right)<\eta.\end{align*} $$

Consequently,

$$ \begin{align*}d(E_i,V_i)<\eta+\eta/n<\delta,\end{align*} $$

and $d(\vec E,\vec V)<\delta $ as desired.

Step 2: Fix $\epsilon>0$ , take $\delta <\epsilon /(4(n+1))$ and $\eta <(n/(n+1))\delta $ . Let $\vec E$ be such that $\Phi (\vec E,\vec f)<\eta $ . Since $\vec E$ is an $\eta $ -partition, by Step 1, there is a partition $\vec V$ such that $d(\vec E,\vec V)<\delta $ . We now show how to find $\vec B$ such that $\Phi (\vec B,\vec f)=0$ and $d(\vec V,\vec B)< \epsilon /2$ , whence $d(\vec E,\vec B)<\epsilon $ , as desired.

First note that, since for each $i=1,\dots ,n$ , $\mu (E_i)\dot -\mu (E_i\cap [\![ \exists x\theta _i(x,\vec f)]\!] )<\eta $ , we have:

$$ \begin{align*}\mu(V_i\cap [\![\neg\exists x\theta_i(x,\vec f)]\!])&=\mu((V_i\cap E_i)\cap [\![\neg\exists x\theta_i(x,\vec f)]\!])\\ & \quad+\mu((V_i\setminus E_i)\cap [\![\neg\exists x\theta_i(x,\vec f)]\!])<\eta+\delta.\end{align*} $$

Now for each $i=1,\dots ,n$ , set

$$ \begin{align*}\Sigma(i)=\{ j\in\{1,\dots,n\}\ |\ (V_i\cap[\![\neg\exists x\theta_i(x,\vec f)]\!])\cap[\![\exists x\theta_j(x,\vec f)]\!]\neq \emptyset\}.\end{align*} $$

If $\Sigma (i)\neq \emptyset $ , let $\{B_j^i\}_{j\in \Sigma (i)}$ be a partition of $V_i\cap [\![ \neg \exists x\theta _i(x,\vec f)]\!] $ such that, for all $j\in \Sigma (i)$ , we have $B_j^i\subseteq [\![ \exists x\theta _j(x,\vec f)]\!] $ . For $k=1,\ldots ,n$ , set

$$ \begin{align*}B_k:=(V_k\cap[\![\exists x\theta_k(x,\vec f)]\!])\cup\bigcup_{\{i\ |\ k\in\Sigma(i)\}}B_k^i.\end{align*} $$

By construction, $\Phi (\vec B,\vec f)=0$ . Now, note that for each $j=1,\dots ,n$ , we have

$$ \begin{align*}d(V_j,B_j)=\mu(V_j)\dot-\mu(V_j\cap[\![\exists x\theta_j(x,\vec f)]\!])+\sum_{\{i\ |\ j\in\Sigma(i)\}}\mu(B_j^i)\end{align*} $$

$$ \begin{align*}<(\delta+\eta)+n(\delta+\eta)<2(n+1)\delta<\epsilon/2\end{align*} $$

and thus $d(\vec V,\vec B)<\epsilon /2$ , as desired.

Proof of Theorem 5.2.

We apply the test from Lemma 5.3. Towards that end, suppose we are given an existential restricted $L^R$ -formula $\varphi (\vec X,\vec A)$ , where $\vec X$ is a tuple of variables of sort $\mathcal K$ and $\vec A$ is a tuple from sort $\mathcal B$ . If $\varphi $ has the form $\inf _C \psi (\vec X,\vec A,C)$ , where C ranges over $\mathcal B$ , then by (the proof of) effective quantifier-elimination for atomless probability algebras, we can effectively approximate $\varphi $ by quantifier-free restricted formulae.

We thus assume that $\varphi $ is an existential formula in $L^R$ of the form

$$ \begin{align*}\displaystyle\inf_X\psi_1(X,\vec{Y},\vec{A}),\end{align*} $$

where $\psi _1$ is a quantifier-free formula in $L^R$ and $X,\vec {Y}$ are variables in sort $\mathcal {K}$ and $\vec {A}$ are variables in sort $\mathcal {B}$ . The variable X occurs in $\psi _1$ in finitely many terms $[\![ \varphi _i(X,\vec {Y})]\!] $ , $i\leq m$ of sort $\mathcal {B}$ , where each $\varphi _i(x,\vec {y})$ is an $\mathcal {L}$ formula. Let $\theta _j(x,\vec {y})$ for $j\leq n=2^m$ be the list of all possible conjunctions

$$ \begin{align*}\varphi_1^{k(1)}\wedge\dots\wedge\varphi_m^{k(m)}\end{align*} $$

where each $k:\{1,\dots ,n\}\to \{0,1\}$ , $\varphi _i^0=\neg \varphi _i$ and $\varphi _i^1=\varphi _i$ for all $i\leq m$ . So using Boolean Axioms, the formula $\psi _1$ is equivalent to a quantifier-free $\psi _2$ in which the variable X occurs only in terms $[\![ \theta _j(X,\vec {Y})]\!] $ . Let $\psi _3(\vec Y,\vec A,\vec B)$ be quantifier-free formula obtained from $\psi _2$ by replacing each term $[\![ \theta _j(X,\vec {Y})]\!] $ by a new variable $B_j$ of sort $\mathcal {B}$ .

Note that the variable X does not occur in $\psi _3$ , and now $\varphi $ is equivalent to

$$ \begin{align*}\inf\{\psi_3(\vec{Y},\vec{A},\vec{B}) \ : \ \Phi(\vec B,\vec Y)=0\}.\end{align*} $$

By Proposition 5.9, this latter expression is effectively approximable by formulae of the form $\inf _{\vec B}\chi (\vec Y,\vec A,\vec B)$ with $\chi $ a restricted quantifier-free formula. However, we already know from the first case that such existential formulae can themselves be effectively approximated by quantifier-free restricted formulae, finishing the proof of the theorem.