\section{Introduction}\label{sec:introduction}

The \emph{Partition Principle} asserts that a surjection between two sets
implies the existence of an injection in the reverse direction:
\[
 \PP:\qquad
 \forall X\,\forall Y\,
 \bigl[(\exists f:X\twoheadrightarrow Y)
       \Longrightarrow(\exists j:Y\hookrightarrow X)\bigr].
\]
Equivalently, every partition of a set admits an injection into that set.
The Axiom of Choice implies this principle by choosing one element of each
fiber. The converse is less direct: the injection supplied by $\PP$ need
not take a part to one of its members. In particular, it need not satisfy
$f\circ j=\id_Y$. The problem is whether this cardinal comparison alone
can recover choice for arbitrary families.

Write $\ACwo$ for Choice for wellorderable families: for every ordinal
$\eta$ and every family $(X_\xi)_{\xi<\eta}$ of nonempty sets, there is a
function $c$ with $c(\xi)\in X_\xi$ for all $\xi<\eta$.
Our principal result is the following ordinary relative-consistency statement.

\begin{theorem}\label{thm:main-consistency}
If $\ZF$ is consistent, then so is $\ZF+\PP+\ACwo+\neg\AC$.
\end{theorem}

The construction also has a separate transitive-model form.

\begin{theorem}\label{thm:main-transitive}
Let $V$ be a countable transitive model of $\ZFC$. There are a set forcing
$\mathbb Q\in V$, a $V$-generic filter $G$, and a transitive symmetric
submodel $W$ of $V[G]$ such that
\[
 V\subseteq W\subseteq V[G],\qquad
 \Ord^W=\Ord^V,\qquad
 W\models\ZF+\PP+\ACwo+\neg\AC.
\]
Every countable sequence of elements of $V$ that belongs to $W$ already
belongs to $V$.
\end{theorem}

Here $\ZF$ is classical first-order set theory with pure sets, Foundation,
and the full Separation and Replacement schemata.
Theorem~\ref{thm:main-consistency} gives a negative answer to the
Partition Principle versus Choice problem under ordinary syntactic
consistency. It permits externally ill-founded models, whereas
Theorem~\ref{thm:main-transitive} starts with a transitive ground and
preserves transitivity. In either conclusion the reverse injections and
the family without a choice function belong to the same model.
Section~\ref{sec:metatheory} gives the two deductions separately.
The consequences for the dual Cantor--Schr\"oder--Bernstein principle
and the Weak Partition Principle are developed in
Remark~\ref{rem:dual-csb-wpp}.

\subsection{History and related methods}

The distinction between comparing the sizes of a partition and its
underlying set, and actually choosing representatives, is longstanding.
Da Silva traces the Partition Principle
to Beppo Levi in 1902 \cite[Section~2, p.~787]{daSilva2021}.
Banaschewski and Moore studied its relation to the dual
Cantor--Bernstein theorem and the surrounding cardinal-comparison
principles \cite{BanaschewskiMoore1990}. These questions concern what
remains of cardinal arithmetic when sets need not be wellorderable.
For example, Blass and Kulshreshtha distinguish several forms of
cardinal well-foundedness and show that they become equivalent under
$\PP$; their August 2026 version still lists $\PP\Rightarrow\AC$
as open \cite[Introduction and Section~9]{BlassKulshreshtha2026}.
Gilson's September 2026 corrections withdraw the model-construction
claims of three earlier approaches
\cite{GilsonSheafCorrection2026,GilsonExternalCorrection2026,GilsonIterationCorrection2026}.

There is already substantial choice in $\PP$. The implication
$\PP\Rightarrow\ACwo$ is classical: Ryan-Smith records the
argument attributed to Pincus by Pelc
\cite[Proposition~3.17, proof and footnote~4]{RyanSmith2025}.
Thus $\ACwo$ in our main statements is not an additional strength
beyond $\PP$. Its separate appearance records the order of the
construction: we establish ordinal-indexed choice first and then use
it to assemble reverse injections for arbitrary sets.

The difficulty of preserving a principle quantified over all sets
can be reduced to a fixed set of parameters. Blass introduced small
violations of choice \cite{Blass1979}. For a nonempty set $A$,
$\mathrm{SVC}(A)$ says that every nonempty set is a surjective image
of $A\times\eta$ for some ordinal $\eta$. The injective version,
$\mathrm{SVC}^{+}(A)$, says that every set embeds into some
$A\times\eta$. See also
\cite[Definition~3.13 and Theorem~3.14]{Usuba2021}.
These presentations let a construction on one set control objects
of arbitrary rank, but their different directions cannot be
interchanged without proof.

Ryan-Smith makes the local-to-global step precise. Under
$\mathrm{SVC}^{+}(A)$, full $\PP$ is equivalent to $\ACwo$
together with reverse injections for surjections between subsets of
$A$ \cite[Proposition~3.17]{RyanSmith2025}. Reverse injections for
surjective images of $A$ are a different local assertion: even with
$\ACwo$ and $\mathrm{SVC}^{+}(A)$, they need not imply full
$\PP$ \cite[Proposition~3.23]{RyanSmith2025}. Our construction
instead makes every nonwellorderable image of $A$ bijective to $A$.
Lemma~\ref{lemma:pp-reduction} uses this stronger classification,
the surjective presentation, and ordinal-indexed choice to carry out
the required all-set reduction. Its slicing argument follows the
method of \cite[Propositions~3.17 and~3.20]{RyanSmith2025}, rather
than identifying the two local principles.

