A Proof of the Schr\"oder-Bernstein Theorem in ACL2
Grant Jurgensen (Kestrel Institute)
TL;DR
This paper formalizes and verifies the Schr"oder-Bernstein theorem within ACL2, providing a mechanized proof that includes a novel theory of chains to define a non-computable witness, thus contributing to formal set theory verification.
Contribution
It introduces a formalization and verification of the Schr"oder-Bernstein theorem in ACL2, including a new chain theory to define a non-computable witness.
Findings
Successful formal proof of the Schr"oder-Bernstein theorem in ACL2
Development of a chain theory to define non-computable witnesses
Enhancement of formal set theory verification methods
Abstract
The Schr\"oder-Bernstein theorem states that, for any two sets P and Q, if there exists an injection from P to Q and an injection from Q to P, then there must exist a bijection between the two sets. Classically, it follows that the ordering of the cardinal numbers is antisymmetric. We describe a formulation and verification of the Schr\"oder-Bernstein theorem in ACL2 following a well-known proof, introducing a theory of chains to define a non-computable witness.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.