Rule induction principles in Harper's PFPL
At the beginning of Section 2.4 the book explains that $\mathcal{P}(J)$ stands for a property of a judgment $J$. That is, the $\mathcal{P}$ in $\mathcal{P}(a\ \mathtt{nat})$ does not stand for a property of numbers, but a property of the judgment $a\ \mathtt{nat}$, which is the judgment that "$a$ is a number".

It just so happens that the inference rules for $a\ \mathtt{nat}$ precisely match those for numbers. Namely, the two rules defining the judgment $a\ \mathtt{nat}$ are
$$\frac{ }{\mathtt{zero}\ \mathtt{nat}}$$
and
$$\frac{a\ \mathtt{nat}}{\mathtt{succ}(a)\ \mathtt{nat}}.$$
Therefore, if we want to show that the judgment $a\ \mathtt{nat}$ has some property $\mathcal{P}$, then we need to show that the base case $\mathtt{zero}\ \mathtt{nat}$ has the property $\mathcal{P}$, and that whenever $\mathcal{P}(a\ \mathtt{nat})$ holds then $\mathcal{P}(\mathtt{succ}(a)\ \mathtt{nat})$ holds as well.

Or to put it the other way, the strange looking "$\mathtt{nat}$" is there because we are not talking about numbers, but about the judgments "expression $a$ satisfies the judgment $\mathtt{nat}$".