| Kommentar |
Abstract
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 theorist took a somewhat more pragmatic approach to prevent paradoxes. All 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 settled (and Gödel's results further fueled but did not resolve the debate).
However, a lot has improved since then: Our understanding and knowledge of logic, type 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 a set- and a type-theoretical perspective, respectively. 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.
Audience
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 part in the seminar only if they have a technical minor (mathematics, computer science, physics, etc.) or an explicit interest in technical details and if they previously attended the lecture ”Einführung in die Sprachphilosophie und Logik”.
Mode
The first half of the seminar will consist of technical talks following the introductory presentation of axiomatic set theory and dependent type theory in [1]. After each session, a problem sheet will be handed out for home work such that the participants have the opportunity to practise the learned material. The problems will be discussed in the next session.
In the second half, the more conceptual talks comparing isolated aspects of both systems should be based on the relevant papers mentioned in the outline and the overview sections in [1]. Instead of a discussion of problem sheets, the talks are followed by an evaluation of the main theses from the talk.
Students who want to earn credits 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 talks. Afterwards, the 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. We suggest that students in computer science choose topics from the first half whereas the second half is subject to the students in philosophy.
The seminar will take place weekly, the first session will be Thursday 18th October 2018, 16:15-17:45, which is our preferred time slot; however, it can be changed, if there is demand for that.
For further information, please visit the following site: https://courses.ps.uni-saarland.de/fom_ws1819/
Outline
1. Organisation, motivation, introduction
2. First-order logic (Section 2.1 in [1])
3. ZF set theory (Sections 2.2.1 - 2.2.2 in [1])
4. Peano arithmetic in ZF (Section 2.2.3 in [1])
5. Untyped lambda calculus (Sections 3.1.1 - 3.1.2 in [1])
6. Simply typed lambda calculus (Sections 3.1.3 - 3.1.4 in [1])
7. Martin-Löf type theory (Sections 3.2.1 - 3.2.3 in [1])
8. Peano arithmetic in MLTT (Section 3.2.4 in [1])
9. Discussion round, Q&A, accessibility, technical solution
10. Classical vs. intuitionistic logic ([2, 3] vs. [4, 5])
11. First-order vs. higher-order logic ([6] vs. [7])
12. Mechanizability: Optimism [8, 9]
13. Mechanizability: Analysis [10, 11]
14. Hilbert reloaded [12, 13]
15. Limitations [14]
16. Optional: relative consistency, alternatives, background [15]
References
[1] Dominik Kirst: Foundations of Mathematics: A Discussion of Sets and Types, 2018. Bachelor’s thesis. URL = <;http://www.ps.uni-saarland.de/~kirst/hok/thesis.pdf>;
[2] Ian Rumfitt: The Boundary Stones of Thought: An Essay in the Philosophy of Logic, OUP, 2015.
[3] Willard Van Orman Quine: Philosophy of Logic, second edition, Prentice-Hall, 1986.
[4] Errett Bishop: Foundations of Constructive Analysis, Ishi Press International, July 1967.
[5] Andrej Bauer: ”Five stages of accepting constructive mathematics”, Bulletin of the American Mathematical Society 54.3, 2017, pp.481–498.
[6] Thoralf Skolem: Einige Bemerkungen zur Axiomatischen Begründung der Mengenlehre, Verlag 1922, pp. 137-52. In: Jean van Heijenoort: From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931. Harvard University Press 1967. pages 137–52.
[7] Jouko Väänänen: ”Second-Order Logic and Foundations of Mathematics”, The Bulletin of Symbolic Logic 7(4), 2001, pp. 504–20.
[8] Randy Pollack: ”How to Believe a Machine-Checked Proof”, BRICS Report Series 97, July 1997.
[9] Penelope Maddy: ”What do we want a foundation to do? Comparing set theoretic, category-theoretic, and univalent approaches” forthcoming in S. Centrone, D. Kant, and D. Sarikaya (eds.): What Are Criteria for a Suitable Foundation of Mathematics?, Synthese Library, Springer.
[10] O. Bradley Bassler: ”Surveyability of Mathematial Proof: A Historic Perspective”, Synthese 148.1, 2006, pp.99-133.
[11] Hannes Leitgeb: "On Formal and Informal Provability", in Linnebo, Bueno (ed.), New Waves in Philosophy of Mathematics, Palgrave Macmillan, 2009, pp. 263-299.
[12] Stephen G. Simpson: ”Partial Realizations of Hilbert's Programm”, JSL 53.2, 1988, pp.349-363.
[13] Wilfried Sieg: Hilbert's Programs and Beyond, OUP, 2013.
[14] Michael Rathjen: ”The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory”, Synthese 147.1, 2005, pp. 81-120.
[15] John Burgess: Rigor and Structure, OUP, 2015. |
