The essential issue is the same as one that has been discussed many times here on MO, for example here and here. Consider the following string $S$.
$$(\exists x \exists y \exists z : xxx + yyy - zzz = 114) \vee (\exists x \exists y \exists z : xxx - yyy - zzz = 114) \vee (\exists x \exists y \exists z : xxx + yyy + zzz = 114)$$
Let me now make a claim.

**Claim.** If there is a valid mathematical proof, using only the mathematical assumptions that are formalized by the axioms of PA along with classical logic, that 114 is the sum of three cubes, then there exists a formal PA-proof of $S$.

The above Claim is not a strictly mathematical claim, because it refers to the informal notion of a "valid mathematical proof," which is not a strictly mathematical entity. By contrast, formal PA-proofs *are* mathematical entities. In effect, the Claim is asserting that, in a certain important sense, formal PA-proofs "capture" the informal notion of "valid mathematical proof" and $S$ "captures" the assertion that 114 is the sum of three cubes. The Claim is somewhat akin to the Church–Turing thesis, in that it asserts that a pre-existing informal concept is adequately captured by a precise mathematical concept.

I happen to believe the Claim, and so does almost everyone. Indeed, it's hard to see why one would study PA-proofs if one did not believe the Claim. But you are not *compelled* to believe the Claim. You are free to deny it. In particular, even if someone manages to prove that $S$ is independent of PA, you could still insist that it remains an open question whether "114 is a sum of three cubes" admits a valid mathematical proof using only the mathematical assumptions formalized by the axioms of PA along with classical logic. In effect, you would be claiming that $S$ fails in some way to be an accurate formalization of "114 is the sum of three cubes."

Because the statement that "114 is the sum of three cubes" is so simple, it is hard to imagine someone seriously arguing against the Claim. However, suppose we now replace "114 is the sum of three cubes" with "PA is consistent" and we replace $S$ with the formal string that is typically given the name "Con(PA)." Since Con(PA) is such a complicated string, and consistency is such a notoriously confusing concept, it's now easier to imagine someone denying the analogous Claim, and maintaining that Con(PA) somehow fails to "capture" the consistency of PA in the sense that the Claim asserts. The late philosopher Michael Detlefsen was perhaps the best-known denialist.

Similarly, Artemov is a denialist in this sense. Artemov, of course, does not deny the truth of Gödel's second incompleteness theorem. But Gödel's 2nd theorem tells us only that Con(PA) is formally unprovable in PA. Artemov denies that we can infer that the consistency of PA cannot be proved from the mathematical assumptions that are formalized by the axioms of PA. To defend this contrarian position, Artemov shows that PA *can* prove some things that seem awfully close to asserting the consistency of PA. I won't go into the details of Artemov's paper, but here is a classical fact: for any finite subset of the axioms of PA (remember that PA contains an axiom *schema* and hence has infinitely many axioms), PA can prove that that finite set of axioms is consistent. That sure seems close to proving consistency, doesn't it? After all, if there is an inconsistency in PA, only finitely many axioms will be needed to derive that inconsistency. Whichever specific list of finitely many axioms you might single out on suspicion of yielding an inconsistency, PA proves that that particular list of axioms is consistent. Maybe you feel that's close enough to "PA proves its own consistency"? Or if not, maybe the results that Artemov proves will strike you as convincing.

In short, I would say that there's nothing particularly novel about Artemov's results. It has been clear to experts from the very beginning that this type of denialism is a philosophical option you can take, so certainly that's not new. Personally, I don't find Con(PA) to be an inadequate expression of the consistency of PA any more than I find $S$ to be an inadequate expression of "114 is the sum of three cubes," and neither do most people. But your mileage may vary.

12more comments