Master Class 2006/2007 on Logic.

Course Information

Below, you find some preliminary descriptions of the courses. This information page is, as yet, still under construction.

FIRST SEMESTER

MODEL THEORY (Wim Veldman)

In mathematics one often studies the class of structures satisfying a given set of formal axioms, for instance the class of groups, the class of fields, or the class of linear orders.
In Model Theory one starts to study the rather general case that the axioms are formulated in a first-order or elementary language. This means that, when interpreting the formulas of such a language, one only quantifies over the domain of the structure, and not, for instance, over the power set of the domain.
The pivotal notion of model theory is the notion of a formula being true in a mathematical structure. This notion has been given a formal definition by A. Tarski.
Structures satisfying the same elementary formulas are called elementarily equivalent. We study Fraïssé 's characterization of this notion.

Given a mathematical structure, one may ask: can we axiomatize the structure, that is, can we find a not too difficult set of sentences that are true in the structure such that every sentence true in the structure is a logical consequence from the sentences in the set? We solve some cases, inspired by Fraïssé.
Axiomatizing a structure is closely related to finding a method to decide which sentences are true in the structure. We shall discuss Tarski's quantifier elimination results.

Given a formal theory, what can we say about the class of its countable models? We give a characterization, due to several mathematicians independently, of theories that have exactly one countable model.
We also consider uncountable structures, and, to this end, we develop a little bit of set theory. We then can prove that theories that have, in some cardinality, only one model (up to isomorphism), must be complete, that is, if a sentence does not follow from the theory, its negation does.

One sometimes says, somewhat jokingly: model theory is about one theorem only: the compactness theorem: any set of sentences with the property that every one of its finite subsets has a model, has itself a model. We pay ample attention to this theorem, to compactness arguments in general, and to the set-theoretic generalization of the compactness theorem: the ultrafilter theorem. Ultrafilters enable us to build many models, including so-called non-standard-models.

Model theory at its best is a delightful blend of abstract and concrete reasoning.

Literature:

Lecture notes
will be available at the start of the course.
C.C. Chang, H.J. Keisler
Model Theory, North Holland Publ. Co., Amsterdam, 1977.
G. E. Sacks
Saturated Model Theory, Benjamin, Reading, Mass., 1972
B. Poizat
Cours de th\'eorie des Mod\`eles, Nur al-Matiq wal-Marifah, 1985.
W. Hodges
a shorter Model Theory, Cambridge University Press, 1997.
D. Marker
Model Theory: an introduction, Springer-Verlag, New York etc. 2002.

RECURSION THEORY AND PROOF THEORY (Sebastiaan Terwijn)

In the first half of the course we treat elementary topics from computability theory including Turing machines, recursive functions, arithmetization, Kleene's normal form theorem, the recursion theorem, the arithmetical hierarchy, and Turing degrees. Here we follow the syllabus (see below).

In the second half we treat elementary topics from proof theory. Basing our treatment mainly on Gentzen style proof systems, we will treat Goedels completeness and incompleteness theorems, cut-elimination, Herbrand's theorem, and consistency proofs using transfinite induction. For this part we will use parts of various book chapters.

Literature:
Sebastiaan A. Terwijn
Syllabus Computability Theory. Can be downloaded here.
S. Buss,
An introduction to proof theory, Handbook of Proof Theory, 1998.
H. Schwichtenberg,
Some applications of cut-elimination, Chapter D2 in Handbook of Mathematical Logic.

TYPED LAMBDA CALCULI (Henk Barendregt)

The untyped lambda terms, Barendregt [1984], form a stylistic universal programming language. Adding various classes of types gives a classification of the untyped terms. The result is that partial or total correctness checks can be made on the basis of types.

The first class of (simple) types are freely generated from atomic types, using the functionspace operator as type constructor. In the second class (recursive types) there are equations between these freely generated types. In the third class (intersection types) a partial order is added on the world of types and even intersections are postulated.

Highpoints of the three systems:
  1. Simple types. There is a type such that equality between terms can be decided on that fixed type, via a 1-1 reduction.
  2. Recursive types. Some of these type only strongly normalizing terms.
  3. Intersection types. Now all untyped terms can be typed in a natural way, providing a uniform way to describe a certain class of untyped lambda (filter) models. Both the class of normalizing and strongly normalizing terms can be characterized via typing.

