The complexity of finiteness

Say that a second-order sentence in the empty language, $\varphi$, characterizes finiteness iff for every set $X$ we have $X\models\varphi$ iff $X$ is finite. I'm interested in the optimal complexity over $\mathsf{ZF}$ of sentences characterizing finiteness.

Many natural candidate sentences are $\Sigma^1_2$ (e.g. "$X$ admits a linear order which is well-ordered and co-well-ordered"), but we can do better: the sentence "$X$ can be linearly ordered and every linear ordering on $X$ is discrete" characterizes finiteness and is $\Sigma^1_1\wedge\Pi^1_1$. (Note that over $\mathsf{ZFC}$ we could drop the first clause, which would bring the comlpexity down to $\Pi^1_1$.)

Meanwhile,$\mathsf{ZF}$ alone proves that there is no $\Sigma^1_1$ sentence characterizing finiteness. First, note that $\mathsf{ZFC}$ proves the downward Lowenheim-Skolem theorem and that ultraproducts preserve $\Sigma^1_1$ sentences. From this we get that if $\varphi$ is $\Sigma^1_1$ and true in every finite structure then $\omega\models\varphi$ is true in $L$. But then by Mostowski absoluteness we in fact get $\omega\models\varphi$ in reality.

This leaves the $\Pi^1_1$ situation open:

Is there a $\Pi^1_1$ sentence in the empty language which $\mathsf{ZF}$ proves characterizes finiteness? Equivalently, is there a first-order sentence $\psi$ (in any language) such that $\mathsf{ZF}$ proves that the cardinalities of models of $\psi$ are exactly the infinite cardinalities?

My suspicion is that the answer is no - indeed, that every amorphous set satisfies all $\Pi^1_1$ sentences true in all finite sets. However, at the moment I don't see how to prove even the weaker claim.

EDIT: note that a negative answer to the question (which James Hanson has provided below) also shows that no $\Sigma^1_1\vee\Pi^1_1$ sentence can characterize finiteness. Suppose $\psi\in\Sigma^1_1$, $\theta\in\Pi^1_1$, and $\psi\vee\theta$ is true in every finite structure. Then either $\psi$ has arbitrarily large finite models in which case $\psi$ has an infinite model, or for some $n\in\omega$ the $\Pi^1_1$ sentence "$\theta\vee[\forall x_1,...,x_{n+1}(\bigvee_{1\le i<j\le n+1}x_i=x_j)]$" is true of every finite structure and hence has an infinite model. Either way, $\psi\vee\theta$ has an infinite model. So James' answer in fact completely resolves the complexity of finiteness over $\mathsf{ZF}$.

As you discussed in the comments, $\Pi_1^1$ formulas $\varphi(X)$ in the empty language are equivalent to statements of the form 'there is no model of $\psi$ whose underlying set is $X$,' where $\varphi$ is a fixed first-order sentence in some language. So if we can show that

• for any structure $\mathfrak{A}$, if the underlying set $A$ is amorphous, then $\mathrm{Th}(\mathfrak{A})$ is pseudo-finite,

where a theory $T$ is pseudo-finite if every sentence $\varphi \in T$ has a finite model, then it will follow that it is consistent with $\mathsf{ZF}$ that no $\Pi_1^1$ sentence characterizes finiteness, because this implies a sort of reverse overspill property for first-order sentences: any sentence that has no finite models has no amorphous models as well.

The desired statement follows from a couple of results that exist in the literature.

Fact 1. If $\mathfrak{A}$ is a structure whose underlying set $A$ is amorphous, then $\mathrm{Th}(\mathfrak{A})$ is $\omega$-categorical and strongly minimal.

I don't know an original reference for this fact (I believe you can find it here), but it's not that hard to prove yourself if you know the Engeler–Ryll-Nardzewski–Svenonius theorem characterizing $\omega$-categorical theories and the characterization of strongly minimal theories as those in which every formula $\varphi(x,\bar{y})$ has a natural number $n_\varphi$ such that for any $\bar{a}$, if $\varphi(x,\bar{a})$ is satisfied by more than $n_\varphi$ many elements, then it is satisfied by all but at most $n_\varphi$ elements. (Note that this means that strong minimality of a theory is an arithmetical property. It's also not hard to show that $\omega$-categoricity is an arithmetical property of a theory.)

Fact 2 (Zilber; Cherlin, Harrington, Lachlan). A countable, complete, totally categorical theory is pseudo-finite.

While Fact 2 is proven in $\mathsf{ZFC}$, like many model theoretic statements it boils down to an arithmetical statement of low complexity, so by absoluteness it holds in $\mathsf{ZF}$ as well. (A more precise proof would be to let $T$ be the theory of whatever structure you have on some given amorphous set, pass to $L(T)$ (thinking of $T$ as a real) and then running one of these proofs there and getting the relevant finite models in $L(T)$, which are then models in $V$ by absoluteness. More advanced model theoretic facts (specifically the fact that every $\omega$-categorical $\omega$-stable theory can be axiomatized by some finite set of axioms together with axioms for each finite $n$ stating that the structure has more than $n$ elements) imply that $T$ is actually just in $L$ anyways, but we don't need this.)

So together with the easy fact that strongly minimal sets are uncountably categorical, we get that any structure on an amorphous set has a pseudo-finite theory. (I'm curious if there is a much more direct proof of this fact.) Therefore any $\Pi_1^1$ sentence in the empty language satisfied by all finite sets is satisfied by all amorphous sets as well.