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 :-)
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”.
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.
Yeah, these proofs just appeal to something stronger and are pretty pointless.
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