An example of a class of structures whose axiomatizability depends on the axiom of choice

Question

Is there an example of a specific class $K$ of structures (in the sense of first-order logic), such that $K$ is first-order axiomatizable if the axiom of choice is assumed, but that its axiomatizability is independent of ZF set theory?

Answer 1

Yes, there is such a class of structures. Working in the empty language, consider the class of well-orderable sets (keeping in mind that a structure in the empty language is just a set, full stop). This is axiomatized by the empty theory if $\mathsf{AC}$ holds, and is non-axiomatizable otherwise.

(To see that the class of well-orderable sets is not first-order axiomatizable if $\mathsf{AC}$ fails, just check that $\mathsf{ZF}$ proves the elementary equivalence of any two infinite pure sets.)

---

In fact, the question - without further restrictions, anyways - is actually trivial: given an arbitrary sentence $\varphi$ in the language of set theory, fixing your favorite non-axiomatizable class $K$ consider the class $$K_\varphi=\begin{cases} \emptyset & \mbox{if $\varphi$ holds}\\ K & \mbox{otherwise}. \end{cases}$$ This class is axiomatizable iff $\varphi$ holds.

So to make the question non-trivial, we need to restrict attention to "nice" (definitions of) classes of structures. One natural framework for doing so is via abstract model theory. Fixing an "appropriately absolute" logic $\mathcal{L}$ we can ask:

Is there a $\mathcal{L}$-sentence $\sigma$ such that the first-order axiomatizability of the class of models of $\sigma$ is undecidable in $\mathsf{ZF}$ (or $\mathsf{ZFC}$, or ...)?

For example, if we take $\mathcal{L}=\mathsf{FOL}$ the answer is obviously no. On the other hand, the example at the start of this answer shows that the answer is yes if $\mathcal{L}=\mathsf{SOL}$, since well-orderability is characterizable in second-order logic.

In my opinion the most natural choice of $\mathcal{L}$ to consider here is existential second-order logic, due to the latter's relative tameness (it is compact and has the downward Lowenheim-Solem property for individual sentences, avoiding contradiction with Lindstrom's theorem by failing to be closed under negation). It is not immediately clear to me what the situation is here.