Borel conjecture and dual Borel conjecture (Q2862130)

A set of reals \(X\) is called strong measure zero (briefly, smz) if for all functions \(f : \mathbb{N} \to \mathbb{N}\) there are intervals \(I_n\) of measure \(\leq 1/f(n)\) covering \(X\). In 1919, Borel conjectured that every smz set is countable. Borel's conjecture \(\mathsf{BC}\) turned out to be independent of \(\mathsf{ZFC}\), the standard axiomatization of mathematics: Sierpiński showed in 1928 that the Continuum Hypothesis \(\mathsf{CH}\) implies that \(\mathsf{BC}\) does not hold, while in 1976 Laver used a countable support iteration of length \(\omega_2\) of Laver forcing to produce a model of \(\mathsf{ZFC}\) where \(\mathsf{BC}\) holds.NEWLINENEWLINEIn 1973 Galvin, Mycielski and Solovay showed that, as conjectured by Prikry, a set \(X\) is smz if and only if every comeager set contains a translate of \(X\). This allows us to define a notion dual to smz sets: A set of reals \(X\) is called strongly meager (briefly, sm) if every set of Lebesgue measure \(1\) contains a translate of \(X\). The dual Borel conjecture (\(\mathsf{dBC}\)) is then the statement: Every sm set is countable. Also \(\mathsf{dBC}\) turned out to be independent of \(\mathsf{ZFC}\): Prikry noted that \(\mathsf{CH}\) also implies the failure of \(\mathsf{dBC}\), while in 1993 Carlson used a finite support iteration of length \(\omega_2\) of Cohen forcing to produce a model of \(\mathsf{ZFC}\) in which \(\mathsf{dBC}\) is satisfied.NEWLINENEWLINEGiven that \(\mathsf{CH}\) implies the failure of both \(\mathsf{BC}\) and \(\mathsf{dBC}\), it is natural to ask whether it is consistent with \(\mathsf{ZFC}\) that \(\mathsf{BC}\) and \(\mathsf{dBC}\) hold simultaneously. Although Laver's and Carlson's constructions are somewhat incompatible, using different methods, the authors show in this paper that if \(\mathsf{ZFC}\) is consistent then so is \(\mathsf{ZFC}+\mathsf{BC}+\mathsf{dBC}\). This is obtained via a new forcing whose construction is rather technical and involves many new ideas and techniques, including almost finite and almost countable support iterations, ultralaver forcings, and Janus forcings.