[FOM] Forward: Provability of Consistency
Timothy Y. Chow
tchow at math.princeton.edu
Fri Mar 22 14:32:50 EDT 2019
Sergei Artemov wrote:
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
More information about the FOM