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

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

Top

Name of the course: Recursion Theory and Proof Theory
Lecturer: H. Schellinx

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

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, Church-Rosser, simple type assignment), logic (first and second-order 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, second-order 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 - 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 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