[FOM] Forward: Provability of Consistency

[Timothy Y. Chow]

Sergei Artemiov wrote:

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

Yes, I read this far, but I don't find this argument convincing.

Let us carefully distinguish between the assertion that PA is consistent 
from the formal string Con(PA).  The traditional argument runs as follows. 
Con(PA) has been constructed to have the following property:

   (*) Any finitistic proof that PA is consistent can be mimicked by a
       formal proof of Con(PA) from the axioms of PA.

Goedel's theorem is that if PA is consistent, then there is no formal 
PA-proof of Con(PA).  If we accept Goedel's theorem, and we accept (*), 
then it follows that if PA is consistent then there is no finitistic proof 
that PA is consistent.

You say in your paper that Con(PA) "states consistency of both standard 
and nonstandard proof codes."  This makes no sense.  Con(PA) is a formal 
string and does not state anything.  If you want to undermine the 
traditional account as I have summarized it above, you either have to 
undermine (*), or you have to explain why Goedel's argument does not, 
despite appearances, concern "real PA-derivations which all have finite 
codes."  On the surface, it seems that you're doing the latter, but your 
argument is unclear.  One thing you could do is adopt a rather radical 
skeptical view, claiming that whenever a mathematician writes a paper that 
is nominally about proofs of finite length, one can always reinterpret all 
the words in the paper---the word "finite" in particular---as having some 
kind of nonstandard meaning.  That is, although Goedel thought he was 
expressing himself clearly, and writing German sentences that proved facts 
about finite derivations in Principia Mathematica, the written text that 
he produced was irremediably ambiguous.  Perhaps I'm wrong, but I don't 
think that you're taking this skeptical route.  If I'm right, then far 
from saying "nothing" about real PA codes, Goedel's proof did in fact 
establish that if PA is consistent then there is no (real, finite) formal 
PA-proof of Con(PA).

I think that what you're really trying to argue is *not* that Goedel's 2nd 
theorem isn't about real PA proofs, but rather that (*) is false, for 
something like the following reason.  You formulate a certain schema, and 
you argue that as long as each instance of the schema admits a finitistic 
proof, then that counts as a finitistic proof of the consistency of PA. 
I happen to think that this is a tenable view to take, but I don't think 
that there's anything new here.  People have understood for a long time 
that this option is available.  I think that the reason that it hasn't 
become mainstream is that this kind of "proof" that PA is consistent is 
really a *proof schema*, and people tend to balk at the notion that a 
schema, each instance of which is a finitistic proof, is itself a 
finitistic entity, despite the infinitely many instances.  But if you 
personally don't balk at this, fine.  It's just not a new idea.

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

Yes, of course.  This is all standard stuff.  I don't see any way in which 
you are applying anything differently.

Tim