80-411 Proof Theory

Units: 9-12 Department: Philosophy Prerequisites: 21-300 or 80-310 or 80-311 Cross-listed: 80-711 Related URLs: http://www.hss.cmu.edu/philosophy This course is an introduction to Hilbert-style proof theory, where the goal is to represent mathematical arguments using formal deductive systems, and study those systems in syntactic, constructive, computational, or otherwise explicit terms. In the first part of the course, we will study various types of deductive systems (axiomatic systems, natural deduction, and sequent calculi) for classical, intuitionistic, and minimal logic. We will prove Gentzen's cut-elimination theorem, and use it to prove various theorems about first-order logic, including Herbrand's theorem, the interpolation theorem, the conservativity of Skolem axioms, and the existence and disjunction properties for intuitionistic logic. In the second part of the course, we will use these tools to study formal systems of arithmetic, including primitive recursive arithmetic, Peano arithmetic, and subsystems of second-order arithmetic. In particular, we will try to understand how mathematics can be formalized in these theories, and what types of information can be extracted using metamathematical techniques.

Popularity index Rank for this semester: #0 Rank in this department: #0   Students also scheduled 36-225 Introduction to Probability and Sta... 82-221 Intermediate German I 15-411 Compiler Design 80-315 Modal Logic 80-251 Modern Philosophy 15-814 Type Systems for Programming Langua... 76-493 Historic Imagination in 19th Centur... 79-432 Historical Imagination in 19 Centur... 21-373 Algebraic Structures 15-815 Automated Theorem Proving

Spring 2005 times

No sections available for semester Spring 2005.