Forcing with random variables in bounded arithmetics and set theory

Abstract

We analyse the Boolean-valued random forcing $B_{M,\Omega}$ in bounded arithmetics developed in Krajicek (Forcing with random variables and proof complexity, vol. 382, Cambridge University Press, 2011) from the perspective of the forcing in set theory. We observe that under the assumption that $M$ is a non-standard $\omega_1$-saturated model of true arithmetics of size $\omega_1$, and $\Omega \in M$ is a non-standard number, $B_{M,\Omega}$ is isomorphic to the probability (random) algebra corresponding to the product measure space on $2^{\omega_1}$ (and hence does not depend on $M$ and $\Omega$). Thus, in a well-defined sense, the forcing $B_{M,\Omega}$ adds a "random integer" to the model $M$, using a non-separable algebra corresponding to $2^{\omega_1}$. If $G$ is a generic filter for $B_{M,\Omega}$ over a transitive model of set theory $V$, we naturally define in $V[G]$ two-valued generic extensions $M[G]^{R}$ of $M$ which correspond to Boolean-valued models in Krajicek's book (where $R$ ranges over collections of random variables which function as names for new integers). We study the relationship between the linear order $(M,<)$ and its extensions $(M[G]^R,<)$, proving several results on the extent of the mutual density of new integers in $M[G]^{R}$ and the "ground-model" integers in $M$. At the end, we discuss some advantages and limitations of interpreting forcing in bounded arithmetics (and other weak theories) in the framework of set-theoretic forcing, providing an alternative to an axiomatic approach to forcing in bounded arithmetics formulated by Atserias and M\"uller in Partially definable forcing and bounded arithmetic, Archive for Mathematical Logic 54 (2015), 1-33.