Hilbert’s consistency proof in the Foundations of Mathematics is model-theoretic. But of course the later Hilbert seeks consistency proofs that don’t depend on model-construction: what then are the resources can be brought to bear in syntactic proof-theory? Well, §3.4 on “Hilbert’s proto-proof theory”, discusses in particular how far induction can be used if we want a non-circular consistency proof of arithmetic. (Note, by the way, following up a comment on the previous section, in this current section when Franks talks of “arithmetic”, he does indeed seem to mean it in the narrow sense of the arithmetic of the natural numbers.)
Poincaré famously challenges the very possibility of a non-circular justification of induction. In response Bernays, in 1922, writes
two types of complete induction are to be distinguished: the narrow form of induction, which relates only to something completely and concretely given, and the wider form of induction, which uses either the general concept of whole number or the operating with variables in an essential manner. [Quoted by Franks, p. 76.]
Now, I make no pretence at all to be any kind of historian. So maybe I’m just reading back into this remark something that only became really clear to the Hilbert school much later. But it seems to suggest the following thought. It is one thing to accept induction over predicates that are sufficiently “concrete” (whose application to a particular case can be determined in a direct way), and something else to accept induction over predicates that e.g. themselves embed variables. It is the latter than we need to get full-strength induction in arithmetic. But perhaps the pre-Gödel Hilbertian hope is that it is the former — which e.g. we might regiment in PRA — that could suffice for proof-theory.
Franks however says this:
[T]he true threat of circularity — and the one Poincaré apparently advances — concerns the strength of the principle used and not the subject matter to which one applies it. Bernays’ defense is therefore inadequate to meet this threat, for he distinguishes only the ranges of application in the narrow and wide uses of induction and not their deductive strengths.
So Franks reads Bernays as just drawing a distinction between domains of application of the same inductive principle (“concrete-intuitive”, as Bernays puts it, vs. arithmetical?) rather than a distinction between the inferential strength of two different principles, i.e. induction for quantifier free predicates and induction for arbitrarily complex predicates. But why is this the right reading? For all I know, it might be. But since Franks doesn’t here even mention what seems — with hindsight? — to be the alternative natural reading, I just don’t know why he prefers a reading which has Bernays making a rather feebly question-begging response to Poincaré rather than read him as pointing to a potentially more promising response (a response that of course must fail, but it will take Gödel to show that). Franks quotes a passage from Hilbert on p. 78 which seems again to invite what I’m calling the natural reading, for it seems to contrast “contentual” induction with induction in cases which essentially involve (non-schematic) variables. But Franks says that Hilbert too is drawing a distinction which “seems to have more to do again with the proper subject matter of the two principles than with their comparative inferential strength”. Again I don’t see why.
There’s another passage I don’t understand near the end of the section. Franks writes that
[E]ven if one follows Hilbert in treating formulas and proofs mechanically, without attributing any meaning to them or the symbols from which they are built up, a statement about proofs and formulas — Bernays’ formulation of consistency for example — is itself not such a formula but rather an ordinary statement. To confirm or refute a statement like this, either one’s proof theory must be sufficiently informal to treat such statements directly, or to a purely mathematical Beweistheorie one must append some extra-mathematical reasoning to determine when informal metatheoretical questions have been settled by mathematical results. The lack of purity in his program thus stemmed from the informality of the consistency statement he aimed to verify. (p. 82)
But what’s the complaint here? We formalize a given mathematical theory T, clarifying its axoims, deductive apparatus etc. Then its syntactical proof-properties, in particular, themselves become possible objects for mathematical enquiry (which doesn’t mean that T lacks content, of course: it is just that investigating T‘s syntactic proof-properties is done without reference to that content). Now the mathematical enquiry about T‘s syntactic properties gives us another theory — call it ‘M‘ for metatheory. And, if we want, M of course can itself be regimented more or less into the ideal of a formalized theory: compare, for example, the theories of first-order syntax given in different levels of logic book. And whether relaxedly informal or souped-up to the most rigorous standards, either way M still treats T‘s syntax “directly”. It isn’t the case that only an informal theory has semantics, or that a mathematics of syntactic structures needs to be supplemented by something else before it can be about those structures. Franks seems here to be sliding between “informal” and “contentful”, “formalized” and “contentless”. But that would just be a mistake — and not one he’s given us reason to suppose, either, that Hilbert was guilty of. Assuming Franks isn’t making that mistake, I don’t see what his point is.
And I lost the will to continue blogging. As I recall, reading on, I didn’t find things improving …