G1が成立する理論のLindenbaum代数はDenseであることは形式化されている. 次のことが成立するので,例えば $\mathsf{PA}$ と $\mathsf{ZF}$ のLindenbaum代数などは全部同型になるという意味でそれほどおもしろくない,という事実を形式化する. > [!NOTE] > 稠密な可算Boolean代数は互いに同型.(この同型はrecursiveに取れる? [Pour-El & Kripke]) 上の事実を形式化する.