In addition to the new special issue celebrating the 50th anniversary of Gödel’s Dialectica interpretation, Wiley-Blackwell has made the original Dialectica issue in which it appeared freely available. That issue itself was a Festschrift in honour of Paul Bernays’s 70th birthday. (I’m sorry I’m late to herewith commemorate the 120th birthday of Bernays, who was born October 17, 1888.) The issue also includes the classics “Hilbert’s programme” by Kreisel, “80 years of foundational studies” by Wang, and “Observation language and theoretical language” by Carnap, in addition to papers by Ackermann, Beth, Curry, Heyting, Fraenkel, Gonseth, Goodstein, Hermes, Péter, A. Robinson, Schütte, Schmidt, Skolem, and Specker.

# Month: November 2008

# The 50th Birthday of the Dialectica Interpretation

Gödel’s paper containing his so-called Dialectica interpretation was published 50 years ago in, well, Dialectica. And so Dialectica has a special issue on Gödel’s Dialectica interpretation, edited by Thomas Strahm. It looks like all the articles are freely available. Here’s (most of) the introduction:

Gödel’s famous dialectica paper (1958), entitled ‘Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes’, was published in a special issue of this journal in 1958 in honour of Paul Bernays’ 70th birthday. In the past fifty years, the dialectica interpretation proposed by Gödel has become one of the most fundamental conceptual tools in logic and the foundations of mathematics. This special issue traces some of the fundamental issues and applications of Gödel’s interpretation. The ideas of Gödel’sdialectica interpretation date back at least as far as 1941, when Gödel presented them in a lecture to the mathematics and philosophy clubs at Yale University. The Yale lecture was entitled ‘In What Sense is Intuitionistic Logic Constructive?’ and can be found in Volume III of the Collected Works (1994). Prior to the Yale lecture, Gödel had delivered two addresses where he raised important thoughts towards the dialectica interpretation: an invited lecture given in 1933 in Cambridge, Massachusetts entitled ‘The Present Situation in the Foundations of Mathematics’ and an informal seminar in 1938 ‘Vortrag bei Zilsel’ delivered in Vienna. The full history of the dialectica paper is presented by Feferman (1993) and Troelstra (1990).

Let us briefly summarize the main rationale of Gödel’s dialectica interpretation. In its most elementary form, it provides an interpretation of intuitionistic number theory in a quantifier-free theory of functionals of finite type. Together with Gödel’s double-negation interpretation from classical arithmetic into its intuitionistic counterpart, the dialectica interpretation also provides a reduction of classical arithmetic. Gödel’s functional interpretation can be seen as a possible realization of the so-called modified Hilbert program in the sense that it enables a reduction of a classical system to a quantifier-free theory of functionals of finite type, thereby reducing the consistency problem for the classical theory to the consistency of a quantifier-free system of higher-type recursion, the latter being informally more finitistic and sufficiently well understood.

Gödel’s interpretation of arithmetic has been substantially extended in the past fifty years both to stronger and weaker theories. In particular, versions of the dialectica interpretation have been proposed for impredicative classical analysis, subsystems of classical arithmetic, theories of ordinals, predicative subsystems of second order arithmetic, analysis with game quantifiers, systems of feasible arithmetic and analysis, admissible and constructive set theories, as well as iterated arithmetical fixed point theories. A comprehensive survey of many of these results can be found in Avigad and Feferman (1995) as well as Troelstra (1973). In more recent years, work on functional interpretations has shifted from purely foundational purposes to applications to concrete proofs in mathematics in the sense of Kreisel’s unwinding program. In connection with this, Kohlenbach’s proof mining program provides very impressive results making use of variants of Gödel’s dialectica interpretation, see his article in this special issue.

Let us now give a brief survey of the articles contained in this special issue.

The paper by Justus Diller gives a broad survey of functional interpretations in the context of constructive set theories and elaborates in detail on the logical problems one has to solve in order to provide such interpretations of set theory. In addition, a new simplified interpretation, the so-called ∧-interpretation, is proposed and analyzed. It is rooted in the Diller-Nahm interpretation of 1974.

Solomon Feferman’s paper gives a vivid account of Gödel’s views on finitism, constructivity and Hilbert’s program, using unpublished articles and lectures as well as Gödel’s correspondence with Paul Bernays. Feferman’s article contains a full section on the dialectica interpretation and on Gödel’s influential Cambridge lecture mentioned above.

Fernando Ferreira’s article gives an informal analysis of Gödel’s dialectica interpretation and presents a balanced mixture between philosophical discussions and technical issues. The paper starts off by a discussion of Gödel’s use of higher types and the relationship to his set-theoretic realism. Further investigations of the paper include the validation of additional principles, higher order equality and monotone functional interpretations.

As already mentioned above, Ulrich Kohlenbach’s article is centred on recent topics in applied proof theory and, in particular, his recent program of proof mining. His paper focuses on the logical aspects of his program and, in particular, on the systematic design and study of variants of the dialectica interpretation, which have been used in applications to concrete proofs from various areas of mathematics.

Finally, Paulo Oliva’s article provides a detailed analysis of Gödel’s dialectica interpretation via linear logic. The latter comes naturally into the picture of Gödel’s interpretation, since contraction is the main source of its asymmetry. The paper analyses various properties of the dialectica interpretation, e.g. the characterization theorem, within the context of linear logic.

# New SEP Entry: Bimbó on Combinatory Logic

Shawn beat me to it: Katalin Bimbó, who’s now at the University of Alberta, just published a nice entry on combinatory logic in the SEP.

# Papers by Konrad Zdanowski

