力迫的的形式化与连续统假设的不可证明性

我们描述了在 Lean 3 定理证明器中利用布尔值模型对力迫进行的形式化，包括力迫基本定理以及带有布尔值可靠性定理的一阶逻辑深嵌入。作为我们框架的应用，我们将构造特化为 Cantor 空间 $2^{\omega_2 \times \omega}$ 的正则开集布尔代数，并在所得模型中形式化验证了连续统假设的失败。