The course starts with a proof theoretic approach to propositional and predicate logic and their completeness, followed by basic recursion theory and it's formalization within formal arithmetic. From this point we can move from arithmetic to Gödel’s Incompleteness Theorem and Gentzen's proof of the consistency of arithmetic. At this point we will delve into basic type theory, Curry-Howard correspondence and it's connection to system T which provides an alternative consistency proof of arithmetic. Both of this Highlight the existence of functions beyond arithmetic of which we provide a few examples . We then discuss Second-order arithmetic, Strong type systems in correspondence with Second-order arithmetic (System F), and the relationship between subsystems of second-order arithmetic and mathematical analysis (Reverse Mathematics).
- Lecturer: David Cerna