Master Class, Master Class 1998/1999, Detailed Course Content
Detailed Content of the Courses
Model Theory - W. Veldman
Lambda Calculus - H. Barendregt, E. Barendsen
Recursion Theory and Proof Theory - H. Schellinx
Logic Panorama - seminar
Type Theory and Applications - H. Barendregt, E. Barendsen
Incompleteness Theorems - J. van Oosten
Sheaves and Logics - I. Moerdijk
Mathematical Logic - seminar
Name of the course: Model Theory
Lecturer: W. Veldman
Prerequisites: Some familiarity with mathematical reasoning.
Literature: C.C. Chang, H.J. Keisler, Model Theory, North Holland
Publ. Co. 1977 W. Hodges, Model Theory, Cambridge UP, 1993
theory studies the variety of mathematical structures that satisfy given
formal theory. It may also be described as a study of mathematical structures
from the logician's point of view. Model theory at its best is a delightful
blend of abstract and concrete reasoning. Among the topics to be treated
in this course are Fraisse's characterisation of the notion 'elementary
equivalence' (structures A,B are called elementarily equivalent if they
satisfy the same first-order-sentences), the compactness theorem and its
many consequences, ultraproducts, some non-standard-analysis, Tarski's
decision method for the field of real numbers by quantifier elimination
and Robinson's notion of model completeness. If time permits, some attention
will be given to constructive and recursive model theory.
Name of the course: Lambda Caluculus
Lectures: Henk Barendregt and Erik Barendsen Computing Science
Institute, University of Nijmegen
Prerequisites: Basic recursion theory (characterisation of computable
functions, semi- decidability, (un)decidability), complete partial orders.
The lambda calculus is a mathematical theory of computable functions.
Lambda calculus gives representations of algorithms and of constructive
proofs. Nowadays, the lambda calculus, especially in combination with
type systems, plays a central role in logic and computer science. Important
applications are functional programming languages and proof development
systems. This course gives an overview of aspects of the type-free lambda
calculus and an introduction to typed lambda calculus. It covers beta
conversion and reduction, representation of data types and computable
functions, reduction strategies (operational semantics), models (denotational
semantics), self-interpretation, undecidability issues and simple type
Name of the course: Recursion Theory and
Lecturer: H. Schellinx
In this 'two-in-one-course' we start by introducing the students to the
elementary notions of general recursion theory - primitive recursion,
(Turing)-computability of (partial) functions of natural numbers, general
recursion, recursive enumerability - and prove some of the basic theorems.
We then turn to proof theory, and introduce the sequent calculi for classical
and intuitionistic first order logic as well as the basics of linear logic.
We prove Gentzen's cut elimination theorem, using a notion of 'reduction
of proofs' related to that of the so called 'proof nets' for linear logic.
If time permits we will sketch Gentzen's proof of the consistency of arithmetic.
Seminar: Logic Panorama
Prerequisites: predicate logic
The logic panorama will introduce the student to the many varieties of
logical research. Possible topics include set theory and ordinal numbers,
intuitionistic logic and Kripke models, categories, Boolean algebra's,
modal logic, rewrite systems, linear logic, etc.
Name of the course: Type Theory and Applications
Lecturers: Henk Barendregt, Erik Barendsen and others Computing
Science Institute, University of Nijmegen
Prerequisites: Basic lambda calculus (beta reduction and conversion,
Church-Rosser, simple type assignment), logic (first and second-order
proposition and predicate logic), elementary recursion theory (computable
There are several typed versions of the lambda calculus. Type systems
usually have a computational and a logical interpretation. The former
setting is used to study types in programming languages; the latter gives
a representation of statements and (constructive) proofs of various logical
systems. This course is concerned with the logical and computational view
on type systems that are integrated in a seamless way. It covers systems
with explicit typing (simply typed lambda calculus, second-order lambda
calculus, dependent types and pure type systems), normalisation, representation
of logic and computations, inductive types, proof assistants, vision on
Name of the course: Incompleteness Theorems
Lecturer: J. van Oosten
Prerequisites: basic predicate logic (in particular, the Godel
completeness theorem) and basic recursion theory (primitive recursion,
general recursive functions)
The formal system of first order arithmetic PA - Representation of primitive
recursive functions in PA - Arithmetization of proofs - Diagonalization
and Godel's first incompleteness theorem - Sigma-1-completeness and Godel's
second incompleteness theorem - Theorems of Rosser and Lob. If time permits,
either: Introduction to the model theory of PA, or: Introduction to the
provability logic of PA, and Guaspari-Solovay completeness theorem for
Name of the course: Sheaves and Logic
Lecturer: I. Moerdijk
Prerequisites: familiarity with predicate logic, basic topology.
Literature: S. MacLane, I. Moerdijk, Sheaves in Logic and Geometry.
In this course it will be explained how presheaves and sheaves can be
used to construct natural models of (higher order) logic. We will study
specific applications to models of intuitionistic logic, as well as to
proof theoretic properties of intuitionistic logic. We will also give
sheaftheoretic proofs of some independence results in set theory, such
as the independence of the axiom of choice. The course will also treat
some aspects of topos theory.
Seminar Mathematical Logic
This will partly be a continuation of the Logic Panorama. Students
will present some selected papers in mathematical logic.
Lecturers: H. Barendregt , J. van Oosten , E. Barendsen ,H.A.J.M.
Schellinx ,I. Moerdijk, W. Veldman