0
$\begingroup$

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$.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.