(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-style1 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"?
- 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.
1 This term is not attested and was invented for the present question.