∑math20

Mathematical logic · Result 244

The Partition Principle does not imply Choice

1 paperLean

Assuming ZF is consistent, constructs a model in which every surjective image of a set injects into that set, yet the axiom of choice fails. Choice for ordinal-indexed families still holds. From any countable transitive model of ZFC, a separate construction gives a transitive symmetric extension with these properties and no new countable sequences of ground-model elements.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of The Partition Principle does not imply Choice

The Partition Principle does not imply Choice

OpenAI · September 24, 2026

We prove that the Partition Principle does not imply the Axiom of Choice: if ZF is consistent, then so is ZF with the Partition Principle, Choice for ordinal-indexed families, and the negation of the Axiom of Choice. Separately, over every countable transitive model of ZFC, we construct a transitive symmetric model of this theory with the same ordinals and no new countable sequences of ground elements.

Read PDF Download Source

Cite
@misc{OAI:The-Partition-Principle-does-not-imply-Choice-September-24-2026,
  author = {{OpenAI}},
  title = {{The Partition Principle does not imply Choice}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-Partition-Principle-does-not-imply-Choice-September-24-2026/partition-principle-without-choice.pdf}{OAI:The-Partition-Principle-does-not-imply-Choice-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The Partition Principle says that every surjection admits an injection in the reverse direction. The formalization proves the relative-consistency implication: if ZF is consistent, then so is ZF with the Partition Principle, Choice for ordinal-indexed families, and failure of the Axiom of Choice.

The linked model-construction result also constructs a transitive model of the Partition Principle without Choice from an externally countable transitive ground model satisfying the stated axioms, including Choice, and containing an internal strongly inaccessible cardinal. The paper's stronger transitive-model preservation assertions are outside that selected construction.

Comparator links

ResultComparator statement
Partition Principle without Choice from a ground modelPartitionPrinciple.lean
Relative consistency of the Partition Principle with ordinal Choice and failure of ChoicePartitionConsistency.lean

Scope note on GitHub →