80-611 Computability and Incompleteness
Instructor: Jeremy Avigad
Units: 12
TR 10:30AM - 11:50AM
BH A51
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.
80-315/80-615 Modal Logic
Instructor Horacio Arló-Costa
Units: 9-12 Units
TR: 03:00PM-04:20PM,
BH 150
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. Special attention is devoted to Scott-Montague models of the
so-called 'classical' modalities. Incompleteness results are reviewed and a
general completeness result for all classical systems is presented in terms of
first order general neighborhood frames.
21-624 Topics in analysis: classical descriptive set theory
Instructor: Ernest Schimmerling
MW 3:30-4:50
PH 126A
12 Units
Description: Descriptive set theory combines analysis and logic. The
required background is undergraduate level analysis, logic and set theory.
The recommended textbook is Kechris, "Classical Descriptive Set Theory",
Graduate Texts in Mathematics 156, Springer-Verlag. Another useful book
is Moschovakis, "Descriptive Set Theory" (out of print).
I posted a very general course description online at
http://www.math.cmu.edu/~eschimme/21-624/syllabus.pdf
The topics that will be covered include:
Polish spaces (Baire space, Cantor space, etc.); classical definability
hierarchies (Borel Hierarchy, Projective Hierarchy); effective
definability hierarchies; the Wadge hierarchy; complete sets, universal
sets; separation; reduction; uniformization; prewellordering; scales;
perfect sets; Baire measurability; Lebesgue measurability; Suslin
operation; substitution property; basis theorems; tree representations;
proofs of determinacy (Borel determinacy); applications of determinacy;
definable winning strategies; theorems on the boundedness of norms;
theorems on the ranks of wellfounded relations (Kunen-Martin); admissible
ordinals; stable ordinals
21-700 Mathematical Logic II
Instructor: Peter Andrews
MWF 12:30
PH 225B
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 A21A
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. Shelah also proposed the 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 Lw1,w. Despite
the existence of about a thousand pages of partial results the conjecture is
still open.
More details can be found on the course webpage at:
21-800 Sec. A. Adv Topics in Logic: Introduction to the theory of algorithms :
Hilbert's 10th problem.
Instructor: Rick Statman
MWF 9:30
BH 231A
12 Units
Course Description: The following is a central problem in number theory:
" Find some or all of the integral solutions to
p(x1, ... ,xn) = 0
where p is a polynomial with integral coefficients"
Hilbert's 10th problem (1900) is to
" Find a general method (algorithm) for deciding which
p have integral zeroes."
Hilbert's 10 problem was shown to be recursively unsolvable by Yuri
Matiyasevich in January 1970. Matiyasavech's result is based on work
by Martin Davis, Julia Robinson and Kurt Godel, in the last case going
back to the 1930's. In this course we shall give an introduction to the
theory of algorithms based on Matiyasavich's negative solution to
Hilbert's 10th problem (although we hope to give a more updated version
of the proof).
21-800 Sec. B. Advanced Topics in Logic: Prikry-style Forcing and Singular
Cardinal Combinatorics
Instructor: James Cummings
MWF 12:30
Wean Hall 5328
12 Units
Description:
Prikry forcing takes a measurable cardinal $\kappa$ and
changes its cofinality to $\omega$, preserving all
cardinals and all cofinalities other than $\kappa$.
Generalisations of Prikry forcing are among the most
powerful tools in the set theorist's toolbox, especially
when we study problems about singular cardinals (for example
regarding cardinal arithmetic). Topics we will cover after a
brief review of Prikry forcing will include (time allowing)
Diagonal Prikry forcing
Supercompact Prikry forcing
Tree Prikry forcing
Radin forcing
The various extender-based Prikry and Radin forcings
Prikry forcing with interleaved collapsing
Iteration of Prikry-type forcing with various supports
21-804 Math Logic Seminar
Ernest Schimmerling
Units 6
Tuesdays 12:00-1:20pm
CFA 211
Description: Topics will come from diverse parts of mathematical
logic and closely related fields. Lectures are by invitation.
Students who speak in the seminar may sign up for a letter grade;
others should register as AUDITORS.
See http://www.math.cmu.edu/~eschimme/seminar.html
15-818A3 Introduction to Separation Logic
Instructor: John Reynolds
Units: 6
MW 1:30-2:50 pm (first half of semester)
Wean Hall 4615A
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.
More details at www.cs.cmu.edu/~jcr
15-818A4 Current Research on Separation Logic
Instructor: John Reynolds
Units: 6
MW 1:30-2:50 pm (second half of semester)
Wean Hall 4615A
Description: We will study and discuss recent papers on separation logic,
grainless semantics, and related topics.
More details at www.cs.cmu.edu/~jcr
15-829/80-813 Practical Decision Procedures
Jeremy Avigad and Ed Clarke
Units: 6/12
F 1:30PM - 2:50PM
WEH 4615A
Description: In recent years, fast propositional satisfiability solvers
have been developed that can often handle formulas in CNF with hundreds
of thousands of variables and millions of clauses. These have made it
possible to apply classical decision procedures to domains where,
previously, they were applicable only in theory. As a result, we can now
reason effectively in the presence of increasingly complex systems of
arithmetic and algebraic constraints. This course will survey the
fundamental methods behind these core decision procedures. Topics will
include Groebner bases, decision procedures for real and integer linear
arithmetic, and decision procedures for real closed fields. We will also
cover Nelson-Oppen methods, which provide ways of combining decision
procedures for languages with restricted overlap. This is a six-unit
seminar, but students can earn an additional six units by completing a
suitable final project.