Sur les questions méthodologiques actuelles de la théorie hilbertienne de la démonstration. (Q2579575)

Bekanntlich hat die Beweistheorie eine Krise durchgemacht, welche durch die Entdeckung verursacht wurde, daß bereits zum Beweis der Widerspruchsfreiheit der Arithmetik wesentlich stärkere Hilfsmittel nötig sind als die Hilbertsche ``finite Einstellung''. Daß dieser Finitismus mit dem Brouwerschen Intuitionismus nicht gleichwertig ist, folgt aus dem Gödelschen Satz, daß die Aussagen der klassischen Arithmetik so gedeutet werden können, daß sie intuitionistisch beweisbar werden. Bernays erwähnt auch nebenbei die rekursive Arithmetik; diese ist noch rein finitistisch. Weiter gibt er Beispiele von finiten und nicht-finiten Betrachtungen. Er geht genauer auf die Überlegungen im Gentzenschen Beweis für die Widerspruchsfreiheit der Arithmetik ein, indem er erklärt, in welcher Art diese über die ursprüngliche finite Einstellung hinausgehen. Da solche stärkere Beweismittel nötig sind, meint er, daß man die Forderung der Evidenz und Sicherheit nicht zu eng fassen muß. In der nachfolgenden Diskussion gab Bernays ein Beispiel für den Unterschied zwischen einem finitistischen und einem intuitionistischen Beweis. Im zweiten kamen Implikationen mit einer Absurdität als Vorderglied vor. Wegen des letzten Umstandes bemerkte Wavre, daß er diesen Beweis nicht als intuitionistisch richtig ansehen könne. Danach gaben Burckhardt und Finsler eine Verteidigung des nichtformalen Denkens und der absolutistisch-mengentheoretischen Auffassung Finslers. Ref., der auch an der Diskussion teilnahm, meinte, daß exaktes Denken nur in formaler Weise möglich sei. Bernays bemerkte, daß die Cantorsche Mengenlehre intuitiv sei und deshalb nicht mit der Finslerschen identisch ist. Zum Schlusse sagte der Präsident Gonseth, daß die Arbeiten von Bernays wohl formalistisch wären, daß er aber andererseits bei der Aufstellung jedes Formalismus stets intuitive Direktiven vor Augen gehabt hätte.