Explicit construction of the transitive closure in the Boolean valued model

Question

Suppose $t\in M^B$ is an element of the Boolean valued model. Since $ZF\vdash\exists$x x=TC({$Val_G(t)$}), there is $s\in M^B$ such that $1\Vdash Val_G(s)$=TC({$Val_G(t)$}). Is it possible to construct $s$ explicitly?

Answer 1

The boolean-valued model satisfies $\sf ZFC$, so you can expect in some sense to perform set theoretical constructions inside the model. As for extracting a name to witness $\Vert \exists x \varphi(x)\Vert=1$, there is indeed some risk that choice is required (even if the proof of $\exists x\varphi(x)$ can be done in $\sf ZF$). However, when we have $\Vert \exists! x\varphi(x)\Vert = 1,$ it doesn't require any choice to extract a witness.

This is given as exercise 1.29 in John Bell's boolean-valued model book. The answer is given as a hint, with the proof left up to the reader: Say $\Vert \exists ! x\varphi(x)\Vert = 1$ and let $\alpha$ be the least ordinal such that $\bigvee_{x\in V^B_\alpha}\Vert\varphi(x)\Vert = 1.$ Then define $u\in V^B$ by $\operatorname{dom}(u)= V_\alpha^B$ and $u(z) = \Vert\exists y(\varphi(y)\land z\in y)\Vert.$ We have $\Vert\varphi(u)\Vert = 1.$

So, in the case like trcl (but much more generally), where we have a definable class function in $\sf ZF$ (i.e. $\sf ZF\vdash \forall x\exists!y\varphi(x,y)$), we know that $\Vert \forall x\exists! y\varphi(x,y)\Vert=1$, and a similar construction to the above shows (without using AC) that for any $u\in V^B$ there is a (canonically definable) $v\in V^B$ such that $\Vert \varphi(u,v)\Vert = 1.$

Answer 2

Let me give a possible construction for a name for the transitive closure although I will not give the precise proof for why it works. We know that $$\operatorname{TC}(a) = \textstyle \bigcup \{\bigcup^n a \mid n<\omega\}.$$ Let us mimic this definition with Boolean-valued names.

For a given $B$-name $\sigma$, let us consider the name $\mathsf{union}(\sigma)$ with the domain $$\{\tau \mid \exists \upsilon \in \operatorname{dom} \sigma[\tau \in\operatorname{dom}\upsilon]\}$$

with the Boolean value

$$(\mathsf{union}(\sigma))(\tau) = \textstyle \sum \{\sigma(\upsilon)\cdot \upsilon(\tau) \mid \tau\in\operatorname{dom}\upsilon, \upsilon \in \operatorname{dom} \sigma\}.$$

You can see that $$\| \mathsf{union}(\sigma)=\bigcup \sigma\|=1$$ for every $B$-name $\sigma$. Then consider the name $\mathsf{tc}(\sigma)$ given as follows:

• The domain of $\mathsf{tc}(\sigma)$ is the union of all $\operatorname{dom}\mathsf{union}^n(\sigma)$ for all $n<\omega$, where $\mathsf{union}^n(\sigma)$ is the name obtained from $\sigma$ by applying $\mathsf{union}$ $n$ times.
• For each $\tau\in\operatorname{dom}\mathsf{tc}(\sigma)$, define $$(\mathsf{tc}(\sigma))(\tau) = \textstyle \sum \{\mathsf{union}^n(\tau) \mid \tau \in\operatorname{dom}\mathsf{union}^n(\sigma)\}.$$