I honestly don't follow your first claim or how it has any bearing on this question. Perhaps you could provide a link to the actual theorem you're describing to clarify.
GP is alluding to the fact that any unprovable true statement about the integers has a counter-model for which the statement is false which the formal system cannot distinguish from the integers. Therefore no formal system characterizes the integers, there are always these false integers lingering.
These objects are highly pathological artifacts of the formal system in question, but that just goes to show how slippery the integers are.
> GP is alluding to the fact that any unprovable true statement about the integers has a counter-model for which the statement is false which the formal system cannot distinguish from the integers.
Again, do you have a link or a name for the theorem you're describing?
Ok, now we're getting somewhere [1]. So various theorems can be used to prove the existence of non-standard models of arithmetic. I'm not sure why I should find this compelling.
There are infinitely many possible models of arithmetic, each of which has different properties. Some of these are isomorphic to standard models in various ways, some of which are not.
But, if the world is governed by mathematics, then at least one such model would best match reality. How would we even speak of a world which was not internally consistent such that it could be formalized in such a fashion?
I'm not sure what you're asking. Any formalization of the integers won't be "the" integers, the totality of which perhaps isn't even a reasonable idea.
Mathematics is a part of the world and does not stand apart from it. There is no reason why such a "best" model should exist, and by any reasonable definition, it doesn't. Mathematics is irrefragably incomplete. It is perhaps the only human discipline that demonstrates its own limits.
> Any formalization of the integers won't be "the" integers, the totality of which perhaps isn't even a reasonable idea.
"The integers" is whatever formal model we all agree has the properties we want of the integers. This is a language game, it's merely a label for a set of properties.
> Mathematics is a part of the world and does not stand apart from it.
If you mean that mathematics follows from naturalism, this is at best a conjecture. We could very well live in a mathematical universe (ala Platonism), in which case our world is itself a particular mathematical structure. This is actually a far less problematic view of mathematics, philosophically.
> There is no reason why such a "best" model should exist
There are many reasons why a "best" model of reality should exist. For one, as I mentioned above, mathematical monism is a less problematic philosophy of mathematics. It then immediately follows that positing a separate physical world is multiplying entities unnecessarily, ergo, considering the universe to be mathematical is the most parsimonious theory.
But even going a different route, as I said many posts up, denying an accurate and precise mathematical of reality entails some irreconcilable inconsistency in reality, which so far has completely failed to manifest itself. We very well could be a brief island of stability in a random output generator, but ordering my hypotheses by likelihood, this would necessarily be dead last (because its incompressible ala Solomonoff induction).
Second order induction could hardly be called a formal system: There is no complete, effective proof system for it. This is the basically the same limitation on first order PA. The standard model for second order arithmetic involves the power set of the naturals which is immediately a far more complex object than any computable system; it essentially presupposes the object that you're trying to formalize in the first place.
I don't see why the lack of a complete effective proof system for it should be a problem.
I do in fact consider the power set of the naturals to exist, so I'm not sure I see the problem? Is it just that uncountable sets have elements that we cannot pick out? I don't have a problem with that.
It matters because it means second order arithmetic isn't a finite object in the same way first order effective theories are where you might have "infinitely" many axioms but they are packaged up in a finite object, an algorithm.
The whole point of a formal system, its formality, is that it doesn't require any semantic notions to describe it. Second order arithmetic with its full model is no such thing. It is inherently infinitary and therefore not formal at all.
And it's a treacherous object. C.f. Richard's paradox which demonstrates that "subset of the integers" is by no means a naive idea.
