Logic Matters

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.