CARNEGIE MELLON UNIVERSITY PROGRAM IN PURE AND APPLIED LOGIC LOGIC AND LOGIC-RELATED COURSES AND SEMINARS FOR FALL 2004 21-600 Mathematical Logic I Instructor: Peter Andrews MWF 11:30am-12:20pm Baker Hall A53 12 Units Description: The study of formal logical systems which model the reasoning of mathematics, scientific disciplines, and everyday discourse. Propositional calculus and first-order logic. Syntax, axiomatic treatment, derived rules of inference, proof techniques, computer-assisted formal proofs, normal forms, consistency, independence, semantics, soundness, completeness, the Lowenheim-Skolem Theorem, compactness, equality. 21-602 Set theory I INSTRUCTOR: Ernest Schimmerling TuTh 3:00-4:20 pm OSC 201 12 units DESCRIPTION: First semester graduate level set theory. The main topics are ZFC, infinitary combinatorics, relative consistency, constructibility, and descriptive set theory. TEXTBOOK: Kenneth Kunen, "Set Theory : An Introduction to Independence Proofs" COMMENT: Students should have a background in undergraduate level set theory (e.g., 21-229) and logic, which includes a working knowledge of basic ordinal and cardinal arithmetic, Gödel's completeness theorem, and the downward Löwenheim-Skolem theorem. An understanding of the statement (but not the proof) of Gödel's theorem on consistency proofs will also be assumed. Those without the required background should meet with the instructor as soon as possible to discuss their options, which may include doing some reading over the summer. Set Theory I is a prerequisite for Set Theory II (21-702), which will be taught by Professor Uri Abraham in Spring, 2005. 80-310/610 Logic and Computation Instructor: Jeremy Avigad TuTh 3:00-4:20 pm Hamerschlag Hall B103 12 units Description: Among the most significant developments in logic in the twentieth century is the formal analysis of the notions of provability and semantic consequence. For first-order logic, the two are related by the soundness and completeness theorems: a sentence is provable if and only if it is true in every interpretation. This course begins with a formal description of first-order logic, and proofs of the soundness and completeness theorems. Other topics may include: compactness, the Lowenheim-Skolem theorems, nonstandard models of arithmetic, definability, other logics, and automated deduction. Prerequisites: 80-210, 80-211, or equivalent background in first-order logic. 80-315/615 Modal Logic Instructor: Horacio Arlo-Costa Wed 1:30-3:50 pm Baker Hall 150 9-12 units. Description: An introduction to first-order modal logic. The course considers several modalities aside from the so-called alethic ones (necessity, possibility). Epistemic, temporal or deontic modalities are studied, as well as computationally motivated modals (like "after the computation terminates"). Several conceptual problems in formal ontology that motivated the field are reviewed, as well as more recent applications in computer science and linguistics. Kripke models are used throughout the course, but we also study recent Kripkean-style systematizations of the modals without using possible worlds. Special attention is devoted to Scott-Montague models of the socalled "classical" modalities. Prerequisites: 80-210, or 80-211, or instructor's permission. 1-703 Model theory II INSTRUCTOR: Rami Grossberg MWF 10:30 Baker Hall 231A 12 units DESCRIPTION: This is a second course in model theory. The main topic of discussion will be classification theory for non-elemntary classes. TEXTBOOK: No official text. DETAILS: I will concentrate in what is the deepest part of pure model theory. Namely non-first order theories. In a typical case we will deal with abstract elementary classes. An AEC is essentially a class K of models all of the same similarity type (or a category of sets) which is closed under direct limits and little more. The aim is to have an analysis of such general classes. Most of the material to be discussed appears in (badly written) papers only. I will start with minimal prerequisites, but will progress quickly to some of the research frontieers of the field. I will emphasize aspects of the theory that may eventually converge to a proof cases of Shelah's categoricity conjecture which is the prominent open problem in the field, it is a parallel to Morley's theorem for L ?1,?, most results will be about more general classes. The common to all these classes is that the compactness theorem fails badly. Hopefully some of the techniques will turn to be usefull also in the study of classes of finite models, but we will concentrate at uncountable models. There will be a more serious use of set theory than needed for model theory of first-order logic. PREREQUISITES: About half of a basic graduate course in set theory and parts of an elementary model theory (about 60-70% of 21-603 ) or permission of the instructor. 80-411/711 Proof Theory Instructor: Jeremy Avigad TuTh 10:30-11:50 am Baker Hall 231A 12 units Description: 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. 15-814 Type Systems for Programming Languages INSTRUCTOR: Robert Harper TuTh 1:30-2:50pm Wean Hall 5409 12 units. DESCRIPTION: This course is an introduction to the theory and practice of type systems for programming languages. Topics include typed lambda calculus, subtyping, polymorphism, data abstraction, recursive types, and objects. PREREQUISITE: Background equivalent to programming skills and programming language exposure afforded by a typical undergraduate Computer Science degree. TEXTBOOK: Benjamin Pierce "Types and Programming Languages" MIT Press 2002. COMMENT: This course satisfies the CS distribution requirement in programming languages. Enrollment is limited to CS PhD students or permission of the instructor.