The most important topics are Model Theory, Recursion Theory, Set Theory and Proof Theory.
Model Theory, to which Chapter 2 of the Foundations course offers an introduction, explores
logical theories from the point of view of their classes of models. An introduction can be accessed
from my teaching page.
As an example of studying logical theories from the point of view of the models, there is the theorem
which says that the class of models of a theory T is closed under directed colimits, precisely
if the theory has a set of axioms of the form "for all x there exists a y", followed by a quantifier-free
formula.
A more sophisticated example concerns quantifier elimination. Suppose that we are
talking about rings; so we have symbols for addition and multiplication, as well as for special
elements 0 and 1. Given a ring R,
we can define certain subsets of R, using only the given symbols and the logical operations.
For example if R is the ring of real numbers, we can define the subset of non-negative real numbers
since this is exactly the set of squares. If R is the ring of integers, the set of non-negative
elements is also definable since by Lagrange's theorem this is the set of sums of four squares.
We say that a ring R has quantifier elimination if every subset which is definable in this way,
can also be defined without quantifiers. Because the formula "x is a square" contains a quantifier
("there exists a y such that x=yy"), the ring of real numbers does not have quantifier elimination.
But the ring C of complex numbers has. This is not a coincidence. The following general theorem holds:
An infinite ring without zero divisors has quantifier elimination, precisely when it is an algebraically
closed field (the right to left implication here is a famous result by Alfred Tarski;
the converse was proved by a.o. the ex-Utrecht logician Lou van den Dries).
Recursion Theory elaborates the
"computing" theme.
Now an abstract computing machine is defined, and a precise meaning is given to the notions of a
program for this machine, and a computation. A computable function is a function f for which
there exists a program P which produces, for every input x, a computation with outcome f(x).
The theory of computable functions leads to some original and, at places, a bit eccentric mathematics.
However it is of paramount importance for Logic, and it occurs in every other branch of the field.
Moreover, the abstract computing machine paradigm, discovered years before the invention of the transistor
which made digital computers possible, is central in theoretical Computer Science. It allows an analysis
of computations in terms of amount of time (computation steps) and space (memory bits) consumed, and from
this a stratification of number-theoretic functions in so-called complexity classes. A famous problem
in this area is the P=NP?-problem, which is still open. Research on this problem has revealed interesting
connections with mainstream mathematics. The problem is on the
Clay Mathematics Institute's list of Millennium Problems, and a solution is rewarded with a million
dollars.
Set Theory is the investigation of the axiom system of Zermelo-Fraenkel, ZF.
This axiom system is accepted by most mathematicians as the foundation of their subject: every mathematical
object can be regarded as a set. When learning set theory, one learns how to use the axioms in order to build
up the mathematical objects as sets, and how to reason about them.
The model theory of ZF is
quite delicate, because Gödel's Incompleteness Theorems imply that one cannot, by using mainstream
mathematical methods, construct models for this theory. An ingenious way out was discovered by Paul Cohen
in the early sixties of the past century, when he found the "forcing method". With the help of this he was
able to show that the Continuum Hypothesis is not a consequence of the Zermelo-Fraenkel axioms.
Gödel's famous Incompleteness Theorems, already alluded to above, are part of the study of
Proof Theory. Roughly, the Incompleteness Theorems say that no consistent set of axioms suffices to
show that ordinary mathematics is free from contradiction.
But Proof Theory has a wider scope. Basically, this subject studies the combinatorial properties
of proof trees. By a celebrated result of Gentzen, such trees can always be calibrated to a specific
normal form. Using this normal form, one can often give a characterization of the functions
which can be defined in a given formal system.
An important topic in proof theory is "ordinal analysis", which aims to classify formal systems by
assigning so-called proof-theoretic ordinal numbers to them.
Another approach in the study of proofs stresses the way a proof tree can be seen as an information
flow system. A proof "acts" on the premises (hypotheses) which can be regarded as input data. This
"proofs as programs" point of view has led to applications, where actual algorithms are being extracted
from formal proof trees.