- This event has passed.
Formalizing Gödel’s System T in Lean
February 25, 2021 @ 10:00 am - 12:00 pm
Title: Formalizing Gödel’s System T in Lean
Speaker: Horațiu Cheval (University of Bucharest)
Abstract:
In 1958, Gödel introduced his functional interpretation as a method of reducing the consistency of first-order arithmetic to that of a quantifier-free system of primitive recursive functionals of higher type. His work has since enabled other advances in proof theory, notably the program of proof mining. We give a brief overview of Gödel’s System T and then explore a formalization thereof as a deep embedding in the Lean proof assistant.
References:
[1] mathlib Community, The Lean Mathematical Library, 2019.