Puzzle: does the following prove that PA is inconsistent, part 2 I asked a question four years ago: Puzzle: Does the following prove that PA is inconsistent?
Back then I was satisfied with at least one of the answers I received, but now I do not understand why I was satisfied. I am going to make my argument clearer and hopefully somebody will be able to explain to me the flaw in my argument:
Let PA mean the Peano axioms, let Con(PA) mean that the Peano axioms are consistent, and let Incon(PA) mean that the Peano axioms are inconsistent.
Godel's 2nd Incompleteness Theorem says that Con(PA) is not a theorem of PA, unless PA is inconsistent. Now consider the following argument that Con(PA) is a theorem of PA:
Suppose that Incon(PA). Then PA implies Con(PA), since PA implies anything as long as PA is inconsistent. So Incon(PA) implies (PA implies Con(PA)). And this statement is logically equivalent to the statement that (PA and Incon(PA)) implies Con(PA).
Also, (PA and Con(PA)) implies Con(PA), obviously.
Therefore, [(PA and Incon(PA)) or (PA and Con(PA))] implies Con(PA).
Then since PA is logically equivalent to [(PA and Incon(PA)) or (PA and Con(PA))], we can conclude that PA implies Con(PA).
Therefore, by Godel's 2nd Incompleteness Theorem, PA is inconsistent.
Where is the error? There has to be an error, or else all of mathematics is wrong.
 A: We trivially have $\mathsf{PA}+Con(\mathsf{PA})\vdash Con(\mathsf{PA})$; that's correct. However, you have not shown that $\mathsf{PA}+\neg Con(\mathsf{PA})\vdash Con(\mathsf{PA})$. Rather, what we get (ignoring "Godelization" issues for brevity) is the more complicated result $$\mathsf{PA}+\neg Con(\mathsf{PA})\vdash \color{red}{[\mathsf{PA}\vdash Con(\mathsf{PA})]}$$ (or in words: "the theory $\mathsf{PA}$ + "$\mathsf{PA}$ is inconsistent" proves that $\mathsf{PA}$ proves that $\mathsf{PA}$ is consistent"). Basically, $\mathsf{PA}$ is strong enough to prove simple facts about provability, including that an inconsistent theory proves everything: for every (description of a) theory $T$ and every sentence $\psi$ we have $$\mathsf{PA}\vdash\neg Con(T)\rightarrow [T\vdash\psi].$$ One instance of this is $$\mathsf{PA}\vdash \color{green}{\neg Con(\mathsf{PA})\rightarrow} [\mathsf{PA}\vdash Con(\mathsf{PA})],$$ and now we just apply the deduction theorem to the green bit.

That point is that the red clause $\color{red}{\mathsf{PA}\vdash Con(\mathsf{PA})}$ which $\mathsf{PA}+\neg Con(\mathsf{PA})$ is able to prove is quite different from $Con(\mathsf{PA})$ itself. In general (unless it's inconsistent of course) $\mathsf{PA}$ cannot prove $X$ from "$\mathsf{PA}$ proves $X$;" see Lob's theorem.