Via Theorem(e), I’ve come across the webpage of Konrad Zdanowski, a logician at the Polish Academy and Paris 7. His papers (mostly on arithmetic) all look incredibly interesting, he has lecture notes on Peano arithmetic, and there’s also a paper on 2nd order intuitionistic propositional logic, which is somewhat related to my own research. If I only weren’t so much behind in grading papers!

# Tait, Cut-Elimination for Predicative Systems

Sitting in a talk at CMU by Bill Tait on cut elimnation for predicative systems. His approach, in contrast to Rathjen and Takeuti, is to try to get the cut-elimination proof to be mostly (or even, only) about the proofs, and not about proofs and (mostly) ordinal notation systems. He’s using the original Tait calculus, in which formulas are all propositional, but infinitary. His cut-elimination theorem applies in all kinds of cases (essentially up through predicative arithmetic), which I hadn’t realized before. But then I don’t think the original paper actually emphasizes that. The main point in that regard is that when you translate axioms from a theory, you can assign the right kinds of ordinals.

Rick Statman made an interesting point, viz., that it’s also important to verify that the infinitary derivations that you get when you translate derivations into Tait calculus are (primitive) recursively described, and that this is preserved when you eliminate the cuts–if this weren’t the case, you wouldn’t be able to carry out the cut-elimination proof in extensions of PRA.

# Taxonomy for Logic and Philosophy of Mathematics

David Chalmers and David Bourget are setting up a new online resource for papers in philosophy, for which they’re designing a taxonomy of philosophical topics to be used for classifying papers in the database. David asks

For now, I’m calling for feedback from the philosophical community, either via e-mail or via comments on this blog. Especially valuable will be thoughts on categories that we’ve missed, on ways to structure categories that don’t yet have much structure, and on better ways of structuring things in tricky cases.

Please post responses at Dave’s blog. The logic and philosophy of math part of the taxonomy right now looks like this:

Logic and Philosophy of Logic

Logics

Classical Logic

Aristotelian Logic

Propositional Logic

Predicate Logic

Deontic Logic

Epistemic Logics

Doxastic and Epistemic Logic

Inductive Logic

Nonmonotonic Logic

Higher-Order Logics

Second-Order Logic

Higher-Order Logics, Misc

Modal and Intensional Logic

Intensional Modal Logic

Modal Logic

Provability Logics

Quantified Modal Logic

Semantics for Modal Logic

Nonclassical Logics

Fuzzy Logics

Infinitary Logics

Intuitionistic Logic

Many-Valued Logics

Paraconsistent Logics

Quantum Logic

Relevance Logics

Substructural Logics

Temporal Logic

Logics, Misc

Logical Pluralism

Logical Consequence and Entailment

Logical Expressions

Logical Constants

Logical Connectives

Quantifiers*

Variables

Logical Paradoxes

Sorites Paradox*

Liar Paradox

Russell's Paradox*

Logical Semantics and Logical Truth

Model Theory and Proof Theory

Philosophy of Logic, Misc

Dialetheism

Epistemology of Logic

Informal Logic

Logical Pluralism

Logic in Philosophy

Philosophy of Mathematics

Epistemology of Mathematics

Apriority in Mathematics

Epistemology of Mathematics, Misc

Mathematics and the Causal Theory of Knowledge

Mathematical Intuition

Mathematical Proof

Godel's Theorem

Computer Proof

Probabilistic Proof

Undecidability

Mathematical Proof, Misc

Revisability in Mathematics

Mathematical Objects

Fictionalism

Indeterminacy

Nominalism

Platonism

Structuralism

Neo-Fregean Approaches

Indispensability Arguments

Numbers

The Nature of Sets*

Mathematical Truth

Analyticity in Mathematics

Axiomatic Truth

Objectivity Of Mathematics

Philosophy of Set Theory

The Nature of Sets

The Iterative Conception of Set

Ontology of Sets

Axioms of Set Theory

Axiomatic Truth*

The Axiom of Choice

The Axiom of Constructibility

The Axiom of Determinacy

The Axiom of Infinity

New Axioms

Independence Results

Cardinals and Ordinals

The Continuum Hypothesis

Large Cardinals

Set Theory as a Foundation

Russell's Paradox

Set Theory and Logicism

Set-Theoretic Constructions

Areas of Mathematics

Algebra

Analysis

Category Theory

Geometry

Logic*

Number Theory

Topology

Theories of Mathematics

Logicism

Formalism

Intuitionism and Constructivism

Predicativism

Mathematical Naturalism

Philosophy of Mathematics, Misc

Explanation in Mathematics

The Infinite

The Application of Mathematics

Logic in the M&E part of the taxonomy:

Metaphysics and Epistemology

Philosophy of Language

Specific Expressions

Conditionals

Truth-Conditional Accounts of Indicative Conditionals

Epistemic Accounts of Indicative Conditionals

Pragmatic Accounts of Indicative Conditionals

Indicative Conditionals and Conditional Probabilities

Indicative Conditionals, Misc

Counterfactuals and Possible Worlds

Subjunctive Conditionals, Misc

Conditionals, Misc

Truth and Vagueness

Theories of Truth

Coherence Theory of Truth

Correspondence Theory of Truth

Minimalism and Deflationism about Truth

Pragmatism about Truth

Tarskian Theories of Truth

Theories of Truth, Misc

Truth, Misc

Relativism about Truth

Truth Bearers

Truth and Justification

Truthmakers*

The Liar Paradox

Theories of Vagueness

Contextual Theories of Vagueness

Degree-Theoretic Theories of Vagueness

Epistemic Theories of Vagueness

Incoherentism about Vagueness

Nihilism about Vagueness

Many-Valued Logic

Supervaluationism

Theories of Vagueness, Misc

Vagueness, Misc

Higher-Order Vagueness

Vague Objects*

Vagueness in Ethics and the Law