Automatisches Beweisen?
Kann man einen Algorithmus entwickeln, der alle wahren mathematischen Aussagen in einem gegebenen formalen System findet?
5 Antworten
Nur dann wenn das formale System rekursiv aufzählbar ist. Und selbst dann muss das System noch lange nicht entscheidbar sein, d.h. es ist dann ggf. Imner noch nicht möglich zu einer gegebenen wohlfeformten Aussage des Systems ihre Gültigkeit zu zeigen.
Das kommt darauf an, um welches formale System es sich handelt. Für das Axiomensystem der Aussagenlogik beispielsweise läßt sich ein Algorithmus entwickeln, der entscheidet, ob eine Aussage beweisbar ist oder nicht und somit auch, ob sie wahr ist oder nicht, da das Axiomensystem der Aussagenlogik korrekt und vollständig ist. In stärkeren formalen Systemen der Logik und der Mathematik ist dies jedoch nicht der Fall. Bereits die Prädikatenlogik 1. Stufe ist nicht entscheidbar, d.h. ein Beweisalgorithmus gibt auf die Frage, ob eine Aussage beweisbar ist oder nicht, nicht immer eine Antwort. Die Prädikatenlogik 1. Stufe ist allerdings semi-entscheidbar, d.h. wenn eine Aussage beweisbar ist, gibt der Algorithmus immer nach endlicher Zeit die Antwort, daß sie beweisbar ist (und somit auch wahr ist, da das Axiomensystem korrekt ist). Bei nicht beweisbaren Aussagen (die somit auch nicht wahr sind, da das Axiomensystem vollständig ist) dagegen kann es vorkommen, daß der Algorithmus keine Antwort gibt. In Prädikatenlogiken höherer Stufen ebenso wie in der Mengenlehre, der Zahlentheorie etc. ist die Situation noch schlimmer: Die sind erstens nicht mal semi-entscheidbar, d.h. es gibt auch beweisbare Aussagen, die der Algorithmus nicht als solche erkennt, und zweitens nicht vollständig, d.h. auch wenn eine Aussage nicht beweisbar ist, kann es trotzdem sein, daß sie wahr ist.
Nicht alle, aber zum Beispiel ein paar Beweise kann auch eine KI wie zum Beispiel ChatGPT. Probier's mal aus. ;)
Würde wahrscheinlich gehen, ja. Man muss nur eben dem Programm sagen was richtig und was falsch ist.
Es ist bei rekursiv aufzählbaren Systemen sehr wohl möglich einen Algorithmus zu konstruieren der irgendwann jede gültige Aussage produziert. Das Problem liegt in der Umkehrung.
Beachte das Gödels Satz für Systeme gilt, die der Bedingung "Hinreichen mächtig" genügen. Demgegenüber ist die Prädikatenlogig Erster Stufe vollständig.
https://de.m.wikipedia.org/wiki/G%C3%B6delscher_Vollst%C3%A4ndigkeitssatz