Notes on the History of Structural Proof Theory
WIP
TODO Select Title
On Ideal Elements in Structural and Axiomatic Proof Theory
TODO Add Date
I mentioned Paul Hertz’s work on axiom systems to a friend a couple weeks ago. He asked if this work was in response to Gödel’s incompleteness theorems. I couldn’t reconstruct the time-line then, but found the question intriguing: what is the connection between Gödel’s work and Hertz’s? I did a bit of reading around this question, and I am presenting some of the interesting aspects of my findings here. I have glossed over most of Gödel’s side of the equation, because that history tends to be well known.
So, iiuc…
The superficial history
Hilbert’s program was advanced in the early 1920s. Granted a sufficient number of caveats, the program can be understood as a formalistic one: proof theory ala Hilbert should explain how a finite number of rules governing a finite number of signs can provide an immanent grounding for the provability of all mathematical reasoning. Gödel’s incompleteness theorems, published in 1931, proved the impossibility of most of Hilbert’s program (at least as Hilbert himself conceived of it).
The kind of proof theory called for by Hilbert’s program is often designated axiomatic proof theory.
Paul Hertz is, arguably, the progenitor of the structural analysis of proofs that Gentzen utilized in order to develop structural proof theory (see Javier Legris’ /Paul Hertz and the Origins of Structural Reasoning/). Hertz published his work, On Axiomatic Systems for Arbitrary Systems of Sentences, in 1922. In a short biography by Hilbert’s collaborator Paul Barneys, Barneys wrote of On Axiomiatic Systems…,
Hier führte er viele methodisch wichtige Begriffsbildungen ein und gelangte zu mathematisch prägnanten Ergebnissen. Diese Untersuchungen sind Vorläufer verschiedener neuerer Forschungen zur mathematischen Logik und Axiomatik, insbesondere hat G. Gentzens Sequenzenkalkul von den H.schen Betrachtungen über Satzsysteme seinen Ausgang genommen.
—
Here he introduced many methodologically important conceptual developments and arrived at mathematically incisive results. These investigations were forerunners of various new researches into mathematical logic and axiomatics, in particular, G. Gentzen’s sequent calculus took its starting point from Hertz’s work on sentence systems.
[/Please pardon my inexpert translation./]
Gentzen’s work was, according to a reductive formulation, the application of Hertz’s approach and core methodology to the problematic set out by Hilbert.
A deeper comparison of the approaches
Hilbert’s Finitism
I want to understand with greater precision and depth what Hilbert had in mind.
The vision Hilbert’s program hoped to realize was colored throughout by finitism. This is first and foremost a metaphysical position.
It is an interesting and striking contrast to the work of Leibniz, Bolzano, and Cantor.
…the definitive clarification of the nature of the infinite, instead of pertaining just to the sphere of specialized scientific interests, is needed for the dignity of the human intellect itself. (185)
After arguing against the reality of infinitude in physics, he turns to the question of whether “the infinite occupies a justified place in our thinking”.
We encounter a completely different and quite unique conception of the notion of infinity in the important and fruitful method of ideal elements. … These ideal “infinite” elements have the advantage of making the system of connection laws as simple and perspicuous as possible. Moreover, because of the symmetry between a point a straight line, there results the very fruitful principle of duality for geometry. (187)
The function and <saving grace> of infinite ideal elements is the facilitation of simplicity, perspicuity, and symmetry.
Let us remember that we are mathematicians and that as mathematicians we have often been in precarious situations from which we have been rescued by the ingenious method of ideal elements. Just as
i=√-1was introduced to preserve in the simplest form the laws of algebra … similarly, to preserve the simple formal rules of ordinary Aristotelian logic, we must supplement the finitary statements with ideal statements. …How do we obtain ideal statements? (On the Infinite, 195)
Hilbert’s work actually ends up being much more like a phenomenology, it seems to me.
TODO Focus on the idea of Ideal Elements in Hilbert and Hertz
Hertz’s Structuralism
Whereas Hilbert sought a tenable set of axioms to provide a self-evident ground for formal proofs of consistency etc., Hertz inquired into the mere topology of axiom systems in general. The opening paragraph of the 1922 paper conveys this:
Whenever a system of sentences is recognized to be valid, it is often not necessary to convey each and every sentence to memory; it is sufficient to choose some of them from which the rest can follow. Such sentences, as is generally known, are called axioms. The choice of these axioms is to a certain degree arbitrary. One can ask, however, if the property of a system of sentences to have several axioms systems is interconnected with other remarkable properties, and if there are systematic approaches to find, as the case may be, that axiomatic system which contains the least possible number of sentences. (Universal Logic, 11)