Well-foundedness: classical equivalence of no infinite descent and accessibility

Question

I have often seen the claim that in a classical setting, well-foundedness of a relation > defined as the absence of an infinite descent x_0 > x_1 > x_2 > ... is equivalent to the constructive definition using an accessibility predicate as in Coq's Acc:

Inductive Acc (x: A) : Prop :=
  Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x.

Definition well_founded := forall a:A, Acc a.

where R : A -> A -> Prop.

It seems it requires some version of choice but I don't know which is weakest one has to assume to construct such a proof.

Answer 1

This is not a Coq proof, but it's a proof sketch using the axiom of dependent choice and LEM to exhibit an equivalence. I believe this is the weakest choice principle you can get away with, but I cannot find a reference. It's too long for a comment unfortunately.

Edit: it's no longer just a paper proof! @kyo dralliam has formalized the below argument in Coq and gone further to show that the choice additional axioms (dependent choice, LEM) are also necessary as well as sufficient.

---

Let's define $\mathsf{idc}(A,R,a)$ to be the proposition which states that there is an infinite descending chain in $(A,R)$ starting with $a$: $$ \mathsf{idc}(A,R,a) = \exists f : \mathbb{N} \to A.\ f(0) = a \land (\forall n.\ f(n) \mathrel{R} f(n + 1)) $$

We will show that $\neg \mathsf{idc}(A,R,a) \iff \mathsf{Acc}(A,R,a)$. The $\Leftarrow$ direction follows by induction on $\mathsf{Acc}$ and requires no non-constructive principles. The inductive step can be summarized as "if $\mathsf{idc}(A,R,a)$ holds, there is some $b$ such that $a \mathrel{R} b$ and $\mathsf{idc}(A,R,b)$ holds."

For the other direction, let's use LEM and assume $\neg \mathsf{Acc}(A,R,a)$ to derive a contradiction. We will achieve this contradiction by constructing an infinite descending chain and this is where we will use the axiom of dependent choice.

To that end, consider the type $B(a) = \{x : A \mid a \mathrel{R^*} x \land \neg \mathsf{Acc}(A,R,x)\}$ and write $S$ for the restriction of $R$ to this type. Let's prove that $S$ is entire, that is if $b : B(a)$ then there exists some $c$ such that $b \mathrel{S} c$. I've deferred this lemma to the bottom of the answer, to not clutter up the proof. Since $(B(a),S)$ is entire and non-empty with $a : B$ by assumption, the axiom of dependent choice gives us an infinite descending chain within $B(a)$: $b_0 \mathrel{S} b_1 \mathrel{S} b_2 \mathrel{S} b_3 \dots$. By definition of $S$, this induces a chain $b_0 \mathrel{R} b_1 \mathrel{R} b_2 \dots$. Moreover, by definition of $B(a)$ we can extend this chain so that it starts with $a$. We now derive our contradiction from $\neg\mathsf{idc}(A,R,a)$.

---

Lemma. $(B(a),S)$ is entire.

Proof. Assume we are given $b : B(a)$. By assumption, $\neg \mathsf{Acc}(A,R,b)$. Unfolding this, we see that it's equivalent to the following: $$ \neg (\forall b. a \mathrel{R} b \to \mathsf{Acc}(A,R,b)) $$

By LEM again, we obtain $c : A$ such that $a \mathrel{R} c$ and $\neg \mathsf{Acc}(A,R,c)$. Therefore, $c : B(a)$ and $b \mathrel{S} c$ as required.

---

Answer 2

The Lean proof is here. It uses the axiom of choice as stated here

I can summarise as follows. We'll prove that if a relation is not well founded, then there is an infinite descending sequence (we used excluded middle here). For any x such that ¬ acc r x, there exists a smaller y such that ¬ acc r y. This is because the definition of acc is that everything smaller is acc. There's another use of excluded middle here.

We also use excluded middle to prove the existence of one x such that ¬ acc r x

So we have ∀ x : {a // ¬ acc r a}, ∃ y : {a // ¬ acc r a}, y.1 < x.1, and from this, using the axiom of choice, we have the existence of a function {a // ¬ acc r a} → {a // ¬ acc r a} such that r (f x) x. We can iterate this function to define our infinite descending sequence.

Answer 3

Interesting question! My guess would be that just using LEM a relation is well-founded iff it does not contain an entire inverse subrelation. Turning this into a descending sequence represented as function from the natural numbers then sounds like dependend choice maybe?

I have checked the argument now in Coq and while the answers given in the meantime perfectly explain the equivalence to DC, here's a brief addition/refinement regarding the use of DC depending on the concrete formulation of infinite descent.

The usual definition Théo already suggested by the notation $x_0>x_1>x_2>\dots$ is based on a function $f:\mathbb N \to X$ representing a descending chain. However, descent can also be formulated as a non-empty set $P$ such that for all $x\in P$ there is $y\in P$ with $y< x$. This notion of an entire subrelation shows up in Daniel's answer and its absence is indeed equivalent to well-foundedness just using LEM:

• If $<$ is well-founded, then there is no entire subrelation $P$. Proof: As before by induction on Acc for the witness $x\in P$ of non-emptiness.

• Given LEM, if there is no entire subrelation, then $<$ is well-founded. Proof: Exactly as before, suppose $x$ were not accessible, then the inaccessible points form an entire subrelation.

This now localises the use of DC, since this is exactly the requirement to turn an entire subrelation into a chain, the other direction is of course for free:

• If there is no entire subrelation, then there is no descending chain. Proof: Assume $f$ were a descending chain, then its range induces an entire subrelation.

• Given DC, if there is no descending chain, then there is no entire subrelation. Proof: Assume $P$ were entire, then using DC on the type $\Sigma P$ and the relation $\lambda x y.\, y < x$ yields a descending chain.

(Of course the above implications are actually proven in the stronger contrapostive form but I chose the weaker form to align with well-foundedness.)