Partition Principle Implies Axiom of Choice

Partition Principle Implies Axiom of Choice

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 244; 2026-09-24), the asserted result is that relative to consistency of ZF, the Partition Principle can hold together with ordinal-indexed choice and failure of full Choice.

Mathematical statement of the claimed result

Manuscript 1.

The Partition Principle $\mathrm{PP}$ means that a surjection $X\twoheadrightarrow Y$ implies some injection $Y\hookrightarrow X$, not necessarily a section. Let $\mathrm{AC}_{\rm wo}$ be choice for every ordinal-indexed family of nonempty sets. The claimed relative consistency is \[ \operatorname{Con}(\mathrm{ZF})\Rightarrow \operatorname{Con}(\mathrm{ZF}+\mathrm{PP}+\mathrm{AC}_{\rm wo}+\neg\mathrm{AC}). \] More concretely, from a countable transitive $V\models\mathrm{ZFC}$ the manuscript claims set forcing and a transitive symmetric intermediate model $V\subseteq W\subseteq V[G]$ with the same ordinals and $W\models\mathrm{ZF}+\mathrm{PP}+\mathrm{AC}_{\rm wo}+\neg\mathrm{AC}$. Every countable sequence of elements of $V$ that lies in $W$ already lies in $V$. Thus PP is claimed not to imply full Choice over ZF at this relative-consistency strength.

Outline of the argument

For manuscript 1 (family 244; 2026-09-24), a symmetric forcing construction creates nonwellorderable generic labels and orbit maps that present arbitrary sets by label--ordinal products. Controlled supports give ordinal-family choices, while quotient classification supplies injections opposite surjections without making the labels wellorderable.

Formal verification

For manuscript 1 (family 244; 2026-09-24), the documented Lean scope is the relative-consistency implication for ZF, the Partition Principle, ordinal-indexed choice, and failure of Choice; a separate transitive-model construction has an inaccessible-cardinal ground assumption and does not encode all the paper's preservation assertions.

The selected statement includes the clause used for this problem.

The linked family Comparator checks are PartitionConsistency.lean, PartitionPrinciple.lean.

Their named declarations include OAI.PartitionConsistency.main_consistency, OAI.PartitionPilot.Forcing.TransitiveGround.exists_model_partitionPrinciple_without_choice.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

• OpenAI, The Partition Principle does not imply Choice, 2026-09-24; citation key OAI:The-Partition-Principle-does-not-imply-Choice-September-24-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main-consistency; Statement source: thm:main-transitive.
• Family 244: Lean scope.
• Comparator PartitionConsistency.json.
• Comparator PartitionConsistency.lean.
• Comparator PartitionPrinciple.json.
• Comparator PartitionPrinciple.lean.
• OpenAI catalogue entry.

Does the Partition Principle Imply Choice?

Definitions and mathematical statement

Shared notation.

Unless a section says otherwise, ${\mathbb{N}}=\{1,2,\ldots\}$, ${\mathbb{Z}}$ is the ring of integers, ${\mathbb{Q}},{\mathbb{R}},{\mathbb{C}}$ are the rational, real, and complex fields, $[N]=\{1,\ldots,\lfloor N\rfloor\}$, and $\log$ is the natural logarithm. For real functions of a parameter tending to infinity, $f\ll g$ and $f=O(g)$ mean $|f|\leq Cg$ eventually for some fixed $C$; $f\gg g$ reverses this comparison; $f=o(g)$ means $f/g\to0$; $f\sim g$ means $f/g\to1$; and $f\asymp g$ means both order bounds. A subscript on $O$ or $\ll$ specifies allowed constant dependence. The expression $n^{o(1)}$ in an upper bound means growth smaller than $n^\epsilon$ for each fixed $\epsilon>0$. Local definitions govern any exception, finite-field convention, or use of the same symbol for another object. An asymptotic claim is not automatically an effective algorithm.

Work in ZF set theory, without assuming the axiom of choice. The partition principle says that whenever there is a surjection $f:A\to B$, there is an injection $g:B\to A$. It does not require $f(g(b))=b$. The axiom of choice asserts a choice function for every family of nonempty sets. Ask whether ZF proves that the former principle implies the latter. [S1] [S2]

Statement recorded in the supplied source.

Does the partition principle (PP) imply the axiom of choice (AC)? [S1]

Short English statement

Does the mere ability to inject the parts of every partition back into the original set already force the full axiom of choice?

Research attempt: a choice-free consequence of PP and the failed section argument

