Kurt Gödel and computability theory

Logical Approaches to Computational Barriers Second Conference on Computability in Europe, CiE 2006, Swansea. Proceedings. LNCS 3988 (Springer, Berlin, 2006) 575-583

Although Kurt Gödel does not figure prominently in the history of computabilty theory, he exerted a significant influence on some of the founders of the field, both through his published work and through personal interaction. In particular, Gödel’s 1931 paper on incompleteness and the methods developed therein were important for the early development of recursive function theory and the lambda calculus at the hands of Church, Kleene, and Rosser. Church and his students studied Gödel 1931, and Gödel taught a seminar at Princeton in 1934. Seen in the historical context, Gödel was an important catalyst for the emergence of computability theory in the mid 1930s.



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