Borel-Determiniertheit aus der Beweistheorie

Das Borel Determiniertheitstheorem ist ein Resultat der unendlichen Spieltheorie, bewiesen von D. A. Martin [Borel Determinacy. Annals of Mathematics 102 (1975), pp. 363-371]. Es besagt, dass eine reichhaltige Familie von Zwei-Spieler Nullsummenspielen mit perfekter Information bestimmt ist, in dem Sinn, dass immer einer der Spieler eine Gewinnstrategie besitzt. Die Schwierigkeit beim Finden des Beweises wird durch ein meta-mathematisches Resultat von H. M. Friedman [Higher Set Theory and Mathematical Practice. Annals of Mathematical Logic 3 (1971), pp. 325-357] erklärt, welches besagt, dass jeder Beweis der Borel Determiniertheit essenziellen Gebruach aller Axiome der Mengenlehre machen muss. Unter anderem aufgrund dieser starken Einschränkung ist bisher kein weiterer Beweis des Resultats bekannt. Ziel dieses Projekts ist es, einen solchen mithilfe beweistheoretischer Methoden zu finden, indem eine starke Version von Gentzens Hauptsatz etabliert wird.