CARNEGIE MELLON UNIVERSITY PROGRAM IN PURE AND APPLIED LOGIC LOGIC AND LOGIC-RELATED COURSES AND SEMINARS FOR SPRING 2005 80-311/611 Computability and Incompleteness Instructor: Jeremy Avigad TR 10:30-11:50 PH 100 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: 15151 or 15399 or 21228 or 21300 or 80210 or 80211 or 80310 or 80317 80-617/80-317/15-399 Instructor: Robert Harper TR 12:00-1:20 WEH 5409AB 12 Units The web page is http://www.cs.cmu.edu/~rwh/courses/logic/www 80-318/618 Computability and Proof Search INSTRUCTOR: Wilfried Sieg Wednesdays 1:30 - 3:50 CFA 102 9-12 units DESCRIPTION: The broad informal question is: Can one "mechanize" significant parts of mathematical reasoning? We carry out case studies for Gödel's incompleteness theorems and an elementary part of set theory. That requires extensive preparatory work in Parts 1 and 2 of the course. The notion of computation (or mechanical procedure) used in mathematical logic and computer science was introduced in the mid-1930s in a variety of different, but equivalent formulations. We survey in PART 1 problems that led to the search for a rigorous notion of computation and give a novel axiomatic analysis (based on work by Turing, Post and Gandy). That provides an appropriate conceptual framework for "mechanization." The decision problem is one of the problems that was solved, negatively, using such a rigorous notion of computation. The theorem of Church and Turing asserts that there is no mechanical procedure deciding whether or not a sentence in the language of first-order logic is a logical truth. However, Gödel's completeness theorem guarantees that any logical truth can be proved - in suitable calculi. A variety of procedures have been developed to search systematically for proofs; PART 2 investigates "proof search procedures" for natural deduction calculi. The strategic considerations underlying a particular procedure, implemented in the AProS algorithm, are extended in PART 3 by general heuristics for establishing mathematical theorems. With this background, we are going to investigate, whether the proofs of Gödel's incompleteness theorems can be found mechanically. At an "abstract level" - taking as axioms the crucial representability and derivability conditions - the theorems can be established "by machine." The next step requires the use of techniques for inductive argumentation and the development of some elementary set theory. TEXTBOOK OR REFERENCES: We will use a variety of classical and contemporary papers, but also parts of books: for Part 1, papers by Gödel, Church, Turing, Post, and Gandy; for Part 2, parts of books by Prawitz and Troelstra & Schwichtenberg, papers by Dyckhoff and Sieg & Byrnes; for Part 3, documentation of the AProS algorithm and papers by Bundy and Hutter. COMMENT: Students are expected to be familiar with (the metamathematics of) first-order logic and a standard system of natural deduction. There is no programming prerequisite, but for students with such experience there will be challenging projects. 80-619 Computability and Learnibility INSTRUCTOR: Kevin T. Kelly MW 10:30-11:50 BH 150 12 units Description: Computation seems very different from learning. The former operates by rules and is guaranteed to find the right answer, whereas inductive generalization is risky because the available information does not determine which answer is right. But that is true only if the computational problem is solvable. Unsolvable formal problems are much more like empirical problems. For example, a computer can't tell for sure if another computation will halt because it can only "see" a finite chunk of that computation by a given time, just as an empirical scientist can only see a finite chunk of experience by a given time. According to this analogy, it is possible to study the solvability of scientific problems the way computer scientists analyze the solvability of formal problems. The subject that results is called computational learning theory. We will answer some of the following questions. Can we describe what it is about a learning problem that makes it solvable in a given sense? (Yes). Is guessing the next datum easier than discovering a hypothesis that predicts all the data? (No). Can we determine from input-output behavior alone whether we are computers? (Only if we aren't). Can we determine whether a theory is true even if the theory has horribly uncomputable predictions? (Yes--- try to guess how). How does Ockham's razor help us find the truth when the truth might be complex? Does too much rationality make computers stupid? (Yes). Recently, computer scientists have developed an approach to learnability called the PAC (probably approximately correct) paradigm. The idea is that a scientific method should probably get close to the right answer in polynomial time. This theory has been applied to practical machine learning questions like the time required to train neural networks. The class will involve an ongoing interplay between computability and ideas drawn from the philosophy of science. Prerequisite: 80-310 or approval of instructor. The grade will be based on exercise sets. Requirements Participation Assigned exercises (75%): To be turned in typed. Final project prospectus (counts as one exercise) Final project due last day of class (35%). To be turned in typed. Some interesting exercises of your own choice. A historical essay about the development of some aspect of the subject. A systematic investigation of some question. A detailed application. Topics 1. Primitive recursion. 2. Indexing and diagonalization. 3. Minimization, partial recursive functions, universal machine, s-m-n theorem. 4. Church-Turing thesis and acceptable numberings. 5. The Kleene recursion thoerem. 6. Reducibility 7. Halting Problem and Skepticism. 8. Rice's theorem and the Rice-Shapiro theorem. 9. Topology and Skepticism. 10. Church's thesis and Hume's problem. 11. Goedel, Incompleteness, and Productive sets. 12. Turing reducibility and the Friedburg-Muchnik theorem. 13. Borel complexity, convergence and skepticism. 14. Laws, convergence, and arithmetical complexity. 15. Complexity analysis of computational and empirical problems. 16. Recursive functionals. 17. Basis theorems and testing theories with uncomputable predictions. 18. Bounded retractions and Putnam's trial-and-error predicates. 19. NP-completeness 20. PAC-learnability, with applications. The class will be based on my own lecture notes, but the material is drawn, at an appropriate level, from such texts as *Computability and Hierarchy Theory:* H. Rogers, /The Theory of Recursive Functions and Computability./ N. Cutland, /Computability/. H. E. Rose, /Subrecursion/, Oxford. Peter Hinman, /Recursion Theoretic Hierarchies/, Springer. Robert Soare, /Recursively Enumerable Sets and Degrees/, Springer. I. Moschavakis, /Descriptive Set Theory/, North Holland. *Computational Learning Theory* K. Kelly, /The Logic of Reliable Inquiry/, Oxford. Kearns and Vazirani, /An Introduction to Computational Learning Theory./ Sharma et. al., /Systems that Learn/, MIT Press. 21-700 Mathematical Logic II Instructor: Peter Andrews MWF 11:30-12:20 DH 1209 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: Uri Abraham MWF 2:30 OSC 201 Units 12 Description: The topic is forcing. The prerequisite is 21-602 or the equivalent. Textbook: The instructor has written an article for the Handbook of Set Theory that will be used in the course. 21-800 Sec.A Advanced Topics in Logic: Lambda Calculus Instructor: Rick Statman (with possible guest lecturers Henk Barendregt, Dana Scott) TR 1:30-1:50 Room TBA 12 Units (This course usually runs under 21-805 in even years; it runs this spring under 21-800 by popular demand) 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 21-800 Section B Advanced Topics in Logic: Set Theory Instructor: Ernest Schimmerling MWF 10:30 Baker Hall 231A 12 Units Description: The course will be on large cardinals and stationary tower forcing, which was invented by Hugh Woodin the 1980's. This forcing notion has many important applications to descriptive set theory and to our understanding of the Continuum Hypothesis. Textbook: Larson, P. B., The stationary tower : notes on a course by W. Hugh Woodin, University Lecture Series, Volume 32, American Mathematical Society, 2004. Available for purchase at http://www.ams.org/bookstore-getitem/item=ulect-32 21-804 Mathematical Logic Seminar Instructor: Ernest Schimmerling Thursdays, 12:00-1:20 HBH 1004 Description: The Mathematical Logic Seminar is scheduled to meet on Thursdays 12 - 1:20 during the coming semester. Please make an effort to keep this time slot free. Students, both undergraduate and graduate, are urged to enroll for 6 units in 21-804. Those invited to speak may enroll for a letter grade while others should audit. (I will sign Permission to Audit forms.) For additional information, please see http://www.math.cmu.edu/~eschimme/seminar.html 15-818 A4 SEPARATION LOGIC INSTRUCTOR: John C. Reynolds MW 10:30-11:50 am (second half of semester) Wean Hall 4615A 6 units DESCRIPTION: Separation logic is an extension of Hoare logic for reasoning about programs that use shared mutable data structures. We will survey the current development of this logic, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, recursive procedures, shared-variable concurrency, and read-only sharing. We will also discuss promising future directions. TEXTBOOK OR REFERENCES: Papers and notes to be distributed in class. COMMENT: Some knowledge of predicate logic and Hoare logic is expected. 15-819 Specification, Verification, and Model Checking ("Spec and Check!") Instructors: Ed Clarke, John Reynolds, and Jeannette Wing Mondays and Wednesdays 1:30-2:50 Wean 4615A Units: 12 Description: This course will focus on the foundations and applications of formal specification and verification.  We will present different specification notations for describing desired system properties and different verification techniques for proving that systems satisfy their specifications.  We will cover in detail two of the most successful approaches to verification: Hoare Logic and Temporal Logic Model Checking.  We will cover in less detail specification notations and tools for describing and checking constraints on software designs.  We will show the benefits of writing formal specifications for large system design and for debugging software.  Examples will come mainly from software systems and protocol verification. Prerequisites: The course is designed to be mostly self-contained. In particular, a prior logic course is not assumed.  Knowledge of programming languages and concurrency (at the undergraduate level) will be helpful. Although Model Checking is useful for hardware verification, no knowledge of computer hardware will be required for this course. Texts: 1) Logic in Computer Science: Modeling and Reasoning about Systems by M.  Huth and M. Ryan 2)  Model Checking by E. M. Clarke, Orna Grumberg, and Doron Peled Method of Evaluation Grading will be based on a set of assignments and a take-home final exam. Topics to be covered: Propositional logic, Predicate calculus, Natural deduction proofs Simple Hoare logic, Weakest preconditions Hoare logic for arrays and for recursive procedures Shared mutable data structures - separation logic Reasoning about behavioral subtyping - abstraction functions The Davis-Putnam procedure and modern SAT procedures (Grasp, Chaff, etc.) Property specification using Computation Tree Logic (CTL) Concurrency (synchronous and asynchronous models), Fairness Explicit state model checking Binary decision diagrams (BDDs) Symbolic model checking Specification notations for software design Case studies of specifying large software systems Tools for checking software design 80-820 Categorical Logic Instructor: Steve Awodey Friday 3:30-5:50 BH 235A 6-12 units Description: This course focuses on applications of category theory in logic and computer science. A leading idea is functorial semantics, according to which a model of a logical theory is a set-valued functor on a category determined by the theory. This gives rise to a syntax-invariant notion of a theory and introduces many algebraic methods into logic, leading naturally to the universal and other general models that distinguish functorial from classical semantics. Such categorical models occur, for example, in denotational semantics. e.g. treating the lambda-calculus via the theory of Cartesian closed categories. Similarly, higher-order logic is treated categorically by the theory of topoi. Note: this course will begin with a 3 week refresher of basic category theory CS students can start after immigration by reviewing on their own.