A formalization of forcing and the consistency of the failure of the continuum hypothesis

Abstract:

Forcing is a technique for constructing new models of set theory where certain statements are "forced" to be true or false, e.g. the axiom of choice, or the continuum hypothesis. We describe a formalization of forcing using Boolean-valued models in the Lean 3 theorem prover. As an application of our framework, we specialize our construction to a Boolean completion of the Cohen poset and formally verify in the resulting model the failure of the continuum hypothesis. This is joint work with Floris van Doorn.

Thursday, April 4, 2019 - 12:00

427 Thackeray Hall