Every so often I hear seemingly mathematical statements involving the concept of being provable. For example:
I’ve seen Gödel’s Incompleteness Theorem stated as “if a mathematical system is powerful enough to express arithmetic, then either it contains a contradiction or there are true statements that it cannot prove.”
On the AI alignment forum, one of the pinned sequences describes Löb’s Theorem as “If Peano Arithmetic can prove that a proof of P would imply the truth of P, then it can also prove P is true”.
I find each of these statements baffling for a different reason:
Gödel: 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.
Löb: How can a system of arithmetic prove anything? Much less prove things about proofs?
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?
[Question] What’s going on with “provability”?
Every so often I hear seemingly mathematical statements involving the concept of being provable. For example:
I’ve seen Gödel’s Incompleteness Theorem stated as “if a mathematical system is powerful enough to express arithmetic, then either it contains a contradiction or there are true statements that it cannot prove.”
On the AI alignment forum, one of the pinned sequences describes Löb’s Theorem as “If Peano Arithmetic can prove that a proof of P would imply the truth of P, then it can also prove P is true”.
I find each of these statements baffling for a different reason:
Gödel: 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.
Löb: How can a system of arithmetic prove anything? Much less prove things about proofs?
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?