80-311/611 Computability and Incompleteness Instructor: Teddy Seidenfeld Tu/Thur 1:30 - 2:50 MM 103 9/12 Units Description: 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. Textbook: /Computable Functions, Logic, and the Foundations of Mathematics, /Epstein and Carnielli 21-700 Mathematical Logic II Instructor: Peter Andrews MWF 11:30am-12:20pm PH A18B 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. An approach to formalizing mathematics which uses only first-order logic is Axiomatic Set Theory, which involves adding the axioms of set theory to the purely logical axioms of first-order logic; it is the subject of a different course (21-602). 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. In the context of first-order logic, it is not always clear what makes a model "standard" or "nonstandard", but from the perspective of type theory this distinction is very clear. 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 this important distinction between standard and nonstandard models. It is shown that theories which have infinite models must have nonstandard models. Henkin's Completeness Theorem and the Weak Compactness Theorem are proved, but it is shown that the Strong Compactness conjecture is false. 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, now published by Springer, 2002, chapters 5-7. 21-702 Set Theory II INSTRUCTOR: Ernest Schimmerling MWF 2:30 PH A20A 12 Units DESCRIPTION: Second semester graduate level set theory following 21-602. Paul Cohen invented the forcing technique and used it to prove that if ZFC is consistent, then so are the theories ZFC + not(CH) and ZF + not(AC). Forcing is the central topic of the course. The mechanics of forcing and Cohen's theorem are the first goals, followed by additional applications of forcing in cardinal arithmetic, infinitary combinatorics, the theory of complete Boolean algebras and descriptive set theory. Topics covered in the last part of the course vary and may include Solovay's model in which all sets of reals are Lebesgue measurable, connections with large cardinals, iterated forcing and/or forcing axioms such as Martin's Axiom, the Proper Forcing Axiom and Martin's Maximum. 21-703 Model Theory II Instructor: Rami Grossberg MWF 12:30 Baker Hall 231A 12 Units Description: The subject started 30 years ago by Shelah, the goal is to discover the concepts and tools necessary for the development of model theory for infinatry logic and ultimately to have a complete theory of invariants of models up to isomorphism whenever this is possible and also establish the reason for inexistence of a theory of invariants. Shelah also proposed a conjecture as a test for the development of the theory: Shelah's categoricity conjecture, it is a parallel to Morley's categoriicty theorem for L_\omega_1,\omega. Despite the existence of about a thousand pages of partial results the conjecture is still open. Shelah in his list of open problems in model theory [Sh 702] writes: ``I see this [classification of Abstract Elementary Classes] as the major problem of model theory.'' Until 2001 virtually nobody besides Shelah published work on AECs. Interest and progress in the field by others materialized from two directions: Boris Zilber managed to construct a function over the complex numbers sharing many formal properties with exponentiation and as well satisfying Schanuel's conjecture over the complex numbers (this is a far reaching conjecture in transcendetal number theory implying solutions to many difficult long standing problems, e.g. it implies that \pi + \e is a transcendetal number). Zilber's construction uses a combination of methods from number theory with abstract model-theoretic concepts of Shelah. In parallel Grossberg and VanDieren introduced the notion of tameness and proved new cases of Shelah's categoricity conjecture. Both directions influenced many new people to enter the field. In the future, fast progress is expected in the pure theory as well as in applications to complicated mathematical structures like homological algebra and quantum groups. 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. I will focus on the basic parts of the theory that may eventually converge to a proof cases of Shelah's categoricity conjecture. I will start the course with some fundamental theorems concerning first-order theories (omitting types and computing Hanf-Morley numbers, characterizations of stability) as well with basic set-theoretic machinary manipulating models of weak set theories and the interplay between stationary sets of ordinals and elementary chains of models. Topics to be covered: Chang and Shelah's presentation theorems, Undefineability of well-ordering, Galois-types, Galois-stability and Galois-saturation. The role of the amalgamation property and its connections with the number of pairwise non-isomorphic models, the connection between properties of models of cardinality \lambda and \lambda^+. Evaluation: Weekly homework assignments (20%) 30%, Midterm 20% and an inclass 3 hour final 50%. Prerequisites: The contents of a basic graduate course in model theory like 21-603 or permission of the instructor. Textbook: A course in Model Theory III: Classification Theory for Abstract Elementary Classes, by Rami Grossberg. More details can be found on the course webpage at: 80-413/713 Category Theory Instructor: Steve Awodey TR 12:00 - 1:20PM DH 1117 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.A text will be provided. Prerequisites: one course in logic or algebra. 80-714 Topics in Logic and Mathematics: Modal Logic Instructor: Steve Awodey and Kohei Kishida M 3:30 - 6:20PM BH 150 12 units Description: A graduate-level seminar in modal logic. We'll cover some formal systems, Kripke and neighborhood semantics, and some related philosophical topics. Text: Hughes and Cresswell, A New Introduction to Modal Logic Prerequisites: Students should have some background in logic through completeness for predicate logic. NOTE: This course will incorporate a 3 week visit by Dana Scott in late March. All are welcome to attend. 21-800 Advanced topics in logic: combinatorial set theory Instructor: James Cummings MWF 1:30 BH 231B 12 units Description: The main goal of the course is to prove the remarkable theorem of Shelah that if $\aleph_\omega$ is strong limit then $2^{\aleph_\omega} < \aleph_{\omega_4}$. Along the way we'll develop many of the important tools of combinatorial set theory: topics to be covered include Elementary substructures and internally approaching chains Club guessing The ideal $I[\lambda]$ Applications of infinite games Reduced products and their cofinalities (PCF theory) If time allows we may also cover some more advanced topics: possibilities include sigma-closed PCF, Jonsson algebras, and the various PCF conjectures. Prerequisites: Set theory I or an equivalent course. No knowledge of forcing, large cardinals or constructibility will be presumed. 21-805 Lambda Calculus Instructor: Rick Statman MWF 3:30 DH 2122 12 units 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. @ Topics covered include (1)Basic properties of reduction and conversion (2)Reduction and conversion strategies (3)Calculability and representation of data types (4)Theory of Ershov numberings (5)Bohm's theorem, easy terms, and other exotic combinations (6)Solvability of functional equations (unification) (7)Combinators and bases (8)Simple and algebraic types (9)Labelled reduction and intersection types (10)Extensionality and the omega rule @ 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: Enrolled students can work together in teams to produce lecture notes due at the end of the semester. There are no other requirements 15-812 Semantics of Programming Languages Instructor: Stephen Brookes MW 10:30am-11:50am NSH 1305 12 units Description: This course introduces the foundational concepts and techniques of programming language semantics. The aim is to demonstrate the utility of a scientific approach in answering questions about program correctness, the pro's and con's of various programming languages, compiler correctness, and other practical issues. We focus on two of the most widely used and most successful frameworks for semantic description: denotational semantics and operational semantics. We use semantically based techniques to prove properties of a language, to analyze programs, to guide the development of correct programs, to prove correctness of compiler optimizations, to validate logics for specifying and proving program correctness, and to obtain general laws of program equivalence. REFERENCES: A full set of lecture notes will be handed out during the course. The following texts are suggested for background reading: Reynolds, Theories of Programming Languages, Cambridge University Press, ISBN 0-521-59414-6. Winskel, The Formal Semantics of Programming Languages: An Introduction, MIT Press, ISBN 0-262-23169-7. COMMENTS: This is a starred course for CS graduate students and may be used to fulfill part of the course requirements in the CS Ph.D. program. Graduate students in other departments, and advanced undergraduates, can take the course with permission of the instructor. Grading will be based on homeworks and exams. Homework will involve written work. Students are encouraged to form study groups, but each student must do the homeworks and exams individually. 15-818A3 Introduction to Separation Logic Instructor: John Reynolds Units: 6 MW noon-1:20 pm (first half of Spring 09 semester) Wean Hall 4623 Description: Separation logic, first developed by O'Hearn and Reynolds, is an extension of Hoare logic originally intended for reasoning about programs that use shared mutable data structures. It is based on the concept of separating conjunction, which permits the concise expression of aliasing constraints. More generally, the logic provides a "frame rule", which enables local reasoning that is the key to the scalability of proofs. Examples of nontrivial proofs include the Schorr-Waite marking algorithm and the Cheney relocating garbage collector. Recently, by generalizing the concept of storage access to ownership and permissions, the logic has been extended to encompass information hiding, shared-variable concurrency, and numerical permissions. We will survey the current development of separation logic, including, as time permits, extensions to unrestricted address arithmetic, dynamically allocated arrays, recursive procedures, shared-variable concurrency, and read-only sharing. More details at www.cs.cmu.edu/~jcr 15-818A4 Current Research on Separation Logic Instructor: John Reynolds Units: 6 MW noon-1:20 pm (second half of Spring 09 semester) Wean Hall 4623 Description: We will study and discuss recent papers on separation logic, grainless semantics, and related topics. More details at www.cs.cmu.edu/~jcr 15-819 Hybrid Systems Analysis and Theorem Proving INSTRUCTOR: Andre Platzer TR 3:00-4:20 12 UNITS Wean 4615A DESCRIPTION: Hybrid systems analysis studies the question "how can we build computerized controllers for physical systems that are guaranteed to meet their design goals?" Application areas include safety-critical systems like adaptive cruise control technology for cars or auto pilots for aircraft collision avoidance. This course covers symbolic analysis techniques for safety-critical hybrid systems design. It will emphasize concise representations of analytic problems in logic and their algorithmic solutions in automated theorem provers and model checkers. It will also indicate elegant connections between the theory, practice and applications of hybrid systems analysis. More generally, the course provides a thorough introduction to logic and automated theorem proving techniques with their extensions to the logic-based analysis of hybrid systems. Starting from basic propositional logic, the class will develop the background in automatic proving and system analysis, including ground and free variable tableau procedures for first-order logic. It will cover extensions to dedicated verification logics for hybrid systems and their verification procedures. The class will provide you with modern techniques for analyzing the correct functioning of important safety-critical systems ranging from embedded systems in cars and biomedical devices, over chemical/physical process control and chip design, to full car, aircraft, and train control. The opportunity to gain practical experience in analysis of cyber-physical systems will be given as part of the course. The class should be appropriate for graduate students in all areas and for advanced undergraduates with a basic interest in mathematical, logical, or formal analysis methods. PREREQUISITES: Basic knowledge in logic (e.g., propositional logic) and calculus is of advantage but not strictly required. TEXT: Basic notes and background material will be handed out. EVALUATION: Grading will be based on a set of homework assignments, including hands-on analysis experience, midterm exam, and a final project. TOPICS TO BE COVERED: Safety-critical Hybrid Systems, Numerical Analysis versus Symbolic Verification, Propositional Logic, Propositional Tableau Procedures, First-order Logic, First-order Tableau Procedures, Dynamic Logic Programs and Dynamical Systems, Hybrid Dynamical Systems & Hybrid Programs, Aircraft, Train, and Car Control, Dynamic Verification Calculi, Decision Procedures, Theorem Proving Modulo, Differential Equations, Differential Variance and Invariance, Disturbances in Hybrid Systems Control, Time permitting: Proof Theory of Hybrid Systems, Fixedpoint Model Checking Engines, Automatic Verification COURSE WEBPAGE: http://www.symbolaris.com/course/15-819.html