21-604 Introduction to Recursion Theory Instructor: Richard Statman MWF 1:30-2:20 DH 2105 12 units Syllabus covers; models of computation,computable functions, solvable and unsolvable problems, reducibilities among problems, recursive and recursively enumerable sets, the recursion theorem, Post's problem and the Friedberg-Muchnik theorem, general degrees and r.e. degrees, the arithmetical hierarchy, the hyperarithmetical hierarchy,the analytical hierarchy, higher type recursion. Prerequisite: 21-300 or its equivalent. 21-624 Selected Topics in analysis: classical descriptive set theory Instructor: Ernest Schimmerling MWF 2:30-3:20 WEH 5320 12 units Descriptive set theory combines analysis and logic. The required background is undergraduate level analysis, logic and set theory. The recommended textbook is Kechris, "Classical Descriptive Set Theory", Graduate Texts in Mathematics 156, Springer-Verlag. Another useful book is Moschovakis, "Descriptive Set Theory". The topics to be covered include: Polish spaces (Baire space, Cantor space, etc.); classical definability hierarchies (Borel Hierarchy, Projective Hierarchy); effective definability hierarchies; the Wadge hierarchy; complete sets, universal sets; separation; reduction; uniformization; prewellordering; scales; perfect sets; Baire measurability; Lebesgue measurability; Suslin operation; substitution property; basis theorems; tree representations; proofs of determinacy (Borel determinacy); applications of determinacy; definable winning strategies; theorems on the boundedness of norms; theorems on the ranks of wellfounded relations (Kunen-Martin); admissible ordinals; stable ordinals. In addition to more standard graduate course mechanics, student will be assigned individual reading projects on which they will lecture towards the end of the semester. 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-703 Model Theory II Instructor: Rami Grossberg MWF 12:30-1:20 BH 231A 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 more than 30 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 a thousand 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 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. Last summer two important books on the field were published: (1) John T. Baldwin. Categoricity, AMS 2009 (235 pages) (2) Saharon Shelah. Classification Theory for Abstract Elementary Classes, College Publications 2009 (824 pages). Textbook: A course in Model Theory III: Classification Theory for Abstract Elementary Classes, by Rami Grossberg. Available 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.10.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. 15-812 Programming Language Semantics Instructor: John C. Reynolds TTh 12:00-1:20 pm GHC 4303 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. Textbook: J. C. Reynolds, Theories of Programming Languages, Cambridge University Press 15-816 Modal Logic Instructors: Frank Pfenning and Andre Platzer TR 1:30-2:50 GHC 4102 12 units Description: Modal logic is the study of the laws of inference for judgments such as "it is necessary that", "it is possible that", "K knows that", "K affirms that", etc. Its roots lie in philosophy and linguistics, but it has a surprisingly rich variety of applications in computer science. This course provides a thorough introduction to both classical and intuitionistic modal logic, with an emphasis on applications in computer science. Specific topics include: intuitionistic logic, justification of logical laws, judgmental S4 and staged computation, classical modal logics, axiom systems, Kripke semantics, correspondence theory, intuitionistic S5 and distributed computation, sequent calculi, cut and identity properties, tableaux systems, completeness of classical modal logics, filtration, decidability, focusing, substructural logics as modal logics, constructive resource semantics, description logics, first-order modal logics, dynamic logic, modal type theories, logics of affirmation and knowledge. Textbook: None, but lecture notes will be provided. Comments: Students from mathematics and philosophy, as well as enterprising undergraduate with a basic foundation in logic are invited. URL: http://www.cs.cmu.edu/~fp/courses/15816-s10 15-819 F Advanced Topics in Programming Languages: Semantics and Logics for Concurrent Programs Instructor: Stephen Brookes MW 10:30-11:50 GHC 4102 12 Units This course explores some exciting new and ongoing research into the theory and practice of concurrent programming, building on recent work, notably separation logic. First we review key historical developments and introduce the foundational techniques and concepts of denotational and operational semantics. We introduce a trace-theoretic denotational semantic framework suitable for modelling diï¬~@erent concurrency paradigms, including shared-memory, asynchronous message-passing, and synchronized message-passing. We present concurrent separation logic, a Hoare-style logic for race-free partial correctness of shared-memory parallel programs with mutable state. After discussing the advantages and limitations of this logic, we explore related work and discuss a series of recent papers which demonstrate the generality and adaptability of this approach, including attempts to adapt ideas of separation logic to message-passing languages such as CSP. We will look both at foundational theoretical problems (e.g. how to provide a tractable semantic model, how to design suitable logics and prove their soundness) and at practical issues that arise in the design and implementation of automated tools based on these foundations. Topics include: â~@¢ historical review: denotational and operation semantics; state transformations, resumptions, failures; â~@~\trueâ~@~] concurrency; deadlock, fairness, safety and liveness; Hoare logics and temporal logics â~@¢ a unifying semantic framework: trace semantics; â~@¢ concurrent separation logic: semantics and soundness; â~@¢ semantic models and logics based on permissions; â~@¢ combining separation logic with rely/guarantee; â~@¢ combining separation logic with procedures; â~@¢ variables as resources; â~@¢ termination proofs using separation logic; â~@¢ automated tools for shape analysis and termination. We also plan to leave room in the schedule for discussion of hot new results or papers. Requirements: This is an elective course for CS graduate students and graduate students in other departments. Advanced undergraduates with suï¬~Ccient training in mathematics and logic can take the course with permission of the instructor. Grading will be based on class participation. Students who wish to take the class for credit should arrange with the instructor to take responsibility for presenting in depth one or more of the relevant research papers. It is also possible to obtain credit by designing and completing a project approved by the instructor.