80-315,80-615 Modal Logic Instructor: Horacio Arlo-Costa TR 3:00-4:20pm SH 219 9 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 so-called 'classical' modalities. 80-618 Logic Mini I Instructor: Wilfried Sieg TR: 3:00-4:20 DH 4303 6 units Description: The course first provides a basic introduction to fundamental concepts of computability through Turing~Rs machines, Gödel~Rs equational calculus, and Kleene~Rs recursive functions. Using an equivalent approach via Post~Rs canonical systems, basic undecidability results are then established, in particular, the undecidability of first-order logic. Finally, Gödel~Rs Incompleteness Theorems are proved for subsystems of Zermelo~Rs set theory ~V in an ~Sabstract~T version that takes for granted representability and derivability conditions. The mathematical presentation is supplemented by historical and philosophical remarks. 80-619 Logic Mini II Instructor: Wilfried Sieg TR: 3:00-4:20 DH 4303 6 units Description: This is an advanced continuation of 80-618. In a first step, the Incompleteness Theorems are proved for elementary number theory; that requires the ~Sarithmetization~T of syntactic concepts and the coding of sequences within number theory. Then, Normal Form Theorems for intuitionist and classical first-order natural deduction systems are established and seen to be useful for automated proof search. Finally, Gentzen~Rs first consistency proof for elementary number theory is presented. Again, the mathematical discussion is supplemented by historical and philosophical remarks. 21-700 Mathematical Logic II Instructor: Peter Andrews MWF 11:30am-12:20pm WEH 5328 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: James Cummings MWF 3:30 Scaife Hall 212 12 Units Description: This course is a sequel to 21-602 Set Theory. The main goal is to prove Solovay's theorem that Con(ZFC + an inaccessible cardinal) implies Con(ZF + DC + every set of reals is Lebesgue measurable). Topics will include Borel codes, a rigorous development of forcing, forcing with complete Boolean algebras, the Levy collapse, relative constructibility, the theory of trees, and the basics of iterated forcing up to the consistency of Martin's Axiom. As time allows we may also cover some more advanced topics: possibilities include countable support iteration, more on forcing axioms, and an introduction to proper forcing. 21-703 Model Theory II Instructor: Rami Grossberg MWF 12:30 Wean 8201 12 units Purpose. This is a second course in model theory. This semester the course will be entirely dedicated to "Classification Theory for Abstract Elementary Classes (AECs)." Course description. The subject started 33 years ago by Shelah, the goal is to discover and introduce essentially category-theoretic concepts and tools sufficient for the development of model theory for various infinatry logics and ultimately to have a complete theory of invariants of models up to isomorphism in all cardinals, whenever this is possible and also establish the reason for nonexistence 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 categoricity theorem for Lw1,w. Despite the existence of about 1,500 pages of partial results the conjecture is still open. The analogue for classes of models of complete first-order theories is a highly developed theory called classification theory. In the last decade several very substantial applications of this theory to algebra, geometry and number theory were discovered. It is expected that eventually classification Theory for AECs will have a much greater impact. 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, this is in part due to the highly complex nature of the original papers that not only introduce many new model-theoretic tools but also required relatively sophisticated set-theoretic considerations. 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 transcendental number theory implying solutions to many difficult long standing problems, e.g. it implies that \pi + \e is a transcendental 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. Hopefully some of the techniques will turn to be useful also in the study of classes of finite models, but I will discuss uncountable models only. I will focus on the parts of the theory that in my opinion are most likely to lead to new significant results. Last year three important books on the field were published: (1) John T. Baldwin. Categoricity, AMS 2009 (235 pages), an online copy is available from the author's website. (2) Saharon Shelah. Classification Theory for Abstract Elementary Classes, College Publications 2009 (824 pages). (3) Saharon Shelah. Classification Theory for Abstract Elementary Classes Volume 2 , College Publications 2009 (694 pages). Textbook: A course in Model Theory III: Classification Theory for Abstract Elementary Classes, by Rami Grossberg. Available to students from my web page. Prerequisites: The contents of a basic graduate course in model theory like 21-603 or permission of the instructor. Evaluation: Weekly homework assignments (20%) 30%, Midterm 20% and an inclass 3 hour final 50%. Course web page: http://www.math.cmu.edu/~rami/mt2.11.desc.html Office: WEH 7204 Phone: x8482 (268-8482 from external lines), messages at x2545 Email: Rami@cmu.edu URL: www.math.cmu.edu/~rami Office Hours: By appointment. 80-711 Proof Theory Instructor: Jeremy Avigad TR 1:30-2:50pm BH 235A 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. TEXTBOOK OR REFERENCES: none required, but Troesltra and Schwichtenberg, *Basic Proof Theory*, is suggested 21-800 Advanced topics in Logic: large cardinals and inner models II Instructor: Ernest Schimmerling MW 1:30-2:50 Wean 7201 12 Units This is a continuation of 21-800 from Fall, 2010, on mice, core models, iteration trees, Woodin cardinals, and related topics as time allows. 15-817 Model Checking and Abstract Interpretation Instructor: Edmund Clarke Wednesday 3:00-4:20pm Gates-Hillman Center 4102 6 Units Description: Forthcoming 15-818A3 Introduction to Separation Logic Instructor: John Reynolds Units: 6 MWF 12:30 pm-1:20 pm or MW noon-1:20 pm* (first half of Spring 11 semester) Gates-Hillman Center 4303 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. * At the first meeting of the course (Monday, January 10, 12:30 pm), we will decide whether to meet two or three times a week. More details at www.cs.cmu.edu/~jcr 15-818A4 Current Research on Separation Logic Instructor: John Reynolds Units: 6 MWF 12:30 pm-1:20 pm or MW noon-1:20 pm* (second half of Spring 11 semester) Gates-Hillman Center 4303 Description: We will study and discuss recent papers on separation logic, grainless semantics, and related topics. * At the first meeting of the course (Monday, March 14, 12:30 pm), we will decide whether to meet two or three times a week. More details at www.cs.cmu.edu/~jcr 15-819N: Logical Analysis of Hybrid Systems Instructor: Andre Platzer MW 3:00-4:50 Place Wean 4623 12 Units Description: Hybrid systems are models for complex physical systems and have become a widely used concept for understanding their behaviour. Many applications are safety-critical, including car, railway, and air traffic control, robotics, physical-chemical process control, and biomedical devices. Hybrid systems analysis studies how we can build computerized controllers for physical systems which are guaranteed to meet their design goals. This course covers mathematical models for complex physical systems, including discrete dynamical systems, continuous dynamical systems, real-time dynamical systems, and hybrid dynamical systems (or hybrid systems for short). Our primary focus will be on the mathematical foundations and analytic techniques for these complex systems. We will study the questions that are important for designing system models and for understanding their behaviour. We will emphasize concise representations of analytic problems in logic and their algorithmic solutions in automated theorem provers and model checkers. 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 and for advanced undergraduates with an interest in mathematical, logical, or formal analysis methods. Objectives: You will develop an understanding for important safety-critical aspects of embedded and cyber-physical systems. You will be able to understand and develop discrete/continuous/hybrid dynamical system models. You will learn how you can analyze if a hybrid system works as intended and if it actually meets its design goals. You will learn how to use formal methods and calculi to analyze system correctness and you will understand how automatic verification techniques work. TEXTBOOK: André Platzer. Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, 2010. Course URL http://symbolaris.com/course/lahs.html