The ambient method is a symmetric submodel of a set-forcing
extension: hereditarily symmetric names for a normal filter of
subgroups give a model of full $\ZF$
\cite[Section~2.1]{Karagila2026}. A more specific antecedent is
Holy and Schilhan's product of Cohen forcing with a forcing of
ground-model hereditarily almost-disjoint towers
\cite[Section~3]{HolySchilhan2025}. Their construction yields
models in which every set can be linearly ordered and higher forms
of Dependent Choice hold, although full Choice fails. They develop
the hereditary almost-disjointness method from Pincus's work on
adding Dependent Choice \cite{Pincus1977}. Their restriction and
support-intersection arguments
\cite[Lemmas~10 and~15]{HolySchilhan2025} are antecedents of the
locality arguments here. Our diagrams have a different geometry:
the monoid must support both exact quotient multiplicities and the
coherent assignment of bijections, not just the descent of supports.

\subsection{Proof strategy}

We construct a set $A$ of distinct generic subsets of the ground-model
$\omega_1$. Symmetry
prevents $A$ from being wellordered. Orbit maps of names show that every
nonempty set is a surjective image of $A\times\eta$ for some ordinal
$\eta$, with no restriction on its rank. The forcing also allows one
wellorderable part of $A$ to meet every member of any given ordinal-indexed
family of nonempty subsets of $A$. Together with the preceding
presentation of arbitrary sets, this yields $\ACwo$.

The central additional property is
\begin{equation}\label{eq:intro-quotient}
 \text{every nonwellorderable surjective image of $A$ is in bijection with $A$.}
\end{equation}
To pass from this property to full $\PP$, partition the target of an
arbitrary surjection into ordinal-indexed disjoint nonempty pieces and
use disjoint source pieces mapping onto them. Each resulting piece is
an image of $A$, though the source pieces need not cover the original
domain. A wellorderable target piece admits a reverse injection by
$\ACwo$. Otherwise both corresponding pieces are in bijection with $A$
by \eqref{eq:intro-quotient}. A further application of $\ACwo$ chooses
the piecewise injections, whose union is the required injection. The
empty target uses the empty injection.

The difficult part is to construct the bijections in
\eqref{eq:intro-quotient} with enough coherence to belong to the symmetric
model. Fix one equivalence relation on $A$ whose quotient is not
wellorderable. Counting its classes on
each support will produce many possible local bijections, but arbitrary
choices of them need not agree on overlapping supports or respect
coordinate changes. The proof solves these two compatibility problems
in three stages.

\begin{enumerate}[leftmargin=*,label=\arabic*.]
\item \textbf{A geometry of diagrams.}
We build a left-cancellative monoid $T$. A diagram is an injective map
$r:T\to I$, where $I$ is the set of label indices. Its subdiagram at $n\in T$
is the map $r_n(x)=r(nx)$. The diagram forcing makes larger diagrams
stronger conditions. Finite amalgamations join independently placed
diagrams. A second extension operation places many copies with prescribed
patterns of intersection. Together these operations give the forcing its
compatibility and support-descent properties. Height and cost functions
reduce the availability patterns introduced next to countable cofinal
paths. A rearrangement of the same monoid construction will later bound
the symmetries that survive along such a path.

\item \textbf{Exact availability fibers.}
A diagram supports names whose definitions are fixed by all permutations
of labels outside its range. For a quotient of $A$, we record the quotient
elements that can be named at each diagram. An element's availability
pattern records the subdiagrams at which it can still be named.
The labels themselves have analogous patterns, determined by which
subdiagrams contain their indices. The copying and support-descent lemmas
show that, for each exact pattern, the available labels and quotient
elements have the same cardinality. Restricting to a subdiagram in that
pattern identifies the corresponding fibers canonically. These
identifications group the fibers into components and are already
compatible; the choices of bijections between label and quotient fibers
are not.

\item \textbf{Covariant choices on each component.}
Each component has a countable cofinal chain of nested diagrams. Codes
along this chain give a preliminary bijection compatible with every
permutation fixing a sufficiently late diagram pointwise. Modulo these
permutations, the remaining symmetries form a countable group. Countably
many bounded initial segments of Cohen subsets distinguish its elements
and select among the transported preliminary bijections. Finally,
transport between components gives assignments that agree under
restriction and respect all required permutations. Their union is one
hereditarily symmetric graph for the fixed quotient.
\end{enumerate}

The countable description of each availability pattern, the reduction of
its symmetries to a countable group, and the final equivariant selection
are the main technical ingredients. The selection is performed between
moved Cohen generics: it does not require permutations to act as
automorphisms of a single fixed forcing extension.

Section~\ref{sec:monoid} constructs $T$ and proves its local rearrangement
property. Section~\ref{sec:forcing} develops the forcing, locality, and the
basic properties of $A$. The quotient construction follows in
three stages: Section~\ref{sec:quotient-fibers} computes exact availability
fibers, Section~\ref{sec:quotient-components} organizes them into components
and controls their symmetries, and Section~\ref{sec:quotient-equivariance}
constructs the coherent bijections. Section~\ref{sec:conclusion} derives
full $\PP$ and identifies a family without a choice function.
Section~\ref{sec:metatheory} gives the ordinary consistency deduction and
the separate transitive-ground result.