OAI.PartitionConsistency.main_consistency

The theorem states a relative consistency result in pure first-order set theory with membership and equality: if ZF, meaning the full axioms of extensionality, empty set, pairing, union, power set, infinity and foundation together with every instance of Separation and Replacement for arbitrary formulas with arbitrary parameters, and without Choice, is consistent, then so is the theory obtained by adding three sentences to ZF. Consistency is syntactic: no finite classical natural-deduction derivation of falsity exists from the theory, allowing any finite supply of free variables. The added sentences are the Partition Principle PP, which says that whenever there is a set surjection from X onto Y then there is a set injection from Y into X, with functions coded internally as sets of Kuratowski pairs and the injection not required to be a section of the surjection; the ordinal-indexed Choice axiom ACwo, which says that for every internal von Neumann ordinal (transitive and internally well-ordered by membership) every family of nonempty sets indexed by it has a choice function; and the negation of full Axiom of Choice AC, which says that every set of nonempty sets has a choice function.