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