What is first-order logic with Dedekind-finite sets of variables?

Question

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?

Answer 1

For sentences, nothing will change. The reason is that every sentence in the abominable language is canonically logically equivalent to a formula in the usual language, since every formula provides an ordering of the variables appearing in it, and they can then be replaced with ordinary variables from an $\omega$-indexed set of variables.

Because every sentence is logically equivalent to any of its notational variants (where we use different formulas), we can transfer any theory to an equivalent theory in the well-behaved language.

For example, a theory in the abominable language will be consistent if and only if its translation is consistent, since the proof system can validate any instance of notational variance, which involves only finitely many variables at a time.

For this reason, any consistent theory in the abominable language will have a completion: just translate it to the regular language, complete it there, and then take all notational variants of assertions of that completion. This will be complete in the abominable language.

A similar idea allows you to define the satisfaction relation for models and formulas in the abominable language. Just translate them to the regular language, use Tarski's definition, and then translate back. This will obey the Tarski recursion, even in the abominable language.

The only remaining issue seems to be when you have types involving infinitely many free variables. In this case, you are dealing with simultaneous assignments on those variables, where amorphicity might come into play.