Hilbert writes
Just as the physicist investigates his apparatus … the mathematician has to secure his theorems by a critique of this proofs, and for this he needs proof theory. (p. 61)
Indeed: if you are a physicist getting surprising results (or worse) thrown up by your apparatus, then you will take a hard look at the apparatus — but that’s a matter of doing more physics, of course, and doesn’t involve going outside the methods of physics. If you are mathematician getting surprising results (or worse, contradictions!) then you’ll similarly want to take a hard look at your purported proofs and the assumptions you’ve been using/smuggling in — and that’s a matter of doing more mathematics. In particular, formalization and “proof theory” is a mathematical tool to help the mathematician put his own house in order, removing any need to search for philosophical “foundations” to ensure consistency. Or at least, that’s the kind of line that we’ve seen Franks attributing to Hilbert.
Sometimes, however, Franks seems to claim more for the project of a Hilbertian proof theory. For example, he comments on the quote above that
Hilbert wants to demonstrate that the reliability [of mathematical techniques] is self-witnessing.
Reliability for what? Mathematical truth? Self-witnessing in what sense? Franks doesn’t say.
I won’t dwell on this, but to see quickly that there is an issue here, suppose you are the kind of set theorist who thinks that mathematics aims to reveal the truth about a unique universe of pure sets which is there for us to explore. For such a theorist, proving consistency of our theory is not enough. We believe, for example, that ZFC + V = L is consistent, but our set theorist typically doesn’t think that that makes it the correct theory of the universe of sets. But then what are the techniques for theory-choice here? And why are they reliable? Proof theory is plainly not much help in answering that question for our set-theorist or for witnessing that his methods are in good order. I’m not saying that the question isn’t answerable from a naturalist perspective, in a broad sense of “naturalism”– cf. Maddy’s discussions of such questions: I’m just noting that taking a Hilbertian line on the significance of consistency proofs — as explained by Franks — falls well short of completing the job.
That said, the first main point of Franks’s third chapter, which is called ‘Arithmetization’, is to claim that Gödel’s “technique for the arithmetization of syntax is perhaps the most significant positive contribution to Hilbert’s program” (p. 64). Which certainly, at first sight, seems a pretty extravagant claim.
Actually, as an aside, it is not the only strange claim in §3.2. Franks writes
Gödel’s two incompleteness theorems follow without much work from an application of the fixed point theorem of Rudolf Carnap [1934] and the traditional analysis of paradoxical sentences like the “liar sentence”. Thus the substantial analytical work preceded him. The innovation in Gödel’s paper was the technique … of the arithmetization of syntax … and is what allowed Gödel to apply the fixed point theorem and the analysis of paradoxical statements to the case of provability. (p. 67)
This is hopeless. (1) The fixed point theorem wasn’t proved by Carnap until after he learnt of Gödelian incompleteness — so that “substantial analytical work” did not in fact precede Gödel. (2) The fixed point theorem for a suitable theory T is of the form that for every open sentence φ(x) there is a sentence γ such that T proves γ ↔ φ(“γ”), where “γ” is the Gödel-number, in a given scheme, for γ. So the fixed point theorem cannot precede the arithmetization of syntax: it requires arithmetization for its very statement. (3) And what on earth is “the traditional analysis of paradoxical sentences like the ‘liar sentence'” and how is that supposed to have been applied in Gödel’s incompletness proof?
Back, though, to the extravagant claim that arithmetization is the most — yes, most — significant positive contribution to Hilbert’s program (so much for Gentzen, then, and work in proof-theory downstream from him; so much for what many regard as the direct descendent of Hilbert’s program in the project of reverse mathematics). What can Franks mean?
Well, the thought is that, even if Gödel’s idea of arithmetization did lead to the incompleteness theorems that sabotaged Hilbert’s more ambitious hopes for proof theory, still this was only possible because
the same discovery vindicated Hilbert’s principal philosophical conviction: that by being cast within mathematics itself important questions about mathematics could be investigated without favouring any philosophical tendencies over others. (p. 66)
But I don’t find that particularly convincing as a defence of the extravagant claim. After all, Hilbert already had emphasized the key point that when we go metatheoretical, and move from thinking about sets (for example) to thinking about formalized-theories-about-sets, we move from considering infinite sets to considering suites of finite formal objects (wffs, and finite sequences of wffs) — and we might then hope to bring to bear, at the metatheoretical level, merely finitary formal reasoning about these suites of finite formal objects in order to prove consistency, etc. It’s the formalization that gives us a new, finitary, subject matter apt for formal investigation — apt, in other words, for mathematical treatment. The additional fact that we can arithmetically code up finite objects by mapping them to numbers means we might be able to bring some more, already familiar, mathematics to bear on these objects (just as when we co-ordinatize a space we can bring the arithmetic of the reals to bear on geometrical objects). But just as we don’t need co-ordinatization to vindicate treating geometrical objects mathematically, we don’t need arithmetization to vindicate bringing formal methods to bear on the formal objects given us when we formalize a theory and go metatheoretical.
First, Peter, concerning the fixed-point theorem/arithmetization priority claim — “hopeless” indeed. I have something to say, not in defense of the claim as found in the book, but at least about how it wound up there. But I’ll spare you the details: The claim is false, and the most charitable thing my readers can do is ignore it and notice that it doesn’t tie in significantly with any of the central points in the book. Obviously I meant for this comment to intensify the ironic assessment of Goedel’s results that I am putting forward. But there wasn’t much to be gained thereby, and that makes my failure look that much more awkward.
As for the more central claim. To call Goedel’s contribution the most significant one should seem ironic, given the usual view about these things, but I’m surprised to see the idea described as extravagant. Once one drops the usual view and sees Hilbert primarily looking for precise mathematical formulations of metatheoretical statements, Goedel’s work on arithmetization surely is the most needed thing beyond what Hilbert already provided. You write:
“It’s the formalization that gives us a new, finitary, subject matter apt for formal investigation — apt, in other words, for mathematical treatment. The additional fact that we can arithmetically code up finite objects by mapping them to numbers means we might be able to bring some more, already familiar, mathematics to bear on these objects”
If I were to compare the relevance of Hilbert’s conception of formalization and Goedel’s work on arithmetization, I would whole-heartedly agree that Hilbert’s own work is more central to his project than is Goedel’s contribution to it. But I’m comparing Goedel’s contribution with others’ — not with Hilbert’s initial framing of his program — and the fact remains that before Goedel’s contribution, the formalization of metatheory was incomplete. Hilbert wasn’t able to determine what principles, precisely, he needed for various metatheoretical investigations (his waffling over the possibility of a non-circular analysis of elementary induction is supposed to illustrate this). Arithmetization doesn’t simply bring more formal techniques into the project, it finally allows one to see exactly what formal techniques one is using at a given time.
We’ll take the charitable line on the fixed-point theorem/arithmetization priority claim! :-)
As to “Arithmetization doesn’t simply bring more formal techniques into the project, it finally allows one to see exactly what formal techniques one is using at a given time” I’m still not sure quite what this means — maybe this will become clearer as I read on through the book [sorry that pressure of other things makes this a slow job!].
There is, however, something that can be put in those kinds of words that I’m very sympathetic to, and which may be what you are after (though it doesn’t really come out in the section I was commenting on). For consider, arithmetization does mean that we can can ask the question: what (subsystem) of (perhaps second-order) arithmetic suffices to prove this or that theorem about the formal syntactic objects under consideration — and we can calibrate the strength of the assumptions needed in this or that proof in terms of the strength of the comprehension principle needed or whether we need König’s lemma etc. etc. as in Simpson’s project. But you nowhere mention Simpson so I’m not sure (yet) whether that connects with the way you are thinking about these things or not.
Thanks for the continued comments on this book. Two things:
Should the quote from p 66 say “without favouring” rather than “with favouring”?
And, btw, have you seen (or heard of) a newly available book called “There’s Something about Godel!: The Complete Guide to the Incompleteness Theorem” by Francesco Berto?
I think it is a translation of a book originally in Italian.
Thanks, yes, “with” should indeed be “without”, and I’ve corrected it.
And yes, I’ve a copy of “There’s Something about Godel!” on its way from Amazon — I’ll let the world know what I think about it here :-)