Hilbert’s program then and now

Dale Jacquette, ed., Philosophy of Logic. Handbook of the Philosophy of Science, vol. 5. (Elsevier, Amsterdam, 2006), 411-447.

Hilbert’s program was an ambitious and wide-ranging project in the philosophy and foundations of mathematics. In order to “dispose of the foundational questions in mathematics once and for all,” Hilbert proposed a two-pronged approach in 1921: first, classical mathematics should be formalized in axiomatic systems; second, using only restricted, “finitary” means, one should give proofs of the consistency of these axiomatic systems. Although Gödel’s incompleteness theorems show that the program as originally conceived cannot be carried out, it had many partial successes, and generated important advances in logical theory and metatheory, both at the time and since. The article discusses the historical background and development of Hilbert’s program, its philosophical underpinnings and consequences, and its subsequent development and influences since the 1930s.

DOI: 10.1016/B978-044451541-4/50014-2


The epsilon calculus and Herbrand complexity

Studia Logica 82 (2006) 133-155
(with Georg Moser)

Hilbert’s \(\varepsilon\)-calculus is based on an extension of the language of predicate logic by a term-forming operator \(\varepsilon x\). Two fundamental results about the \(\varepsilon\)-calculus, the first and second epsilon theorem, play a role similar to that which the cut-elimination theorem plays in sequent calculus. In particular, Herbrand’s Theorem is a consequence of the epsilon theorems. The paper investigates the epsilon theorems and the complexity of the elimination procedure underlying their proof, as well as the length of Herbrand disjunctions of existential theorems obtained by this elimination procedure.

Review: Mathematical Reviews 2205042 (2006k:03127) (Mitsuru Yasuhara) 

DOI: 10.1007/s11225-006-6610-7


Decidability of quantified propositional intuitionistic logic and S4 on trees of height and arity ≤ ω

Journal of Philosophical Logic 33 (2004) 155–164.

Quantified propositional intuitionistic logic is obtained from propositional intuitionistic logic by adding quantifiers \(\forall p\), \(\exists p\), where the propositional variables range over upward-closed subsets of the set of worlds in a Kripke structure. If the permitted accessibility relations are arbitrary partial orders, the resulting logic is known to be recursively isomorphic to full second-order logic (Kremer, 1997). It is shown that if the Kripke structures are restricted to trees of at height and width at most \(\omega\), the resulting logics are decidable. This provides a partial answer to a question by Kremer. The result also transfers to modal S4 and some Gödel-Dummett logics with quantifiers over propositions.

Review: M. Yasuhara (Zentralblatt 1054.03011)

DOI 10.1023/B:LOGI.0000021744.10237.d0


Hilbert’s “Verunglückter Beweis,” the first epsilon theorem, and consistency proofs

History and Philosophy of Logic 25(2) (2004) 79–94.

In the 1920s, Ackermann and von Neumann, in pursuit of Hilbert’s Programme, were working on consistency proofs for arithmetical systems. One proposed method of giving such proofs is Hilbert’s epsilon-substitution method. There was, however, a second approach which was not reflected in the publications of the Hilbert school in the 1920s, and which is a direct precursor of Hilbert’s first epsilon theorem and a certain ‘general consistency result’ due to Bernays. An analysis of the form of this so-called ‘failed proof’ sheds further light on an interpretation of Hilbert’s Program as an instrumentalist enterprise with the aim of showing that whenever a ‘real’ proposition can be proved by ‘ideal’ means, it can also be proved by ‘real’, finitary means.

Review: Dirk Schlimm (Bulletin of Symbolic Logic 11/2 (2005) 247–248)

DOI: 10.1080/01445340310001606930


The practice of finitism: Epsilon calculus and consistency proofs in Hilbert’s Program

Synthese 137 (2003) 211-259.

After a brief flirtation with logicism in 1917–1920, David Hilbert proposed his own program in the foundations of mathematics in 1920 and developed it, in concert with collaborators such as Paul Bernays and Wilhelm Ackermann, throughout the 1920s. The two technical pillars of the project were the development of axiomatic systems for ever stronger and more comprehensive areas of mathematics and finitistic proofs of consistency of these systems. Early advances in these areas were made by Hilbert (and Bernays) in a series of lecture courses at the University of Göttingen between 1917 and 1923, and notably in Ackermann’s dissertation of 1924. The main innovation was the invention of the epsilon-calculus, on which Hilbert’s axiom systems were based, and the development of the epsilon-substitution method as a basis for consistency proofs. The paper traces the development of the “simultaneous development of logic and mathematics” through the epsilon-notation and provides an analysis of Ackermann’s consistency proofs for primitive recursive arithmetic and for the first comprehensive mathematical system, the latter using the substitution method. It is striking that these proofs use transfinite induction not dissimilar to that used in Gentzen’s later consistency proof as well as non-primitive recursive definitions, and that these methods were accepted as finitistic at the time.

Note: his is a revised version of Chapter 3 of my dissertation.

