Seminar: Konstruktive Analysis
Zeit und Ort
Mo 14-16, B252; Beginn Montag, 13. Oktober 2025. Bitte melden Sie sich im LSF an.Inhalt
Grundlage des Seminars sind Arbeiten "Yet another predicative completion of a uniform space" und "A constructive integration theory: a topological approach" von Hajime Ishihara, die auf einer konstruktiven Mengenlehre (ECST) aufbauen. Im Seminar soll stattdessen ein typentheoretischer Ansatz (TCF) verwendet werden, der auch eine Implementierung (in Minlog) ermöglicht. In den genannten Arbeiten geht es um(i) die Vervollständigung metrischer und uniformer Räume
(ii) Vektorverbände und
(iii) Anwendungen in der Integrationstheorie.
Die Beweise sollen auch in formalisierter Form geführt werden.
Vorausgesetzt werden Grundkenntnisse in Mathematischer Logik, mindestens in dem Umfang in dem sie in der im WS25/26 stattfindenden einführenden Logik-Vorlesung vermittelt werden. Ferner wird vorausgesetzt, daß die Teilnehmer das Tutorium des Beweisassistenten Minlog durchgearbeitet haben. Nach erfolgreichem Besuch des Seminars ist es möglich, eine Bachelor- oder Masterarbeit zu einem Thema aus diesem Umkreis zu schreiben.
Vorträge
Neben den genannten Arbeiten von Ishihara werden auch Teile eines Skripts verwendet, das Sie (auch) auf der Seminarseite finden. Es soll jeweils eine Übersicht über wichtige Definitionen und Theoreme gegeben werden, und an einer oder mehreren Stellen der Beweis am Rechner geführt werden. Ausserdem soll eine Textfassung der behandelten Gegenstände angefertigt werden, die dann als Abschnitt in das Seminarskript eingefügt werden kann.Literatur
Allgemein
- Bishop/Bridges, Constructive Analysis. Springer 1985.
- A. Bauer, Five stages of accepting constructive mathematics (Bull AMS, 2016)
- Handbook of Constructive Mathematics. Cambridge UP, 2023
Speziell
Sprechstunde
- Helmut Schwichtenberg, Mi 13-14, B434.