Email Gateway (May 13 2026 at 14:55): Email Gateway (May 13 2026 at 14:55):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce a rare contribution for Isabelle/ZF: the Mostowski Collapse Theorem, a basic set-theoretic result. It’s great that LLMs can write code for Isabelle/ZF, with its distinctive syntax and utterly different proof environment, since it doesn’t have much native automation.
The Mostowski Collapse Theorem
Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Abstract
This entry formalizes the Mostowski collapse theorem in Isabelle/ZF [3, 4]. For a set equipped with a well-founded extensional relation, the development defines the collapsing map by well-founded recursion, proves that its range is transitive, and shows that the map is an order isomorphism between the original relation and membership on the transitive range. The construction is also proved unique among maps satisfying the same recursive equation. The result is a standard bridge from abstract well-founded extensional structures to transitive membership structures, and complements the existing Isabelle/ZF and AFP developments on ordinals, cardinals, forcing, and transitive models [2, 1]. AI assistance was used for proof engineering. The final definitions, statements, and proofs are checked by Isabelle
https://isa-afp.org/entries/Mostowski_Collapse.html
Last updated: May 23 2026 at 03:31 UTC