Higher set theory (V4A3)
Formal Derivations and Natural Proofs

Lecturer

• Prof.Dr. Peter Koepke (Lectures)
• Ioanna Dimitriou (Exercises)

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.

Remark

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.

Vorbemerkung

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.

Contents

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 http://www.naproche.net). The course also introduces the theory of logic programming and uses the Prolog programming language.

Topics include

• review of standard first-order calculi
• a “natural language” first-order calculus
• analysing and processing simple natural language
• the resolution calculus and logic programming
• Prolog and natural language processing
• formal mathematics with a discussion of the underlying formal systems
• methods of automatic theorem proving
• ...
• the Naproche system

Script

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

Exercise sheets

• Exercise sheet 1 and its attachment. Solutions to be handed in on Thursday 21 October 2010.
• Exercise sheet 2. Solutions to be handed in on Thursday 28 October 2010.
• Exercise sheet 3. Solutions to be handed in on Thursday 4 November 2010.
• Exercise sheet 4. Solutions to be handed in on Thursday 11 November 2010.
• Exercise sheet 5. Solutions to be handed in on Thursday 18 November 2010.
• Exercise sheet 6. Solutions to be handed in on Thursday 25 November 2010.
• Exercise sheet 7. Solutions to be handed in on Thursday 9 December 2010.
• Exercise sheet 8. Solutions to be handed in on Thursday 16 December 2010.
• Exercise sheet 9. Solutions to be handed in on Tuesday 11 January 2011.
• Exercise sheet 10. Solutions to be handed in on Tuesday 20 January 2011.

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