First, the question of "provability" is whether something can be proved using a given collection of axioms and rules.
That is, we are not concerned about whether a smart mathematician with great communication skills could convince us about the veracity of a statement. Instead, we are concerned about whether we can construct a sequence of statements culminating with the given statement, such that each step can be verified by a rather simple computer program, by matching it to the few predetermined patterns.
So it is perfectly okay to have a statement that is obviously true, but still cannot be proved using some set of axioms and rules. Think about it as a weakness of the given set of axioms and rules, rather than a property of the statement itself. In other words, we never talk about "provability of X" (except as a shortcut), but always about "provability of X in system S". Provability is a relation between X and S.
Therefore, Gödel's Theorem is not about statements that are unprovable per se (i.e. some more complicated version of "math will never be able to prove that 2 + 2 equals 4"), but rather it means "if you give me a non-contradictory system S of axioms and rules, I can create a statement X such that its veracity will be beyond the reach of S". Plus there is an algorithm for creating a specific X for given S. The generated X will be tailored to the given S. (For different systems S1, S2, S3 you would get different X1, X2, X3; and it's always S1 having a problem with X1, S2 with X2, and S3 with X3; but maybe X1 and X2 are easy to prove or disprove in S3.)
More specifically, the statement X generated by Gödel for system S is cleverly designed to be equivalent to "X cannot be proved by S" without being self-referential. To discuss the clever construction is beyond the scope of this comment.
.
Second, once we start talking about things like sets, we are now far outside the realm of reality. It doesn't make sense to ask whether "sets really have a property P", if the fact is that "in the first place, set's don't really exist".
It would be like trying to use experimental physics to verify whether fairies are heavier than 10 grams. You simply can't, because there are no fairies to measure. So if you have two competing theories of physics-including-supernatural, one saying that fairies are heavier than 10 grams, and the other saying they are not, well, you have a problem that cannot be resolved experimentally. A set theory with the Axiom of Choice, and a set theory with some incompatible axiom, are two such theories: they agree about everything that really exists, and they disagree about the properties of fairies... ahem, infinite sets. You can't resolve this conflict by talking about what really exists; and the arguments about what doesn't exist are by their nature arbitrary. (You can't prove internal inconsistency, because both theories are internally consistent. They just disagree with each other.)
So how can we study sets if they are not real? By defining axioms and rules, and examining which statements can be proved using given axioms and rules. "ZF" is such a set of axioms; there are statements you can prove using it, there are statements you can disprove, and there are statements where the system provides no answer.
The underlying reason is that if you imagine a Platonic realm where all abstractions allegedly exist, the problem is that there are actually multiple abstractions ["models"] compatible with ZF, but different from each other in many important ways. In some of them, Axiom of Choice is true. In others, it is false. This is what it means that Axiom of Choice can be neither proved nor disproved in ZF. The problem is that "sets" have never been unambiguously defined in the first place!
However, adopting the Axiom of Choice (or any of its competitors) won't actually solve the problem. There will still remain many abstractions compatible with ZFC (or whatever), but different from each other. So you will sooner or later find other exciting properties of the fairies... ahem, infinite sets, that can be neither proved nor disproved by ZFC (or whatever). The problem, again, is that we still don't have an unambiguous definition of "sets".
And... but I am way out of my depth here... maybe we can't have an unambiguous definition of "sets", ever, because of the Gödel Theorem. So we will have to keep adding new axioms, but there is no territory to guide us in their choice, so different people will prefer different choices, mutually contradictory.
At the end the set theory research will be fractured into hundreds of competing definitions, all underspecified. The statements will have to be prefaced by ever longer "according to this collection of axioms" which will make things difficult and error-prone. (Things you will learn under one collection of axioms may be false or even nonsensical under other collections. So you will have to re-learn everything over and over again if you switch to a different system.) And the preferred collection of axioms, which will most likely provide you opportunity in the peer-reviewed journals and research grants, will be decided "politically" (as the most popular among the currently established researchers); which according to some people has already happened with ZF(C).
Thanks for this great answer. I have a couple of follow-up questions that anybody should feel free to jump in and answer.
The underlying reason is that if you imagine a Platonic realm where all abstractions allegedly exist, the problem is that there are actually multiple abstractions ["models"] compatible with ZF, but different from each other in many important ways. In some of them, Axiom of Choice is true. In others, it is false. This is what it means that Axiom of Choice can be neither proved nor disproved in ZF.
There are models where the ...
So it is perfectly okay to have a statement that is obviously true, but still cannot be proved using some set of axioms and rules.
The underlying reason is that if you imagine a Platonic realm where all abstractions allegedly exist, the problem is that there are actually multiple abstractions ["models"] compatible with ZF, but different from each other in many important ways.
So, when you say Godel's sentence is obviously true, in which "abstraction" is it true?
Proofs, Implications, and Models introduces some of these ideas more slowly. Other stuff from the Highly Advanced Epistemology 101 for Beginners is relevant too, and includes more realism-flavored concerns about choosing between systems.
I know enough about this to not have these questions, but not enough to explain the answers to anyone else. So I'll recommend a book by Torkel Franzén, who was definitely able to both understand and teach this, "Gödel’s Theorem: An Incomplete Guide to Its Use and Abuse". The book costs money, but as a preview, here's a review of it.
Douglas Hofstadter has written a lot on the subject for a popular audience, but is better avoided until you understand the subject yourself well enough to recognise the unstated technical underpinnings of his exposition, and to see where he glosses over things a step too far. But when you are at that point, there is no need to read him.
One source that can help you learn more about the concept of provability is Gödel, Escher, Bach: An Eternal Golden Braid by Douglas Hofstadter. It talks about Gödel's Theorem and helps to get a deeper understanding of it. Plus, it's just a very interesting book.
In answer to the question of how can something be true, but not provable I want to point to the Goldbach conjecture which says "every even number > 2 is the sum of two primes". If the Goldbach conjecture is false then there's a counterexample which can be checked in finite time (eg. just try adding all pairs of primes less than that number although there are faster ways). If there isn't a counterexample then the Goldbach conjecture is true. To be provable however, there would have to exist a proof of the Goldbach conjecture. No such proof is known to exist. Here "truth" is exactly what it intuitively means. Either a counterexample exists or it doesn't. The "truth" of the Goldbach conjecture won't depend on your choice of axioms. All you need are the primitives necessary to define the natural numbers, primality, and addition (in particular, it won't depend on AC).
Note that you can prove "P or not P".
In what sense? In Classical Logic it's an axiom, and in the Calculus of Indutive Constructions it's unprovable.
(Interestingly, you can prove in Coq that the negation of "forall P, P or not P" is unprovable. So it's safe to assume it: https://stackoverflow.com/questions/32812834/how-to-prove-excluded-middle-is-irrefutable-in-coq )
Is this just because there are some statements such that neither P nor not-P can be proven, yet one of them must be true? If so, I would (stubbornly) contest that perhaps P and not-P really are both non-true.
Sure, truth is delicate. To move forward in studying this topic, just go with the interpretation that "neither P nor not-P can be proven".
Löb: How can a system of arithmetic prove anything? Much less prove things about proofs?
Arithmetization. If you have a bunch of axioms (which are finite strings in a finite alphabet) and a bunch of rules of inference (which are mechanistic rules for deriving new strings from old ones) then both can be encoded as integers and arithmetic. Then something like "there exists a sequence of deductions leading to such-and-such theorem" can be encoded as "there exists an integer such that..." and then a bunch of arithmetic.
For example, I’ve heard that there are proofs that PA is consistent. Let’s say one of those proofs is set in Proof System X. Now how do we know that Proof System X is consistent? Perhaps it can be proven consistent by using Proof System Y? Do we just end up making an infinite chain of appeals up along a tower of proof systems?
Yeah, these proofs just appeal to something stronger and are pretty pointless.
Oh, speaking of ZFC. There seems to be a debate about whether we should accept the Axiom of Choice. Isn’t it...obviously true?
Well, it doesn't follow from the other axioms, and it has some counterintuitive consequences. That's enough to make it debatable :-)
A non-technical summary of how arithmetization is used in this argument: https://plato.stanford.edu/entries/goedel-incompleteness/#AriForLan
What could it mean for a statement to be "true but not provable"? Is this just because there are some statements such that neither P nor not-P can be proven, yet one of them must be true? If so, I would (stubbornly) contest that perhaps P and not-P really are both non-true.
Can you give an example where both P and not-P are both non-true?
Sure. For example, if P is the Continuum Hypothesis, eg "There exists a set with a cardinality greater than that of the integers but less than that of the real numbers".
In this case we know that ZF cannot prove this statement true and also cannot prove it false. In this case, I'd be tempted to say that it really is not true and not false.
(I'm told that this statement would have to be either true or false in any "model of ZF", but I don't understand model theory well enough to have a good grasp of what that means. It might be the case that what I'm really saying is that I'm unwilling to grant "truth status" to model A but not model B if both models satisfy the axioms of ZF. I'll probably have to to both more learning and more thinking before I can clarify my thoughts on this any further, but anyone reading this should feel free to prod me with thought experiments, cutting questions, etc.)
Let me mention my favorite intuition pump against the axiom of choice - the prisoners with infinite hats. For any finite number of prisoners, if they can't communicate they can't even do better than chance, let alone saving all but a tiny fraction. But as soon as there are infinitely many, there's some strange ritual they can do that lets them save all but an infinitely small fraction. This is unreasonable.
The issue is that once you have infinite prisoners you can construct these janky non-measurable sets that aren't subject to the laws of probability theory. There's an argument to be made that these are a bigger problem than the axiom of choice - the axiom of choice is just what lets you take the existence of these janky, non-constructive sets and declare that they give you a recipe for saving prisoners.
Every so often I hear seemingly mathematical statements involving the concept of being provable. For example:
I find each of these statements baffling for a different reason:
And I also have one more general confusion. What systems of reasoning could these kinds of theorems be set in? For example, I've heard that there are proofs that PA is consistent. Let's say one of those proofs is set in Proof System X. Now how do we know that Proof System X is consistent? Perhaps it can be proven consistent by using Proof System Y? Do we just end up making an infinite chain of appeals up along a tower of proof systems? Or do we eventually drive ourselves into the ground by reaching system that nobody could deny is valid? If so, why don't we just stop and PA or ZFC?
Oh, speaking of ZFC. There seems to be a debate about whether we should accept the Axiom of Choice. Isn't it...obviously true? I don't really understand this topic well enough to have any particular question about the AC debate, but my confusion definitely extends to that region of concept space.
So here's my question: Where can I learn about "provability" and/or what clarifying insights could you share about it?