1
$\begingroup$

I have seen in places I have read about Godel's incompleteness theorem that the second incompleteness theorem can be summarized as saying:

No axiomatic system with sufficiently strong arithmetic can prove its own consistency.

Can someone explain what that means? I would think it is trivially the case that no system could prove its own consistency, since consistency and completeness are "meta" notions, and aren't formalized in the object language.

$\endgroup$
6
  • $\begingroup$ I think it follows from the first incompleteness theorem that there will be true statements that are not provable using a formal axiomatic system. To be consistent, a system should be able to prove or disprove any statement expressed in it's language. $\endgroup$
    – Vasili
    Jan 26, 2023 at 15:35
  • $\begingroup$ @Vasili Oh okay that makes more sense. So the second theorem is more of a corollary to the first? $\endgroup$ Jan 26, 2023 at 16:07
  • 3
    $\begingroup$ "consistency and completeness are "meta" notions, and aren't formalized in the object language" But they can be formalized in the object language. That's the whole trick behind the proof. $\endgroup$ Jan 26, 2023 at 16:09
  • 1
    $\begingroup$ Minor nitpick but the "axiomatic system" needs to also be consistent and effective (recursively enumerable). $\endgroup$
    – blargoner
    Jan 26, 2023 at 16:33
  • 2
    $\begingroup$ @Vasili You are conflating consistency with completeness. To be consistent, a system must NOT prove AND disprove $A$ for any sentence $A$ -- but it may fail to do both. A system which DOES prove or disprove each sentence $A$ is said to be complete. $\endgroup$
    – Ned
    Jan 26, 2023 at 17:25

1 Answer 1

2
$\begingroup$

As lemontree says in the comments, the axiomatic systems to which the incompleteness theorem applies are capable of discussing their own consistency, that's the whole reason this theorem is possible. This is done using the "sufficiently strong arithmetic."

The upshot of "sufficiently strong arithmetic," say first-order Peano arithmetic ("PA") to be specific, is that it lets you discuss the behavior of arbitrary Turing machines, including the Turing machine which prints out a list of all the theorems of PA. So you can discuss the statement "the Turing machine which prints out a list of all the theorems of PA never prints 'false,'" which is equivalent to the consistency of PA. The claim then is that PA can't prove this, although it can state it.

Note that in order to do this the axiomatic system must be computable in a suitable sense, so that one can actually write down this Turing machine. This is a crucial part of both the statement and proof of the incompleteness theorem and people always omit it when they state the theorem informally; without this condition the theorem is false. The incompleteness theorem does not apply to non-computable axiomatic systems, such as true arithmetic, the system whose axioms consist of all true statements about the natural numbers. True arithmetic can't discuss itself in the same way that Peano arithmetic can because it doesn't know what its own axioms are (and neither do we!) - this is Tarski's undefinability theorem.

$\endgroup$
3
  • $\begingroup$ Thank you! Your comment actually helps me connect the dots a lot on this, at least I think. So The point of Godel's numbers is to "arithemtize" statements of the theory, so that it can be expressed within the theory itself? Am I off the mark here? Do you know of any good resources for helping me understand his theorem, and Tarksi's theorem on the undefinability of truth? $\endgroup$ Jan 26, 2023 at 19:33
  • $\begingroup$ @Nikolas: yes, that's what the Godel numbers are doing. The best explanation I've seen of this stuff, that among other things makes the connection to Turing machines explicit, is from a series of lectures from Scott Aaronson, which was later expanded into his book Quantum Computing since Democritus: scottaaronson.com/democritus/lec3.html $\endgroup$ Jan 26, 2023 at 19:39
  • $\begingroup$ I appreciate the help and the reference! $\endgroup$ Jan 26, 2023 at 19:41

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .