Metamathematics and Proof Theory
Advanced level course, 7.5 hp, Spring 2015.
Time: Thu 2015-01-22 10.15 - 12.00
Location: Room 306, building 6, Kräftriket, Department of mathematics, Stockholm university
Participating: Erik Palmgren, Stockholm university
Metamathematics is usually defined as the study of mathematics itself with mathematical methods. It includes the fundamental question of (relative) consistency of mathematical theories and how it may be resolved by investigating the structure of formal proofs. This theory of proofs has also many applications in automated theorem proving and complexity theory.
Contents
Background: Hilbert's Programme. Structural proof theory for sequent calculus, natural deduction and type theory. Cut elimination and normalisation. Incompleteness theorems and combinatorial results. Consistency proof for arithmetic. Ordinal analysis of theories. Arithmetical theories capturing complexity classes.
Course literature
A.S. Troelstra and H. Schwichtenberg, Basic Proof Theory, second edition. Cambridge University Press 2000.
S. Negri and J. von Plato, Structural Proof Theory, Cambridge University Press 2001.
Supplementary material on incompleteness, type theory and ordinal analysis.
Reference literature
S.C. Kleene, Introduction to Metamathematics, Van Nostrand 1952.
H. Schwichtenberg and S.S. Wainer, Proofs and Computations, Cambridge University Press 2011.
Schedule
Lectures on Thursdays 10:15-12:00 starting January 22 and ending in May. Venue: Room 306, Building 6, Kräftriket.