[FOM] Forward: Provability of Consistency
Timothy Y. Chow
tchow at math.princeton.edu
Sun Mar 24 17:52:32 EDT 2019
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
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.
More information about the FOM