80-611 Computability and Incompleteness Instructor: Jeremy Avigad Units: 12 TR 10:30AM - 11:50AM BH A51 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. 80-315/80-615 Modal Logic Instructor Horacio Arló-Costa Units: 9-12 Units TR: 03:00PM-04:20PM, BH 150 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. Special attention is devoted to Scott-Montague models of the so-called 'classical' modalities. Incompleteness results are reviewed and a general completeness result for all classical systems is presented in terms of first order general neighborhood frames. 21-624 Topics in analysis: classical descriptive set theory Instructor: Ernest Schimmerling MW 3:30-4:50 PH 126A 12 Units Description: 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" (out of print). I posted a very general course description online at http://www.math.cmu.edu/~eschimme/21-624/syllabus.pdf The topics that will 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 21-700 Mathematical Logic II Instructor: Peter Andrews MWF 12:30 PH 225B 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-703 Model Theory II Instructor: Rami Grossberg MWF 1:30-2:20PM PH A21A 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. Shelah also proposed the 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 Lw1,w. Despite the existence of about a thousand pages of partial results the conjecture is still open. More details can be found on the course webpage at: 21-800 Sec. A. Adv Topics in Logic: Introduction to the theory of algorithms : Hilbert's 10th problem. Instructor: Rick Statman MWF 9:30 BH 231A 12 Units Course Description: The following is a central problem in number theory: " Find some or all of the integral solutions to p(x1, ... ,xn) = 0 where p is a polynomial with integral coefficients" Hilbert's 10th problem (1900) is to " Find a general method (algorithm) for deciding which p have integral zeroes." Hilbert's 10 problem was shown to be recursively unsolvable by Yuri Matiyasevich in January 1970. Matiyasavech's result is based on work by Martin Davis, Julia Robinson and Kurt Godel, in the last case going back to the 1930's. In this course we shall give an introduction to the theory of algorithms based on Matiyasavich's negative solution to Hilbert's 10th problem (although we hope to give a more updated version of the proof). 21-800 Sec. B. Advanced Topics in Logic: Prikry-style Forcing and Singular Cardinal Combinatorics Instructor: James Cummings MWF 12:30 Wean Hall 5328 12 Units Description: Prikry forcing takes a measurable cardinal $\kappa$ and changes its cofinality to $\omega$, preserving all cardinals and all cofinalities other than $\kappa$. Generalisations of Prikry forcing are among the most powerful tools in the set theorist's toolbox, especially when we study problems about singular cardinals (for example regarding cardinal arithmetic). Topics we will cover after a brief review of Prikry forcing will include (time allowing) Diagonal Prikry forcing Supercompact Prikry forcing Tree Prikry forcing Radin forcing The various extender-based Prikry and Radin forcings Prikry forcing with interleaved collapsing Iteration of Prikry-type forcing with various supports 21-804 Math Logic Seminar Ernest Schimmerling Units 6 Tuesdays 12:00-1:20pm CFA 211 Description: Topics will come from diverse parts of mathematical logic and closely related fields. Lectures are by invitation. Students who speak in the seminar may sign up for a letter grade; others should register as AUDITORS. See http://www.math.cmu.edu/~eschimme/seminar.html 15-818A3 Introduction to Separation Logic Instructor: John Reynolds Units: 6 MW 1:30-2:50 pm (first half of semester) Wean Hall 4615A 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. More details at www.cs.cmu.edu/~jcr 15-818A4 Current Research on Separation Logic Instructor: John Reynolds Units: 6 MW 1:30-2:50 pm (second half of semester) Wean Hall 4615A Description: We will study and discuss recent papers on separation logic, grainless semantics, and related topics. More details at www.cs.cmu.edu/~jcr 15-829/80-813 Practical Decision Procedures Jeremy Avigad and Ed Clarke Units: 6/12 F 1:30PM - 2:50PM WEH 4615A Description: In recent years, fast propositional satisfiability solvers have been developed that can often handle formulas in CNF with hundreds of thousands of variables and millions of clauses. These have made it possible to apply classical decision procedures to domains where, previously, they were applicable only in theory. As a result, we can now reason effectively in the presence of increasingly complex systems of arithmetic and algebraic constraints. This course will survey the fundamental methods behind these core decision procedures. Topics will include Groebner bases, decision procedures for real and integer linear arithmetic, and decision procedures for real closed fields. We will also cover Nelson-Oppen methods, which provide ways of combining decision procedures for languages with restricted overlap. This is a six-unit seminar, but students can earn an additional six units by completing a suitable final project.