Rule induction principles in Harper's PFPL I have a few small questions about section 2.4 ("Rule induction") in Practical Foundations for Programming Languages (p. 19).

(1) In the rule induction principles for nat,


  To show P(a nat) whenever a nat, it is enough to show:
  (1) P(zero nat).
  (2) for every a, if (a nat and) P(a nat), then P(succ(a) nat).


why is the bracketed "(a nat and)" clause necessary (and similarly for tree)?  This seems "natural" - we shouldn't need to prove things about syntactic entities that don't define nats - but doesn't appear in the definition given of property P "respecting the rules" defining nat/tree (also on p. 19), which is how the rule induction principle is defined.  In the proof of Lemma 2.1, the extra "a nat and" part has become part of the definition of the property P - what's going on here?

(2) I don't understand the induction step of Lemma 2.1 (succ(a) nat implies a nat).  If I were doing this proof, I'd just invert the rules for nat right away, or, using Harper's property P, say: If succ(a) is of form succ(b), then by injectivity, a equals b, hence b nat as a nat, but injectivity hasn't been proven yet.  It seems instead that Harper applies the induction hypothesis about a directly to succ(a) - I must be missing something.

(3) In a more naive framework, Lemma 2.3 would just follow from sufficiency of the = nat relation rules ("inversion"), but I don't know how to write down a proof in this style.  Why is induction even needed?

I'm sorry if these questions seem like nitpicking, but Martin-Löf/LF feels very foreign to me.  If I squint and pretend I'm doing everything in a more "traditional" operational semantics, I can read other parts of the book (with slightly different proofs), but I feel I'm missing the point in doing so.

If these questions are too tedious to answer individually, are there other references on doing semantics in this style?
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}$".