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.