Als ich studiert habe, waren Vorlesungen mit Gödel und mit Kohomologie immer die beliebtesten. Daher geht’s heute mal wieder um Gödel und den Unvollständigkeitssatz. Um den hinzubekommen, muss man aber erst die Mathematik durchnummerieren, und zwar nicht wie Graf Zahl, sondern so, dass man aus den Zahlen auch wieder die Aussagen zurückberechnen kann. Von da aus ist es nicht mehr weit zu Quines — Computerprogrammen, die ihren eigenen Quelltext ausgeben.
- Graf Zahl zählt Hotdogs (YouTube)
- Neinhorn
- Über formal unentscheidbare Sätze (Gödel, 1931)
- Gödels Theorem auf Goodreads
- Gödel, Einstein und die Folgen (Rezension auf spektrum.de)
- Das Paris-Harrington-Theorem ist wahr aber nicht beweisbar.
- Quine-Programme
- Rice-Theorem
- Gödels Theorem (Peter Cameron)
Feedback gerne an feedback (bei) eigenpod.de oder in die Kommentare unten.
Fun Fact: Nicht immer kann man tatsächlich berechnen, ob etwas ein gültiges Programm ist, die Syntax von C++ ist beispielsweise unentscheidbar.
Ich habe den Beweis nicht mehr komplett im Kopf, das hat mir mal ein befreundeter Informatiker erzählt, aber es läuft darauf hinaus, dass man in das Template-System von cpp (so heißen generics in cpp) eine allgemeine Turingmaschine embedden kann. So bekommt man eine Reduktion auf das Halteproblem.
Moderne Compiler lösen das so, dass sie nach einer bestimmten Rekursionstiefe einfach einen Error werfen, da das in der Praxis aller Wahrscheinlichkeit nach ein Programmierfehler ist. Technisch gesehen verletzen sie damit aber die cpp-Spezifikation.
LG
Interessant. Wenn das so ist, dann gibt es da bestimmt noch viele andere unentscheidbare Dinge. Wie wäre es mit Syntax-Highlighting? Z.B. kann man in LaTeX in einer Mathe-Umgebung wieder eine normale Text-Umgebung öffnen und darin wieder eine Mathe-Umgebung usw. Ist es möglich im Editor alle Textbausteine korrekt einzufärben, sodass Mathe-Umgebungen eine andere Farbe haben als Text?
das ist vielleicht etwas gecheatet, aber LaTeX-Macros sind ja Turingvollständig, man könnte sich vermutlich ein Enviroment definieren, dass entweder ein equation- oder ein text-enviroment ist, je nachdem, was beim Halteproblem herauskommt. Das kann dann natürlich nicht korrekt gesyntax-highlightet werden.