How to understand the two definitions of finite descent are logical equivalent?

Question

I find two definitions of finite descent principle.

The first is in the book "A beginner's guide to mathematical logic", Ch4, P40: Suppose a property P is such that for any natural number n, if P holds for n, then P also holds for some natural number less than n. Then P doesn't hold for any natural number.

But I also see another kind of definition. Suppose P is such that for any natural number n, if P fails for n, then P fails for some number less than n. Then P holds for all natural numbers. For example, such definition is used in this post: Infinite descent method and strong induction

So I infer that the two definition must be logically equivalent, but how to understand the equivalence?

Answer 1

Yes, you are correct. Symbolically, the first definition says:

$\left(P(n), n\in \mathbb{N} \Rightarrow \exists m\in \mathbb{N}, m<n, P(m) \right) \Rightarrow (\lnot P(n)\forall n \in \mathbb{N})$

and the second definition says:

$\left(\lnot P(n), n\in \mathbb{N} \Rightarrow \exists m\in \mathbb{N}, m<n, \lnot P(m) \right) \Rightarrow (P(n)\forall n \in \mathbb{N})$

so thesecond definition is equivalent to the first, with $P$ replaced by $\lnot P$ and $\lnot P$ replaced by $P$.

Answer 2

I try to answer it myself.

Since the finite descent principle holds for all properties, including P and -P. So if we replace P of the first definition, then we get the second definition.

Is my understanding right?