I recently heard some speculation on the origin of the term “Hilbert system” for the axiomatic systems that are used to inflict pain on logic students, particularly at the start of proof theory classes. A long time ago, at least when Gentzen wrote, they were called logistic systems. The first publication in which they were called “Hilbert systems” seems to have been Entailment, vol. 1. Does anyone know if there are earlier uses? I’d be quite happy if that turned out to be the origin of the term.
Advertisements
5 comments
Comments feed for this article
September 27, 2008 at 1:19 pm
ansten
Kleene’s Introduction to Metamathematics (1952), ch. 15, dubs the type of system you are referring to `Hilbert-type system,’ and Kleene calls his particular system H. He also introduces the term `Gentzen-type system,’ and a few specimens thereof, namely G1, G2, G3 and G3a (all being different sequent calculi). From Kleene’s wording it sounds as if he is baptizing the systems there and then; besides, Kleene was meticulous in his references to other work, so it is likely that he would have referred to other uses of these terms had there been any such uses to refer to. I conclude that the term `Hilbert system’ originated with Kleene. This conclusion can of course be tested by a couple of days in the library; maybe some other readers will be in a position to correct me.
Sam Buss in his Handbook of Proof Theory introductory chapter calls Hilbert-type systems Frege systems. Even if the “axioms” of Buss’ system has some formal resemblance with the axioms (without quotation marks) of Frege’s ideography, Buss’ baptism misses a crucial point: `Hilber-type system’ is a name of certain mathematical study object, and as such the use of Hilbert’s name in them is suitable, given his ideas of a Beweistheorie. Frege’s ideography on the other hand is a logistic system to the use of logicians, a system Frege himself wanted to use to show that the truths of arithmetic rested on logical truths; these logical truths were not mere strings of symbols but rather like the sentences I am writing here, sentences expressing certain thoughts.
The term `logistic’ is interesting, not the least for its rather exotic flavour. Tarski uses it in his 1923 paper Sur le terme primitif de la Logistique, so it was presumably in use among the Polish logicians. The term also occurs much later in Church’s Introduction to Mathematical Logic. For him a logistic system is an uninterpreted calculus (p. 48); this is of course not the understanding the Polish logicians could have had — for them a logistic system was an interpreted system with meaningful, indeed true, axioms and theorms.
September 27, 2008 at 3:11 pm
Shawn
Ansten,
Thanks for pointing out the Kleene reference. While not an exact match, that is close enough I expect. The authors of Entailment definitely read Kleene.
I think Poincare uses the term “logistic” in his papers criticizing Russell, so there is probably some history to that too. I didn’t realize that logistic systems were interpreted for the Polish logicians.
September 29, 2008 at 12:39 pm
ansten
This is not directly related to your initial inquiry, but since the history of the term logistics has been brought up, I would like to report on footnote 125 in Church’s book, which in fact outlines such a history. According to Church, logistic, or its Latin brother, logistica, originally meant the art of calculation or common arithmetic; Leibniz used it synomously with his logica mathematica, calculus ratiocinator, and other terms. Moreover, “Its modern use for mathematical logic dates from the International Congress of Philosophy of 1904, where it was proposed independently by Itelson, Lalande, and Couturat” [the latter of these published La Logique de Leibniz (1901)].
Church in this footnote — one of a total of 590 — also points out that the term somethins “has been used with special reference to the school of Russell or to the Frege-Russell doctrine that mathematics is a branch of logic.” This may explain Poincare’s use of the term to which you refer.
To complete the picture, one should perhaps point out that the more domestic logistics [a topic my grandmother took me as studying when I told her I study logic — did anyone else experience something similar?] derives according to the OED from French loger (lodge). I don’t know whether this logistics is related to our logistics.
October 19, 2008 at 1:44 pm
Jeff Rubard
Eat this comment.
The reason they’re called “Hilbert systems” is that they derive from Hilbert and Ackermann’s Grundzuege der theoretischen Logik, which also formulated the Entscheidungsproblem by codifying first-order logic (which is why it’s non-ideal to call them “Frege systems”). “Hilbert system” is the inelegant Englishing of that fact, but a logical one if you are writing English (and not right on top of Hilbert, like Gentzen).
October 8, 2012 at 6:55 am
S Reza Musavi
from A. S. Troelstra in “basic proof theory”:
2.5.3. Hilbert systems. Kleene [1952a] uses the term “Hilbert-type system”;
this was apparently suggested by Gentzen [1935], who speaks of “einem dem Hilbertschen Formalismus angeglichenen Kalkiil”. Papers and books such as Hilbert [1926,1928], Hilbert and Ackermann [1928], Hilbert and Bernays [1934] have made such formalisms widely known, but they date from long before Hilbert; already Frege [1879] introduced a formalism of this kind (if one disregards the enormous notational differences). We have simplified the term “Hilbert-type system” to “Hilbert system”. There is one aspect in which our system differs from the systems used by Hilbert and Frege: they stated the axioms, not as schemas, but with proposition variables and/or relation variables for A, B, C, and added a substitution rule. As far as we know, von Neumann [1927] was the first to use axiom schemas.
but I should take a look at A. Church’ Great Book.