The proofs of basic statements of the form (examples below) $\mathsf{PA}^-\vdash\varphi$ use some sort of induction on the natural numbers, and I wonder what explicitly gives us the idea that this is a valid form of argument?
I understand these meta proofs are not in $\mathsf{PA}^-$, but what are we reasoning in? They are statements about the natural numbers, and so to prove statements about the natural numbers are we not implictly working from some set of axioms?
Some examples which use such proofs:
Let $n,k,l\in\mathbb{N}$. Denote by $\underline n$ the closed terms $\underline n=\underbrace{1+\ldots+1}_{n\;\text{times}}$ for $n\in\mathbb{N}$. Then
- if $n=l+k$ then $\mathsf{PA}^-\vdash\underline n=\underline l + \underline k$;
- if $n=l\cdot k$ then $\mathsf{PA}^-\vdash\underline n=\underline l \cdot \underline k$;
- $\mathsf{PA}^-\vdash \forall x(x\le \underline k \rightarrow x=\underline 0\vee\cdots\vee x=\underline k).$
In this kind of proof we are using induction ("in the metalanguage") to prove something about the theory that does not have induction as an axiom ("in the object language").
Is it legitimate ?
Of course, this sort of proof can be formalized in $\mathsf {PA}$.
In general, is hard to imagine that we can manage the meta-theory of a mathematical theory without some sort of induction. Consider e.g the proof of soundness of first-order logic : it needs induction on the lenght of the derivation.