[xavxav]

Indeed, the first incompleteness theorem tells us that any logical framework which can express Peano arithmetic must necessarily contain true (resp. false) facts for which no (resp. counter) proof can be given.

Sometimes you can prove that no proof exists about a specific sentence (that's what his incompleteness proof does), and I think you could extend this technique to construct sentences where no proof exists of whether it has a proof, etc...

[lisper]

> the first incompleteness theorem tells us that any logical framework which can express Peano arithmetic must necessarily contain true (resp. false) facts for which no (resp. counter) proof can be given.

Not quite. Any logical framework which can express Peano arithmetic must necessarily contain true facts for which no proof can be given within PA. The proof of Godel's theorem itself is a (constructive!) proof of the truth of such a statement. It's just that Godel's proof cannot be rendered in PA, but even that is contingent on the assumption that PA consistent, which also cannot be proven within PA if PA is in fact consistent. In order to prove any of these things you need to transcend PA somehow.

[Tainnor]

> It's just that Godel's proof cannot be rendered in PA

This is incorrect, the proof can be carried out in very weak subsystems of PA.

[zajio1am]

> must necessarily contain true (resp. false) facts for which no (resp. counter) proof can be given

This formulation misses the important aspect that whether the statement is 'true' is not absolute property (outside logical truths). We can consider truthfulness of a statement in a specific structure or in a specific theory.

E.g. a statement can be undecidable in Peano arithmetic (a theory) while true in natural numbers (a structure, model of Peano arithmetic), but that just means there is a different structure, different model of Peano arithmetic in which this statement is false.

[Tainnor]

Discussing Gödel in terms of "truth" immediately brings about deep philosophical discussions about what that actually means in the context of mathematics. If the "true" nature of the (standard model of) arithmetic is unknowable in full, does it even exist?

I like to be pragmatically classical in my mathematical outlook (I don't worry about LEM), but when we come to foundations, I find that we need to be a little bit more careful.

Gödel's original proof (or rather, the slightly modified Gödel-Rosser proof) avoids notions of absolute truth - it says that for any consistent model of arithmetic, there must exist undecidable sentences. These are ultimately purely syntactical considerations.

(I'm not claiming that there is no relation to "truth" at all in this statement, just that things become less precise and more philosophical once that's how we're going to frame things)

[Filligree]

The latter would be an axiom. A disproof would be a proof that there is no proof, so if you’d proven that no proof exists one way or the other then you’ve proven it can’t be disproven _or_ proven.

Which means you’ve hit a branch in mathematics. You can assume it to be either true or false, and you’ll get new results based on that; both branches are equally valid.

[LegionMammal978]

Constructively speaking, a disproof is a "proof that a statement leads to a contradiction". A "proof that there is no proof (assuming consistency)" can exist just fine, and that's exactly what the incompleteness theorem is, alongside a "proof that there is no disproof, i.e., that a contradiction cannot be derived from the statement (assuming consistency)".

[strbean]

> any logical framework which can express Peano arithmetic

(with a finite list of axioms)

[jrvidal]

I think the precise pre-condition is that the theory should be recursive, which means either a finite list of axioms _or_ a computable check to determine whether a given formula is an axiom.