Is there a model of ZF¬C where some program always terminates but has no loop variant?

Question

Wikipedia has a proof that every loop that terminates has a loop variant—a well-founded relation on the state space such that each iteration of the loop results in a state that is less than the previous iteration's state under the relation. Here, well-founded refers to the usual classical definition of a well-founded relation: every nonempty subset has a minimal element.

The proof given in the linked article is as follows:

1. Let the loop variant be the "iteration" relation, i.e. the reflexive transitive closure of the transition relation.
2. Since the loop always terminates, the loop variant has no infinite descending chains.
3. Apply the axiom of choice to conclude that the loop variant is well-founded.

My question is about step 3. Using the full, uncountable axiom of choice here feels like swatting a fly with an atom bomb. Elsewhere on Wikipedia, we have the following:

Equivalently, assuming the axiom of dependent choice, a relation is well-founded if it contains no countable infinite descending chains: that is, there is no infinite sequence $x_0, x_1, x_2, \dots$ of elements of $X$ such that $x_{n+1}\ R\ x_n$ for every natural number $n$.

So the much weaker axiom of dependent choice is sufficient.

It seems like it might be possible to weaken this assumption further. The state space of a computer program is not an arbitrary set from the entire Von Neumann universe of ZF. Maybe countable choice suffices, since the state space of any program is countable?

On the other hand, if dependent choice is required and countable choice will not suffice, then (assuming ZF is consistent) there must exist a model of ZF + countable choice where there is some program that (a) always terminates, (b) has an iteration relation with no infinite descending chains, yet (c) has no well-founded loop variant. This seems deeply weird.

My question is:

1. Is there a model of ZF where a program always terminates but has no loop variant?
2. If the answer to 1 is yes, then what is the weakest choice principle that, when added to ZF, changes the answer to no?
3. If the answer to 1 is yes, is it possible to write down an explicit example of such a program (a la Harvey Friedman's explicit formulas equivalent to the strengths of ordinals), or does such a program necessarily correspond to a non-standard natural number?

Answer 1

I think you are really asking a question about the definition of the notion of well-foundedness.

I think the notion of loop variants is a bit of a red herring here: I would argue that any reasonable definition of well-foundedness should enable proving that a loop is terminating iff there is a well-founded relation which acts as a variant for it, almost as a tautology.

The issue is that the classical definition of a well-founded order $<$ on $X$:

There are no infinite sequences $x_1>x_2>x_3>\ldots$

is not a very nice definition, either from a constructive standpoint or when one is uncomfortable with the use of the axiom of (dependent, thanks Andrej!) choice. Assuming the latter, this definition is equivalent to the much nicer definition:

Every non-empty subset $P\subseteq X$ has a minimal element, that is, some $x\in P$ such that $y \not< x$ for every $y\in P$.

This definition is already much nicer, and I think it can be used to prove the variant lemma without choice.

Finally, the constructive version of well-foundedness is this:

For every $P\subseteq X$, if for every $x\in X$, $\{\ y\ |\ y < x\ \}\subseteq P$ implies $x\in P$, then $P = X$.

This definition seems more unwieldy, but it is actually the one you want: it enables induction over well-founded orders, without using either choice or excluded middle. Assuming excluded middle, it is equivalent to the previous one.

Finally, the business in the wikipedia article about ordinals is not really necessary for any technical analysis of termination, and, in addition, choice is not required if you define $\omega_1$ to be the order type of the set of countable ordinals (ordered by the prefix relation).