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

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?

• 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. – hardmath Aug 4 '18 at 17:02
• 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. – DanielV Aug 5 '18 at 8:10
• @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. – Юрій Ярош Aug 5 '18 at 8:13

• 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.