I think this is wrong. Because we can run the Turing machines for max(n1, n2) steps. If a machine halts after that many steps, then it rules out the lesser value. If none of them halts after that many steps it rules out the greater value.
So our only uncertainty is between one specific number, and some unspecific bigger number that forever recedes into the distance as we try to approach it.
You propose that the issue is some pesky non-standard numbers that are bigger than any other number. But I'm thinking the issue is rather the for-all symbol.
Like from the outside of the theory we can see that we can prove a certain property for 1, for 2, for 3 etc, in fact we can prove this property for any number. But inside the theory we cannot prove that for-all n the property holds. So there is a divergence between what we want for-all to mean and what it actually ends up meaning?
Or using the there-exists perspective, if there exists an actual object inside a theory that satisfies a property P, then there-exists x such that P(x) will be true. But it can also be true without such an actual object existing.
However, your description is just another way of saying what I'm saying about nonstandard numbers. From outside of the theory you can prove P(1), P(2), P(n) for any N that is an actual natural number, but from inside of the theory you can't do that. Why not? Because from inside of the theory there is a model that is completely consistent with Peano arithmetic but contains some object E that is greater than any standard natural number. The theory can not eliminate the existence of this E and in fact it's possible to construct an E such that P(E) is false.
So our only uncertainty is between one specific number, and some unspecific bigger number that forever recedes into the distance as we try to approach it.
You propose that the issue is some pesky non-standard numbers that are bigger than any other number. But I'm thinking the issue is rather the for-all symbol.
Like from the outside of the theory we can see that we can prove a certain property for 1, for 2, for 3 etc, in fact we can prove this property for any number. But inside the theory we cannot prove that for-all n the property holds. So there is a divergence between what we want for-all to mean and what it actually ends up meaning?
Or using the there-exists perspective, if there exists an actual object inside a theory that satisfies a property P, then there-exists x such that P(x) will be true. But it can also be true without such an actual object existing.