Zentrum für interdisziplinäre Forschung
 
 
Plakat

ZiF-Arbeitsgemeinschaft

FoMUS: Foundations of Mathematics: Univalent Foundations and Set Theory

Termin: 18. – 23. Juli 2016

Leitung: Balthasar Grabmayr (Berlin, GER), Deborah Kant (Berlin, GER), Lukas Kühne (Bonn, GER), Deniz Sarikaya (Hamburg, GER), Mira Viehstädt (Hamburg, GER)

Spätestens mit Bernard Bolzano begannen MathematikerInnen ihren modernen präzisen Stil zu entwickeln. Grund hierfür waren unter anderem begriffliche Streitigkeiten (beispielsweise was genau ist eine Funktion oder sind die reellen Zahlen). Es zeigte sich, dass die Mengenlehre (oder ihr formales Gegenstück ZFC, d.h. die Zermelo-Fraenkel-Axiomatisierung der Mengenlehre mit Auswahlaxiom) eine Sprache und Theorie bietet, in der alle mathematischen Gebiete rekonstruiert werden können. Mit anderen Worten: ZFC ist eine Grundlegung der Mathematik. Diese Rolle wird ihr innerhalb der Mathematikergemeinschaft weitgehend unangefochten zugesprochen. In den letzten Jahren formiert sich jedoch eine wachsende Gruppe an Forschern, unter anderem um den Fields-Medaillisten Vladimir Voevodsky, die an den sogenannten Univalent Foundations (UF), einer alternativen Grundlegung der Mathematik arbeitet. Dieser neue Ansatz basiert auf der Homotopietypentheorie (HoTT), einer Verbindung der intuitionistischen Typentheorie Per Martin-Löfs mit der Homotopietheorie der Topologie.

Diese Entwicklung diente als stimulierende Ausgangslage dieser Arbeitsgruppe. Als zentrale Frage wurde diskutiert, was eine adäquate Grundlegung der Mathematik ausmacht und welchen Anforderungen sie entsprechen sollte. Diese Fragestellung wurde interdisziplinär vor dem Hintergrund der Mathematik, Philosophie und Informatik behandelt. Im Rahmen eines sechstägigen Workshops wurden die Grundlegungen ZFC und UF in ihren Grundzügen vorgestellt und in Vorträgen und Diskussionen gegenübergestellt. Darüber hinaus erörterten Philosophen der Mathematik die grundsätzlichen Anforderungen einer guten Grundlegung der Mathematik, ihrer Grenzen und Natürlichkeit. Eine wichtige Frage war zudem, ob ein Wechsel der Grundlegung der Mathematik als Revolution in der Mathematik aufgefasst werden kann. Zusätzlich wurde der Frage nach einer im Computer implementierbaren Grundlegung nachgegangen, die hinsichtlich der rasanten Entwicklung von maschinengestützten Beweissystemen (wie beispielsweise Coq) von hoher praktischer Relevanz für zukünftige Generationen von MathematikerInnen ist.

Das Programm bestand aus einer einführenden Hälfte, die den Charakter einer Sommerschule hatte, und einem fortgeschrittenen Teil, der als Forschungstagung konzipiert wurde. Im ersten Teil wurden in fünf einführenden Vorlesungen sowie fünf Workshops wesentliche Konzepte und Techniken aus Mengenlehre und HoTT vorgestellt, womit auch für weniger fortgeschrittene Teilnehmer eine hinreichende Wissensbasis für die Teilnahme am forschungsorientierten Teil geschaffen wurde. Dieser bestand aus 14 Vorträgen sowie zwei Podiumsdiskussionen. Aus mathematischer Sicht wurden u.a. verschiedene Identitätsbegriffe in UF und deren Verhältnis zur Isomorphie behandelt. Zusätzlich wurden neue beweistheoretische Eigenschaften von formalen Ausarbeitungen von UF vorgestellt, die in weiterer Folge zu mengentheoretischen Axiomatisierungen in Beziehung gesetzt wurden. Es wurden ferner sowohl mathematische als auch philosophische Positionen zur Multiversen Ansicht aus der Philosophie der Mengenlehre erörtert. Zudem wurden mögliche Grenzen von UF als Grundlegung anhand eines Beispiels aus der topologischen unendlichen Graphentheorie diskutiert. Einen informatischen Schwerpunkt stellten Beiträge zur Formalisierbarkeit von Mengenlehre mittels des interaktiven Theorembeweisers Isabelle dar.

Angeregt erörtert wurden diese Themen in zwei Podiumsdiskussionen, eine zu mathematischen, die andere zu philosophischen Aspekten von Adäquatheitskriterien von Grundlegungen. Zusätzlich wurden in Ad-Hoc-Meetings in kleineren Gruppen Inhalte des Workshops aufgegriffen und vertiefend diskutiert.

Weitere Sponsoren dieses Workshops waren die Association for Symbolic Logic (ASL), die Deutsche Mathematiker-Vereinigung (DMV), die Berlin Mathematical School (BMS), die Deutsche Vereinigung für Mathematische Logik und für Grundlagenforschung der Exakten Wissenschaften (DVMLG), die Studienstiftung des deutschen Volkes (Stipendiaten machen Programm), der Fachbereich Grundlagen der Informatik der Gesellschaft für Informatik (GI) und die Gesellschaft für Analytische Philosophie (GAP).

Teilnehmerinnen und Teilnehmer

Sadjad Abolfathi (Teheran, IRI), Benedikt Ahrens (Nantes, FRA), Thorsten Altenkirch (Nottingham, GBR), Clemens Ballarin (Karlsruhe, GER), Jonas Betzendahl (Bielefeld, GER), Marc Bezem (Bergen, NOR), Alexander C. Block (Hamburg, GER), Tobias Boege (Magdeburg, GER), Roland Bolz (Berlin, GER), Nathan Bowler (Hamburg, GER), Fortune Buchholtz (Pittsburgh, USA), Ulrike Buchholtz (Pittsburgh, USA), Mirna Dźamonja (Norwich, GBR), Ionna Matilde Dimitriou Henriquez (Bonn, GER), Anton Golov (Utrecht, NED), Rafal Gruszczynski (Toruń, POL), Regula Krapf (Bonn, GER), James Ladyman (Bristol, GBR), Benedikt Löwe (Amsterdam, NED), Robart Lubarsky (Boca Raton, USA), Paige North (Cambridge, GBR), Andrew M. Pitts (Cambridge, GBR), Michael Rathjen (Leeds, GBR), Andrei Rodin (Moskau, RUS), Urs Schreiber (Bonn, GER), Samuel Speight (Pittsburgh, USA), Bas Spitters (Aarhaus, DEN), Thomas Streicher (Darmstadt, GER), Claudio Ternullo (Wien, AUT), Vladimir Voevodsky (Princeton, USA), Philip David Welch (Bristol, GBR), Sayed Yarandi (Santa Barbara, USA)



Drucken
ZiF - Zentrum für interdisziplinäre Forschung - Startseite > AG > ZiF-Arbeitsgemeinschaften 2016 >