What if someone comes up with a proof of consistency of arithmetic under the following conditions?

Question

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?

Answer 1

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.