The strength of "There are no $Pi^1_1$-pseudofinite sets"

My "hunch" in the comments to the question appears to be correct! This model comes from Howard, Paul E.; Yorke, Mary F., Definitions of finite, Fundam. Math. 133, No. 3, 169-177 (1989). ZBL0704.03033. The paper has a few confusing typos and, in particular, the proof of Theorem~15 appears insufficient, so I'm sketching the argument in some detail, with another proof of that theorem.

---

$newcommand{supp}{operatorname{supp}nolimits} newcommand{fix}{operatorname{fix}nolimits}$Fix a ground model $mathfrak{M}$ of ZFA+AC where the set $U$ of atoms is countably infinite and fix a dense linear ordering ${<}$ of $U$ without endpoints. Let $mathcal{P}$ be the lattice of finite interval partitions of $U$, i.e., patitions of $U$ into finitely many blocks where each block is an interval of any shape. This is a lattice under refinement $P leq Q$ iff every block of $P$ is contained in a block of $Q$. The meet $P sqcap Q$ consists of all nonempty intersections of a block from $P$ and a block from $Q$. The join $P sqcup Q$ is more complicated: the blocks of $P sqcup Q$ are maximal unions of the form $B_1cup B_2 cup cdots cup B_k$ where $B_1,B_2,ldots,B_k in P cup Q$ and $B_1 cap B_2, B_2 cap B_3, ldots, B_{k-1} cap B_k$ are all nonempty. Given an interval partition $P$, we write ${sim_P}$ for the associated equivalence relation: $x sim_P y$ iff $x$ and $y$ belong to the same block of $P$.

Let $G$ be the group of permutations $pi$ of $U$ with finite support $supppi = { x in U : pi(x) neq x }$. Given an interval partition $P$ of $U$, let $$G_P = { pi in G : (forall B in P)(pi(B) = B) }.$$ Note the following facts:

1. $G_{P sqcap Q} = G_P cap G_Q$.
2. If ${x}$ is a block of $P$ for each $x in supppi$ then $pi G_Ppi^{-1} = G_P$.
3. $G_{P sqcup Q}$ is the subgroup generated by $G_P cup G_Q$.

It follows that these subgroups generate a normal filter $mathcal{F}$ of subgroups of $G$. Let $mathfrak{N}$ be the symmetric submodel associated to $mathcal{F}$: $$mathfrak{N} = { X in mathfrak{M} : fix(X) in mathcal{F} land X subseteq mathfrak{N} }.$$ Note that by 3, for every $X in mathfrak{N}$ there is a coarsest interval partition $supp(X)$ such that $G_P subseteq fix(X)$, namely $$supp(X) = bigsqcup { P : G_P subseteq operatorname{fix}(X) }.$$

Lemma. For any set $X$ in $mathfrak{N}$, if $pi in fix(X)$ then for every $x_0 in U$, $pi(x_0)$ is not in a block of $supp(X)$ which is adjacent to that of $x_0$.

Proof. Suppose, for the sake of contradiction, that $A,B$ are adjacent blocks of $supp(X)$ and $x_0 in A$, $pi(x_0) in B$ for some $x_0$. We will show that for any $a in A$ and $b in B$ the transposition $(a,b)$ fixes $X$. Note that at least one of $A$ or $B$ must be infinite. Let's assume that $B$ is infinite, the other case is symmetric.

1. Suppose $a = x_0$ and $b notin supppi$. Then $(a,b) = (x_0,b) = pi^{-1}(pi(x_0),b)pi$.
2. Suppose $a = x_0$ and $b in supppi$. Then pick $b' in B setminus supppi$ and note that $(a,b) = (a,b')(b,b')(a,b')$.
3. Suppose $a neq x_0$. Then $(a,b) = (a,x_0)(x_0,b)(a,x_0)$

It follows that any permutation of $A cup B$ fixes $X$, which contradicts the fact that $supp(X)$ is the coarsest partition such that $G_{supp(X)} subseteq fix(X)$.

Claim 1 (Howard & Yorke, Theorem 15). $mathfrak{N}$ contains no amorphous sets.

Proof. Suppose $X in mathfrak{N}$ is infinite. If $G_{supp(X)}$ fixes $X$ pointwise, then $X$ is wellorderable and therefore not amorphous. Pick $x_0 in X$ such that $P_0 = supp(x_0)sqcapsupp(X)$ properly refines $supp(X)$. Let $A,B$ be two adjacent blocks of $P_0$ which belong to the same block of $supp(X)$. Suppose $A$ has a right endpoint $a$; the case where $B$ has a left endpoint is symmetric.

Let $P_1$ be obtained from $P_0$ by replacing $A$ with $Asetminus{a}$ and $B$ with $Bcup{a}$. Note that for $phi,psi in G_{P_1}$, $phi(x_0) = psi(x_0) iff phi(a) = psi(a)$. Fix $b in B$ such that $Bcap(-infty,b)$ and $Bcap[b,+infty)$ are both infinite. Let $$X_0 = { pi(x_0) : pi in G_{P_1}, pi(a) < b }$$ and $$X_1 = { pi(x_0) : pi in G_{P_1}, pi(a) geq b }.$$ These are two disjoint infinite subsets of $X$. Moreover, $X_1, X_2 in mathfrak{N}$ since they are both fixed by $G_Q$ where $Q$ is a refinement of $P_0, P_1$, and ${(-infty,b),[b,+infty)}$. Therefore $X$ is not amorphous.

Claim 2. $U$ is $Pi^1_1$-pseudofinite in $mathfrak{N}$.

Sketch. Suppose, for the sake of contradiction, that $$(forall Y subseteq X^n, Z subseteq X^m,ldots )phi(X,Y,Z,ldots)$$ is a $Pi^1_1$ statement which is true of every finite set $X$ but false for $X = U$. Let $Y subseteq U^n, Z subseteq U^m,ldots$ be sets in $mathfrak{N}$ such that $lnotphi(U,Y,Z,ldots)$. Let $P = supp(Y)sqcapsupp(Z)sqcapcdots$

Note that there are only finitely many possibilities for $Y, Z, ldots$ For example, when $n=1$ then $Y$ must be a union of some of the intervals from $P$. When $n=2$, $Y$ must be a boolean combination of cartesian products of two intervals from $P$ and the diagonal set ${(x,x) : x in U}$. And so on...

By an EF-style argument, if $V subseteq U$ is a finite set such that that contains all the endpoints of intervals from $P$ each of the sets $P cap B$ is sufficiently large when $B$ is an infinite interval from $P$, then $phi(U,Y,Z,ldots)$ is equivalent to $phi(V, Y cap V^n, Z cap V^m,ldots)$. It follows that $lnotphi(V, Y cap V^n, Z cap V^m, ldots)$ for some finite set $V subseteq U$, but this contradicts the assumption.

---

Since the ultimate goal is to obtain a more concrete understanding of what $Pi^1_1$-pseudofinite means, I will propose an alternate conjecture.

Recall Tarski's notion of II-finite: every chain of subsets of $X$ has a maximal element. This is equivalent to the $Pi^1_1$ statement: every total preordering of $X$ has a maximal element. So every $Pi^1_1$-pseudofinite set is II-finite. It seems that the converse might be true but I will only propose the following:

Conjecture. There is no infinite $Pi^1_1$-pseudofinite set if and only if there is no infinite II-finite set.