Can Godel's Unprovable Formulae Be Proven from Peano Axioms?

[Cincinnatus]

One of Godel's results would imply that there must be arithmetic facts (formulae?) that cannot be derived from the peano axioms. (Unless my understanding here is wrong that is).

So I wonder, has anyone found such a formula? How could it be proved?

 

[D H]

Your understanding is close. A better statement of the Gödel's First Incompleteness Theorem is that that any consistent and sufficiently powerful number theory must include undecidable propositions.

The Continuum Hypothesis is the most famous undecidable proposition. Gödel proved no contradiction would result should the Continuum Hypothesis be added to ZF set theory. Cohen later proved no contradiction would result should the negation of the hypothesis be added to ZF.

 

[Hurkyl]

There are a lot of very subtle nuances when dealing with formal logic.

As a theory, the arithmetic of natural numbers is incomplete: that means there exists a statement P that cannot be proven or disproven from the axioms.

However, one might have a model of the natural numbers. One of the things you can do with a model is to evaluate the truth of any statement.

Therefore, for any model of the natural numbers, there must exist a true statement P that cannot be proven or disproven from the axioms. (Of course, P might be false in a different model of the natural numbers)


Here's an example of a suitable statement P:

http://mathworld.wolfram.com/GoodsteinsTheorem.html

In formal set theory, we usually use a particular model of the natural numbers. Intuitively, each natural number is defined to be the set of all smaller natural numbers. So, 0 = {}, 1 = {0} (= {{}}), 2 = {0, 1}, et cetera. Goodstein's theorem is true for this model of the natural numbers.

However, it would be false for some other model of the natural numbers.

 

[Cincinnatus]

Goodstein's theorem sounds like what I was getting at.

Interesting...

 

[benorin]

I remember reading that if a statement cannot be proved from the Peano's axioms, the it is necessarily true. But memory doesn't serve where, or why that was so. Anybody going to rebuke me?

 

[matt grime]

If a statement cannot be proven from the axioms of peano then it is necessarily true? Erm, no, because 1+1=3 cannot be proven from the axioms since it is false.

What kind of statement? In what model?

 

[benorin]

sorry, perhaps it was if it is undecidable from the axioms...