[FOM] Please post this version (a typo was corrected)

[Artemov, Sergei]

Well, I suggest actually reading the PoC paper 
https://arxiv.org/abs/1902.07404 
in which one could find answers to the questions raised in Chow’s review. 

> I was unconvinced that he <Detlefsen> had identified anything unsatisfactory about the usual string Con(PA).

Here is the argument from the PoC paper. By G2, PA|-/- Con_РА hence there are models of PA with inconsistent proofs. However, all such "bad" proof codes are necessarily infinite, hence G2 says nothing about real PA-derivations which all have finite codes and which Hilbert's consistency program has been all about. Furthermore, each PA-derivation is proved consistent in PoC. This appears to be a serious argument that G2 is not about real proofs and hence does not kill Hilbert’s program. Moreover, this argument undermines the whole idea of using Con_T as a formalization of consistency, cf. the discussion and examples in PoC paper. 

> for any finite set of axioms of ZF, ZF proves the existence of a countable transitive model for it (see, for example, Corollary II.5.4 in Kunen's book "Set Theory," 2013 revised version).

This is irrelevant to Hilbert’s program of finitary consistency proofs. 

> Similar tricks are known for proving the consistency of "arbitrarily large fragments of PA" (suitably defined) in PA.

Sure, tricks are well-known (e.g. partial truth definitions for PA used in PoC paper), but they were applied differently. The claim “PA proves consistency of its fragment F” does not automatically provide a finitary proof of consistency of F, since such a conclusion requires assuming soundness of PA, which is itself stronger than the goal (consistency). For example, an inconsistent T proves Con_T, and so what? One has to carefully work this way in an opposite direction: provide an external finitary mathematical proof of consistency and only then formalize it in PA to ensure its finitistic character. This is done in the paper.

Viewing consistency of PA as a scheme is the way to formalize Hilbert’s notion of consistency. As it was mentioned earlier, Con_PA just does not do the job.