[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)

[zajio1am]

These deep philosophical discussions are about absolute "truth" in general, but in logic, the truthness of formula in specific mathematical structure is well-defined through structural induction over the formula, although with non-finite, non-computable steps. Yes, from strict-finitistic point of view even the concept of truth in the standard model of arithmetic could be problematic.

[Tainnor]

I'm personally not a constructivist or even finitist (mostly for pragmatic reasons), but discussions about Gödel get sidetracked by musings about either of these philosophies so often that I feel it's important to point out that there is an understanding of Gödel's theorems that can be understood and discussed regardless of one's commitment to a particular philosophy of mathematics (well, at least assuming some "reasonable" base).

If you are a finitist, you could interpret Gödel's theorem to mean that infinite systems such as the natural numbers don't actually exist, because they can never be understood in full (I'm not a finitist, so maybe I'm wrong in this conclusion). If you're a classical platonist, they would mean that the "natural numbers" do exist in some platonic realm, but will never fully be captured by human mathematics. If you're a formalist like me, maybe you'd say that it's very useful to pretend that the natural numbers exist, but that strictly speaking we don't really fully understand what they are or should be (but it turns out not to matter all that much).

Either way, a complete theory of the natural numbers doesn't exist.

[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.