Review: John W. Dawson, Jr (Mathematical Reviews 2038463 (2005b:03008))

DOI: 10.1023/A:1026247421383 (Subscription required)


Characterization of the axiomatizable prenex fragments of first-order Gödel logics

In: 33rd International Symposium on Multiple-valued Logic. Proceedings. Tokyo, May 16-19, 2003 (IEEE Computer Society Press, 2003) 175-180 (with Matthias Baaz and Norbert Preining)

The prenex fragments of first-order infinite-valued Gödel logics are classified. It is shown that the prenex Gödel logics characterized by finite and by uncountable subsets of [0, 1] are axiomatizable, and that the prenex fragments of all countably infinite Gödel logics are not axiomatizable.

DOI: 10.1109/ISMVL.2003.1201403


Tableaux for reasoning about atomic updates

Logic for Programming, Artificial Intelligence, and Reasoning. 8th International Conference, LPAR 2001. Proceedings, LNAI 2250. (Springer, Berlin, 2001) 639-653
(with Christian G. Fermüller and Georg Moser)

A simple model of dynamic databases is studied from a modal logic perspecitve. A state \(\alpha\) of a database is an atomic update of a state \(\beta\) if at most one atomic statement is evaluated differently in \(\alpha\) compared to \(\beta\). The corresponding restriction on Kripke-like structures yields so-called update logics. These logics are studied also in a many-valued context. Adequate tableau calculi are given.

DOI: 10.1007/3-540-45653-8_44


Quantified propositional Gödel logics

Voronkov, Andrei, and Michel Parigot (eds.) Logic for Programming and Automated Reasoning. 7th International Conference, LPAR 2000. Proceedings, LNAI 1955 (Springer, Berlin, 2000) 240-256
(with Matthias Baaz and Agata Ciabattoni)

It is shown that \(\mathbf{G}^\mathrm{qp}_\uparrow\), the quantified propositional Gödel logic based on the truth-values set \(V_\uparrow = {1 – 1/n : n = 1, 2, . . .} \cup {1}\), is decidable. This result is obtained by reduction to Büchi’s theory S1S. An alternative proof based on elimination of quantifiers is also given, which yields both an axiomatization and a characterization of \(\mathbf{G}^\mathrm{qp}_\uparrow\) as the intersection of all finite-valued quantified propositional Gödel logics.

DOI: 10.1007/3-540-44404-1_16


Hypersequents and the proof theory of intuitionistic fuzzy logic

Clote, Peter G., and Helmut Schwichtenberg (eds.), Computer Science Logic. 14th International Workshop, CSL 2000. Fischbachau, Germany, August 21-26, 2000. Proceedings. (Springer, Berlin, 2000) 187-201
(with Matthias Baaz)

Takeuti and Titani have introduced and investigated a logic they called intuitionistic fuzzy logic. This logic is characterized as the first-order Gödel logic based on the truth value set [0, 1]. The logic is known to be axiomatizable, but no deduction system amenable to proof-theoretic, and hence, computational treatment, has been known. Such a system is presented here, based on previous work on hypersequent calculi for propositional Gödel logics by Avron. It is shown that the system is sound and complete, and allows cut-elimination. A question by Takano regarding the eliminability of the Takeuti-Titani density rule is answered affirmatively.

DOI: 10.1007/3-540-44622-2_12


Completeness before Post: Bernays, Hilbert, and the development of propositional logic

Bulletin of Symbolic Logic 5 (1999) 331–366.

Some of the most important developments of symbolic logic took place in the 1920s. Foremost among them are the distinction between syntax and semantics and the formulation of questions of completeness and decidability of logical systems. David Hilbert and his students played a very important part in these developments. Their contributions can be traced to unpublished lecture notes and other manuscripts by Hilbert and Bernays dating to the period 1917-1923. The aim of this paper is to describe these results, focussing primarily on propositional logic, and to put them in their historical context. It is argued that truth-value semantics, syntactic (“Post-“) and semantic completeness, decidability, and other results were first obtained by Hilbert and Bernays in 1918, and that Bernays’s role in their discovery and the subsequent development of mathematical logic is much greater than has so far been acknowledged.

Note: A slightly revised version constitutes of Chapter 2 of my dissertation.


Volker Peckhaus (Zentralblatt für Mathematik 942.03003)
Hourya Sinaceur (Mathematical Reviews 1791358)


DOI: 10.2307/421184
JSTOR: 421184 



Note on generalizing theorems in algebraically closed fields

Archive for Mathematical Logic 37 (1998) 297–307
(with Matthias Baaz)

The generalization properties of algebraically closed fields \(\mathit{ACF}_p\) of characteristic \(p > 0\) and \(\mathit{ACF}_0\) of characteristic 0 are investigated in the sequent calculus with blocks of quantifiers. It is shown that \(\mathit{ACF}_p\) admits finite term bases, and \(\mathit{ACF}_0\) admits term bases with primality constraints. From these results the analogs of Kreisel’s Conjecture for these theories follow: If for some \(k\), \(A(1 + … + 1)\) (\(n\) 1’s) is provable in \(k\) steps, then \((\forall x)A(x)\) is provable.

