80-611 Computability and Incompleteness
INSTRUCTOR: Jeremy Avigad
MW 3:00-4:20p.m.
Margaret Morrison A14
Units: 12
DESCRIPTION: The 1930's witnessed two revolutionary developments in
mathematical logic: first, Goedel'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,
Goedel, 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.
21-700 Mathematical Logic II
INSTRUCTOR: Peter Andrews
MWF 11:30-12:30
Wean Hall 5320
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-702 Set Theory II
INSTRUCTOR: Ernest Schimmerling
MWF 2:30-3:20
Porter Hall A21A
12 Units
DESCRIPTION: Second semester graduate level set theory. Paul Cohen
invented the forcing technique and used it to prove that if ZFC is
consistent, then so are the theories ZFC + not(CH) and ZF + not(AC).
Forcing is the central topic of the course. The mechanics of forcing and
Cohen's theorem are the first goals, followed by additional applications
of forcing in cardinal arithmetic, infinitary combinatorics, the theory of
complete Boolean algebras and descriptive set theory. Topics covered in
the last part of the course vary and may include Solovay's model in which
all sets of reals are Lebesgue measurable, connections with large
cardinals, iterated forcing and/or forcing axioms such as Martin's Axiom,
the Proper Forcing Axiom and Martin's Maximum. The minimum background is
most of 21-602 but not constructibility and descriptive set theory.
Students who lack some of the required background should consult with the
instructor in advance.
21-703 Model Theory II
INSTRUCTOR: Rami Grossberg
MWF 2:30-3:20
PH A19A
12 Units
DESCRIPTION: The subject started 30 years ago by Shelah, the goal is to
discover the concepts and tools necessary for the development of model
theory for infinatry logic and ultimately to have a complete theory of
invariants of models up to isomorphism whenever this is possible and also
establish the reason for inexistence of a theory of invariants. Shelah
also proposed a conjecture as a test for the development of the theory:
Shelah's categoricity conjecture, it is a parallel to Morley's
categoriicty theorem for L_\omega_1,\omega. Despite the existence of about
a thousand pages of partial results the conjecture is still open.
Shelah in his list of open problems in model theory [Sh 702] writes:
``I see this [classification of Abstract Elementary Classes] as the major
problem of model theory.''
Until 2001 virtually nobody besides Shelah published work on AECs.
Interest and progress in the field by others materialized from two
directions: Boris Zilber managed to construct a function over the complex
numbers sharing many formal properties with exponentiation and as well
satisfying Schanuel's conjecture over the complex numbers (this is a far
reaching conjecture in transcendetal number theory implying solutions to
many difficult long standing problems, e.g. it implies that \pi + \e is a
transcendetal number). Zilber's construction uses a combination of methods
from number theory with abstract model-theoretic concepts of Shelah. In
parallel Grossberg and VanDieren introduced the notion of tameness and
proved new cases of Shelah's categoricity conjecture. Both directions
influenced many new people to enter the field.
In the future, fast progress is expected in the pure theory as well
as in applications to complicated mathematical structures like homological
algebra and quantum groups. 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.
I will focus on the basic parts of the theory that may eventually
converge to a proof cases of Shelah's categoricity conjecture. I will start
the ocurse with some fundamental theorems concerning first-order theories
(omitting types and computing Hanf-Morley numbers, characterizations of
stability) as well with basic set-theoretic machinary manipulating models
of weak set theories and the interplay between stationary sets of ordinals
and elementary chains of models. Topics to be covered: Chang and Shelah's
presentation theorems, Undefineability of well-ordering, Galois-types,
Galois-stability and Galois-saturation. The role of the amalgamation
property and its connections with the number of pairwise non-isomorphic
models, the connection between properties of models of cardinality \lambda
and \lambda^+.
EVALUATION: Weekly homework assignments (20%) 30%, Midterm 20% and an
inclass 3 hour final 50%.
PREREQUISITES: The contents of a basic graduate course in model theory
like 21-603 or permission of the instructor.
TEXTBOOK: A course in Model Theory III: Classification Theory for Abstract
Elementary Classes, by Rami Grossberg.
More details can be found on the course webpage at:
21-803 Math Logic Seminar
INSTRUCTOR: James Cummings
R 12-1:20
Doherty Hall 1217
DESCRIPTION: See http://logic.cmu.edu/seminar.html
21-805 Unification and Matching in Typed Lambda Calculus
INSTRUCTOR: Rick Statman
MWF 3:30-4:20
(this course will probably move to a TR time slot)
Doherty Hall 2122
12 Units
15-812A Programming Language Semantics
INSTRUCTOR: John C. Reynolds
MW 1:30-2:50
Wean Hall 4615A
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 programing
(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.
PREREQUISITES: There are no specific prerequisites, but the course
requires some background in programming languages and basic mathematics.
To get a feel for what is needed look at Appendix A of the text and skim
over the first couple of chapters. If these seem unduely difficult, meet
with the instructor.
TEXTBOOK: J. C. Reynolds, "Theories of Programming Languages", Cambridge
University Press 1998.
WEB PAGE:
/afs/cs.cmu.edu/project/fox-19/member/jcr/www15812As2008/cs812-08.html
80-619 Computability and Learnability
Instructor: Kevin Kelly
TR 1:30-2:50 BH A53
Baker Hall A53
12 Units
Description: This course is conceived as an alternative way to fulfill the
80-311, Computability and Incompleteness requirement for students who are
more interested in rationality, learning, and scientific method than in
logic and the foundations of mathematics. A solid grounding in the theory
of computability will be provided, but the applications will concern
computational learning theory, which studies what can be learned or
discovered by computational agents from empirical data rather than what
can be proved in a logical system. The application is more natural than it
might seem at first. The problem of induction is that a general law may be
refuted by the next observation, no matter how long it has withstood test.
But there is a parallel problem about algorithmic halting: no matter how
long a computation fails to halt, it may halt as soon as a world-be
decision procedure concludes that it never will. In both cases, the
difficulty can be sidestepped by entertaining methods that converge to the
right answer without announcing when they have done so. We will delve into
this analogy, using the theory of computability to investigate such
questions as what machines can learn, whether machines could discover
uncomputable truths, why irrational machines may be smarter, and what good
it would do to have an infinite regress of methods, each of which checks
whether its predecessor will find the truth. All topics covered are
self-contained, but students are expected to have some basic background in
logic, computation, or discrete mathematics. The text will consist of
handout lecture notes. The course grade will be based on exercises and two
short papers that will provide vital practice in writing articles for
conference proceedings.