80-618 Logic Mini I
Instructor TBA
TR 12:00PM-01:20PM
DH 4303
6 units
Computability, undecidability, and the incompleteness theorems
80-619 Logic Mini II
Instructor: Jeremy Avigad
TR 12:00PM-01:20PM
DH 4303
6 units
Special topics in logic and computability
21-700 Mathematical Logic II
Instructor: Peter Andrews
MWF 11:30am-12:20pm
WEH 7201
12 Units
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.
An approach to formalizing mathematics which uses only
first-order logic is Axiomatic Set Theory, which involves adding the
axioms of set theory to the purely logical axioms of first-order
logic; it is the subject of a different course (21-602).
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.
In the context of first-order logic, it is not always clear
what makes a model "standard" or "nonstandard", but from the
perspective of type theory this distinction is very clear. 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 this important distinction between standard and nonstandard
models. It is shown that theories which have infinite models must
have nonstandard models. Henkin's Completeness Theorem and the Weak
Compactness Theorem are proved, but it is shown that the Strong
Compactness conjecture is false.
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, now published by Springer, 2002, chapters 5-7.
21-702 Set Theory II
INSTRUCTOR: Ernest Schimmerling
MWF 3:30
Wean Hall 8201
12 Units
DESCRIPTION: Second semester graduate level set theory following 21-602.
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.
21-703 Model Theory II
Instructor: Rami Grossberg
MWF 12:30
Wean Hall 8201
12 units
Purpose. This is a second course in model theory. This semester the course
will be entirely dedicated to "Classification Theory for Abstract Elementary
Classes (AECs)."
Course description.
The subject started 33 years ago by Shelah, the goal is to discover and
introduce essentially category-theoretic concepts and tools sufficient for
the development of model theory for various infinatry logics and ultimately
to have a complete theory of invariants of models up to isomorphism in all
cardinals, whenever this is possible and also establish the reason for
nonexistence 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
categoricity theorem for Lw1,w.
Despite the existence of about 1,500 pages of partial results the conjecture
is still open. The analogue for classes of models of complete first-order
theories is a highly developed theory called classification theory. In the
last decade several very substantial applications of this theory to algebra,
geometry and number theory were discovered. It is expected that eventually
classification Theory for AECs will have a much greater impact.
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, this is
in part due to the highly complex nature of the original papers that
not only introduce many new model-theoretic tools but also required
relatively sophisticated set-theoretic considerations. 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 transcendental number theory implying solutions to many
difficult long standing problems, e.g. it implies that \pi + \e is a
transcendental 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.
Hopefully some of the techniques will turn to be useful also in the study of
classes of finite models, but I will discuss uncountable models only.
I will focus on the parts of the theory that in my opinion are most likely
to lead to new significant results.
Last year three important books on the field were published:
(1) John T. Baldwin. Categoricity, AMS 2009 (235 pages), an online copy is
available from the author's website.
(2) Saharon Shelah. Classification Theory for Abstract Elementary Classes,
College Publications 2009 (824 pages).
(3) Saharon Shelah. Classification Theory for Abstract Elementary Classes
Volume 2 , College Publications 2009 (694 pages).
Textbook: A course in Model Theory III: Classification Theory for Abstract
Elementary Classes, by Rami Grossberg.
Available to students from my web page.
Prerequisites: The contents of a basic graduate course in model theory like
21-603 or permission of the instructor.
Evaluation: Weekly homework assignments (20%) 30%, Midterm 20% and an
inclass 3 hour final 50%.
Course web page: http://www.math.cmu.edu/~rami/mt2.12.desc.html
Office: WEH 7204
Phone: x8482 (268-8482 from external lines), messages at x2545
Email: Rami@cmu.edu
URL: www.math.cmu.edu/~rami
Office Hours: By appointment.
21-800 Advanced topics in logic: Large cardinals and infinite games
Instructor: James Cummings
MWF 2:30-3:20
Wean Hall 7201
12 Units
Description: The study of infinite two-player games of perfect
information is a central topic in modern set theory. The Axiom of
Determinacy (AD) asserts that every game with payoff set a subset of the
Baire space is determined, that is to say that one player has a winning
strategy. The goal of this course is to give both directions in
the proof of the following result:
Theorem (Woodin): AD is equiconsistent with the existence of omega many
Woodin cardinals.
Background: Some experience with descriptive set theory, forcing and
large cardinals is desirable but I will try make the course
reasonably self-contained.
21-805 Lambda Calculus
Instructor: Rick Statman
MWF 1:30
Wean Hall 7201
12 units
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.
@ Topics covered include
(1)Basic properties of reduction and conversion
(2)Reduction and conversion strategies
(3)Calculability and representation of data types
(4)Theory of Ershov numberings
(5)Bohm's theorem, easy terms, and other exotic combinations
(6)Solvability of functional equations (unification)
(7)Combinators and bases
(8)Simple and algebraic types
(9)Labelled reduction and intersection types
(10)Extensionality and the omega rule
@ 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: Enrolled students can work together in teams to produce
lecture notes due at the end of the semester. There are
no other requirements
15-812 Semantics of Programming Languages
Instructor: Stephen Brookes
TR 3:00-4:20
GHC 4102
12 units
This lecture course introduces the foundational concepts and techniques of
programming language semantics. The aim is to demonstrate the utility of a
scientific approach, based on mathematics and logic, with applications to
program analysis, language design, and compiler correctness. We focus on
widely applicable frameworks for semantic description: denotational,
operational, and axiomatic semantics. We use semantics to analyze program
behavior, guide the development of correct programs, prove correctness of a
compiler, validate logics for program correctness, and derive general laws
of program equivalence. We discuss a variety of imperative and functional
languages, sequential and parallel, as time permits.
Requirements
This is a starred course for CS graduate students and may be used to fulfill
part of the course requirements in the CS Ph.D. program. Graduate students
in other departments, and advanced undergraduates, can take the course with
permission of the instructor. The course is 12 units.
Grading is based on homeworks and a (take-home) final exam. Students are
encouraged to form study groups, but each student must do homework and exams
individually.
15-816 Linear Logic
Instructor: Frank Pfenning
MW 12:00-1:20
GHC 4303
12 units
Description: This graduate course provides an introduction to
linear logic with an emphasis on its applications in computer science.
This includes the theory of functional, logic, imperative, and
concurrent programming languages. We will also develop a linear type
theory which will serve as a meta-language in which the theory of
programming languages with state can be formalized effectively.
Textbook: Lecture notes will be handed out.
Comment: This is an introductory course with no formal prerequisites,
but an exposure to logic and type systems would be helpful.
Enterprising undergraduate are welcome to attend this course.
15-817 Automated Theorem Proving: Coq, Vampire, Z3: Three Very Different
Approaches
Instructor: Edmund Clarke
W 3:00-4:20pm
GHC 4102
6 Units
Description: Coq is a powerful proof assistant for higher-order logic,
Vampire is the CADE champion resolution theorem prover, and Z3 is an SMT
solver developed at Microsoft Research that uses efficient decision
procedures. It is used for many practical applications, especially in
program analysis.
The primary goal of this course is to develop a working knowledge of Coq. We
will cover Z3 and Vampire as time permits according to student interest.
However each of these could take a full semester by itself.
URL: http://www.cs.cmu.edu/~emc/15817-s12