A 'third way' to consistency (besides Dedekind's and Gentzen's)? Hilbert's 'unverstanden' 1904 Heidelberg ICM proposal for consistency proofs

Question

Question.

(bibliographic) Are there recommendable, preferably modern, detailed and technical discussions in the literature on the kind of consistency proofs that Otto Blumenthal mentions Hilbert proposed in 1904 in an address to the third ICM in Heidelberg?

(philosophical) Do you think it is meaningful to distinguish between the following three, given in chronological order, essentially different kinds of consistency proofs:

• semantic consistency-proofs (roughly: constructing a model of the axioms, the model preferably being perceived as reasonable by others)

• Heidelberg-style¹ consistency-proofs (this kind of consistency proof is the topic of this question; by these I mean the ones mentioned by Blumenthal, and they seem not to be discussed in the technical literature, probably with a reason, for perhaps this is not known to work, which is why I am asking, yet extrapolating from the words this means: define a group of symmetries acting on all wellformed formulae over the relevant signature, then show that sets of sentences which are inconsistent have, in some precise sense, little symmetry, then turn toward the axioms whose consistency one would like to prove, and prove that these axiom do have much symmetry, which implies consistency; this sounds like vague speculation and wishful thinking and I have not seen this made precise anywhere, which is perhaps explained by Blumenthal's dismissive words 'erwiesen sich bei genauerem Eingehen als unzulänglich'.

• syntactic consistency-proofs (by this I mean consistency proofs more-or-less in the style of Gentzen's famous 1936 'Zur Widerspruchsfreiheit der reinen Zahlentheorie'; this is very well documented, not the topic of this question, and I won't say more about this here)

(mathematical) Do you know a specific mathematical reason for and/or discussion in the literature of Blumenthal's verdict "unzulänglich"?

Commentary.

• In Otto Blumenthal's biographical essay about David Hilbert, written on the occasion of the 1935 Springer publication of the third volume of Hilbert's collected works, Blumenthal mentions 'misunderstood' what one might, perhaps distortingly, call a failed proposal of Hilbert's for consistencies proofs for formal systems.

The highlighted passages can be translated thus

[...] basic idea of his later proof theory: that one should examine the form of the formulae that can be deduced from a given system of axioms, and that then a certain invariance of this form would become apparent [...] formulas which are contradictory do not exhibit this invariance [...] the talk remained, for all I know, completely ununderstood, and the approaches proposed in the talk turned out to be unsuitable upon a closer examination

• Part of my motivation is working on a non-ahistorical answer to this MO question. Hilbert's address predates Zermelo's comments by several years, so this seems relevant.

Bibliographic remark. The published version of Hilbert's 1904 ICM talk at Heidelberg was published in the proceedings of the conference:

David Hilbert Über die Grundlagen der Logik und der Arithmetik, Verhandlungen des 3. Internationalen Mathematiker-Kongresses in Heidelberg vom 8. bis 13. August 1904, pp. 174-185 (available e.g. from University of Heidelberg)

and there is at least one translated version:

David Hilbert On the foundations of logic and arithmetic, The Monist, Vol. 15, No. 3 (July 1905), pp. 338-352. Translated by George Bruce Halsted.

¹ This term is not attested and was invented for the present question.

Answer 1

In regards to your bibliographic question, I suggest the highly informative essay by Craig Smoryński, Hilbert's programme; he gives a highly compressed account of Hilbert's 1904 proof on pp.7-8 of the pdf file (pp. 9-10 of the paper), including some commentary on its limitations.

In regards to your "philosophical" question, first, note that, if Smoryński is right, then Hilbert's 1904 proof is not exactly like the idea you suggested, since there is no need to invoke group theoretic ideas. Rather, the "invariant property" claimed for the axioms and theorems is that of being homogeneous equations, that is, equations whose equated terms have the same number of symbols. And the proof here is a simple induction on the length of proofs: the axioms are all homogeneous equations, and the rules of inference also take homogeneous equations to homogeneous equations (this is immediate by inspection, if you look at the axioms and rules on p. 7 of the pdf). This shows that the the system is consistent because it's clear that, say, 0=S(0) is not homogeneous, so the system can't derive that particular equation. Although very primitive, this is essentially the idea behind Gentzen's consistency proof of the first-order sequent calculus: cut elimination shows that every canonical proof has the subformula property, and any purported derivation of a contradiction would not have this property (because a contradiction, in the sequent calculus, has no subformulas---unfortunately, as is well-known, this strategy won't work for Peano Arithmetic).