Dialectica Logical Principles

 

 `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' says Thomas Strahm in his introduction to the special volume of Dialectica dedicated to 50 years of the original paper. Shame that despite being more than ten years old (2008) the articles are not open access, so you can read about them in Richard Zach's blog post, but you'll have to find the articles themselves in the authors' pages or somewhere else.

`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.'

So far, so good. The mathematicians interested in foundations ought to be happy. I am. Especially because Davide Trotta (above) spoke  last Thursday in the Ottawa Category Theory Seminar about our second paper together with Matteo Spadetto. This is "Dialectica Logical Principles" which explains how our categorical modelling of Gödel’s dialectica interpretation also models the principles of Independence of Premise (IP) and Markov's Principle (MP), just like the dialectica does. This is not surprising, but it underscores how faithful the modelling is, a big win for categorical logic. Just like our previous paper,  The Gödel Fibration, which is nice because it puts some more explicit steps in the connections between the categorical modelling and the logical system modelled: see the case of quantifier-free objects discussed here.

But 'mathematicians interested in foundations' is a very small demographic. What can we say to others? What about the mythical "person-on-the street"? Have been thinking a lot about it. Recently google Scholar sent me news about Modal Functional (“Dialectica”) Interpretation (by HERNEST AND TRIFONOV. Maybe this will help.