Algebra Seminar talk
2026-10-09
Alexander Klenner
Konstruktive Mathematik am Beispiel der Heyting-Arithmetik
Abstract:
Wir arbeiten in einem konstruktiven Beweiskalkül, das klassische Tautologien, wie $A \lor \lnot A$ oder $\lnot \lnot A \to A$, ohne Weiteres nicht beweisen kann. Eine solche Einschränkung führt dazu, dass wir zwar oft weniger beweisen können, aber es uns möglich ist, wesentlich stärkere beweistheoretische Aussagen zu treffen. Diesen Vorteil werden wir im Rahmen der konstruktiven Heyting-Arithmetik ($\mathrm{HA}$) weiter untersuchen und unter anderem relative Konsistenzaussagen in Bezug auf die Peano-Arithmetik treffen. Schließlich werden wir zeigen, dass man den Zeugen zu jeder Existenzaussage $\exists x \varphi(x)$, die wir in $\mathrm{HA}$ beweisen können, auch algorithmisch durch eine berechenbare Funktion ermitteln kann und dass diese aus dem Beweis von $\exists x \varphi(x)$ hervorgeht.