Topics in Logic: Proof Theory

Catalog description

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 first-order intuitionist and classical logic. The questions, Why these logics?, Why these calculi?, lead to a discussion of proof theory's 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. Hilbert's 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. Hilbert's consistency programs (1899 - 1931) Interlude: G and #246;del's theorems 2. Reductions of "classical" to "constructive" theories Interlude: Formality according to G and #246;del, 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…