The lectures form a sneak preview of the forthcoming book with the same name of Barendregt, Dekkers and Statman See here for a draft in pdf format.

Literature:
Barendregt, H.P. [1984]
The Lambda Calculus, its Syntax and Semantics, Elsevier, Amsterdam.
Barendregt, H.P., W. Dekkers and R. Statman [2007]
Typed Lambda Calculi

CATEGORY THEORY SEMINAR (Ieke Moerdijk and Jaap van Oosten)

In this seminar, the students will teach each other the basics of Category Theory.
Category Theory, invented by Eilenberg and MacLane around 1945, rapidly developed into an indispensable tool in topics like algebraic topology and algebraic geometry.
Applications of Category Theory to Logic, apparently less obvious, were developed from the sixties on. Two main types can be distinguished:
1) Applications to Proof Theory (this was actually initiated by MacLane himself). Here, one sees a formula as a functor, and a proof as a natural transformation. MacLane (who, incidentally, had been a fellow student of Gentzen in Göttingen) found a neat connection between the so-called `coherence problem for monoidal closed categories' and `normalization of proofs in propositional logic'.
2)Applications to the Model Theory of constructive logics. Here the study of categories of sheaves is very important.

Literature: we shall work through this text. Other literature may be given during the course.

SECOND SEMESTER

TOPOS THEORY (Ieke Moerdijk and Jaap van Oosten)

preliminary lecture notes in pdf format

ARITHMETIC (Albert Visser)

This class provides some capita selecta concerning arithmetical theories. We will address two major themes.

THEME I: metamathematics of classical theories
We will discuss a selection of the following topics.
1) Arithmetization in S^1_2
2) Sequential Theories and the method of Definable Cuts
3) Pudlák's general version of Gödel's Second Incompleteness Theorem
4) The Orey-Hájek and the Friedman Characterization of Interpretability.
5) The relationship between PRA and I\Sigma_1
6) Predicate Logics of theories.

THEME II: metamathematics of constructive theories
We will discuss a selection of the following topics.
1) Heyting's Arithmetic
2) Metamathematical results using Kripke models
3) De Jongh's Theorem
4) Realizability
5) Propositional Logics for Realizability

SET-THEORETICAL AND CONSTRUCTIVE ASPECTS OF THE CONTINUUM (Wim Veldman and Bas Spitters)

.

The modern study of the continuum may be said to have started with Cantor's discovery of the uncountability of the reals in 1873. This discovery, and the further work that followed, soon gave rise to a number of difficult questions, that, even today, have not found a final answer, like: The continuum hypothesis: is every uncountable subset of the reals equivalent with the whole set? Does there exist a well-ordering of the continuum? Is every subset of the reals Lebesgue-measurable?

We want to study these questions and the partial answers that have been found, some of them involving the axiom of choice. We also want to find out which sense these questions and answers could make from a constructive point of view. We shall consider Brouwer's view and his proposals to change the language and axioms of mathematics. We shall study what happens if one requires every real to be given by an algorithm. We will try to see what light is shed upon them by the so-called formal or pointless topology.

SEMINAR TYPE THEORY AND PROOF ASSISTANTS (Herman Geuvers and Bas Spitters)

Type theory is a central topic in the foundations of mathematics, logic and computer science. In this course you will continue the course by Henk Barendregt which treats simple types. In the present course you will study on dependent types, inductive and coinductive types. The course is of foundational interest by providing a foundation for (constructive) mathematics, but you will be introduced to the emerging  field of computer assisted proofs. You will get some hands-on experience using a type theory based proof assistant.

Topics include:
Polymorphic lambda calculus
Polymorphic lambda calculus: Data types and theory
Dependent Type theory I: Logical Framework
Dependent Type theory II: lambda-P
Higher Order Logic
lambda-HOL (a Type theory for Higher Order Logic)
Extensions to lambda-HOL: the Lambda Cube
Pure Type Systems
Inductive Types.
CoInductive types tutorial
Formalization of mathematics in type theory
Quotient types
Curry-Howard isomorphism
If time permits we will touch upon categorical type theory.

The seminar will be given by the students themselves. Each student will have one or two occasions to give a talk. There is a wide variety of possible subjects and the students may, up to a certain degree, follow their own preference, if they have one. They also will obtain some advice from the organizers.
Here is a Web page for the seminar