CARNEGIE MELLON UNIVERSITY
PROGRAM IN PURE AND APPLIED LOGIC
LOGIC AND LOGIC-RELATED COURSES AND SEMINARS FOR FALL 2004
21-600 Mathematical Logic I
Instructor: Peter Andrews
MWF 11:30am-12:20pm
Baker Hall A53
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, equality.
21-602 Set theory I
INSTRUCTOR: Ernest Schimmerling
TuTh 3:00-4:20 pm
OSC 201
12 units
DESCRIPTION: First semester graduate level set theory. The main topics
are ZFC, infinitary combinatorics, relative consistency, constructibility,
and descriptive set theory.
TEXTBOOK: Kenneth Kunen, "Set Theory : An Introduction to Independence
Proofs"
COMMENT: Students should have a background in undergraduate level set
theory (e.g., 21-229) and logic, which includes a working knowledge of
basic ordinal and cardinal arithmetic, Gödel's completeness theorem, and
the downward Löwenheim-Skolem theorem. An understanding of the statement
(but not the proof) of Gödel's theorem on consistency proofs will also be
assumed. Those without the required background should meet with the
instructor as soon as possible to discuss their options, which may include
doing some reading over the summer.
Set Theory I is a prerequisite for Set Theory II (21-702), which
will be taught by Professor Uri Abraham in Spring, 2005.
80-310/610 Logic and Computation
Instructor: Jeremy Avigad
TuTh 3:00-4:20 pm
Hamerschlag Hall B103
12 units
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: 80-210, 80-211, or equivalent background in first-order
logic.
80-315/615 Modal Logic
Instructor: Horacio Arlo-Costa
Wed 1:30-3:50 pm
Baker Hall 150
9-12 units.
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. Kripke models are used throughout the course, but we also study
recent Kripkean-style systematizations of the modals without using possible
worlds. Special attention is devoted to Scott-Montague models of the
socalled "classical" modalities.
Prerequisites: 80-210, or 80-211, or instructor's permission.
1-703 Model theory II
INSTRUCTOR: Rami Grossberg
MWF 10:30
Baker Hall 231A
12 units
DESCRIPTION: This is a second course in model theory. The main topic of
discussion will be classification theory for non-elemntary classes.
TEXTBOOK: No official text.
DETAILS: I will concentrate in what is the deepest part of pure model
theory. Namely non-first order theories. In a typical case we will deal
with abstract elementary classes. An AEC is essentially a class K of
models all of the same similarity type (or a category of sets) which is
closed under direct limits and little more. The aim is to have an analysis
of such general classes. Most of the material to be discussed appears in
(badly written) papers only. I will start with minimal prerequisites, but
will progress quickly to some of the research frontieers of the field. I
will emphasize aspects of the theory that may eventually converge to a
proof cases of Shelah's categoricity conjecture which is the prominent
open problem in the field, it is a parallel to Morley's theorem for L
?1,?, most results will be about more general classes. The common to all
these classes is that the compactness theorem fails badly. Hopefully some
of the techniques will turn to be usefull also in the study of classes of
finite models, but we will concentrate at uncountable models. There will
be a more serious use of set theory than needed for model theory of
first-order logic.
PREREQUISITES: About half of a basic graduate course in set theory and
parts of an elementary model theory (about 60-70% of 21-603 ) or
permission of the instructor.
80-411/711 Proof Theory
Instructor: Jeremy Avigad
TuTh 10:30-11:50 am
Baker Hall 231A
12 units
Description: This course is an introduction to Hilbert-style proof theory,
where
the goal is to represent mathematical arguments using formal deductive
systems, and study those systems in syntactic, constructive,
computational, or otherwise explicit terms.
In the first part of the course, we will study various types of
deductive systems (axiomatic systems, natural deduction, and sequent
calculi) for classical, intuitionistic, and minimal logic. We will
prove Gentzen's cut-elimination theorem, and use it to prove various
theorems about first-order logic, including Herbrand's theorem, the
interpolation theorem, the conservativity of Skolem axioms, and the
existence and disjunction properties for intuitionistic logic.
In the second part of the course, we will use these tools to study
formal systems of arithmetic, including primitive recursive
arithmetic, Peano arithmetic, and subsystems of second-order
arithmetic. In particular, we will try to understand how mathematics
can be formalized in these theories, and what types of information can
be extracted using metamathematical techniques.
A solid understanding of the syntax and semantics of first-order
logic, as obtained from courses like 80-310/610 or 21-300/600, is
required. A course covering issues topics like primitive recursion and
coding, like 80-311/611 or 21-700, would be helpful, but is not
essential.
15-814 Type Systems for Programming Languages
INSTRUCTOR: Robert Harper
TuTh 1:30-2:50pm
Wean Hall 5409
12 units.
DESCRIPTION: This course is an introduction to the theory and practice
of type systems for programming languages. Topics include typed lambda
calculus, subtyping, polymorphism, data abstraction, recursive types,
and objects.
PREREQUISITE: Background equivalent to programming skills and
programming language exposure afforded by a typical undergraduate
Computer Science degree.
TEXTBOOK: Benjamin Pierce "Types and Programming Languages" MIT Press
2002.
COMMENT: This course satisfies the CS distribution requirement in
programming languages. Enrollment is limited to CS PhD students or
permission of the instructor.