A Proof of the Schröder-Bernstein Theorem in ACL2
By: Grant Jurgensen
Potential Business Impact:
Proves sets can be matched if they fit inside each other.
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.
Similar Papers
Semi-Algebraic Proof Systems for QBF
Logic in Computer Science
Proves hard computer problems faster than before.
Arithmetics within the Linear Time Hierarchy
Logic in Computer Science
Makes math problems solvable by computers.
The Seifert-van Kampen Theorem via Computational Paths: A Formalized Approach to Computing Fundamental Groups
Logic in Computer Science
Makes math proofs about shapes easier for computers.