80-611 Computability and Incompleteness INSTRUCTOR: Jeremy Avigad MW 3:00-4:20p.m. Margaret Morrison A14 Units: 12 DESCRIPTION: The 1930's witnessed two revolutionary developments in mathematical logic: first, Goedel'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, Goedel, 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. 21-700 Mathematical Logic II INSTRUCTOR: Peter Andrews MWF 11:30-12:30 Wean Hall 5320 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-702 Set Theory II INSTRUCTOR: Ernest Schimmerling MWF 2:30-3:20 Porter Hall A21A 12 Units DESCRIPTION: Second semester graduate level set theory. 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. The minimum background is most of 21-602 but not constructibility and descriptive set theory. Students who lack some of the required background should consult with the instructor in advance. 21-703 Model Theory II INSTRUCTOR: Rami Grossberg MWF 2:30-3:20 PH A19A 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 ocurse 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: 21-803 Math Logic Seminar INSTRUCTOR: James Cummings R 12-1:20 Doherty Hall 1217 DESCRIPTION: See http://logic.cmu.edu/seminar.html 21-805 Unification and Matching in Typed Lambda Calculus INSTRUCTOR: Rick Statman MWF 3:30-4:20 (this course will probably move to a TR time slot) Doherty Hall 2122 12 Units 15-812A Programming Language Semantics INSTRUCTOR: John C. Reynolds MW 1:30-2:50 Wean Hall 4615A 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 programing (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. PREREQUISITES: There are no specific prerequisites, but the course requires some background in programming languages and basic mathematics. To get a feel for what is needed look at Appendix A of the text and skim over the first couple of chapters. If these seem unduely difficult, meet with the instructor. TEXTBOOK: J. C. Reynolds, "Theories of Programming Languages", Cambridge University Press 1998. WEB PAGE: /afs/cs.cmu.edu/project/fox-19/member/jcr/www15812As2008/cs812-08.html 80-619 Computability and Learnability Instructor: Kevin Kelly TR 1:30-2:50 BH A53 Baker Hall A53 12 Units Description: This course is conceived as an alternative way to fulfill the 80-311, Computability and Incompleteness requirement for students who are more interested in rationality, learning, and scientific method than in logic and the foundations of mathematics. A solid grounding in the theory of computability will be provided, but the applications will concern computational learning theory, which studies what can be learned or discovered by computational agents from empirical data rather than what can be proved in a logical system. The application is more natural than it might seem at first. The problem of induction is that a general law may be refuted by the next observation, no matter how long it has withstood test. But there is a parallel problem about algorithmic halting: no matter how long a computation fails to halt, it may halt as soon as a world-be decision procedure concludes that it never will. In both cases, the difficulty can be sidestepped by entertaining methods that converge to the right answer without announcing when they have done so. We will delve into this analogy, using the theory of computability to investigate such questions as what machines can learn, whether machines could discover uncomputable truths, why irrational machines may be smarter, and what good it would do to have an infinite regress of methods, each of which checks whether its predecessor will find the truth. All topics covered are self-contained, but students are expected to have some basic background in logic, computation, or discrete mathematics. The text will consist of handout lecture notes. The course grade will be based on exercises and two short papers that will provide vital practice in writing articles for conference proceedings.