A formalization of forcing and the unprovability of the continuum hypothesis
I'm pleased to announce that the Flypitch project has passed a major milestone: we have completed a formalization of the unprovability of the continuum hypothesis from ZFC (by way of forcing with Boolean-valued models). This required implementing, among other things, a deep embedding of first-order logic with a proof system, the Godel completeness theorem, Boolean-valued semantics for first-order logic, a Boolean-valued soundness theorem, constructing a Boolean-valued model of ZFC, and some delicate transfinite combinatorics.
A draft of our paper describing this result is available here. It has been submitted to ITP 2019.
Interestingly, in translating the forcing argument to dependent type theory, not much set theory was actually needed do forcing. We didn't even need to start with an existing standard model or end up with a two-valued model of ZFC. It turns out that the commonly-used Aczel-Werner encoding of ZFC into (dependent type theory + calculus of inductive constructions) is actually a special case of the recursive name-construction from forcing, which allowed us to easily construct forcing extensions—as long as one is willing to work in a many-valued logic; otherwise, you have to carry a generic filter around to collapse the names into a two-valued model.
Since one can also use forcing to show the consistency of CH, and we have already set up much of the required infrastructure, I expect that we will soon have a complete formal proof of the independence of the continuum hypothesis.
Our formalization is in the Lean theorem prover, which implements a hierarchy of type universes to handle proper classes. Our construction for Boolean-valued models of set theory is universe-polymorphic—it takes a type universe and constructs a model of set theory one universe level up. Every conceivable forcing argument can be carried out at the bottom level of the universe hierarchy Type 0, and each new model of set theory lives in the next universe of types Type 1, and thus informs the structure of any models of set theory formed from Type 1, which live in Type 2, and so on. To me, this is a striking illustration of the richness of Lean's metatheory (in a way, unsurprising, since it is mutually interpretable with ZFC + countable many inaccessibles).
I should mention that forcing with Boolean-valued models is very close in spirit to forcing using double-negation sheaves. Lean's category theory library is not quite ready to handle involved arguments about sheaves on sites, but it is under heavy development, and it is conceivable that we could soon have a formalization of Kripke-Joyal semantics, after which it will be easy, given our existing work, to complete the sheaf-theoretic forcing argument for negating CH (again, with no need to perform the cumulative hierarchy construction to extract an actual model of ZFC—the soundness theorem for intuitionistic logic implicit in the Kripke-Joyal semantics specialized to a soundness theorem for classical logic in a Boolean topos will be enough.)
