80-618 Logic Mini I Instructor TBA TR 12:00PM-01:20PM DH 4303 6 units Computability, undecidability, and the incompleteness theorems 80-619 Logic Mini II Instructor: Jeremy Avigad TR 12:00PM-01:20PM DH 4303 6 units Special topics in logic and computability 21-700 Mathematical Logic II Instructor: Peter Andrews MWF 11:30am-12:20pm WEH 7201 12 Units 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 3:30 Wean Hall 8201 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 Wean Hall 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.12.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. 21-800 Advanced topics in logic: Large cardinals and infinite games Instructor: James Cummings MWF 2:30-3:20 Wean Hall 7201 12 Units Description: The study of infinite two-player games of perfect information is a central topic in modern set theory. The Axiom of Determinacy (AD) asserts that every game with payoff set a subset of the Baire space is determined, that is to say that one player has a winning strategy. The goal of this course is to give both directions in the proof of the following result: Theorem (Woodin): AD is equiconsistent with the existence of omega many Woodin cardinals. Background: Some experience with descriptive set theory, forcing and large cardinals is desirable but I will try make the course reasonably self-contained. 21-805 Lambda Calculus Instructor: Rick Statman MWF 1:30 Wean Hall 7201 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 TR 3:00-4:20 GHC 4102 12 units This lecture course introduces the foundational concepts and techniques of programming language semantics. The aim is to demonstrate the utility of a scientific approach, based on mathematics and logic, with applications to program analysis, language design, and compiler correctness. We focus on widely applicable frameworks for semantic description: denotational, operational, and axiomatic semantics. We use semantics to analyze program behavior, guide the development of correct programs, prove correctness of a compiler, validate logics for program correctness, and derive general laws of program equivalence. We discuss a variety of imperative and functional languages, sequential and parallel, as time permits. Requirements 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. The course is 12 units. Grading is based on homeworks and a (take-home) final exam. Students are encouraged to form study groups, but each student must do homework and exams individually. 15-816 Linear Logic Instructor: Frank Pfenning MW 12:00-1:20 GHC 4303 12 units Description: This graduate course provides an introduction to linear logic with an emphasis on its applications in computer science. This includes the theory of functional, logic, imperative, and concurrent programming languages. We will also develop a linear type theory which will serve as a meta-language in which the theory of programming languages with state can be formalized effectively. Textbook: Lecture notes will be handed out. Comment: This is an introductory course with no formal prerequisites, but an exposure to logic and type systems would be helpful. Enterprising undergraduate are welcome to attend this course. 15-817 Automated Theorem Proving: Coq, Vampire, Z3: Three Very Different Approaches Instructor: Edmund Clarke W 3:00-4:20pm GHC 4102 6 Units Description: Coq is a powerful proof assistant for higher-order logic, Vampire is the CADE champion resolution theorem prover, and Z3 is an SMT solver developed at Microsoft Research that uses efficient decision procedures. It is used for many practical applications, especially in program analysis. The primary goal of this course is to develop a working knowledge of Coq. We will cover Z3 and Vampire as time permits according to student interest. However each of these could take a full semester by itself. URL: http://www.cs.cmu.edu/~emc/15817-s12