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 do worry that there’s some technical subtlety not obvious until the end game that makes this particular construction impossible. I’ve been trying to spot some places where something might go wrong, and there are a few parts I don’t know how to fill in. I think there might be a problem relativizing a proof of the totality of ordinal multiplication which may prevent either the proof predicate relativization or the transfinite induction derivation from working. Or there may be some more subtle reason the steps I outlined won’t work. I was hoping that someone in the community might be able to say “I’ve seen this before, and it didn’t work because of XYZ”, but that hasn’t happened yet, which means I’ll probably have to attempt to formalize the whole argument to get a definitive answer, which I’m not confident is worth the effort.
Regardless, I don’t think my idea relies on this specific construct. The example from the beginning of the post that I find unsatisfying already sidesteps lob’s theorem, and just because I’m unsatisfied with it doesn’t mean it, or something equally as simple, isn’t useful to someone. Even if there’s a mistake here, I think the broad idea has legs.