21-700 Mathematical Logic II
Instructor: Peter Andrews
MWF 11:30am-12:20pm, in WEH 7201
Spring, 2012
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.