Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] A milestone for the AFP: Formalization of Forc...

Email Gateway (Aug 23 2022 at 09:04):

From: Lawrence Paulson <lp15@cam.ac.uk>
I’m delighted to announce the first ever AFP entry for Isabelle/ZF. It’s a formalisation of forcing, building on my own ZF-Constructible development from nearly two decades ago. Working in Isabelle/ZF is tough (no sledgehammer, no nitpick, not even linarith), so this is doubly impressive!

We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct a proper generic extension and show that the latter also satisfies ZFC.

It’s online at https://www.isa-afp.org/entries/Forcing.html

Larry

Last updated: Nov 21 2024 at 12:39 UTC