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.