Suppose that one day, someone comes up with a proof of consistency of Peano arithmetic (PA) within itself. Then, does it mean that PA is actually inconsistent? Because, by the Gödel's incompleteness theorem, it is impossible to do so if PA is consistent. So, by contradiction it means that PA is inconsistent. Is my reasoning right? If not, why? If yes, in what theory/set of axioms it is inconsistent by that reasoning?

  • 1
    $\begingroup$ Gödel gave a precise statement in Peano arithmetic Consis, which has a clear intuitive meaning that Peano arithmetic is consistent, based on Gödel numbering of formulas and proofs. If you were able to prove Consis in Peano arithmetic, then yes, that would establish that Peano arithmetic is inconsistent. $\endgroup$ – hardmath Aug 4 '18 at 17:02
  • $\begingroup$ IMO if such a thing were to happen we would probably examine the proof and find an instance of induction wherein to declare the predicate used in that instance to be invalid. $\endgroup$ – DanielV Aug 5 '18 at 8:10
  • $\begingroup$ @DanielV I understand that such a proof would be checked, but I talked about the consequences of such a proof which would be right after checking. $\endgroup$ – Юрій Ярош Aug 5 '18 at 8:13

You are correct. Even more is true:

  • When we appropriately formulate the expressions "Con(PA)" and "PA proves ---" in the language of arithmetic, it is the case that PA proves "If PA proves Con(PA), then $\neg$ Con(PA)." That is, PA proves that you are correct.

  • In fact, the initial PA can be weakened and the later PAs can be vastly strengthened: e.g. PRA proves "If ZFC proves Con(ZFC), then $\neg$ Con(ZFC)." That is, Godel's theorem is provable from very little and applies to very much.

  • Moreover, this is all done constructively. Specifically - taking PA as an example - there is an explicit (if messy to write down) algorithm $\alpha$ which would convert any PA-proof of Con(PA) into (say) a PA-proof of "$0=1$," and the fact that $\alpha$ does this can be proved in a very weak system. It's this last bit that makes this statement non-vacuous, since - assuming PA is in fact consistent - there are no PA-proofs of "$0=1$" at all, and hence any $\alpha$ will do if we drop the "provable behavior" requirement.

    • This $\alpha$, and the proof of its correctness, are a bit messy, but if you're interested I can summarize it.
  • $\begingroup$ It's worth mentioning - to forestall possible future confusion - that the various "consistency proofs of PA" kicking around (e.g. Gentzen's) are proofs of Con(PA) in systems other than PA. They are quite interesting and surprising since the system they take place in is usually PRA (much weaker than PA) + something fairly innocuous-seeming (for Gentzen, a weak transfinite induction principle); in particular, the theory in which these proofs take place does not extend PA. $\endgroup$ – Noah Schweber Aug 4 '18 at 18:12

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.