[FOM] Forward: Provability of Consistency

[Timothy Y. Chow]

Sergei Artemov wrote:

> https://arxiv.org/abs/1902.07404

I haven't worked through the details of the construction, but I think that 
this kind of thing has been known for a long time.

Artemov's main contention is that the formal string Con(PA) that is 
standardly taken to "express" the consistency of PA does not perform that 
job properly; it is "too strong," and hence Goedel's second incompleteness 
theorem does not, as is conventionally believed, kill Hilbert's program of 
proving the consistency of PA by finitary means.

Long ago, Michael Detlefsen tried to argue for the same conclusion.  As I 
recall, Detlefsen's argument relied heavily on Rosser predicates, and I 
was unconvinced that he had identified anything unsatisfactory about the 
usual string Con(PA).

As I understand it, Artemov's argument takes a slightly different tack, by 
replacing Con(PA) with a schema that is "weaker" than Con(PA) itself.  If 
I'm right, then this sort of thing is well known.  For example, 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).  Similar tricks are known for 
proving the consistency of "arbitrarily large fragments of PA" (suitably 
defined) in PA.

So I remain unpersuaded that Artemov has provided any kind of new 
philosophical insight.

Tim