Review: Yehuda Rav (Mathematical Reviews 2000a:03057)

DOI: 10.1007/s001530050100


Labeled calculi and finite-valued logics


Studia Logica 61 (1998) 7–33
(with Matthias Baaz, Christian G. Fermüller, and Gernot Salzer)

A general class of labeled sequent calculi is investigated, and necessary and sufficient conditions are given for when such a calculus is sound and complete for a finite­-valued logic if the labels are interpreted as sets of truth values (sets­-as­-signs). Furthermore, it is shown that any finite­-valued logic can be given an axiomatization by such a labeled calculus using arbitrary “systems of signs,” i.e., of sets of truth values, as labels. The number of labels needed is logarithmic in the number of truth values, and it is shown that this bound is tight.

Review: Radim Belohlávek (Mathematical Reviews 99m:03043)

DOI: 10.1023/A:1005022012721


Numbers and functions in Hilbert’s finitism

Taiwanese Journal for Philosophy and History of Science 10 (1998) 33–60
(special issue on philosophy of mathematics edited by Charles Chihara)

David Hilbert’s finitistic standpoint is a conception of elementary number theory designed to answer the intuitionist doubts regarding the security and certainty of mathematics. Hilbert was unfortunately not exact in delineating what that viewpoint was, and Hilbert himself changed his usage of the term through the 1920s and 30s. The purpose of this paper is to outline what the main problems are in understanding Hilbert and Bernays on this issue, based on some publications by them which have so far received little attention, and on a number of philosophical reconstructions and criticisms of the viewpoint (in particular, by Hand, Kitcher, Parsons, and Tait).

Review: Hourya Sinaceur (Mathematical Reviews 2001g:01033)


Compact propositional Gödel logics


28th International Symposium on Multiple Valued Logic. May 1998, Fukuoka, Japan. Proceedings (IEEE Computer Society Press, Los Alamitos, 1998) 108-113
(with Matthias Baaz)


Entailment in propositional Gödel logics can be defined in a natural way. While all infinite sets of truth values yield the same sets of tautologies, the entailment relations differ. It is shown that there is a rich structure of infinite-valued Gödel logics, only one of which is compact. It is also shown that the compact infinite-valued Gödel logic is the only one which interpolates, and the only one with an r.e. entailment relation.

DOI: 10.1109/ISMVL.1998.679315


Incompleteness of an infinite-valued first-order Gödel logic and of some temporal logics of programs

In: Computer Science Logic. 9th Workshop, CSL’95. Selected Papers (Springer, Berlin, 1996) 1-15
(with Matthias Baaz and Alexander Leitsch)

It is shown that the infinite-valued first-order Gödel logic G0 based on the set of truth values \(\{0\} \cup \{1/k : k = 1, 2, 3, \dots\}\) is not r.e. The logic G0 is the same as that obtained from the Kripke semantics for first-order intuitionistic logic with constant domains and where the order structure of the model is linear. From this, the unaxiomatizability of Kröger’s temporal logic of programs (even of the fragment without the nexttime operator) and of the authors’ temporal logic of linear discrete time with gaps follows.

DOI: 10.1007/3-540-61377-3_28


Generalizing theorems in real closed fields

Annals of Pure and Applied Logic 75 (1995) 3–23
(with Matthias Baaz)

Jan Krajicek posed the following problem: Is there is a generalization result in the theory of real closed fields of the form: If \(A(1 + \dots + 1)\) (\(n\) occurrences of 1) is provable in length \(k\) for all \(n = 0, 1, 2, \dots\), then \((\forall x)A(x)\) is provable? It is argued that the answer to this question depends on the particular formulation of the “theory of real closed fields.” Four distinct formulations are investigated with respect to their generalization behavior. It is shown that there is a positive answer to Krajicek’s question for (1) the axiom system RCF of Artin-Schreier with Gentzen’s LK as underlying logical calculus, (2) RCF with the variant LKB of LK allowing introduction of several quantifiers of the same type in one step, (3) LKB and the first-order schemata corresponding to Dedekind cuts and the supremum principle. A negative answer is given for (4) any system containing the schema of extensionality.

DOI: 10.1016/0168-0072(94)00054-7


Elimination of cuts in first-order finite-valued logics

Journal of Information Processing and Cybernetics 29 (1993) 333–355
(with Matthias Baaz and Christian G. Fermüller)

A uniform construction for sequent calculi for finite-valued first-order logics with distribution quantifiers is exhibited. Completeness, cut-elimination and midsequent theorems are established. As an application, an analog of Herbrand’s theorem for the four-valued knowledge-representation logic of Belnap and Ginsberg is presented. It is indicated how this theorem can be used for reasoning about knowledge bases with incomplete and inconsistent information.

Note Errata section at very end for corrected inference rules for the Dunn-Belnap (FDE) system used as an example in the paper.