CARNEGIE MELLON UNIVERSITY PROGRAM IN PURE AND APPLIED LOGIC LOGIC AND LOGIC-RELATED COURSES AND SEMINARS FOR SPRING 2006 80-602 Journal Seminar Monday 4:30 - 6:50 BH 150 Topic: Modal Logic Instructor: Awodey This graduate seminar is intended provide students with an opportunity to discuss topics of current interest with faculty guests in a relaxed setting. Dinner is provided! This semester we will focus on the history and philosophy of modal logic, with readings by Carnap, Kripke, Quine, and others. Faculty guests will include Tom Ricketts, Horacio Arlo-Costa, Dana Scott, and Johan van Bentham. 80-611 Computability and Incompleteness Instructor: Jeremy Avigad TR 12:00-1:20 BH 136A 12 units The 1930's witnessed two revolutionary developments in mathematical logic: first, Gödel's famous incompleteness theorems, which demonstrate the limitations of formal mathematical reasoning, and second, the formal analysis of the notion of computation in the work of Turing, Gödel, Herbrand, Church, Post, Kleene, and others, together with Turing's results on the limits of computation. This course will cover these developments, and related results in logic and the theory of computability. Prerequisites: 80-210 or 80-211, or an equivalent course in Mathematics or Computer Science. 12 units 80-612 Philosophy of Mathematics INSTRUCTOR: Wilfried Sieg TR 1:30-2:50 PH 225B 12 units DESCRIPTION: The 20th century witnessed remarkable developments in mathematics - rooted in the radical transformation of the subject during the 19th century. An analysis of this transformation is at the center of the course, as it led to significant foundational problems and provoked a variety of well-known programmatic responses: logicism, intuitionism, and finitism. To gain a deeper understanding of fundamental issues, the course starts out by discussing mathematical background (going back to Greek mathematics, in particular,to Eudoxos' theory of proportion). The second and third part survey systematic foundational work that has been pursued throughout the 20th century. We will discuss in detail set-theoretic and constructive approaches; that is complemented by an analysis of meta-mathematical studies initiated by Hilbert and pursued by Gödel, Church, Turing and many others. Against this background, the final part makes explicit important aspects of mathematical experience; they find their articulation in the framework of reductive structuralism deeply influenced by the philosophical considerations of Paul Bernays. PREREQUISITES: Some familiarity with logic and basic notions of modern mathematics (as provided, for example, by 80-210, 80-211 or 80-212, or 21-127) 21-700 Mathematical Logic II Instructor: Peter Andrews MWF 11:30-12:20 CFA 212 12 units DESCRIPTION: This course is open to, and suitable for, students who have had an introductory logic course such as 21-300 Basic Logic, 21-600 Mathematical Logic I, or 80-310 Logic and Computation. After one has learned the basics of logic from such a course, it is natural to consider formal systems in which one can formalize mathematics and other disciplines. This requires the ability to quantify over variables for predicates, sets and functions as well as individuals; indeed, one needs to be able to discuss sets of sets, sets of sets of sets, etc., as well as functions whose arguments and values can be functions and sets of various types. Such a system, called type theory, was developed by the eminent philosopher Bertrand Russell, who used it as the logical basis for the great three-volume work Principia Mathematica (written jointly with Alfred North Whitehead), which provided substantial support for Russell's then novel thesis that all of mathematics is a branch of logic. 21-700 provides an introduction to a version of type theory due to Alonzo Church which contains lambda-notation for functions; it is both an enhancement and a simplification of Russell's type theory. Type theory is also known as higher-order logic, since it incorporates not only first-order logic, but also second-order logic, third-order logic, etc. The notation of this version of type theory is actually very close to that of traditional mathematics, and it has been found to be a good language for use in automated theorem proving systems which prove theorems of mathematics involving sets and functions. Another important application of type theory is in the formal specification and verification of hardware and software systems. Familiarity with Church's type theory provides fundamental background for the study of denotational semantics for functional programming languages. 21-700 starts with a general treatment of the syntax and semantics of type theory. Students use the computer program ETPS (Educational Theorem Proving System) as an aid in constructing certain formal proofs. Skolem's paradox about countable models for formalizations of set theory in which one can prove the existence of uncountable sets is resolved with the aid of the important distinction between standard and nonstandard models. It is shown that theories which have infinite models must have nonstandard models. Henkin's Completeness Theorem is proved. Attention then turns to showing how certain fundamental concepts of mathematics can be formalized in type theory. It is shown how cardinal numbers and the set of natural numbers can be defined, and Peano's Postulates are derived from an Axiom of Infinity. It is shown how recursive functions can be represented very elegantly in type theory. The last part of the course concerns the fundamental limitations of any system in which mathematics can be formalized. The famous incompleteness, undecidability and undefinability results of Godel and Tarski are presented, along with Lob's Theorem about the sentence which says "I am provable". The rich notation of type theory makes it possible to present very elegant proofs of these deep theorems. TEXT: Peter B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Second Edition, Kluwer Academic Publishers, 2002, chapters 5-7. 21-703 Model Theory II Instructor: Rami Grossberg MWF 1:30 -2:20PM PH A19A 12 units PURPOSE. This is a second course in model theory. The main topic of discussion will be what is widely recognized as pure model theory, namely "classification theory", with a special emphasis on the forking relation and its basic properties. COURSE DESCRIPTION: The material to be covered: Shelah's "Forking calculus" will be developed it its outmost generality in the context of simple theories (which is a generalization of stability). The fundamental properties of stable, superstable and simple unstable theories will be developed. The machinery will be used to solve several model-theoretic problems. Including stability spectrum theorem, uniqueness of prime models and various characterizations. PREREQUISITES: An introduction to model theory, like 21-603. Text: Rami Grossberg, A course in model theory, a book in preparation. Most of the material (and much more) appears in the following books: * John T. Baldwin. Fundamentals of Stability Theory. Springer-Verlag, Berlin, 1988. * Steve Buechler. Essential Stability Theory. Springer-Verlag, Berlin, 1996. * Bruno Poizat, A course in Model Theory, Springer-Verlag 2000. * Saharon Shelah, Classification Theory North-Holland 1991. Evaluation: Will be based on homework assignments (20%), a 50 minutes midterm (20%) and a 3 hours in class comprehensive final written examination (60%). 80-413/713 Category Theory INSTRUCTOR: Steve Awodey Tuesday, Thursday 3 - 4:20 Baker Hall 235B 9-12 units DESCRIPTION: Category theory, a branch of abstract algebra, has found many applications in mathematics, logic, and computer science. Like such fields as elementary logic and set theory, category theory provides a basic conceptual apparatus and a collection of formal methods useful for addressing certain kinds of commonly occurring formal and informal problems, particularly those involving structural and functional considerations. This course is intended to acquaint students with these methods, and also to encourage them to reflect on the interrelations between category theory and the other basic formal disciplines. TOPICS: Elementary theory of categories Functors Natural transformations Functor categories Yoneda's lemma Limits Universality Adjointness Cartesian closed categories Monads and their algebras Categorical logic TEXTBOOK: A draft textbook will be provided. PREREQUSITES: one course in logic or algebra 21-805 Lambda Calculus (Preliminary Announcement) Instructor: Rick Statman with possible guest lecturers Henk Barendregt, Dana Scott Where and when: TBA, MWF 3:30 (we hope to go only twice a week for 90 minutes - say MW 3:30-5pm - this will be decided by students schedules) Textbook: The Lambda Calculus by Henk Barendregt North Holland 1981, ISBN 0 444 85490 8 (2nd edition & paperback editions OK) Description: @ Although an introductory graduate course the only prerequisite for this course is an undergraduate course in logic and computability theory. @ We intend to include an extensive introduction to recursion theory as a preliminary to the theory of Ershov numberings and their application to lambda calculus @ The course will include material on the typed case not normally included in 21-805. Toward this end certain material on lambda theories will be excluded. @ Topics covered include (1)Basic properties of reduction and conversion (2)Reduction and conversion strategies (3)Calculability and representation of data types (4)Turing machines,other models,and Church's thesis (5)Recursive functions and relations (6)Enumeration,universal machines,and the recursion theorem (7)Theory of Ershov numberings (8)Bohm's theorem, easy terms, and other exotic combinations (9)Solvability of functional equations (unification) (10)Combinators and bases (11)Simple and algebraic types (12)Labelled reduction and intersection types @ Each of these topics includes several beautiful research problems.These range in difficulty from ones suitable for senior thesese to ones suitable for PhD dissertations. Students are free to pursue whichever problems appeal to them. Requirements: A good supply of homework exercises will be given out and those returned will be graded. I regard these exercises as optional but if at some stage a student wants me to say something good about him or her then I need to have some basis for my remarks. 15-812 Semantics of Programming Languages Instructor: John C. Reynolds TR 1:30-2:50 Wean 5409 12 Units DESCRIPTION: We survey the theory behind the design, description, and implementation of programming languages, and of methods for specifying and verifying program behavior. Both imperative and functional programming languages are covered, as well as ways of integrating these paradigms into more general languages. Coverage will include: - program specification and proof (including Hoare logic, weakest preconditions, and separation logic) - concurrent programming (including shared-variable and message-passing approaches) - functional programming (including continuations and lazy evaluation) - type systems (including subtyping, polymorphism, and modularization) In exploring these topics, we will use a variety of fundamental concepts and techniques, such as compositional semantics, binding structure, domains, transition systems, and inference rules. Textbook: J.C. Reynolds, Theories of Programming Languages, Cambridge University Press. 15-819-I Advanced Topics in Programming Language Semantics Instructor: Stephen Brookes MW 12:00-1:20 Wean 4623 12 units Description: This course will discuss recent developments in logic and semantics, with emphasis on the development and validation of concurrent programs. The topics will be drawn from a variety of recent papers, by the lecturer and by others, and will include: trace models for shared-memory programs and for networks of communicating processes, grainless semantics, concurrent separation logic and permission-accounting logics, and proofs of correctness for various protocols. We will identify challenges for future research and explore the potential of promising new approaches. We assume familiarity with basic concepts and techniques of programming language semantics, as seen for example in the CS Programming Languages starred course (15-812). The course is designed for graduate students in Computer Science, Mathematics, or Philosophy, with adequate background in logic and mathematics. Undergraduates with sufficient preparation may obtain permission from the instructor. CS 810 Seminar in Programming Languages: Model Checking Instructor: Edmund M. Clarke Fridays 12:00pm – 1:20pm Wean Hall 4623 This course will focus on fast propositional satisfiability solvers and practical decision procedures (Presburger arithmetic, the theory of the reals with and without multiplication, the theory of lists and arrays, etc.) and their application to model checking, automated theorem proving, program verification, and program analysis. The course will be self-contained although some knowledge of propositional and predicate logic will be helpful. In particular, no previous knowledge of model checking will be required. Students will be expected to give a lecture or do a course project. Specific topics to be covered will include: Overview and Background Decision Procedures for Propositional Logic Theorem Proving Techniques for First-Order Logic Decision Procedures for Equality Decidable Fragments of First Order Logic Presburger Arithmetic Algebraically Closed Fields Gröbner Bases Real Closed Fields Combining Decision Procedures Class starts meeting on January 20th