6
$\begingroup$

I am studying an undergraduate book of mathematical logic. After proving the two Gödel's theorems of incompleteness of formal theories, it asserts that some proofs of arithmetic's consistency exist. About this it mentions the use of infinite planar tree. It mentions Kruskal's theorem too.

I looked on Google for something about that proofs, but I found nothing.

$\endgroup$
  • 2
    $\begingroup$ Coherency is not a word I am familiar with in the context of logic. Perhaps this is a rather garbled reference to a Gentzen-style consistency proof. $\endgroup$ – André Nicolas Jul 17 '13 at 20:14
  • $\begingroup$ I voted to reopen, this question can certainly be answered in its present form. $\endgroup$ – Carl Mummert Jul 18 '13 at 1:48
  • 4
    $\begingroup$ Regardless, please add the name and author of the book you mentioned, as this may help people calibrate the level and details of their answers. $\endgroup$ – Andrés E. Caicedo Jul 18 '13 at 2:01
  • $\begingroup$ Variant: Is there a consistent theory which proves that PA is consistent? $\endgroup$ – Pierre-Yves Gaillard Apr 10 '18 at 15:57
12
$\begingroup$

There are several proofs of the consistency of Peano arithmetic. The main obstacle is the incompleteness theorem, which shows that no consistency proof of Peano arithmetic can use methods that can be formalized in Peano arithmetic itself. Thus any consistency proof has to use some method that cannot be formalized in Peano arithmetic.

With that limitation in mind, there are at least three standard ways to prove that Peano arithmetic is consistent:

  1. Showing that $\mathbb{N}$ is a model, as WillO says in his answer. This can be done in ZFC or weaker theories such as second-order arithmetic ($Z_2$).

  2. Gentzen's method. Basically: a proof in Peano arithmetic (where every proof is finite) is converted into an infinite tree whose nodes are labeled with formulas, with the conclusion of the proof at the bottom of the tree. Then it is proved, by transfinite induction, that none of these infinite trees can end with a contradiction. Thus Peano arithmetic is unable to prove a contradiction. This has a (short) article on Wikipedia.

  3. Gödel's method (the "Dialectica interpretation"). First, Peano arithmetic is interpreted into an intuitionistic arithmetic known as Heyting arithmetic, so that if Peano arithmetic is inconsistent then so is Heyting arithmetic. Then, it is shown that any provable formula in Heyting arithmetic has a "witness term" in a different theory known as "System T". So if Peano arithmetic is inconsistent, so is System T. This has an article on Wikipedia.

Unfortunately, it is hard to give a rigourous and elementary summary for (2) or (3); you have to get into the details to really see what is going on. But they have both been re-worked and extended by many mathematicians, and written in textbooks, so there is no more chance they are wrong than any other well known mathematical result.

One interesting thing is that the way that each of these proofs works is different - they use different methods that go beyond Peano arithmetic. So for Peano arithmetic to be inconsistent, all three of these methods would have to fail separately.

$\endgroup$
  • $\begingroup$ Professor Mummert, do you by any chance know some article with the full proof of Gentzen's method? I tried Kleene's Introduction to Metamathematics but they only summarize it. Of course, I can read the original paper but I'm looking for something more digestable $\endgroup$ – Guillermo Mosse Feb 20 '18 at 20:39
  • $\begingroup$ There are full treatments of this in proof theory texts, but they tend to aim more generally than just Gentzen's original result. One place to start might be Schwichtenberg's article in the Handbook of Mathematical Logic. The method used in Gentzen's proof is usually called "cut elimination". $\endgroup$ – Carl Mummert Feb 20 '18 at 20:52
7
$\begingroup$

The simplest proof that Peano arithmetic is consistent goes like this: Peano arithmetic has a model (namely the standard natural numbers) and is therefore consistent. This proof is easy to formalize in ZFC, so it's certainly a proof by the ordinary standards of everyday mathematics.

Another way to say the same thing without jargon like "model" is this: All of the Peano axioms are true statements about the natural numbers. Because the axioms are true, so are all their logical consequences. Therefore no false statements, and hence no contradictions, can be proven in Peano arithmetic.

There are other proofs as well, such as Gentzen's. But the above is surely the simplest and the easiest to grasp.

$\endgroup$
  • $\begingroup$ How do you know: "All of the Peano axioms are true statements about the natural numbers."? That is the unresolved issue. See: mathpages.com/home/kmath347/kmath347.htm See also the pdf "Do_integers_exist?" by Jack Schwartz (google it). $\endgroup$ – user113606 Dec 5 '13 at 11:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.