# Definition of Boolean truth value and its expression in meta theory.

In Bell's set theory book, the statement 'the axiom scheme of separation is true in $$V^{B}$$(Boolean valued model) for any complete Boolean algebra $$B$$' is proved in $$ZFC$$ by fixing arbitrary formula $$\phi$$ and showing $$\forall u\exists v\forall x[x\in v \iff x\in u \land\phi(x)]$$ is true in $$V^{B}$$.

And he says that $$ZFC$$ cannot completely formalize the construction of the Boolean value $$\Vert{\sigma}\Vert^{B}$$ for arbitrary sentence $$\sigma$$.

My question is, how can I express the above statement in first order arithmetic($$PA$$)?

I wish to express in $$PA$$ that if $$\phi(x)$$ is a formula in which $$v$$ is not free, then $$ZFC\vdash\Vert\forall u\exists v\forall x[x\in v \iff x\in u \land\phi(x)]\Vert=1$$

But I don't know whether $$\Vert\forall u\exists v\forall x[x\in v \iff x\in u \land\phi(x)]\Vert$$ can be expressed for arbitrary $$\phi$$ in the meta theory $$PA$$.

There is no difficulty expressing $$\Vert\forall u\exists v\forall x[x\in v \iff x\in u \land\phi(x)]\Vert$$ in the metatheory. Specifically, you can write down an algorithm that takes a formula $$\sigma$$ in the language of ZFC and outputs a formula $$\varphi$$ in the language of ZFC that defines (with $$B$$ as a parameter) $$\Vert{\sigma}\Vert^{B}$$ (that is, $$\Vert{\sigma}\Vert^{B}$$ is the unique $$x$$ such that $$\varphi(x,B)$$). This is just the usual definition of $$\Vert{\sigma}\Vert^{B}$$ by recursion on formulas.
What ZFC cannot formalize is that ZFC cannot define a function that takes a formula $$\sigma$$ as an input and outputs the value of $$\Vert{\sigma}\Vert^{B}$$. It can take $$\sigma$$ and output a formula that defines this value, but it can't actually evaluate this defining formula to get a value of $$B$$. This is an instance of the non-definability of truth: ZFC can't define a function that takes a formula $$\varphi$$ and outputs the unique set that $$\varphi$$ defines (if $$\varphi$$ defines a unique set), because ZFC can't define what it means for a set to satisfy $$\varphi$$. This is not a problem for expressing a purely syntactic statement like $$ZFC\vdash\Vert\forall u\exists v\forall x[x\in v \iff x\in u \land\phi(x)]\Vert=1$$, though, since this only requires a formula that defines $$\Vert\forall u\exists v\forall x[x\in v \iff x\in u \land\phi(x)]\Vert$$ in the language of set theory.