CARNEGIE MELLON UNIVERSITY
PROGRAM IN PURE AND APPLIED LOGIC
LOGIC AND LOGIC-RELATED COURSES AND SEMINARS FOR SPRING 2006
80-602 Journal Seminar
Monday 4:30 - 6:50
BH 150
Topic: Modal Logic
Instructor: Awodey
This graduate seminar is intended provide students with an
opportunity to discuss topics of current interest with faculty guests
in a relaxed setting. Dinner is provided! This semester we will
focus on the history and philosophy of modal logic, with readings by
Carnap, Kripke, Quine, and others. Faculty guests will include Tom
Ricketts, Horacio Arlo-Costa, Dana Scott, and Johan van Bentham.
80-611 Computability and Incompleteness
Instructor: Jeremy Avigad
TR 12:00-1:20
BH 136A
12 units
The 1930's witnessed two revolutionary developments in mathematical logic:
first, Gödel'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ödel,
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, or an equivalent course in Mathematics or
Computer Science. 12 units
80-612 Philosophy of Mathematics
INSTRUCTOR: Wilfried Sieg
TR 1:30-2:50
PH 225B
12 units
DESCRIPTION: The 20th century witnessed remarkable developments in
mathematics - rooted in the radical transformation of the subject during
the 19th century. An analysis of this transformation is at the center of
the course, as it led to significant foundational problems and provoked a
variety of well-known programmatic responses: logicism, intuitionism, and
finitism.
To gain a deeper understanding of fundamental issues, the course starts
out by discussing mathematical background (going back to Greek mathematics,
in particular,to Eudoxos' theory of proportion). The second and third part
survey systematic foundational work that has been pursued throughout the
20th century. We will discuss in detail set-theoretic and constructive
approaches; that is complemented by an analysis of meta-mathematical
studies initiated by Hilbert and pursued by Gödel, Church, Turing and many
others.
Against this background, the final part makes explicit important aspects
of mathematical experience; they find their articulation in the framework
of reductive structuralism deeply influenced by the philosophical
considerations of Paul Bernays.
PREREQUISITES: Some familiarity with logic and basic notions of modern
mathematics (as provided, for example, by 80-210, 80-211 or 80-212, or
21-127)
21-700 Mathematical Logic II
Instructor: Peter Andrews
MWF 11:30-12:20
CFA 212
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 A19A
12 units
PURPOSE. This is a second course in model theory. The main topic of
discussion will be what is widely recognized as pure model theory, namely
"classification theory", with a special emphasis on the forking relation
and its basic properties.
COURSE DESCRIPTION: The material to be covered: Shelah's "Forking calculus"
will be developed it its outmost generality in the context of simple
theories (which is a generalization of stability). The fundamental
properties of stable, superstable and simple unstable theories will be
developed. The machinery will be used to solve several model-theoretic
problems. Including stability spectrum theorem, uniqueness of prime models
and various characterizations.
PREREQUISITES: An introduction to model theory, like 21-603.
Text: Rami Grossberg, A course in model theory, a book in preparation.
Most of the material (and much more) appears in the following books:
* John T. Baldwin. Fundamentals of Stability Theory. Springer-Verlag,
Berlin, 1988.
* Steve Buechler. Essential Stability Theory. Springer-Verlag, Berlin,
1996.
* Bruno Poizat, A course in Model Theory, Springer-Verlag 2000.
* Saharon Shelah, Classification Theory North-Holland 1991.
Evaluation: Will be based on homework assignments (20%), a 50 minutes
midterm (20%) and a 3 hours in class comprehensive final written
examination (60%).
80-413/713 Category Theory
INSTRUCTOR: Steve Awodey
Tuesday, Thursday 3 - 4:20
Baker Hall 235B
9-12 units
DESCRIPTION:
Category theory, a branch of abstract algebra, has found many
applications in mathematics, logic, and computer science. Like such
fields as elementary logic and set theory, category theory provides a
basic conceptual apparatus and a collection of formal methods useful
for addressing certain kinds of commonly occurring formal and
informal problems, particularly those involving structural and
functional considerations. This course is intended to acquaint
students with these methods, and also to encourage them to reflect on
the interrelations between category theory and the other basic formal
disciplines.
TOPICS:
Elementary theory of categories
Functors
Natural transformations
Functor categories
Yoneda's lemma
Limits
Universality
Adjointness
Cartesian closed categories
Monads and their algebras
Categorical logic
TEXTBOOK: A draft textbook will be provided.
PREREQUSITES: one course in logic or algebra
21-805 Lambda Calculus (Preliminary Announcement)
Instructor: Rick Statman
with possible guest lecturers Henk Barendregt, Dana Scott
Where and when: TBA, MWF 3:30 (we hope to go only twice a week for 90 minutes - say MW 3:30-5pm - this will be decided by students schedules)
Textbook: The Lambda Calculus by Henk Barendregt
North Holland 1981, ISBN 0 444 85490 8
(2nd edition & paperback editions OK)
Description:
@ Although an introductory graduate course the only prerequisite
for this course is an undergraduate course in logic and
computability theory.
@ We intend to include an extensive introduction to recursion
theory as a preliminary to the theory of Ershov numberings
and their application to lambda calculus
@ The course will include material on the typed case not normally
included in 21-805. Toward this end certain material on lambda
theories will be excluded.
@ Topics covered include
(1)Basic properties of reduction and conversion
(2)Reduction and conversion strategies
(3)Calculability and representation of data types
(4)Turing machines,other models,and Church's thesis
(5)Recursive functions and relations
(6)Enumeration,universal machines,and the recursion theorem
(7)Theory of Ershov numberings
(8)Bohm's theorem, easy terms, and other exotic combinations
(9)Solvability of functional equations (unification)
(10)Combinators and bases
(11)Simple and algebraic types
(12)Labelled reduction and intersection types
@ Each of these topics includes several beautiful research
problems.These range in difficulty from ones suitable for
senior thesese to ones suitable for PhD dissertations.
Students are free to pursue whichever problems appeal to them.
Requirements: A good supply of homework exercises will be given out and those
returned will be graded. I regard these exercises as optional but if at some
stage a student wants me to say something good about him or her then I need
to have some basis for my remarks.
15-812 Semantics of Programming Languages
Instructor: John C. Reynolds
TR 1:30-2:50
Wean 5409
12 Units
DESCRIPTION: We survey the theory behind the design, description, and
implementation of programming languages, and of methods for specifying
and verifying program behavior. Both imperative and functional
programming languages are covered, as well as ways of integrating these
paradigms into more general languages. Coverage will include:
- program specification and proof
(including Hoare logic, weakest preconditions, and separation logic)
- concurrent programming
(including shared-variable and message-passing approaches)
- functional programming
(including continuations and lazy evaluation)
- type systems
(including subtyping, polymorphism, and modularization)
In exploring these topics, we will use a variety of fundamental concepts and
techniques, such as compositional semantics, binding structure, domains,
transition systems, and inference rules.
Textbook: J.C. Reynolds, Theories of Programming Languages,
Cambridge University Press.
15-819-I Advanced Topics in Programming Language Semantics
Instructor: Stephen Brookes
MW 12:00-1:20
Wean 4623
12 units
Description: This course will discuss recent developments in logic and
semantics, with emphasis on the development and validation of concurrent
programs. The topics will be drawn from a variety of recent papers, by the
lecturer and by
others, and will include: trace models for shared-memory programs and
for networks of communicating processes, grainless semantics,
concurrent separation logic and permission-accounting logics, and
proofs of correctness for various protocols. We will identify
challenges for future research and explore the potential of promising
new approaches. We assume familiarity with basic concepts and
techniques of programming language semantics, as seen for example in
the CS Programming Languages starred course (15-812). The course is
designed
for graduate students in Computer Science, Mathematics, or
Philosophy, with adequate background in logic and mathematics.
Undergraduates with sufficient
preparation may obtain permission from the instructor.
CS 810 Seminar in Programming Languages: Model Checking
Instructor: Edmund M. Clarke
Fridays 12:00pm – 1:20pm
Wean Hall 4623
This course will focus on fast propositional satisfiability solvers and
practical decision procedures (Presburger arithmetic, the theory of the
reals with and without multiplication, the theory of lists and arrays,
etc.)
and their application to model checking, automated theorem proving,
program
verification, and program analysis.
The course will be self-contained although some knowledge of
propositional
and predicate logic will be helpful. In particular, no previous
knowledge of
model checking will be required. Students will be expected to give a
lecture
or do a course project. Specific topics to be covered will include:
Overview and Background
Decision Procedures for Propositional Logic Theorem Proving
Techniques for
First-Order Logic Decision Procedures for Equality Decidable
Fragments of
First Order Logic Presburger Arithmetic Algebraically Closed Fields
Gröbner Bases Real Closed Fields Combining Decision Procedures
Class starts meeting on January 20th