80-819 Topics in Logic: Proof Theory
12 units, Carnegie Mellon University
The course is of interest to graduate and advanced undergraduate students in philosophy, computer science, and mathematics. We start out with a paradigmatic result, the cut elimination theorem for sequent calculi in firstorder intuitionist and classical logic. The questions, Why these logics, Why these calculi, lead to a discussion of proof theorys origins. Proof theory developed to analyze aspects of mathematical experience and methodological problems in the foundations of mathematics. These problems are traceable to the transformation of mathematics in the nineteenth century the emergence of abstract mathematics, its reliance on set theoretic notions, and its focus on logic in a broad sense. Attempting to mediate between foundational positions, Hilbert shifted issues, around 1900, from a mathematical to a vaguely conceived metamathematical level. That approach was realized in the 1920s taking advantage of the possibility of formalizing mathematics in formal systems and investigating them from a strictly constructive, finitist standpoint. Hilberts approach raised deep metamathematical questions from semantic completeness through mechanical decidability to syntactic incompleteness. The failure of his finitist consistency program only deepened the methodological questions. A broadened array of problems with only partial solutions has created a vibrant subject that spans computational, mathematical, and philosophical issues and joins them with a rich history. Here are the core issues 1. Hilberts consistency programs 1899 1931 Interlude Gdels theorems 2. Reductions of classical to constructive theories Interlude Formality according to Gdel, Post, and Turing 3. Interactive theorem proving or formal verification Interlude Some techniques based on resolution 4. Mathematical proofs as objects Interwoven Normal forms of natural deduction proofs
Prerequisites: none listed
Courseweave needs JavaScript to show sections, workloads and planning tools.