21-600 Mathematical Logic I Instructor: Peter Andrews MWF 11:30am-12:20pm HH B131 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 and Downward Lowenheim-Skolem Theorems, compactness. TEXTBOOK: Peter B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Second Edition, Kluwer Academic Publishers, now published by Springer, 2002. 21-602 Intro to Set Theory Instructor: Ernest Schimmerling MWF 3:30 WEH 7201 12 Units Description: See http://www.math.cmu.edu/graduate/graduatecourses/21602.htm 21-603 Model Theory I Instructor: Rami Grossberg (rami@cmu.edu) MWF 1:30 WEH 7201 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. The purpose of this course to introduce the student to some of the most important ideas of the field with a special attention to "classification theory" which is the most important subfield of modern model theory. The main focus of the course is Morely's categoricity theorem, the related conceptual infrastructure and extensions. Topics will include: compactness theorem, model completeness, elementary decideability results, cardinal transfer theorems, Henkin's omitting types theorem, prime models. Elementary chains of models, some basic two-cardinal theorems, saturated models (characterization and existence), special models, the monster model, 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 students where undergraduates, so the prerequisites are kept to the minimum of "an undergraduate-level" course in logic. Motivated undergraduate students are encouraged to take this course. 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.11.desc.html 80-310/610 Logic & Computation Instructor: Steve Awodey TR 10:30 - 11:50pm PH A18B 12 Units Description: Among the most significant developments in modern logic is the formal analysis of the notions of provability and logical consequence for the logic of relations and quantification, known as first-order logic. These notions are related by the soundness and completeness theorems: a logical formula is provable if and only if it is true under every interpretation. This course provides a formal specification of the syntax and semantics of first-order logic and then proves the soundness and completeness theorems. Other topics may include: basic model theory, intuitionistic, modal, and higher-order logics. Text Book: van Dalen, Logic and Structure. Prerequisites: 15251 or 80210 or 80211 or 80212 80-612 Philosophy of Mathematics Instructor: Wilfried Sieg W 12:00 - 2:50 BH 150 12 units Description: The 20th century witnessed remarkable and novel developments of mathematics - with deep roots in the 19th century. The beginnings of these developments were beset with foundational problems and provoked a variety of programmatic responses: logicism, intuitionism, and finitism. For a deeper study of basic issues, we review a part of classical Greek mathematics (the theory of proportions) that is closely connected to the foundations of analysis in the 19th century. We analyze set theoretic and constructive approaches, and discuss fundamental metamathematical results and their philosophical implications. A "reductive structuralist" position will finally provide a perspective for understanding the abstract character of mathematics as well as its usefulness in applications. 80-514/814 Categorical Logic Seminar Instructor: Steve Awodey M 12 - 2:50pm BH 150 12 Units Description: Topics in category-theoretic logic including: Lawvere duality, regular and coherent categories, topos theory, constructive type theory. Intended for students who have already taken Category Theory 80-413/713 or equivalent. Course notes will be provided. 15-814 Types and Programming Languages Instructor: Robert Harper TR 10:30-11:50 GHC 4102 12 Units Description: This is an introductory course on the foundations of programming languages. The central organizing principle of language design is the identification of language features with types. The theory of programming languages, therefore, reduces to the theory of types. Type theory is a comprehensive foundational theory of computation. Type theory has its origins in proof theory (the theory of human reason) and is closely related to category theory (the general theory of mathematical structures). The tripartite relationship between type theory, proof theory, and category theory is fundamental to the study of programming languages. We will place special emphasis on the propositions-as-types correspondence, in which programs of a type are identified with proofs of the corresponding proposition. (Similar correspondences hold between type theory and category theory (types are objects, programs are maps) and between category theory and proof theory (propositions are objects, proofs are maps), but we shall not consider these in this course.) Also see http://www.cs.cmu.edu/~rwh/courses/typesys