In $\textsf{ZF}$ with first-order logic we can prove that the well-ordering theorem ($\textsf{WO}$) and the axiom of choice ($\textsf{AC}$) are equivalent. I was wondering how far (in a vague sense) these theorems' equivalence goes.
[1] notes that in $\textsf{ZFC}$ without the powerset axiom we are unable to recover the well-ordering theorem (though I wasn't sure whether we can prove its negation?); [2] gives the result from Shapiro's Foundations Without Foundationalism that if we take second-order logic as our foundation for mathematics instead of $\textsf{ZFC}$, then we can prove $\textsf{WO} \to \textsf{AC}$, but not the converse.
Any further similar results are welcome, but in particular I'd be interested to know if there are any non-trivial systems where we have $\neg\textsf{AC}$ and $\textsf{WO}$ or the converse. Thanks!
[1] Can Well Ordering Theorem Be Proved Without the Axiom of Power Set?
Any theory $T$ over which $\mathsf{WO}$ doesn't imply $\mathsf{AC}$ (that is, which is compatible with $\mathsf{WO+\neg AC}$) must have only very weak set formation ("comprehension") axioms: otherwise, the "pick the least element" argument would get $\mathsf{AC}$ from $\mathsf{WO}$. To find systems this weak we have to go below the usual weak set theories like $\mathsf{KP}$ and $\mathsf{Z}$.
At the risk of self-promotion, let me mention a positive result along these lines. There is a particular theory $\mathsf{RCA_0^3}$, of relevance to higher-order reverse mathematics, about which one can prove the following:
The proof is a bit technical; there's a plausible alternate argument which is much more elegant, but it has a gap I haven't been able to fill. Very briefly (and not optimizing at all), the idea of the proof I do know is as follows.
Over a countable transitive model $M$ of $\mathsf{ZFC}$ (actually that's massive overkill but meh), we force with the poset $\mathbb{P}$ of countable partial injections from $\mathbb{R}$ to $\omega_1$; let $G$ be the generic bijection $\mathbb{R}\rightarrow\omega_1$, and let $\trianglelefteq$ be the well-ordering of $\mathbb{R}$ gotten by "pulling back" the usual ordering on $\omega_1$ along $G$. Note that recovering $G$ from $\trianglelefteq$ is relatively difficult (even determining $G^{-1}(0)$ requires a kind of unbounded search over $\trianglelefteq$); normally in set theory this wouldn't be significant, but per the first paragraph of this answer we actively want to pay attention to rather fine details re: computational power right now.
A model of $\mathsf{RCA_0^3}$ consists of a natural numbers part, a real numbers part, and a functionals part. We produce such a model $N$ as follows. The naturals and reals of $N$ are just those of $M$ itself, which are in turn those of the generic extension $M[\trianglelefteq]$ since $\mathbb{P}$ is countably closed. As to the functionals, we use a kind of "iterated truth-table reducibility." Roughly speaking, a functional $f\in M[\trianglelefteq]$ is in $N$ iff there is in $M$ an algorithm for computing $f(a)$ (for $a$ a real) with the following behavior: given $a$, we first ask about the $\trianglelefteq$-relationships between some countable set of reals $A_{a,0}$; based on the result of those questions, we whip up another countable set of reals $A_{a,1}$ whose $\trianglelefteq$-relationships we ask about; and so on for some finite number of steps. Now for $r\in\mathbb{R}$ let $$U_r=\{s\in\mathbb{R}: r\triangleleft s\}.$$ This sequence is in $N$, but we can show that no choice function for the sequence $(U_r)_{r\in\mathbb{R}}$ can be "computed" in the sense above.
As an aside, note that the whole iterated truth-table reducibility idea is specific to higher computability theory: in the classical setting it just collapses to truth-table reducibility itself, the point being that "$\mathit{finite}^{\mathit{finite}}=\mathit{finite}$" (which breaks down at higher cardinalities of course).