Education,
Master Class, Master Class 1998/1999, Detailed Course Content
Detailed Content of the Courses
Course content
1st semester:
Model Theory  W. Veldman
Lambda Calculus  H. Barendregt, E. Barendsen
Recursion Theory and Proof Theory  H. Schellinx
Logic Panorama  seminar
2nd semester:
Type Theory and Applications  H. Barendregt, E. Barendsen
Incompleteness Theorems  J. van Oosten
Sheaves and Logics  I. Moerdijk
Mathematical Logic  seminar
Courses
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
Contents: Model
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 firstordersentences), the compactness theorem and its
many consequences, ultraproducts, some nonstandardanalysis, 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.
Top
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.
Contents:
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 typefree 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), selfinterpretation, undecidability issues and simple type
systems.
Top
Name of the course: Recursion Theory and
Proof Theory
Lecturer: H. Schellinx
Contents:
In this 'twoinonecourse' 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.
Top
Seminar: Logic Panorama
Lecturers: varying
Prerequisites: predicate logic
Contents:
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.
Top
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,
ChurchRosser, simple type assignment), logic (first and secondorder
proposition and predicate logic), elementary recursion theory (computable
functions, decidability).
Contents:
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, secondorder lambda
calculus, dependent types and pure type systems), normalisation, representation
of logic and computations, inductive types, proof assistants, vision on
'computer mathematics'.
Top
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)
Contents:
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  Sigma1completeness 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 GuaspariSolovay completeness theorem for
this logic.
Top
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.
Contents:
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.
Top
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
Top
