Ein berühmter Satz von Kurt Gödel, auch der „Gödel’sche Satz“ genannt, besagt:
1) „Das System S ist nicht entscheidungsdefinit, d. h. es gibt darin Sätze A (und solche sind auch angebbar), für welche weder A noch ~A beweisbar ist.“
2) „Ein Widerspruchsfreiheitsbeweis des Systems S kann also nur mit Hilfe von Schlußweisen geführt werden, die im System S selbst nicht formalisiert sind, und Analoges gilt auch für andere formale Systeme, etwa das Zermelo-Fränkelsche Axiomensystem der Mengenlehre.“ (Kurt Gödel, Einige metamathematische Resultate über Entscheidungsdefinitheit und Widerspruchsfreiheit, Sätze I u. II).
Ich interpretiere das folgendermaßen:
1) Ein formales Axiomensystem kann als ein widerspruchsfreies nur erwiesen werden mit „Schlußweisen“, die in dem System selbst „nicht formalisiert sind“, wie Gödel im zweiten Satz ausdrücklich schreibt. Mit anderen Worten, dieses System kann ein erwiesenermaßen widerspruchsfreies nur sein, indem es externe Beweisgründe unterstellt.
2) Indem dieses System externe Beweisgründe unterstellt, kann es nicht vollständig, nicht universell sein.
3) Das heißt: Entweder dieses System ist universell, und dann kann es nicht erwiesenermaßen widerspruchsfrei ausfallen, oder es fällt erwiesenermaßen widerspruchsfrei aus, dann aber muß es auf externe Beweisgründe bauen und kann mithin nicht universell sein.