If well-founded induction holds, then the relation $\to$ on a reduction system terminates I am trying to understand a proof from &quot;Term Rewriting and All That&quot; by Baader and Nipkow.
Well-founded induction (WFI) is the following statement:

$\forall x \in A(\forall y \in A(x \stackrel{+}{\to}y \Rightarrow P(y))\Rightarrow P(x)) \Longrightarrow \forall x\in A (P(x))$

Here is the proof I cannot understand.

Theorem: If well-founded induction holds, then the relation $\to$ on a reduction system terminates.
Proof: by WFI, where $P(x):=$ &quot;there exist no infinite chain starting from $x$&quot;. The induction step is simple: If there exist no infinite chains starting from any successor of $x$, then there exist no infinite chains starting from $x$. Hence, the premise of WFI holds, and we can conclude that $P(x)$ holds for all $x$ i.e., $\to$ terminates.

Why can we define $P(x)$ to be &quot;there exist no infinite chain starting from $x$&quot;?
Well-founded induction, like all other forms of induction, holds for any predicate $P$. That can mean two different things:


Well-founded induction holds for every predicate which you can express in your formal system.
Well-founded induction holds for every subset $P \subseteq A$.


Either way, informally speaking you can define $P$ to be whatever you want. 

Formally speaking, you might run into set-theoretic issues, those that separate naive (or elementary) set theory from axiomatic set theory. But presumably this is not the focus of the book, so you can just ignore such issues.

(The gap is that in case 1, you need to show how to express $P$, and in case 2, you need to show that the set $\{x \in A : \text{there exists no infinite chain starting at $x$}\}$ exists.)