Recall the definition of a well-founded relation from Coq's library :
Inductive Acc (A : Set) (R : A -> A -> Prop) (x : A) : Prop :=
Acc_intro : (forall y : A, R y x -> Acc A R y) -> Acc A R x.
Definition well_founded (A : Set) (R : A -> A -> Prop) :=
forall x : A, Acc A R x.
In other words, if all the predecessors y of an element x are accessible, then x is accessible too. This Coq definition accepts all usual mathematical well-founded relations, for example the strict order < on the natural numbers.
However, how can we prove that the strict order on the signed integers is not well-founded in this Coq sense ? As a constructive proof of a negation, we would start by assuming by contradiction that the order on signed integers is well-founded. That means all signed integers are accessible. Where is the contradiction in that ? Acc_intro looks happy with it.
But if we axiomatize that the order on signed integers is well-founded, we will be able to define a function recursively on them. The computation of this function will be an infinite loop, which seems to break the consistency of Coq's logic.
Did I make a mistake somewhere ?
If < were well-founded on the integers, the following function would terminate:
f : Z -> False
f x = f (x - 1)
Thus, f 0 would yield a proof of False. We can formalize this argument in Coq as follows:
Require Import Coq.ZArith.ZArith.
Lemma Z_lt_not_well_founded : ~ well_founded Z.lt.
Proof.
intros Hwf.
exact (Fix Hwf (fun _ => False) (fun x IH => IH (Z.pred x) (Z.lt_pred_l x)) 0%Z).
Qed.