Forcing with random variables in bounded arithmetics and set theory

TL;DR

This paper explores how Boolean-valued random forcing in bounded arithmetics relates to set-theoretic forcing, showing it adds a 'random integer' and analyzing the structure of resulting models.

Contribution

It establishes an isomorphism between the Boolean-valued forcing algebra and a product measure space, connecting bounded arithmetics forcing to classical set theory.

Findings

Forcing adds a 'random integer' to models of bounded arithmetics.

The algebra used in forcing is isomorphic to a product measure space on 2^{ω₁}.

Results on the density and relationship of new and ground-model integers in extensions.

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.