15-414 Bug Catching Instructor: Edmund Clarke TuTh 3:00-4:20 p.m. Wean Hall 5312 9 units DESCRIPTION: Automated Program Verification and Testing Many CS and ECE students will be developing software and hardware that must be ultra reliable at some point in their careers. Logical errors in such designs can be costly, even life threatening. There have already been a number of well publicized errors like the Intel Pentium floating point error and the Arian 5 crash. In this course we will study tools for finding and preventing logical errors. Three types of tools will be studied: automated theorem proving, state exploration techniques like model checking and tools based on static program analysis. Although students will learn the theoretical basis for such tools, the emphasis will be on actually using them on real examples. This course can be used as one of the Fundamentals of Algorithms requirement. 21-600 Mathematical Logic I Instructor: Peter Andrews MWF 11:30am-12:20pm Hamerschlag Hall B103 12 Units Description: The study of formal logical systems which model the reasoning of mathematics, scientific disciplines, and everyday discourse. Propositional calculus and first-order logic. Syntax, axiomatic treatment, derived rules of inference, proof techniques, computer-assisted formal proofs, normal forms, consistency, independence, semantics, soundness, completeness, the Lowenheim-Skolem Theorem, compactness. 21-602 Set Theory I Instructor: Ernest Schimmerling MW 3:30 - 4:50 p.m. Wean Hall 5312 12 Units DESCRIPTION: First semester graduate level set theory. Godel proved that if ZF is consistent, then so is ZFC + GCH; this is the most important theorem that will be covered in the course. The main topics are ZFC, cardinal arithmetic, the rank hierarchy, the H(\kappa) hierarchy, absoluteness, relative consistency, infinitary combinatorics, constructibility and descriptive set theory. TEXTBOOK: Kenneth Kunen, "Set theory : An introduction to independence proofs". COMMENT: The minimum background in undergraduate level set theory (e.g., 21-229) and logic, which includes a working knowledge of basic ordinal and cardinal arithmetic, Godel's completeness theorem and the downward Lowenheim-Skolem theorem. An understanding of the statement of Godel's theorem on consistency proofs will also be assumed. Students who lack some of the required background should meet with the instructor as soon as possible to discuss the option of doing some reading and exercises over the summer. Set Theory I is a prerequisite for Set Theory II (21-702), which we anticipate will be offered in Spring, 2008. 21-603 Model Theory I Instructor: Rami Grossberg (rami@cmu.edu) MWF 1:30-2:20 p.m. PH A19A 12 Units DESCRIPTION: Model theory is one of the four major branches of mathematical logic. There are many applications of model theory to algebra (e.g. field theory, algebraic geometry, number theory, and group theory), analysis (non-standard analysis, complex manifolds and the geometry of Banach spaces) and theoretical computer science (via finite model theory) as well as set theoretic topology and set theory. This course is the first in a sequence of three courses. The purpose of this 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 and abstract elementary classes, computation of Hanf-Morley numbers. PREREQUISITE: This is a graduate level course, while at the beginning the pace will be slow, the pace will speed up in the second half. In the past many of students where undergraduates, so the prerequisites are kept to the minimum of "an undergraduate-level" course in logic. Motivated undergraduate students are encouraged to contact the instructor. TEXT: Rami Grossberg, A course in model theory, a book in preparation. Most of the material (and 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 provide access to my notes on a weekly basis. EVALUATION: Will be based on weekly homework assignments (20%), a 50 minutes midterm (20%) and a 3 hours in-class comprehensive final written examination (60%). COURSE WEBPAGE: www.math.cmu.edu/~rami/mt1.07.desc.html 80-310,80-610 Logic and Computation Instructor: Kevin T. Kelly TuTh 1:30-2:50 p.m. Scaife Hall 214 Units 9,12 DESCRIPTION: Among the most significant developments in logic in the twentieth century is the formal analysis of the notions of provability and semantic consequence. For first-order logic, the two are related by the soundness and completeness theorems: a sentence is provable if and only if it is true in every interpretation. This course begins with a formal description of first-order logic, and proofs of the soundness and completeness theorems. Other topics may include: compactness, the Lowenheim-Skolem theorems, nonstandard models of arithmetic, definability, other logics, and automated deduction. PREREQUISITES: either 80-210, 80-211, 15-251, or consent of the instructor. 21-804 Math Logic Seminar Coordinator: James Cummings Tuesday 12:00-1:20 p.m. Scaife Hall 219 DESCRIPTION: Topics will come from diverse parts of math logic and closely related fields. Lectures are by invitation. Interested students should enroll in 21-804. Students who speak in the seminar may sign up for a letter grade. Others should register as Auditors.