If a relation is terminating, then well-founded induction holds.

29 Views Asked by At

Proposition: If the relation $\to$ is terminating, then well-founded induction holds.

ProofAttempt: If $\to $ terminates, then $\exists$ no infinite descending chains such as $a_0 \to a_1 \to \cdots$. Suppose $\forall x (\forall y (x \xrightarrow{+} y)\Rightarrow P(y))\Rightarrow P(x)$. We assert that $\to$ is terminating implies $\to$ is normalizing. If $\to$ is not normalizing, then $\exists x$ such that $x$ does not have a normal form. In other words, $\forall y$ $x \xrightarrow{+} y \Rightarrow \exists \gamma(y \to \gamma)$; i.e., there exists an infinite descending chain (e.g. $x\to \cdots y \to \cdots \gamma \to \cdots$). Thus, $\to $ is not terminating. By contraposition, our assertion holds. Since our assertion holds, then $\forall x \exists y$ such that $x \overset{+}{\to} y$. If $x \overset{+}{\to}y$ implies $P(y)$ is true, then by assumption $P(x)$ is true. Since $x$ is arbitrary, then $P(x)$ holds for all $x$, as desired.