This book gives a detailed treatment of functional interpretations of arithmetic, analysis, and set theory. The subject goes back to Gödel's Dialectica interpretation of Heyting arithmetic which replaces nested quantification by higher type operations and thus reduces the consistency problem for arithmetic to the problem of computability of primitive recursive functionals of finite types. Regular functional interpretations, in particular the Dialectica interpretation and its generalization to finite types, the Diller-Nahm interpretation, are studied on Heyting as well as Peano arithmetic in finite types and extended to functional interpretations of constructive as well as classical systems of analysis and set theory. Kreisel's modified realization and Troelstra's hybrids of it are presented as interpretations of Heyting arithmetic and extended to constructive set theory, both in finite types. They serve as background for the construction of hybrids of the Diller-Nahm interpretation of Heyting arithmetic and constructive set theory, again in finite types. All these functional interpretations yield relative consistency results and closure under relevant rules of the theories in question as well as axiomatic characterizations of the functional translations.

Gerhard Gentzen has been described as logic’s lost genius, whom Gödel called a better logician than himself. This work comprises articles by leading proof theorists, attesting to Gentzen’s enduring legacy to mathematical logic and beyond. The contributions range from philosophical reflections and re-evaluations of Gentzen’s original consistency proofs to the most recent developments in proof theory. Gentzen founded modern proof theory. His sequent calculus and natural deduction system beautifully explain the deep symmetries of logic. They underlie modern developments in computer science such as automated theorem proving and type theory.

Paris of the year 1900 left two landmarks: the Tour Eiffel, and David Hilbert's celebrated list of twenty-four mathematical problems presented at a conference opening the new century. Kurt Gödel, a logical icon of that time, showed Hilbert's ideal of complete axiomatization of mathematics to be unattainable. The result, of 1931, is called Gödel's incompleteness theorem. Gödel then went on to attack Hilbert's first and second Paris problems, namely Cantor's continuum problem about the type of infinity of the real numbers, and the freedom from contradiction of the theory of real numbers. By 1963, it became clear that Hilbert's first question could not be answered by any known means, half of the credit of this seeming faux pas going to Gödel. The second is a problem still wide open. Gödel worked on it for years, with no definitive results; The best he could offer was a start with the arithmetic of the entire numbers. This book, Gödel's lectures at the famous Princeton Institute for Advanced Study in 1941, shows how far he had come with Hilbert's second problem, namely to a theory of computable functionals of finite type and a proof of the consistency of ordinary arithmetic. It offers indispensable reading for logicians, mathematicians, and computer scientists interested in foundational questions. It will form a basis for further investigations into Gödel's vast Nachlass of unpublished notes on how to extend the results of his lectures to the theory of real numbers. The book also gives insights into the conceptual and formal work that is needed for the solution of profound scientific questions, by one of the central figures of 20th century science and philosophy.

This volume commemorates the life, work and foundational views of Kurt Gödel (1906–78), most famous for his hallmark works on the completeness of first-order logic, the incompleteness of number theory, and the consistency - with the other widely accepted axioms of set theory - of the axiom of choice and of the generalized continuum hypothesis. It explores current research, advances and ideas for future directions not only in the foundations of mathematics and logic, but also in the fields of computer science, artificial intelligence, physics, cosmology, philosophy, theology and the history of science. The discussion is supplemented by personal reflections from several scholars who knew Gödel personally, providing some interesting insights into his life. By putting his ideas and life's work into the context of current thinking and perceptions, this book will extend the impact of Gödel's fundamental work in mathematics, logic, philosophy and other disciplines for future generations of researchers.

a

Bridging the foundations and practice of constructive mathematics, this text focusses on the contrast between the theoretical developments - which have been most useful for computer science - and more specific efforts on constructive analysis, algebra and topology.