Rank-Induction Principle (following Van Dalen's Logic and Structure, 4th edition)

Question

This post contains questions on understanding Van Dalen's proof of the Rank-Induction principle and questions concerning its wording and presentation. Please don't feel obliged to answer everything. Anyways, we begin with the theorem's statement:

Theorem 1.1.8 (Induction on rank-Principle) If for all $\varphi$, [$A(\psi)$ for all $\psi$ with rank less than $r(\varphi)$] $\Rightarrow A(\varphi)$, then $A(\varphi)$ holds for all $\varphi \in PROP$.

I assume here that the theorem is simply a statement of a strong mathematical induction principle on the rank of propositions. Please correct me if this is the wrong interpretation of the theorem's statement. Assuming this is the case, why must we show that strong (mathematical) induction on rank is equivalent to the previously defined structural induction (Theorem 1.1.3)? In other words, what is the significance of this equivalence? Moving on, we continue with the author's proof:

Let us show that induction on $\varphi$ and induction on the rank of $\varphi$ are equivalent. First we introduce a convenient notation for the rank-induction: write $\varphi \prec \psi$ ($\varphi \preceq \psi$) for $r(\varphi) < r(\psi)$ ($r(\varphi) \leq r(\psi)$). So $\forall\psi\preceq\varphi A(\psi)$ stands for "$A(\psi)$ holds for all $\psi$ with rank at most $r(\varphi)$". The Rank-Induction Principle now reads $$\forall\varphi(\forall\psi\prec\varphi A(\psi) \Rightarrow A(\varphi)) \Rightarrow \forall\varphi A(\varphi).$$ We will now show that the rank-induction principle follows from the induction principle. Let $\forall\varphi(\forall\psi\prec\varphi A(\psi) \Rightarrow A(\varphi))$ be denoted by ($\dagger$). In order to show $\forall\varphi A(\varphi)$ we have to indulge in a bit of induction loading. Put $B(\varphi) := \forall\psi\preceq\varphi A(\psi)$. Now show $\forall\varphi B(\varphi)$ by induction on $\varphi$.

It appears that this part of the proof is showing that rank induction follows from structural induction. But, later in the proof Van Dalen writes

For the converse we assume the premises of the induction principle.

This made me further confused as to the organization of the proof. It seems as if the first section is using structural induction to show $\forall\varphi B(\varphi)$, but then the second part starts off by assuming the premises of structural induction. Are these not proving the same direction (i.e. rank induction follows from structural induction)? Moreover, what motivates the definition of $B(\varphi)$? Doesn't strong induction only require that we show a property holds for all propositions with rank strictly less than the rank of the current proposition $\varphi$? Yet the author uses $\preceq$ when stating the property $B$.

If someone could either carefully trace through the author's proof or provide an alternative proof, it would be greatly appreciated.

Answer 1

Van Dalen's approach is explained in the previous paragraph:

"The introduction of the rank function above is not a mere illustration of the ‘definition by recursion’, it also allows us to prove facts about propositions by means of plain complete induction (or mathematical induction). We have, so to speak, reduced the tree structure to that of the straight line of natural numbers."

Th.1.1.3 is structural induction because it uses the construction tree.

Th.1.1.8 (Induction on rank-Principle) is strong induction based on rank that is a natural number: thus, it is the "usual" mathematical induction.

The equivalence is showed in two steps: the first one concludes that $A(\varphi)$ holds for all $\varphi \in \text {PROP}$ assuming that

"if $A$ holds for all formulas $\psi$ with rank less than that of $\varphi$, then $A$ holds of formula $\varphi$".

This is the antecedent of Th.1.1.8 ["iff for all $\varphi$ [$A(\psi)$ for all $\psi$ with rank less than ..."] and we have to prove the consequent: "then $A(\varphi)$ holds for all ...".

To derive it, the author defines a new property $B$ and shows that $B$ holds of atomic formulas, and that it "propagates" along the construction tree (the two basic cases with connectives $\lnot$ and $\square$).

Thus, using Th.1.1.3 [structural induction], it follows that "$∀\varphi B(\varphi)$, and as a consequence $∀\varphi A(\varphi)$", which is the conclusion of Th.1.1.8 [rank induction].

The second part proves Th.1.1.3 using Th.1.1.8.

So, again, we assume the antecedent of Th.1.1.3: "$A$ holds for atomic formulas and propagates with connectives" and we have to prove the consequent: "$A(\varphi)$ holds for all $\varphi \in \text {PROP}$".

To do this, the author shows that from the assumptions above it follows that the formula ["dagger"] holds. This formulas expresses the antecedent of Th.1.1.8 [rank-induction]; thus, from it and modus ponens we conclude with the consequent of the theorem, that is the consequent of Th.1.1.3 [structural induction].