[Epistemic status: I think everything I write here is true, but I would feel better if a passing logician would confirm.]
Great question! The important thing to keep in mind is that truth only makes sense relative to an interpretation. That is, given a statement S in your system, you can ask whether it’s true in a particular interpretation, but it might be true in some interpretations and false in others.
Here’s a fun fact: S is true in every interpretation of the system if and only if Sis provable. (Proof: clearly if S is a theorem then it is true in every interpretation. Conversely, Godel’s completeness theorem says that if S is true in every interpretation then it is a theorem.)
So when you ask for “naturally occurring” true-but-unprovable statements, do you want
a statement which is true in every interpretation but unprovable? or
a statement which is true in some interpretation but unprovable?
If it’s (1), then the fun fact above says that no such statements exist. If you want (2), then by taking the contrapositive of the fun fact, you’ll see that this is the very same as asking for a statement S such that neither S nor ‘not S’ is a theorem! In other words, you’re looking for a statement which is independent of your system. And you probably already know of oodles of these: the axiom of choice is independent of ZF set theory, the continuum hypothesis is independent of ZFC, large cardinal axioms, etc.
--
I have a feeling that this purely mathematical explanation may have done nothing to cure your core confusion, so let me write something else here which I think strikes more at the heart of the question. We often like to think that the integers exist; that there’s a God-given copy of the integers sitting out there in metaphysical space, not a formal model, but the real thing which the axioms are trying to capture. By the discussion above, we know that no matter what axioms we impose, we’ll never be able to fully capture the integers (because any formal system will always have unproveable truths, and therefore multiple interpretations, and therefore allow for models of the integers with are different than the real ones).
So when you ask for unproveable truths, maybe you’re not asking for an unproveable statement which is true in some interpreation, maybe you’re asking for an unproveable statement which is true in the one true interpretation. That is, you want a statement which is true about the actual integers, the real out-in-the-world number system that we’re trying to model, but unproveable. I don’t know of any “naturally occurring” statements like that off the top of my head (though some people think that the Goldbach conjecture might be one).
But if you replace “integers” everywhere in the last paragraph with “universe of sets” you can say very much the same thing. That is, we might intuitively believe that there is an actual universe of sets which the ZFC axioms are merely trying to model. And then you can take a statement independent of ZFC—the continuum hypothesis say—and ask “is this is true in the real, actual universe of sets?” If yes, then that’s your unproveable truth. If no, then its negation is.
So yes, naturally occurring unproveable truths abound, at least in set theory (but depending on what you think the real universe of sets looks like, you might disagree with others about what they are).
By the discussion above, we know that no matter what axioms we impose, we’ll never be able to fully capture the integers (because any formal system will always have unproveable truths, and therefore multiple interpretations, and therefore allow for models of the integers with are different than the real ones).
Assuming we use first-order logic, right?
Here is the part where I got stuck.. what exactly causes this attitude that if something cannot be accomplished using first-order logic, the reasonably thing is to give up? I assume there is a good reason behind that, but I have never heard it said explicitly, so to me it kinda sounds like “we found out that it is impossible to build a spaceship using wood, therefore there shall be no space travel”, as opposed to trying to find a more suitable material for building spaceships.
So, there is some first-order-logicness in the very concept of proof? Like, if you describe something using the first-order logic, then you can use a machine to algorithmically check the validity of the proof… and using some stronger methods could allow us to make the interpretation less ambiguous, but the cost would be that now we no longer can mechanically check the correctness?
Your original question (about the focus on first-order logic) was a very good one. I asked a logician friend about it, and his answer was the same as the one that you and Samuel settled on here—first-order logic is likely the best that humans brains (or machines) are able to access. So yeah, basically a version of the Church-Turing thesis.
They referred me to Lindström’s theorem as a concrete result in that direction. I don’t know enough to understand the statement of the theorem, but it seems to say something along the lines of “first-order logic is the strongest logic which still has [some properties that computable systems ought to have?].”
Fun fact I learned in the conversation: it is a theorem of first-order ZFC that the models of second-order ZFC are constrained enough to single out a canonical model of the integers.
Thank you for this answer. You also helped make another point of confusion clearer: When I read the op I wasn’t sure what the interpretation of number theory is. There must be one or the incompleteness theorem wouldn’t apply but what is it?
Based on your comment here I understand this better and it makes more sense why people might disagree about for example the continuum hypothesis being “reasonable”. While mostly everyone agrees on the standard ZFC axioms not everyone agrees on the interpretation of ZFC.
Then there must also be hardliners who take ZFC as the truth without interpretation and thus do not allow statements independent of it as they are not provable. It would be interesting to see what proofs they miss out on. (Not requesting anyone to list them for me, just thinking out loud.)
I think this interpretation is both intriguing and clarifying, thanks. It suggests that a good framing of the incompleteness theorem is:
Any sufficiently rich system S can be extended by multiple interpretations I, such that all of its provable theorems are true for all of I, but I contains interpretations who disagree on the truth of some unprovable statements of S
And if you try to narrow down the interpretations, you either don’t get far enough—because there are infinitely many possible interpretations, and no matter how many times you exclude half of them by adding a new axiom, still infinitely many possible interpretations remain—or you introduce some new concept—but then this new concept has its own multiple interpretations.
For example, if you try to make axioms for integers, it turns out that there are also some “nonstandard integers” which technically satisfy the axioms, even if they are obviously not the thing we meant. The traditional way out is to add an axiom like “the actual integers are the smallest set (from the perspective of set inclusion) of things that satisfy these axioms”, but now you have invoked the concept of a set, and if you try to define what that means, you just open another can of worms… and this process never stops.
[Epistemic status: I think everything I write here is true, but I would feel better if a passing logician would confirm.]
Great question! The important thing to keep in mind is that truth only makes sense relative to an interpretation. That is, given a statement S in your system, you can ask whether it’s true in a particular interpretation, but it might be true in some interpretations and false in others.
Here’s a fun fact: S is true in every interpretation of the system if and only if S is provable. (Proof: clearly if S is a theorem then it is true in every interpretation. Conversely, Godel’s completeness theorem says that if S is true in every interpretation then it is a theorem.)
So when you ask for “naturally occurring” true-but-unprovable statements, do you want
a statement which is true in every interpretation but unprovable? or
a statement which is true in some interpretation but unprovable?
If it’s (1), then the fun fact above says that no such statements exist. If you want (2), then by taking the contrapositive of the fun fact, you’ll see that this is the very same as asking for a statement S such that neither S nor ‘not S’ is a theorem! In other words, you’re looking for a statement which is independent of your system. And you probably already know of oodles of these: the axiom of choice is independent of ZF set theory, the continuum hypothesis is independent of ZFC, large cardinal axioms, etc.
--
I have a feeling that this purely mathematical explanation may have done nothing to cure your core confusion, so let me write something else here which I think strikes more at the heart of the question. We often like to think that the integers exist; that there’s a God-given copy of the integers sitting out there in metaphysical space, not a formal model, but the real thing which the axioms are trying to capture. By the discussion above, we know that no matter what axioms we impose, we’ll never be able to fully capture the integers (because any formal system will always have unproveable truths, and therefore multiple interpretations, and therefore allow for models of the integers with are different than the real ones).
So when you ask for unproveable truths, maybe you’re not asking for an unproveable statement which is true in some interpreation, maybe you’re asking for an unproveable statement which is true in the one true interpretation. That is, you want a statement which is true about the actual integers, the real out-in-the-world number system that we’re trying to model, but unproveable. I don’t know of any “naturally occurring” statements like that off the top of my head (though some people think that the Goldbach conjecture might be one).
But if you replace “integers” everywhere in the last paragraph with “universe of sets” you can say very much the same thing. That is, we might intuitively believe that there is an actual universe of sets which the ZFC axioms are merely trying to model. And then you can take a statement independent of ZFC—the continuum hypothesis say—and ask “is this is true in the real, actual universe of sets?” If yes, then that’s your unproveable truth. If no, then its negation is.
So yes, naturally occurring unproveable truths abound, at least in set theory (but depending on what you think the real universe of sets looks like, you might disagree with others about what they are).
Assuming we use first-order logic, right?
Here is the part where I got stuck.. what exactly causes this attitude that if something cannot be accomplished using first-order logic, the reasonably thing is to give up? I assume there is a good reason behind that, but I have never heard it said explicitly, so to me it kinda sounds like “we found out that it is impossible to build a spaceship using wood, therefore there shall be no space travel”, as opposed to trying to find a more suitable material for building spaceships.
So, there is some first-order-logicness in the very concept of proof? Like, if you describe something using the first-order logic, then you can use a machine to algorithmically check the validity of the proof… and using some stronger methods could allow us to make the interpretation less ambiguous, but the cost would be that now we no longer can mechanically check the correctness?
Your original question (about the focus on first-order logic) was a very good one. I asked a logician friend about it, and his answer was the same as the one that you and Samuel settled on here—first-order logic is likely the best that humans brains (or machines) are able to access. So yeah, basically a version of the Church-Turing thesis.
They referred me to Lindström’s theorem as a concrete result in that direction. I don’t know enough to understand the statement of the theorem, but it seems to say something along the lines of “first-order logic is the strongest logic which still has [some properties that computable systems ought to have?].”
Fun fact I learned in the conversation: it is a theorem of first-order ZFC that the models of second-order ZFC are constrained enough to single out a canonical model of the integers.
Thanks for the links! I will try to explore in this direction.
Thank you for this answer. You also helped make another point of confusion clearer: When I read the op I wasn’t sure what the interpretation of number theory is. There must be one or the incompleteness theorem wouldn’t apply but what is it?
Based on your comment here I understand this better and it makes more sense why people might disagree about for example the continuum hypothesis being “reasonable”. While mostly everyone agrees on the standard ZFC axioms not everyone agrees on the interpretation of ZFC.
Then there must also be hardliners who take ZFC as the truth without interpretation and thus do not allow statements independent of it as they are not provable. It would be interesting to see what proofs they miss out on. (Not requesting anyone to list them for me, just thinking out loud.)
I think this interpretation is both intriguing and clarifying, thanks. It suggests that a good framing of the incompleteness theorem is:
Any sufficiently rich system S can be extended by multiple interpretations I, such that all of its provable theorems are true for all of I, but I contains interpretations who disagree on the truth of some unprovable statements of S
And if you try to narrow down the interpretations, you either don’t get far enough—because there are infinitely many possible interpretations, and no matter how many times you exclude half of them by adding a new axiom, still infinitely many possible interpretations remain—or you introduce some new concept—but then this new concept has its own multiple interpretations.
For example, if you try to make axioms for integers, it turns out that there are also some “nonstandard integers” which technically satisfy the axioms, even if they are obviously not the thing we meant. The traditional way out is to add an axiom like “the actual integers are the smallest set (from the perspective of set inclusion) of things that satisfy these axioms”, but now you have invoked the concept of a set, and if you try to define what that means, you just open another can of worms… and this process never stops.