/afs/cs/project/pal/pal-courses-s01 CARNEGIE MELLON UNIVERSITY PROGRAM IN PURE AND APPLIED LOGIC LOGIC AND LOGIC RELATED COURSES AND SEMINARS FOR FALL 2000 21-603 Model Theory I Instructor: Rami Grossberg MWF 1:30, PH A19D 12 Units DESCRIPTION: Model theory is one of the four major branches of mathematical logic, and has a number of applications to algebra (e.g.field theory, algebraic geometry, number theory, and group theory), analysis (non standard analysis, geometry of Banach spaces) and theoretical computer science (via finite model theory) as well as to set theoretic topology and set theory. This course is the first in a sequence of three courses. The purpose of this course is to present the basic concepts and techniques of model theory with an emphasis on pure model theory. The main theorem of the course is Morley's theorem. It will be presented in a way that permits several powerful extensions. CONTENTS: Similarity types, structures. Downward Lowenheim-Skolem theorem. Construction of models from constants, applications of the compactness theorem, model completeness, elementary decideability results, Henkin's omitting types theorem, prime models. Elementary chains of models, some basic two-cardinal theorems, saturated models (characterization and existence), basic results on countable models including Ryll-Nardzewski's theorem. Indiscernible sequences, and connections with Ramsey theory, Ehrenfeucht- Mostowski models. Introduction to stability (including the equivalence of the order-property to instability), chain conditions in group theory corresponding to stability/superstablity/omega-stability, strongly minimal sets, various rank functions, primary models, and a proof of Morley's categoricity theorem. Basic facts about infinitary languages, computation of Hanf-Morley numbers. PREREQUISITE: An undergraduate level course in logic. TEXT: Rami Grossberg, A course in model theory, a book in preparation. Most of the material (and much more) appears in the following books: 1. C. C. Chang and H. J. Keisler, Model Theory, North-Holland 1990. 2. Bruno Poizat, A course in Model Theory, Springer-Verlag 2000. 3. S. Shelah, Classification Theory, North-Holland 1991. I will not use a text, but will distribute my own notes on a weekly basis. EVALUATION: Will be based on weekly homework assignments (20%), a 50 minutes midterm (20%) and a 3 hours inclass comprehensive final written examination (60%). COURSE WEBPAGE: www.math.cmu.edu/~rami/mt1.01.desc.html 80-311/611 Computability & Incompleteness Instructor: Jeremy Avigad MW 10:30-11:50am, Wean Hall 8427 9-12 Units Description: The 1930's witnessed two revolutionary developments in mathematical logic: first, G=F6del'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=F6del, 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: 80-210 or 80-211, 80-310, or consent of the instructor 80-314/614 Logic in Artificial Intelligence Instructor: Horacio Arlo-Costa WF 1:30-2:50pm, HBH 1511 9-12 Units Description: An introduction to several formalisms used in knowledge representation and database theory. The emphasis is placed on nonmonotonic logic, conditional logic and belief revision methods. We will also study recent issues in the logics of knowledge and belief and consider applications in distributed =AI. Several methodological problems in AI are discussed. Prerequisites: A basic course in logic is recommended but not required. 80-316/616 Probability & Artificial Intelligence Instructor: Peter Spirtes MW 9:00-10:20am, Room TBA 9-12 Units Description: In this course we will examine foundational questions about the concepts of causality and probability, how artificial intelligence techniques can be used to solve some of the computational problems presented by the use of probabilities and representations of causal relations, and how probabilities and representations of causal relations have been incorporated into recently developed expert systems. The foundational questions we will examine are: What do causal and probabilistic statements mean? How can probabilities and causal relations be inferred? Are there any axioms relating causal relations to probability distributions? What are the advantages and disadvantages of using probabilities as compared to alternative representations of uncertainty? We will then discuss recent developments in Artificial Intelligence (e.g. Bayesian networks) which have solved some of the long-standing computational problems associated with the use of probabilities and statements about causal relations. Finally, we will study in detail some expert systems, such as QMR and Pathfinder, which have incorporated these new techniques in order to perform medical diagnosis. 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. 21-702 Set theory II Instructor: James Cummings Time: MWF 9:30 a.m., OSC 202 12 units DESCRIPTION: Set theory I (21-602) introduced constructibility and forcing, and the basic facts about infinite combinatorics and sets of real numbers. The main topics of this course are 1) Large cardinals and their significance in set theory. 2) New forcing posets (e.g. Sacks forcing, Solovay forcing, Mathias forcing) 3) Analysing generic extensions 4) Basic equiconsistency results in set theory 5) Structural properties of reals and sets of reals. The course will culminate in the proof of Solovay's theorem that Con(ZFC + an inaccessible) -> Con(ZF + DC + every set of reals is Lebesgue measurable). If time allows we may also discuss Shelah's converse result. TEXT OR REFERENCES: No text. Books that may be helpful include Kunen: "Set theory" Jech: "Set theory" and "Multiple forcing" PREREQUISITE: Set theory I or the permission of the instructor. COMMENTS: There will be weekly homework, a midterm and a final. 80-405/705 Game Theory Instructor: Cristina Bicchieri Thursday, 2:00-4:20pm, Baker Hall 235A 9-18 Units Description: The first part of course will be a standard introduction to noncooperative games. The second part will cover special topics such as formal models of players' reasoning and experimental results on Trust, Ultimatum, and Social Dilemma games. Prerequisites for undergraduates: 80-305 Rational Choice 21-800 Advanced Topics in Logic: Set Theory INSTRUCTOR: Ernest Schimmerling TIME: TuTh 10:30 - 11:50, BH 231A 12 units DESCRIPTION: The topic of the course will be core models and their applications. During the first few weeks, we'll quickly cover some of Jensen's work on L, Kunen's on L[U], and Silver's on 0#. Then we'll begin Steel's forthcoming handbook of set theory article "An outline of innermodel theory" which is available from http://www.math.berkeley.edu/~steel/ and possibly also his book "The core model iterability problem" of which I have enough copies for everyone interested to borrow. REFERENCES: Thomas Jech, "Set Theory" (sections on L, L[U], and 0#), Academic Press, 1978. Ronald Jensen, "The fine structure of the constructible hierarchy", Ann. Math. Logic, 4 (1972) 229-308. Keith Devlin, "Constructibility", Springer-Verlag, 1984. John Steel, "An outline of inner model theory". Available from http://www.math.berkeley.edu/~steel William Mitchell and John Steel, "Fine structure and iteration trees", Springer Lecture Notes in Logic 3, 1994. May be purchased from http://www.aslonline.org/asl/LNL/LNL.htm. John Steel, "The core model iterability problem", Springer Lecture Notes in Logic 8, 1996. May be borrowed from the instructor or purchased from http://www.aslonline.org/asl/LNL/LNL.htm. Donald Martin and John Steel, "Iteration trees", J. Amer. Math. Soc. 7 (1994) 71-125. PREREQUISITE: Background equivalent to at least 21-602 and concurrent enrollment in 21-702. 21-804 Math Logic Seminar Organizer: Rami Grossberg Monday 4:30-6:00pm, WEH 8427 12 units Description: The purpose of the seminar is to offer a forum for discussion of some recent developments in mathematical logic. We will concentrate in the areas of Model Theory and Set Theory. We will have weekly two hour meetings where faculty and students present papers (typically not authored by local people) at the level which will be appropriate to the level of participants (assume not much more than a first graduate course in mathematical logic). It is possible to take this seminar for credit, and in order to get a grade, you will have to present at least one paper (usually 3 - 5 lectures). You may also be interested to participate passively (without giving a talk - not for credit). The structure is like a sequence of several mini-courses. Every few weeks the topic will be changed, and often the subjects of discussion are independent. 80-513/813 Seminar on the Foundations of Mathematics Instructor: Wilfried Sieg Wednesday, 2:30-4:50pm, Baker Hall 150 9-12 Units Description: The seminar focuses on mathematical and logical work, important for foundational issues. That may range from the detailed presentations of "constructive" consistency proofs through conceptual analyses of central mathematical concepts to the discussion of ontological and epistemological issues. 80-515/815 Seminar on the Foundations of Statistics Instructor: Teddy Seidenfeld Monday 3:30-4:50pm, Porter Hall A20 Wednesday 2:30-3:50pm, Porter Hall A20 12 Units Prerequisites: A basic course in probability. Description: For Spring term 2001, the "Foundations" seminar will focus on topics in statistical decision theory. L.J. Savage's "Foundations of Statistics" is to be read as the principal text. The course goals include understanding how Bayesian decision theory differs from its rivals, and understanding where Savage's position is located within the Bayesian program. This course is cross-listed with Statistics and is open to undergraduates by permission of the instructor. 15-819A Reasoning about Low-Level Programming Languages Instructor: John Reynolds MW 1:00-2:20pm, WEH 4615A 6 units DESCRIPTION: Type systems and program correctness for low-level programming languages,including languages that permit shared mutable data structures (structures where many pointers can address the same location, which can be updated in-place by the program) and embedded code (pointers from data structures to machine code). There will be no textbook. The course will cover at least the following research papers: Reynolds, J. C., Intuitionistic Reasoning about Shared Mutable Data Structure Ishtiaq, S. and O'Hearn, P. W., BI as an Assertion Language for Mutable Data Structure Walker, D. and Morrisett, G., Alias Types for Recursive Data Structures. 15-819B Game Semantics Instructor: John Reynolds MW 1:00-2:20pm, WEH 4615A 6 Units DESCRIPTION: In game semantics, the semantics of a programming language is described by a game (or conversation) between the computer and its environment; a type (or protocol) determines the rules of a game, while a program is a strategy for playing the game. This approach has provided more abstract models than conventional denotational semantics for languages as varied as PCF and Idealized Algol. It also suggests the design of novel languages in which a game-like interaction between the computer and its environment is the central paradigm. There will be no textbook. The course will be based on Samson Abramsky's Marktoberdorf Lecture Notes on Game Semantics, plus selected research papers. 15-851 Computation and Deduction Instructor: Frank Pfenning TR 1:00-2:20, WeH 5409 12 units DESCRIPTION: We explore the theory of programming languages using deductive systems. We use such systems to specify, implement, and verify properties of functional and logic programming languages. The deductive approach to the specification of programming languages has become standard practice, and one of the goals of this course is to provide a good working knowledge of how to engineer such language descriptions. Throughout the course we will use Twelf as a uniform meta-language in which we can express specification, implementation, and meta-theory of the object languages we are considering. An implementation of Twelf and examples will be available on-line for experimentation. TEXTBOOK: Course notes will be handed out. PREREQUISITES: No formal prerequisites. Enterprising undergraduates are welcome. 21-905 Seminar on Automated Deduction Organizer: Peter Andrews Time: to be arranged 6-18 variable units DESCRIPTION: The purpose of this seminar will be to help and encourage the participants to gain greater familiarity with certain parts of the literature on automated theorem proving, to become better acquainted with work on theorem proving at CMU and elsewhere, and to acquire the background on which future developments may be built. Choice of topics will be influenced by the interests of the participants.