CARNEGIE MELLON UNIVERSITY PROGRAM IN PURE AND APPLIED LOGIC LOGIC AND LOGIC-RELATED COURSES AND SEMINARS FOR FALL 2006 21-600 Mathematical Logic I Instructor: Peter Andrews MWF 11:30am-12:20pm HH B103 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. 21-603 Model Theory I Instructor: Rami Grossberg (rami@cmu.edu) MWF 1:30-2:20PM Porter Hall A21A 12 Units DESCRIPTION: Model theory is one of the four major branches of mathematical logic. There are many applications of model theory to algebra (e.g. field theory, algebraic geometry, number theory, and group theory), analysis (non-standard analysis, complex manifolds and the geometry of Banach spaces) and theoretical computer science (via finite model theory) as well as set theoretic topology and set theory. This course is the first in a sequence of three courses. The purpose of this compactness theorem, model completeness, elementary decideability results, Henkin's omitting types theorem, prime models. Elementary chains of models, some basic two-cardinal theorems, saturated models (characterization and existence), basic results on countable models including Ryll-Nardzewski's theorem. Indiscernible sequences, and connections with Ramsey theory, Ehrenfeucht- Mostowski models. Introduction to stability (including the equivalence of the order-property to instability), chain conditions in group theory corresponding to stability/superstablity/omega-stability, strongly minimal sets, various rank functions, primary models, and a proof of Morley's categoricity theorem. Basic facts about infinitary languages and abstract elementary classes, computation of Hanf-Morley numbers. PREREQUISITE: This is a graduate level course, while at the beginning the pace will be slow, the pace will speed up in the second half. In the past many of students where undergraduates, so the prerequisites are kept to the minimum of "an undergraduate-level" course in logic. Motivated undergraduate students are encouraged to contact the instructor. TEXT: Rami Grossberg, A course in model theory, a book in preparation. Most of the material (and more) appears in the following books: 1. C. C. Chang and H. J. Keisler, Model Theory, North-Holland 1990. 2. Bruno Poizat, A course in Model Theory, Springer-Verlag 2000. 3. S. Shelah, Classification Theory, North-Holland 1991. I will not use a text, but will provide access to my notes on a weekly basis. EVALUATION: Will be based on weekly homework assignments (20%), a 50 minutes midterm (20%) and a 3 hours in-class comprehensive final written examination (60%). COURSE WEBPAGE: www.math.cmu.edu/~rami/mt1.06.desc.html 21-702 Set Theory II INSTRUCTOR: Ernest Schimmerling MW 3:30-4:50 Porter Hall A20 TEXTBOOK: Kunen DESCRIPTION: The topic is forcing. Students planning to enroll are asked to describe their background in logic and set theory to the instructor as soon as possible by email to eschimme. 80-711 Proof Theory INSTRUCTOR: Jeremy Avigad TTh 10:30-11:50 Porter Hall A22 12 units DESCRIPTION: This is an introduction to proof theory. In the first part of the course, we will discuss formal systems of deduction for classical and intuitionistic logic, cut elimination, and applications (such Herbrand's theorem, interpolation theorems, and the elimination of Skolem functions). The second part of the course will focus on the metamathematics of first-order arithmetic, from proof- and model-theoretic perspectives. We will consider, for example, conservation results involving the collection axioms, and combinatorial independences like the Paris-Harrington theorem. TEXTBOOK OR REFERENCES: none required. I will circulate draft chapters of a textbook I am writing. Troelstra and van Dalen's *Basic Proof Theory* and Kaye's *Models of Peano Arithmetic* are good supplementary references. 21-804 Math Logic Seminar Instructor: Ernest Schimmerling Tuesday 12:00-1:20p.m. Wean Hall 5304 Description: See http://www.math.cmu.edu/users/eschimme/seminar.html 15-814 Type Systems for Programming Languages Instructor: Robert Harper Tue-Thu 1:30-2:50 5409 Wean Hall 12 Units Description: The course studies the theory of type systems, with a focus on applications of type systems to practical programming languages. The emphasis is on the mathematical foundations underlying type systems and operational semantics. The course includes a broad survey of the components that make up existing type systems, and also teaches the methodology behind the design of new type systems. For additional detailed information go to http://www.cs.cmu.edu/~rwh/courses/typesys 15-819K Logic Programming INSTRUCTOR: Frank Pfenning TuTh 10:30-11:50 Wean 4623 12 units DESCRIPTION: Logic programming is a paradigm where computation arises from proof search in a logic according to a fixed, predictable strategy. It thereby unifies logical specification and implementation in a way that is quite different from functional or imperative programming. This course provides a thorough, modern introduction to logic programming. It consists of a traditional lecture component and a project component. The lecture component introduces the basic concepts and techniques of logic programming followed by successive refinement towards more efficient implementations or extensions to richer logical concepts. We plan to cover a variety of logics and operational interpretations. The project component will be one or several projects related to logic programming. TEXTBOOK OR REFERENCES: Course notes will be handed out. COMMENT: Undergraduates welcome with 15-399 Constructive Logic or 15-312 Foundations of Programming Languages as prerequisite. 80-520/820 Categorical Logic INSTRUCTOR: Steve Awodey TR 3 - 4:20 BH 235B 9-12 units DESCRIPTION: This course focuses on applications of category theory in logic and computer science. A leading idea is functorial semantics, according to which a model of a logical theory is a set-valued functor on a category determined by the theory. This gives rise to a syntax-invariant notion of a theory and introduces many algebraic methods into logic, leading naturally to the universal and other general models that distinguish functorial from classical semantics. Such categorical models occur, for example, in denotational semantics. e.g. treating the lambda-calculus via the theory of Cartesian closed categories. Similarly, higher-order logic is treated categorically by the theory of topoi. PREREQUISITES: 80-413/713 Category Theory or equivalent WEBPAGE: http://www.andrew.cmu.edu/user/awodey/catlog/