I think you’ve misunderstood what I was saying. I am not claiming that we can prove a material equivalence, an internal formal equivalence, between N and Na; that would require induction. The only things which that statement claimed were being formally proved within Q were 1. and 2. Neither of those statements require induction. 1. allows us to treat Na as, at most, N. 2. allows us to treat Na as, at least, N. Both together allow us to treat Na as N (within limits). Only 1. and 2. are internal, there are no other formal statements. That 1. and 2. are sufficient for demonstrating that N and Na are semantically the same is a metatheoretic observation which I think is intuitively obvious.
The point is that we can see, through internal theorems, that N and Na are the same, not with a material equivalence, but with some weaker conditions. This justifies treating Na as an alternative definition of N, one which we can use to formally prove more than we could with N. This is a different perspective than is usually taken with formal mathematics where there’s often considered only one definition, but incompleteness opens the possibility for formally distinct, semantically equivalent definitions. I think that’s exploitable but historically hasn’t been exploited much.
I think you’ve misunderstood what I was saying. I am not claiming that we can prove a material equivalence, an internal formal equivalence, between N and Na; that would require induction. The only things which that statement claimed were being formally proved within Q were 1. and 2. Neither of those statements require induction. 1. allows us to treat Na as, at most, N. 2. allows us to treat Na as, at least, N. Both together allow us to treat Na as N (within limits). Only 1. and 2. are internal, there are no other formal statements. That 1. and 2. are sufficient for demonstrating that N and Na are semantically the same is a metatheoretic observation which I think is intuitively obvious.
The point is that we can see, through internal theorems, that N and Na are the same, not with a material equivalence, but with some weaker conditions. This justifies treating Na as an alternative definition of N, one which we can use to formally prove more than we could with N. This is a different perspective than is usually taken with formal mathematics where there’s often considered only one definition, but incompleteness opens the possibility for formally distinct, semantically equivalent definitions. I think that’s exploitable but historically hasn’t been exploited much.