Disclaimer: I am not an expert in the proof theory of arithmetic. However, I don’t think one needs to be to assess this paper. It is admirably clear, well-written, and well-referenced, so it’s not onerous to verify that its precise mathematical claims and proofs all seem perfectly correct, and not particularly controversial. However, its main extra-mathematical claim, that these results can be viewed of a proof of consistency of PA, formalisable in PA, seems unconvincing, and its arguments for this claim are not I think particularly novel (though Artemov presents them unusually clearly).
The main precise mathematical claims are (very slightly paraphrased):
- for each $n$, PA proves the statement “$n$ does not code a proof of $\bot$ in PA” (which we abbreviate as “$\lnot (n \colon \bot)$”)
- moreover, there is a primitive recursive function taking each $n$ to the proof of “$\lnot (n \colon \bot)$”
These are fairly straightforwardly provable using standard techniques from the proof theory of arithmetic, in several ways (Artemov uses truth-definitions for $\Sigma_n$ formulas). There is nothing controversial about these results.
The tenuous step is when Artemov argues that this can be seen a proof of consistency of PA, within PA. The stretch becomes clear when we carefully break the claim down to definitions. “PA is consistent” means “there is no proof of contradiction in PA”, i.e. “there is no $n$ which codes a proof of $\bot$ in PA”, or equivalently “for each $n$, $n$ does not code a PA-proof of $\bot$”. Thus a proof of “PA is consistent” in PA should be a proof of “for all $n$, $\lnot (n \colon \bot)$” in PA.
Artemov argues that since for each $n$ we can prove “$\lnot (n \colon \bot)$” in PA, we can view that as a proof of the consistency of PA in PA. But note that the quantifier “for each $n$” has been moved outside the provability claim. So we have proved in PA a schema of statements, and then outside PA we can put that schema together and see that it amounts to asserting the consistency of PA. But the last step is happening outside PA! We have not presented a proof in PA of any single statement that can be read as “PA is consistent”. Artemov’s argument here reminds me of an old joke: “If you call a dog’s tail a leg, how many legs does a dog have?” “Four — calling the tail a leg doesn’t mean it is one.”
The parametric proof of this scheme certainly shows that PA comes very close to proving its own consistency. A similar argument for ZF can be given by for instance the reflection theorem — that for any finite list of axioms of ZF, ZF proves there’s some $V_\alpha$ which models them (and hence that they’re consistent). Most textbook presentations of these reflection principles that I’ve seen discuss this point explicitly — they note that these results bring the theory very close to proving its own consistency, but on close inspection, don’t quite prove it.
A piece of background worth noting here (a point which iirc I learned from Timothy Chow on this site) is that Hilbert’s consistency programme was not just to prove consistency of arithmetic within arithmetic — that would prima facie be a rather weak result, since an inconsistent theory would still prove its own consistency. Hilbert’s hope was to prove the consistency of some kind of set theory from some theory of arithmetic — justifying a more abstract theory by means of a more self-evident one, which would be a genuinely valuable result. The point of Gödel’s theorem was showing that not even the much weaker result was attainable — let alone the stronger result Hilbert had hoped for. So while reflection-principle arguments show that PA and ZF come tantalisingly close to proving their own consistency — close enough that a little good rhetoric can stretch tenuously across the gap — they don’t come at all so close to Hilbert’s actual dream, of proving consistency of set theory from arithmetic; and by Gödel they can’t, since finite fragments of set theory suffice to prove consistency of PA.