CARNEGIE MELLON UNIVERSITY
PROGRAM IN PURE AND APPLIED LOGIC
LOGIC AND LOGIC-RELATED COURSES AND SEMINARS FOR SPRING 2005
80-311/611 Computability and Incompleteness
Instructor: Jeremy Avigad
TR 10:30-11:50
PH 100
12 Units
Description: 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: 15151 or 15399 or 21228 or 21300 or 80210 or 80211 or 80310
or 80317
80-617/80-317/15-399
Instructor: Robert Harper
TR 12:00-1:20
WEH 5409AB
12 Units
The web page is http://www.cs.cmu.edu/~rwh/courses/logic/www
80-318/618 Computability and Proof Search
INSTRUCTOR: Wilfried Sieg
Wednesdays 1:30 - 3:50
CFA 102
9-12 units
DESCRIPTION: The broad informal question is: Can one "mechanize"
significant parts of mathematical reasoning? We carry out case studies for
Gödel's incompleteness theorems and an elementary part of set theory. That
requires extensive preparatory work in Parts 1 and 2 of the course.
The notion of computation (or mechanical procedure) used in mathematical
logic and computer science was introduced in the mid-1930s in a variety of
different, but equivalent formulations. We survey in PART 1 problems that
led to the search for a rigorous notion of computation and give a novel
axiomatic analysis (based on work by Turing, Post and Gandy). That provides
an appropriate conceptual framework for "mechanization."
The decision problem is one of the problems that was solved, negatively,
using such a rigorous notion of computation. The theorem of Church and
Turing asserts that there is no mechanical procedure deciding whether or
not a sentence in the language of first-order logic is a logical truth.
However, Gödel's completeness theorem guarantees that any logical truth can
be proved - in suitable calculi. A variety of procedures have been
developed to search systematically for proofs; PART 2 investigates "proof
search procedures" for natural deduction calculi.
The strategic considerations underlying a particular procedure,
implemented in the AProS algorithm, are extended in PART 3 by general
heuristics for establishing mathematical theorems. With this background,
we are going to investigate, whether the proofs of Gödel's incompleteness
theorems can be found mechanically. At an "abstract level" - taking as axioms
the crucial representability and derivability conditions - the
theorems can be established "by machine." The next step requires the use
of techniques for inductive argumentation and the development of some
elementary set theory.
TEXTBOOK OR REFERENCES: We will use a variety of classical and contemporary
papers, but also parts of books: for Part 1, papers by Gödel, Church,
Turing, Post, and Gandy; for Part 2, parts of books by Prawitz and
Troelstra & Schwichtenberg, papers by Dyckhoff and Sieg & Byrnes; for Part
3, documentation of the AProS algorithm and papers by Bundy and Hutter.
COMMENT: Students are expected to be familiar with (the metamathematics of)
first-order logic and a standard system of natural deduction. There is no
programming prerequisite, but for students with such experience there will
be challenging projects.
80-619 Computability and Learnibility
INSTRUCTOR: Kevin T. Kelly
MW 10:30-11:50
BH 150
12 units
Description: Computation seems very different from learning. The former
operates by
rules and is guaranteed to find the right answer, whereas inductive
generalization is risky because the available information does not
determine which answer is right. But that is true only if the
computational problem is solvable. Unsolvable formal problems are much
more like empirical problems. For example, a computer can't tell for
sure if another computation will halt because it can only "see" a finite
chunk of that computation by a given time, just as an empirical
scientist can only see a finite chunk of experience by a given time.
According to this analogy, it is possible to study the solvability of
scientific problems the way computer scientists analyze the solvability
of formal problems. The subject that results is called computational
learning theory. We will answer some of the following questions. Can
we describe what it is about a learning problem that makes it solvable
in a given sense? (Yes). Is guessing the next datum easier than
discovering a hypothesis that predicts all the data? (No). Can we
determine from input-output behavior alone whether we are computers?
(Only if we aren't). Can we determine whether a theory is true even if
the theory has horribly uncomputable predictions? (Yes--- try to guess
how). How does Ockham's razor help us find the truth when the truth
might be complex? Does too much rationality make computers stupid?
(Yes). Recently, computer scientists have developed an approach to
learnability called the PAC (probably approximately correct) paradigm.
The idea is that a scientific method should probably get close to the
right answer in polynomial time. This theory has been applied to
practical machine learning questions like the time required to train
neural networks. The class will involve an ongoing interplay between
computability and ideas drawn from the philosophy of science.
Prerequisite: 80-310 or approval of instructor. The grade will be based
on exercise sets.
Requirements
Participation
Assigned exercises (75%): To be turned in typed.
Final project prospectus (counts as one exercise)
Final project due last day of class (35%).
To be turned in typed.
Some interesting exercises of your own choice.
A historical essay about the development of some aspect of the subject.
A systematic investigation of some question.
A detailed application.
Topics
1. Primitive recursion.
2. Indexing and diagonalization.
3. Minimization, partial recursive functions, universal machine,
s-m-n theorem.
4. Church-Turing thesis and acceptable numberings.
5. The Kleene recursion thoerem.
6. Reducibility
7. Halting Problem and Skepticism.
8. Rice's theorem and the Rice-Shapiro theorem.
9. Topology and Skepticism.
10. Church's thesis and Hume's problem.
11. Goedel, Incompleteness, and Productive sets.
12. Turing reducibility and the Friedburg-Muchnik theorem.
13. Borel complexity, convergence and skepticism.
14. Laws, convergence, and arithmetical complexity.
15. Complexity analysis of computational and empirical problems.
16. Recursive functionals.
17. Basis theorems and testing theories with uncomputable predictions.
18. Bounded retractions and Putnam's trial-and-error predicates.
19. NP-completeness
20. PAC-learnability, with applications.
The class will be based on my own lecture notes, but the material is
drawn, at an appropriate level, from such texts as
*Computability and Hierarchy Theory:*
H. Rogers, /The Theory of Recursive Functions and Computability./
N. Cutland, /Computability/.
H. E. Rose, /Subrecursion/, Oxford.
Peter Hinman, /Recursion Theoretic Hierarchies/, Springer.
Robert Soare, /Recursively Enumerable Sets and Degrees/, Springer.
I. Moschavakis, /Descriptive Set Theory/, North Holland.
*Computational Learning Theory*
K. Kelly, /The Logic of Reliable Inquiry/, Oxford.
Kearns and Vazirani, /An Introduction to Computational Learning
Theory./
Sharma et. al., /Systems that Learn/, MIT Press.
21-700 Mathematical Logic II
Instructor: Peter Andrews
MWF 11:30-12:20
DH 1209
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: Uri Abraham
MWF 2:30
OSC 201
Units 12
Description: The topic is forcing. The prerequisite is 21-602 or the
equivalent.
Textbook: The instructor has written an article for the Handbook of Set
Theory that will be used in the course.
21-800 Sec.A Advanced Topics in Logic: Lambda Calculus
Instructor: Rick Statman (with possible guest lecturers Henk Barendregt,
Dana Scott)
TR 1:30-1:50
Room TBA
12 Units
(This course usually runs under 21-805 in even years; it runs this spring
under 21-800 by popular demand)
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
21-800 Section B Advanced Topics in Logic: Set Theory
Instructor: Ernest Schimmerling
MWF 10:30
Baker Hall 231A
12 Units
Description: The course will be on large cardinals and stationary tower
forcing, which was invented by Hugh Woodin the 1980's. This forcing notion
has many important applications to descriptive set theory and to our
understanding of the Continuum Hypothesis.
Textbook: Larson, P. B., The stationary tower : notes on a course by W.
Hugh Woodin, University Lecture Series, Volume 32, American Mathematical
Society, 2004.
Available for purchase at
http://www.ams.org/bookstore-getitem/item=ulect-32
21-804 Mathematical Logic Seminar
Instructor: Ernest Schimmerling
Thursdays, 12:00-1:20
HBH 1004
Description: The Mathematical Logic Seminar is scheduled to meet on
Thursdays 12 - 1:20 during the coming semester. Please make an effort to keep
this time slot free.
Students, both undergraduate and graduate, are urged to enroll for 6 units
in 21-804. Those invited to speak may enroll for a letter grade while
others should audit. (I will sign Permission to Audit forms.)
For additional information, please see
http://www.math.cmu.edu/~eschimme/seminar.html
15-818 A4 SEPARATION LOGIC
INSTRUCTOR: John C. Reynolds
MW 10:30-11:50 am (second half of semester)
Wean Hall 4615A
6 units
DESCRIPTION: Separation logic is an extension of Hoare logic for reasoning
about programs that use shared mutable data structures. We will
survey the current development of this logic, including extensions
that permit unrestricted address arithmetic, dynamically allocated
arrays, recursive procedures, shared-variable concurrency, and
read-only sharing. We will also discuss promising future directions.
TEXTBOOK OR REFERENCES: Papers and notes to be distributed in class.
COMMENT: Some knowledge of predicate logic and Hoare logic is expected.
15-819 Specification, Verification, and Model Checking ("Spec and Check!")
Instructors: Ed Clarke, John Reynolds, and Jeannette Wing
Mondays and Wednesdays 1:30-2:50
Wean 4615A
Units: 12
Description: This course will focus on the foundations and applications of
formal specification and verification. We will present different
specification notations for describing desired system properties and
different verification techniques for proving that systems satisfy their
specifications. We will cover in detail two of the most successful
approaches to verification: Hoare Logic and Temporal Logic Model Checking.
We will cover in less detail specification notations and tools for
describing and checking constraints on software designs. We will show the
benefits of writing formal specifications for large system design and for
debugging software. Examples will come mainly from software systems and
protocol verification.
Prerequisites: The course is designed to be mostly self-contained. In
particular, a prior logic course is not assumed. Knowledge of programming
languages and concurrency (at the undergraduate level) will be helpful.
Although Model Checking is useful for hardware verification, no knowledge
of computer hardware will be required for this course.
Texts:
1) Logic in Computer Science: Modeling and Reasoning about Systems by
M. Huth and M. Ryan
2) Model Checking by E. M. Clarke, Orna Grumberg, and Doron Peled
Method of Evaluation
Grading will be based on a set of assignments and a take-home final exam.
Topics to be covered:
Propositional logic, Predicate calculus, Natural deduction proofs
Simple Hoare logic, Weakest preconditions
Hoare logic for arrays and for recursive procedures
Shared mutable data structures - separation logic
Reasoning about behavioral subtyping - abstraction functions
The Davis-Putnam procedure and modern SAT procedures (Grasp, Chaff, etc.)
Property specification using Computation Tree Logic (CTL)
Concurrency (synchronous and asynchronous models), Fairness
Explicit state model checking
Binary decision diagrams (BDDs)
Symbolic model checking
Specification notations for software design
Case studies of specifying large software systems
Tools for checking software design
80-820 Categorical Logic
Instructor: Steve Awodey
Friday 3:30-5:50
BH 235A
6-12 units
Description: This course focuses on applications of category theory in logic
and computer science. A leading idea is functorial semantics, according to
which a model of a logical theory is a set-valued functor on a category
determined by the theory. This gives rise to a syntax-invariant notion of a
theory and introduces many algebraic methods into logic, leading naturally
to the universal and other general models that distinguish functorial from
classical semantics. Such categorical models occur, for example, in
denotational semantics. e.g. treating the lambda-calculus via the theory of
Cartesian closed categories. Similarly, higher-order logic is treated
categorically by the theory of topoi. Note: this course will begin with a 3
week refresher of basic category theory CS students can start after
immigration by reviewing on their own.