2
$\begingroup$

From Wikipedia, Gödel’s first incompleteness theorem states that “no consistent system of axioms whose theorems can be listed by an effective procedure (i.e. an algorithm) is capable of proving all truths about the arithmetic of natural numbers.”

How is the truth about the arithmetic of natural numbers defined? Isn’t it defined in terms of axioms, like the Peano axioms? Does Gödel’s theorem state that Peano’s axioms are not a complete formulation of arithmetic? Do we have some other means of ascertaining truth except by axioms? (Maybe intuition?) Can the theorems of Peano arithmetic (I mean, the theorems that follow from the Peano axioms) be enumerated? I would think that in any axiomatic system with a countable number of axioms, the theorems could be enumerated. So you see, I am a little confused, because it seems to me that Peano arithmetic exhausts truth about arithmetic, and it seems that its theorems should be able to be enumerated with a straightforward computer program. I know I’m probably overlooking something big and obvious, but I need help to see it. Thanks

$\endgroup$
4
  • 1
    $\begingroup$ Truth and provability, in the context of the quote you give, are not the same thing -- in that context, truth means "true in the natural numbers" which intuitively assumes a meta theory (often taken to be some form of set theory) in which the natural numbers with the usual operations can be defined. If you want to avoid that, then take the 1st incompleteness theorem to say " no consistent system of axioms whose theorems can be listed by an effective procedure (and which proves some particular basic facts of arithmetic) can be complete" $\endgroup$
    – Ned
    Aug 2, 2021 at 13:53
  • 1
    $\begingroup$ Probably the best thing is to read Gödel's Proof by Nagel/Newman and Gödel's Theorem. An Incomplete Guide to Its Use and Abuse by Torkel Franzén. The Nagel/Newman book is a well-known classic widely discussed on the internet, and a review of Franzén's book can be found here. $\endgroup$ Aug 2, 2021 at 14:10
  • 2
    $\begingroup$ The idea is that every sentence must be either true or false, whether or not we can determine which it is. But it is only a theorem if it is not only true, but also has a proof. You can certainly enumerate all theorems, but what Gödel says is that there will be some sentences S such that neither "S" nor "not S" appear on your list. $\endgroup$ Aug 2, 2021 at 14:29
  • $\begingroup$ The big gotcha is that in the original (informal) formulation of Peano's axioms, the induction principle holds for arbitrary properties of natural numbers. But when this is formalised in first-order logic, the resulting induction principle is far too weak to deliver all truths of arithmetic, such as the consistency of systems like first-order Peano Arithmetic. $\endgroup$
    – Rob Arthan
    Aug 2, 2021 at 19:59

2 Answers 2

0
$\begingroup$

I try to clarify this :

Goedel's first theorem states that for every consistent theory that is strong enough to satisfy the Representation theorem (The Presburger arithmetic does not satisfy it : In fact , it is known to be both complete and consistent) there are statements that can be formulated within this theory, but neither be proven nor disproven within this theory.

The proof of Goedel's theorem is usually done in a meta-theory, but it could be formalized with theorem-provers.

Provable are exactly those statements that are true under every possible interpretation. Hence the undecidable statements are true with respect to at least one interpretation and false with respect to at least one interpretation.

Usually such undecidable statements cannot be dectected , but in some cases , this is possible (most famous example : the continuum hypothesis)

Finally, a stronger theory can be able to prove something that cannot be proven in a weaker theory. Goodstein's theorem for example cannot be proven within the peano axioms (PA) , but it can be proven within the much stronger set theory (ZFC).

I hope that I could shed some light on this difficult and subtile topic.

$\endgroup$
0
$\begingroup$

GIT finds a statement $P(k)$, where $P(0)$ has a proof, and $P(1)$ has a proof,and $P(2)$ has a proof (etc). In fact the proof is as simple as "just evaluate the statement."

But $P$ is chosen based on the specific axioms/inferences of the logic so that $\forall k. P(k)$ doesn't have a proof.

$\endgroup$
1
  • $\begingroup$ I realize this question is probably a duplicate a million times over but the answer is simple enough I didn't want to make the questioner dig through the swamp of abstract answers to this question. $\endgroup$
    – DanielV
    Aug 2, 2021 at 14:17

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