The Consistency of the Axiom of Choice with Zermelo-Fraenkel (ZF) Set Theory: An Automated Deduction

摘要

Set theory is the foundation of mathematics: from it (together with some definitions), all the rest of mathematics can in principle be derived. The most commonly used formulation of set theory is "ZFC" (Zermelo-Fraenkel (ZF), together with the Axiom of Choice (AOC)). Of all the axioms of ZFC, the AOC is the most controversial because it is not constructive. Regardless, the AOC appears to be indispensable: it has been used in the proofs of more than 200 major theorems in logic, algebra, and topology. A fundamental question in any axiomatic theory is whether each axiom is consistent with the other axioms of that theory. Here I present an automated proof of the consistency of the AOC with the axioms of ZF. The approach demonstrates that automated first-order deduction techniques can provide useful insights into the foundations of set theory; the proof appears to be novel.