In my proof theory monograph there is this exercise:

"The natural proof of PA cannot be carried out in PA. Why? (This proof consists in showing that all theorems of PA are ture.)"

Apparently, by 'natural' proof he means that we accept the (usual) interpretations of the axioms of PA to be true statements and that the rules of the predicate calculus preserve truth (if one likes to consider this a proof).

Isn't the answer simply exactly the second incompleteness theorem? It seemed too easy so I wondered whether there was more to it..

Thanks, Ettore

Here's a link to the question on overflow: https://mathoverflow.net/questions/319417/why-the-natural-consistency-proof-of-pa-cannot-be-carried-out-textbfin-pa

  • 1
    $\begingroup$ Admittedly, I'm not sure what you mean by "consider the axioms of PA to mean true statements", because the axioms of PA are something very concrete and explicit, whereas "true statements" (even if taken as "true in $\Bbb N$") is something not very explicit, in the sense that it is not definable in $\Bbb N$. $\endgroup$ – Asaf Karagila Dec 4 '18 at 16:37
  • $\begingroup$ Thank you. English is not my native tongue. I hope I improved now. $\endgroup$ – Ettore Dec 4 '18 at 17:36
  • 6
    $\begingroup$ I don't think the second incompleteness theorem is the answer to that question. The theorem tells you that, if you attempt to formalize the natural proof in PA, something must go wrong. But it doesn't tell you what goes wrong. Where does the "formalized natural proof" break down? I think that's the intended question. $\endgroup$ – Andreas Blass Dec 4 '18 at 17:49
  • 2
    $\begingroup$ Related: math.stackexchange.com/questions/2396084/… $\endgroup$ – Eric Wofsey Dec 4 '18 at 17:59
  • 3
    $\begingroup$ @Ettore Yes, the natural proof presupposes a truth predicate and some facts about it. And by Tarski's theorem, no truth predicate for arithmetical sentences can be defined in the language of arithmetic --- not even if the only property you require is that a sentence X and the sentence "X is not true" can't hold simultaneously. $\endgroup$ – Andreas Blass Dec 4 '18 at 22:27

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.