The usual set up of first-order logic is with an infinite reservoir of variables which we can use in formulas. This is one of the annoying reasons why we need to put $aleph_0$ into the cardinal equations, but it also provides us with the expressive freedom that we need.

It is not hard to see that there is no reason to consider any other cardinal, except $aleph_0$, in this case: since formulas are finite, and proofs are finite, in any kind of proof there will only be finitely many variables. So anything larger than $aleph_0$ is kind of irrelevant. But this assumes that all cardinals are comparable, and the Axiom of Choice makes things kinda nice.

Assuming that the Axiom of Choice fails, and badly, what happens when we substitute the reservoir of variables with some Dedekind-finite set? In particular, a set $A$ whose finite subsets (and finite injective sequences) form a Dedekind-finite set, or even an amorphous set?

Can we prove some interesting results (read: not entirely equal to standard first-order logic) in $sf ZF$ (+ whatever set we needed exists), or at least some consistency results? For example, we don’t need choice to prove that every theory in a finite language has a complete theory extending it, or that it has a model. What happens when we switch to this abominable version of first-order logic?