Shuangshuang Shu (University of Leeds)

Functional interpretations are generalisations of Goedel's Dialectica interpretation of Heyting arithmetic into a primitive-recursive functional system, which arose from a disbelief in universal quantifiers and integrated the ideas of functionals and proofs; the Dialectica interpretation shows the consistency of Heyting arithmetic (hence that of Peano arithmetic) with respect to that primitive-recursive functional system. We give an introduction to the idea of functional interpretations, and in the course, we will see how a seemingly innocuous inference rule called contraction (from A\vee A, deduce A) interferes with the interpretations.