Alice Stina Emilia Brolin: Extracting Computational Content From Proofs

Abstract: Kurt Gödel developed a translation, called the Dialectica translation, from Heyting Arithmetic into a type system called T. This type system can be described by a lambda calculus. I present Gödel’s translation and then, to get a sense of how it functions in practice, I apply it to two theorems in Heyting Arithmetic. The first theorem is about ≤ being a total order on the natural numbers. When I apply the Dialectica translation I get lambda terms for subtraction and for the characteristic function of ≤. The second theorem is about there being arbitrarily large prime numbers. This gives me under the translation a lambda term for a function that from any natural number can produce a prime number bigger than that number. I also implement these lambda terms as functions in the programming language Haskell.