What is the computational content of induction?

I must first admit that I have troubles formulating my question. I'll try to do my best.

Peano Arithmetic postulates induction as an axiom out of the thin air. I understand the convenience of this setup for various tasks, nevertheless it seems quite specialized to me.

I'm looking for alternative 'axioms' that might be more 'natural' and might be sufficient to have 'general inference rules' as a consequence, in particular natural number induction, perhaps structural induction.

ZFC seems to achieve that through axiom of infinity, but perhaps even that is not needed.

I want to understand the computational content of induction as deeply as I can.

I took the natural numbers as a case study. A definition:

$$\frac{}{\mathsf{Nat\; Z}}\;\mathsf{(NZ)}$$

$$\frac{\mathsf{Nat}\;a}{\mathsf{Nat\;S}\;a}\;\mathsf{(NS)}$$

Now let's try to prove that the predecessor of non-Z Nat is Nat:

$$\frac{\mathsf{Nat\;S}\;a}{\mathsf{Nat}\;a}\quad\mathsf{(N\;pred)}$$

I don't see a way to derive this rule just from rules (NZ) and (NS) above. I don't see how to formulate this rule as a consequence of the other two (in '$a$-generic' way).

On the other hand, for any proof of $\mathsf{Nat\;S}\;a$ derived using only the rules (NZ) and (NS) I see an algorithm to transform it into a proof of $\mathsf{Nat}\;a$.

Here are some random ideas on how to achieve the missing annotation 'only (NZ) and (NS) produce Nat judgements':

• Have the set of rules globally fixed (close to System T approach?). Prove the induction in meta-logic.

• Allow introduction of 'closed' types like $\mathsf{Nat}\;a$ (no additional rules added later). Automatically provide case analysis rule. [This seems to me similarly ad-hoc to PA induction axiom]

• Perhaps another place to attach this information could be (N pred) rule i.e. 'assumes premise was created using (NZ) or (NS)'.

• Perhaps encode Nat in System F and use parametricty. Is this sufficient? Is it more principled?

How can I understand the topic better ?

Is there a good question that capture what I want to understand ?

• Can you clarify why you find the induction scheme in PA (or the induction axiom in second-order PA) ad hoc? – Noah Schweber May 29 '18 at 0:33
• I guess it is a subjective, and almost aesthetic judgement. The fact that it naturally applies only to the natural numbers and not trees (I am aware of possible but non-unique encodings). Existence of coinductive data and proofs might weight in on that too. – Łukasz Lew May 29 '18 at 5:19