Loading Events

« All Events

  • 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.

Details

Date:
February 25, 2021
Time:
10:00 am - 12:00 pm
Event Category:
Website:
https://cs.unibuc.ro/~lleustean/Seminar-Logic/seminar-logic.html