A saturation property of structures obtained by forcing with a compact family of random variables (Q1935366)

The paper presents a framework for building Boolean-valued models with a certain amount of saturation. The models are constructed using the method of forcing with random variables introduced in [\textit{J. Krajíček}, Forcing with random variables and proof complexity. Cambridge: Cambridge University Press (2011; Zbl 1219.03071)]. The results are motivated by potential applications to independence results for weak systems of arithmetic and computational complexity theory. A notion of saturation for Boolean-valued structures is introduced, and it is shown that if \(L\) is an arithmetically definable language, then, under certain assumptions on the set of random variables \(F\) (\(M\)-finite functions with a fixed infinite domain in an \(\aleph_1\)-saturated model \(M\) of true arithmetic), the resulting Boolean \(L\)-structure \(K(F)\) is saturated with respect to countable sets of open formulas in one variable. A theorem on saturation with respect to sets of existential formulas is derived and an example is given to show that the result fails in the universal case.