Seminar: Foundations of Mathematics Wilfried Keller, Dominik Kirst, Gert Smolka

Seminar, Winter Semester 2018

An Introduction to Sets and Types

Orthodoxy has it that the ambitious project of laying the foundation of mathematics (or at least of arithmetic and analysis) in pure logic (or some sort of set or class theory), provided with suitable definitions of mathematical expressions, got into trouble at the turn of the 20th century by running into paradoxes (most notably Russell's antinomies). In reaction, the Logicists modified their approach by introducing a (ramified) hierarchy of types (in order to avoid impredicativity, which was blamed for the paradoxes), while the set theorists took a somewhat more pragmatic approach to prevent paradoxes. All of this was deemed insufficient by Brouwer who advocated revolution: Only constructive methods should be allowed, only those covered by 'intuition', hence 'Intuitionism'. Finally, Hilbert and his school tried 'Münchhausen's trick' and wanted mathematics to save itself from contradiction by rigorous but finitary proof theory. This conflict never got completely resolved (and Gödel's results in fact established the unsolvability by purely formal means).

However, a lot has improved since then: Our understanding and knowledge of logic, type theory and set theory has considerably grown, as has the repertoire of fine-tuned techniques of building foundations. And finally some mixing of ideas has taken place and a new generation of foundational strategies (and systems) has been developed. In the course of this seminar we will focus on two direct approaches of providing a uniform foundation: The more classical way of set theoretic reduction will be compared to the constructive approach pioneered by Per Martin-Löf using his dependent type theory. Both provide a sophisticated, expressive and comprehensive framework in which to build up the whole of mathematics.

At first, we will have a close look on these foundations, i.e. we will start by working out the basic techniques applicable in the respective foundational settings. The test case will, of course, be arithmetics, i.e. we will develop the very rudiments of number theory from set- and type theoretical perspective. Getting some familiarity with these 'mechanics' is essential for competently evaluating the merits and success of each programme.

In the second part of the seminar, we will turn to the more philosophical side, by trying to contrast foundations in the technical sense (that very sense we tried to elaborate before) with a philosophical sense, i.e. a set of criteria and questions, that a proper foundation should meet and enable us to answer. Among these will be traditional ones concerning epistemology, certainty and ontology (and some old disputes that carry over, mutatis mutandis, like questions concerning logic - first-order vs. higher-order, classical vs. intuitionistic), but also more recent ones: How accessible are the respective frameworks, how well do they fit to current mathematical practice? Quite recently, the question of computer-mechanizability has become prominent; it integrates with older questions (concerning the preciseness ['Bündigkeit'] of proof, e.g.), but is accompanied by a host of rather new questions. This topic will be a further focal point of the seminar. But in the end we might even shake things up a bit by throwing some heir to Hilbert's programme into the mix.

Credit

Official credit for the seminar is achievable for students in philosophy (as a bachelor seminar) and computer science (as a seminar). Interested students from neighbouring fields are welcome to attend all sessions. As particularly the first half of the seminar has a rather formal character, we recommend that students in philosophy take the seminar if they have a technical minor (mathematics, computer science, physics, etc.) or an explicit interest in technical details, and if they previously took the lecture "Sprachphilosophie und Logik".

Students who want to get credit for the seminar need to host one of the sessions listed in the outline. This means they either prepare a technical talk, formulate at least 3 suitable exercises, and lead the discussion in the following week, or they prepare a conceptual talk, formulate at least 3 theses, and lead the discussion right after their talk. Afterwards, the given talk or a related topic has to be summarized in a short (10 pages) report. We expect that all participants read the core material for every session and try to solve the problem sheets.

Organisation

The seminar will take place weekly in room 528 in building E1.3 in a time slot to be fixed at the first meeting. The first meeting will take place on Thursday, October 18, 16:15-17:45. Available timeslots for the regualar sessions are as follows:

• Tuesday 16-18
• Thursday 14-16
• Thursday 16-18

Once registered in this course system, students can indicate their preferences.