Logo Department of Mathematics, Utrecht University
Intern
Home > Research > Logic > Topics >

Which are the important topics in Logic?

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.

 
P.O.box 80010, NL-3508 TA Utrecht, The Netherlands, telephone +31 30 253 1430, fax +31 30 251 8394, e-mail department@math.uu.nl
   Webmaster: webmaster@math.uu.nl     Last modified: Wednesday 04 Apr 2007
xhtml   css