[Question] What’s going on with “provability”?

Every so of­ten I hear seem­ingly math­e­mat­i­cal state­ments in­volv­ing the con­cept of be­ing prov­able. For ex­am­ple:

  • I’ve seen Gödel’s In­com­plete­ness The­o­rem stated as “if a math­e­mat­i­cal sys­tem is pow­er­ful enough to ex­press ar­ith­metic, then ei­ther it con­tains a con­tra­dic­tion or there are true state­ments that it can­not prove.”

  • On the AI al­ign­ment fo­rum, one of the pinned se­quences de­scribes Löb’s The­o­rem as “If Peano Arith­metic can prove that a proof of P would im­ply the truth of P, then it can also prove P is true”.

I find each of these state­ments baf­fling for a differ­ent rea­son:

  • Gödel: What could it mean for a state­ment to be “true but not prov­able”? Is this just be­cause there are some state­ments such that nei­ther P nor not-P can be proven, yet one of them must be true? If so, I would (stub­bornly) con­test that per­haps P and not-P re­ally are both non-true.

  • Löb: How can a sys­tem of ar­ith­metic prove any­thing? Much less prove things about proofs?

And I also have one more gen­eral con­fu­sion. What sys­tems of rea­son­ing could these kinds of the­o­rems be set in? For ex­am­ple, I’ve heard that there are proofs that PA is con­sis­tent. Let’s say one of those proofs is set in Proof Sys­tem X. Now how do we know that Proof Sys­tem X is con­sis­tent? Per­haps it can be proven con­sis­tent by us­ing Proof Sys­tem Y? Do we just end up mak­ing an in­finite chain of ap­peals up along a tower of proof sys­tems? Or do we even­tu­ally drive our­selves into the ground by reach­ing sys­tem that no­body could deny is valid? If so, why don’t we just stop and PA or ZFC?

Oh, speak­ing of ZFC. There seems to be a de­bate about whether we should ac­cept the Ax­iom of Choice. Isn’t it...ob­vi­ously true? I don’t re­ally un­der­stand this topic well enough to have any par­tic­u­lar ques­tion about the AC de­bate, but my con­fu­sion definitely ex­tends to that re­gion of con­cept space.

So here’s my ques­tion: Where can I learn about “prov­abil­ity” and/​or what clar­ify­ing in­sights could you share about it?