80-711 Proof Theory

Units: 9-12 Department: Philosophy Cross-listed: 80-411 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. A solid understanding of the syntax and semantics of first-order logic, as obtained from courses like 80-310/610 or 21-300/600, is required. A course covering issues topics like primitive recursion and coding, like 80-311/611 or 21-700, would be helpful, but is not essential. .

Popularity index Rank for this semester: #0 Rank in this department: #0   Students also scheduled 21-804 Mathematical Logic Seminar 21-703 Model Theory II 21-602 Introduction to Set Theory I 69-160 Swim-Fit 62-323 The sink has dripped dry: A Sound A... 39-800 Preparing for a Faculty Career 98-043 Student Taught Courses (StuCo): Che... 06-423 Unit Operations Laboratory 06-422 Chemical Reaction Engineering 06-421 Chemical Process Systems Design

Spring 2005 times

No sections available for semester Spring 2005.