Bonn Mathematical Logic Group

Higher set theory (V4A3)
Formal Derivations and Natural Proofs


Time and location

Lecture: Tuesdays 16:00-18:00 in room 0.007, and Thursdays 16:00-18:00 in room 1.007, both in the main building in Endenicher Allee 60.
Exercice class: Thursday 12:15-13:45 in room 0.003, in the main building of Endenicher Allee 60.


This interdisciplinary course is centered around the topic of “mathematical proof”, involving formal logic, linguistics, computer science, and even philosophy of mathematics. It is recommended as a sequel to a standard Mathematical Logic course as read at the University of Bonn, or as a general advanced logic course. Due to its broad character it does not squarely fit into the classifications of Bachelor or Master courses. Formally it is classified as the Master module “Higher Set Theory, V4A3”, in view of set theory being a standard background theory for mathematical proofs. An exercise class will be offered. The course can be read as a preparation for the practical training course “Practical Project in Mathematical Logic”, P4A1.


Diese interdisziplinäre Vorlesung behandelt das Thema “mathematischer Beweis” aus Sicht der formalen Logik, Linguistic, Informatik und auch der Philosophie der Mathematik. Als Voraussetzung genügt eine Einführungsvorlesung in die Mathematische Logik. Wegen ihres übergreifenden Charakters passt die Vorlesung nicht genau in das Schema der üblichen Bachelor- und Mastervorlesungen. Formal wurde ihr das Master Modul “Higher Set Theory”, V4A3 zugeordnet, zumal Mengenlehre auch als Hintergrundtheorie mathematischer Beweise benutzt wird. Eine Übungsgruppe wird angeboten. Im Rahmen des Bachelorstudiums kann die Vorlesung im freien Wahlpflichtbereich eingesetzt werden. Sie ist eine gute Vorbereitung auf das “Praktikum Mathematische Logik”, P2A1. Weitere Fragen zur Einordnung in das Bachelorstudium können mit dem Dozenten besprochen werden.


Formal logic models argumentative methods (in idealised domains). Apparently, formal derivations are very different from ordinary mathematical proofs. This lecture course examines both perspectives in detail, with the intention of bridging the gap. On the formal side we present calculi and proof algorithms designed for naturality and efficiency. We also present various systems of formal mathematics. On the other hand we study the common language of mathematics and show how methods of formal linguistics may be used to restrict to a controlled natural language with a definite formal interpretation. The lecture course provides theoretical foundations for the Naproche system (Natural language proof checking) which is being developed at Bonn (see The course also introduces the theory of logic programming and uses the Prolog programming language.

Topics include


The script will be updated weekly so check again in the end of each week.

Exercise sheets

A pdf with the contents of the lecture can be found by clicking here.

Last changed: 2 September 2010