Status and source correction. All deductions below take place in ZF. We do not prove PP implies AC or construct a separating model. The inspected arXiv record for [S2] lists Adonai S. Sant'Anna, Otavio Bueno, Marcio P. P. de França and Renato Brodzinski. Its abstract claims a model through its Flow framework. We do not assume that claimed construction or certify it from the abstract; the arguments here are independent of it.

1. The stronger statement really is equivalent to AC

If every surjection $f:A\to B$ has a right inverse $s:B\to A$ with $f(s(b))=b$, apply this to the projection from the disjoint union $\bigsqcup_{i\in I}X_i$ of any family of nonempty sets onto $I$. The right inverse selects one member of each $X_i$, giving AC. Conversely AC chooses one member of each nonempty fiber of any surjection and gives a right inverse. A right inverse is injective, so AC implies PP.

PP supplies only an injection $j:B\to A$. The composite $f\circ j$ need not be onto, let alone the identity. Even in finite sets take $A=\{a_0,a_1,a_2\}$, $B=\{0,1\}$, let $f(a_0)=f(a_1)=0$, $f(a_2)=1$, and take $j(0)=a_0,j(1)=a_1$. Then $f\circ j$ is constant. This does not refute PP implies AC; it refutes the proposed one-step conversion of an arbitrary injection into a section by inverting its composite.

2. PP rules out amorphous sets

A set $A$ is amorphous when it is infinite but cannot be partitioned into two infinite subsets. We prove PP excludes such sets. Let $\operatorname{Fin}(A)$ be the set of finite subsets of an arbitrary infinite $A$. The function \[\operatorname{Fin}(A)\longrightarrow\mathbb N_0,\qquad F\longmapsto|F| \] is surjective: ZF proves that an infinite set contains an $n$-element subset for each individual finite $n$. This statement does not simultaneously choose such subsets. PP now gives an injection $j:\mathbb N_0\to\operatorname{Fin}(A)$, so the finite sets $F_n=j(n)$ are all distinct.

Their union cannot be finite, since a finite set has only finitely many subsets. Recursively choose the least index $n_k$ for which $F_{n_k}$ contains a point outside the finite union of previously selected $F_{n_i}$, and put \[B_k=F_{n_k}\setminus\bigcup_{i<k}F_{n_i}.\] Such an index exists at every stage; the union of all $F_n$ is infinite while the previously selected union is finite. Each $B_k$ is nonempty and finite, and the blocks are pairwise disjoint. The recursion chooses least natural-number indices, not arbitrary elements of the blocks, so it uses no form of countable choice. Both $\bigcup_k B_{2k}$ and $\bigcup_k B_{2k+1}$ are infinite, because each contains infinitely many disjoint nonempty blocks. Put any remaining elements of $A$ into one side to get a partition of $A$ into two infinite subsets. Hence an amorphous set contradicts PP.

3. A solvable case and the exact missing repair

If the domain $A$ of a surjection is already well-ordered, its fibers have least elements, giving a right inverse in ZF without PP. For a general set no such fiberwise order is available. The block argument above also does not supply a point from each $B_k$: pairwise disjoint nonempty finite blocks need not come with chosen representatives in ZF. Replacing the least-index recursion by arbitrary element choices would hide exactly the kind of choice principle under investigation.

The adversarial audit therefore checks every selection in the proof: finite existence is used one size at a time, the single injection is supplied by PP, and all recursive choices are from well-ordered natural numbers. The result is the precise necessary consequence "PP implies no amorphous sets." It is weaker than AC and provides no equivalence. A mechanism turning the unrestricted injection promised by PP into simultaneous fiber representatives, or a fully verified ZF model showing this impossible, remains missing.

Sources

• S1 ULAM.AI, UnsolvedMath, supplied problems.json, record 1347 (ST-001), statement and background. The embedded literature-review date is 2026-08-17; that is the archive’s review date, not a fresh certification. Dataset landing page: https://huggingface.co/datasets/ulamai/UnsolvedMath.

• S2 A. S. Sant'Anna, O. Bueno, M. P. P. de França and R. Brodzinski, Flow: the Axiom of Choice is independent from the Partition Principle, arXiv:2010.03664. https://arxiv.org/abs/2010.03664. Bibliographic information from the supplied record.

• S3 A Gentle Introduction to the Axiom of Choice, Mathematical Intelligencer $2026$. https://doi.org/10.1007/s00283-026-10531-4. Bibliographic information from the supplied record.