What does Gödel’s First Theorem mean?

Question

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

Answer 1

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.

Answer 2

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.