Master Class 2006/2007 on Logic.

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.

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.

- 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.

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:- Simple types. There is a type such that equality between terms can be decided on that fixed type, via a 1-1 reduction.
- Recursive types. Some of these type only strongly normalizing terms.
- 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

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.

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

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.

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