1. 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)$”)
2. 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.”

1. 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)$”);
2. moreover, this is witnessed by a primitive recursive function taking each $n$ to the proof of “$\lnot (n \colon \bot)$”;
3. these two facts can themselves be proven in PA.

The first two facts are fairly straightforwardly provable using standard techniques from the proof theory of arithmetic, in several ways (Artemov uses truth-definitions for $\Sigma_n$ formulas); and the fact that PA is a sufficient metatheory for them (indeed, small fragments such as PRA suffice) is also standard, as discussed in e.g. the answers of this old MO question. There is nothing controversial or questionable about any of this.

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$”. So just taking things to mean what they’re defined to, 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, and we can prove that schematic-provability using PA as metatheory, we can view this overall as a proof of the consistency of PA in PA. But note that the quantifier “for each $n$” has been moved to between provability claim. So we have proved in the inner-PA a schema of statements, and then in the outer-PA, we can assert the provability of that schema as a single statement. But we have not presented a proof in either copy of PA of a single statement that can be read as “PA is consistent”. In the inner PA, we have proven a schema of statments about specific finite derivations in PA. In the outer PA, we’ve proven a fact about PA which certainly can’t be read as “PA is consistent”, since we could prove the same schema for an inconsistent theory of arithmetic. Artemov’s argument that this can be called a proof in PA of consistency of PA 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.”

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.

These are fairly straightforwardly provable using standard techniques from the proof theory of arithmetic (truth-definitions for $\Sigma_n$ formulas). There is nothing controversial about these claims.

The slippery step is when Artemov argues that this can be seen a proof of the consistency of PA, within PA. The weakness 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.

The parametric proof of this scheme certainly shows that PA comes very close to proving its own consistency. A similar argument for ZF is given by 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.

One bit 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 obviously be an almost worthlessly 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’s theorem they can’t, since finite fragments of set theory suffice to prove consistency of PA.

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

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.

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.