16
$\begingroup$

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.

$\endgroup$
0

3 Answers 3

15
$\begingroup$

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.


$\endgroup$
4
  • $\begingroup$ This argument more precisely that $\mathsf{idc}(A,R,a) \iff \neg\mathsf{Acc}(A,R,a)$. LEM is necessary to prove this: Take $A=\{a\}$ then $\mathsf{idc}(A,R,a) \iff a \mathrel{R} a$ and $\mathsf{Acc}(A,R,a) \iff \lnot(a \mathrel{R} a)$. Since $R$ is arbitrary, LEM follows from the equivalence. The stated equivalence $\lnot\mathsf{idc}(A,R,a) \iff \mathsf{Acc}(A,R,a)$ appears to be a bit more subtle. $\endgroup$ Mar 18 at 9:03
  • 9
    $\begingroup$ Dependent choice is also necessary, see here for a proof in Coq. $\endgroup$ Mar 18 at 12:44
  • $\begingroup$ @kyodralliam: Very good, you beat me to it in formalization :-) The answer should be updated with a refefence to Kenji's proof. $\endgroup$ Mar 18 at 16:09
  • $\begingroup$ @kyodralliam Very cool! I've added a paragraph to the above answer. $\endgroup$ Mar 18 at 17:11
8
$\begingroup$

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.

$\endgroup$
4
  • 1
    $\begingroup$ I think “y such that ¬ acc r x” should be “y such that ¬ acc r y”, but edits must be 6 characters, so I can't make the change. $\endgroup$
    – mudri
    Mar 17 at 22:45
  • $\begingroup$ Thanks, I made the edit $\endgroup$ Mar 17 at 23:15
  • $\begingroup$ If I could I would have accepted this answer too. Thank you very much. $\endgroup$ Mar 18 at 10:29
  • $\begingroup$ Just to point out, dependent choice is strictly weaker than full AC (addressing the "weakest" part of the question). $\endgroup$
    – Josh Chen
    Mar 18 at 16:30
3
$\begingroup$

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.)

$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.