News
19.10.2018

Timeslot Change and TopicsFrom week 3 the seminar will move to the Tuesday 1618 time slot. The first Tuesday session will be October 30, as we meet next week still on Thursday at 16:30 (!!!). You should also have received some information about your participation and topic, in case you... Read more From week 3 the seminar will move to the Tuesday 1618 time slot. The first Tuesday session will be October 30, as we meet next week still on Thursday at 16:30 (!!!). You should also have received some information about your participation and topic, in case you feel like you were missed please just contact me.

18.10.2018

OrganisationJust a reminder that the next seminar session will take place next Thursday 16:3018:00. Please note that we have to shift by 15min from the usual c.t. as the room is blocked beforehand. Also, you can now indicate your preferences concerning the regular time slot... Read more Just a reminder that the next seminar session will take place next Thursday 16:3018:00. Please note that we have to shift by 15min from the usual c.t. as the room is blocked beforehand. Also, you can now indicate your preferences concerning the regular time slot on your personal status page. This will help us find the best option promptly. I've just uploaded the slides from today's presentations about the organisation and content of this seminar. You can find them in the Materials section, where we will upload all future slide sets and texts. 
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 finetuned 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 MartinLö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  firstorder vs. higherorder, 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 computermechanizability 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:1517:45. Available timeslots for the regualar sessions are as follows:
 Tuesday 1618
 Thursday 1416
 Thursday 1618
Once registered in this course system, students can indicate their preferences.