Anfang

Die Frage, die mich interessiert, lautet:

Welche Rolle kommt der Interpretation eines formalen Systems zu?

Mir scheint die eingangs zitierte Behauptung von Penrose richtig zu sein. Eine entsprechende Bemerkung findet sich auch bei S. Feferman [6]:

Mathematical thought as it is actually produced is not mechanical; I agree with Penrose that in this respect, understanding is essential, and it is just this aspect of actual mathematical thought that machines cannot share with us.

Während Penrose sich zur Stützung seiner These allerdings auf Gödel beruft, hält Feferman den Gödelschen Unvollständigkeitssatz in diesem Zusammenhang für irrelevant:

Though I am convinced of the extreme implausibility of a computational model of the mind, Penrose's Gödelian argument does nothing for me personally to bolster that point of view.

Beim Nachdenken über die o.g. Frage haben mich bislang die folgenden Punkte beschäftigt; vielleicht enthält die Liste etwas, über das es sich zu sprechen lohnt.

1. Bei interpretierten Systemen hat man `intuitiv' eine Idee, welche Sätze vermutlich wahr sind, und der formale Beweis (= Ableitung) wird dann im Nachherein gesucht.

   Die Suche nach einer formalen Ableitung ist natürlich nur bei nicht-entscheidbaren Systemen (Prädikatenlogik aufwärts) nicht-trivial. Wichtig ist aber, daß auch vollständige Systeme (ohne Gödel-Sätze) in der Regel nicht-entscheidbar sind. D.h. nicht die Unvollständigkeit schafft Probleme derart, daß man für einen vermutlich wahren Satz ggf. keinen Beweis findet, weil es nämlich aufgrund der Unvollständigkeit keinen gibt, sondern die Suche nach Beweisen ist immer dann ein Problem, wenn es kein Entscheidungsverfahren gibt.

2. Wenn die Axiome eines formalen Systems in einer gegebenen Interpretation wahr sind, muß man darüberhinaus noch die Wahrheitsbewahrung der Regeln voraussetzen, um sicher zu sein, daß auch die Theoreme wahr sein werden. Aber kann man überhaupt solche Regeln, wie sie in der Formulierung der Zahlentheorie verwendet werden, als wahrheitsbewahrend beweisen? Mithilfe welcher Art von Argumenten könnte das geschehen? Diese müßten selbst wieder gerechtfertigt werden.

   Wenn diese Frage gleichbedeutend ist mit der nach der Konsistenz des Systems, so hat Gödel die Antwort bereits gegeben: Es ist nicht möglich -- wie Hilbert vorhatte -- sich auf eine kleinere Menge an Axiomen und Regeln zu beschränken: Jedes System, das stark genug ist, die Konsistenz der Zahlentheorie zu zeigen, muß mindestens so stark wie die Zahlentheorie selbst sein [7], p. 230.

   Ist diese Aussage wiederum äquivalent damit, zu sagen: Man befolgt syntaktische Regeln and the semantics will take care of itself [8], p. 23?

3. Was ist eine `stimmige' Interpretation?

   Bei einer physikalischen Theorie werden die verwendeten Symbole so interpretiert, daß die Axiome als wahr gelten. Unter der Voraussetzung, daß die Ableitungsregeln wahrheitsbewahrend sind, ergeben sich Folgerungen, deren Wahrheit in der Natur überprüft werden kann. Abweichungen bedeuten, daß die Interpretation nicht `stimmig' ist oder daß die Axiome nicht wahr sind.

   Werden in der Mathematik die Symbole interpretiert? Und woran wird deren `Stimmigkeit' gemessen? Gibt es auch dort eine Vergleichsmöglichkeit? Wie Feferman [6] schreibt, ist die Frage, ob es in der Mathematik eine `beabsichtigte', `gemeinte', `intendierte' Interpretation gibt, umstritten. Im Vorwort zu einem klassischen Lehrbuch der Analysis [9] steht:

   Als weitere Konsequenz ergibt sich ferner die Notwendigkeit, sich strikt an axiomatische Methoden zu halten und sich in keiner Weise auf die ``geometrische Anschauung'' zu berufen, wenigstens in den formalen Beweisen. ...Nach meiner Meinung muß der fortgeschrittene Student unserer Tage so schnell wie möglich an den sicheren Gebrauch dieser abstrakten und axiomatischen Denkweise gewöhnt werden, wenn er jemals verstehen soll, was sich heute in der mathematischen Forschung abspielt.

   Ohne Interpretation (ob intendiert oder nicht) gibt es aber nicht die Möglichkeit der intuitiven Einsicht bzw. einer Idee, welche Sätze sich vermutlich als wahr erweisen werden.

4. Aufgrund wovon erkennen wir z.B. Gödel-Sätze als wahr?

   Feferman [6] verweist hierzu auf die von ihm entwickelte relativierte Form des Hilbertschen Programmes, nachdem er das Penrose-Argument und seine Kritik daran zusammengefaßt hat:

   The argument goes something as follows: how could we know that F [the formal system] is sound if we did not understand what F is about -- its intended interpretation -- and see that the axioms of F are all true of that interpretation and that its rules of inference all preserve truth? It is by such means, the argument continues, that we recognize the soundness of systems from PA [Peano Arithmetic] all the way up to ZF [Zermelo Fränkel] set theory and beyond. And once we recognize the soundness of a system F and accept it as part of the principles on which we can rely, we see that G(F) [Gödel Sentence of F] is true and must accept it too, and so by Gödel's theorem, we are required to accept something that goes beyond F.

   Two problems with this argument are that (i) there may be other ways of recognizing the truth of G(F) than through a global notion of truth for F, and (ii) the assumption of an intended interpretation for set-theoretical formalisms is highly problematic. The first is what is achieved by proof theory. ...Relativized proof theory yields verification of the consistency of a system F by reduction to the consistency of another system F', and progress is achieved thereby when one has more compelling reasons for accepting F' than F to begin with.

   In jedem Fall (so meine ich) legen wir eine Interpretation zugrunde.

   Denn halten wir nicht-ableitbare Sätze wie G(F) nicht erst aufgrund einer als stimmig unterlegten Interpretation für wahr?

   Daß wir uns bei dieser `Erkenntnis' nicht getäuscht haben, zeigen wir dann durch Ableitung in einem umfassenderen formalen System, denn in der Regel gelten nur Ableitungen in formalen Systemen als sichere Erkenntnisquelle, oder?

5. Der Gödel-Satz eines formalen Systems ist jedoch nicht in allen Interpretationen wahr. [10]

   Assuming consistency, Gödel's sentence is not simply true i.e. not in all interpretations (else it would be provable, by the completeness theorem, also proved by Gödel: provability is truth in all interpretations). The first theorem shows that if the system is consistent, it can be consistently extended with the negation of the Gödel sentence, which means that the sentence is actually false in some models of the system ... Gödel's theorem thus shows that there must always exist such unusual, unintended interpretations of the system; as Henkins says, quoted in [12]:

   We tend to reinterpret Gödel's incompleteness result as asserting not primarily a limitation on our ability to prove but rather on our ability to specify what we mean ...

   Wie kann man dann davon sprechen, daß er von außerhalb des Systems betrachtet als (allgemein) wahr erkannt wird?

6. Eine (unbewußte) Interpretation eines formalen Systems kann hinderlich oder förderlich sein:
   • Hinderlich ist sie wie im Beispiel Euklids, wenn man Assoziationen mit den Symbolen verbindet, die durch das formale System nicht gestützt werden.

   • Förderlich -- vielleicht gar notwendig -- ist sie, um - wie Penrose oder auch Feferman meinen - überhaupt wahre Sätze zu finden bzw. deren Wahrheit zu vermuten, was anschließend durch einen formalen Beweis gesichert wird.

7. Die Symbole eines formalen Systems haben `Bedeutung' in der Weise, daß sie miteinander in bestimmter formaler Beziehung stehen. Insofern legt ein formales System die Bedeutung der verwendeten Symbole fest, genauer ihr Zusammenwirken. Die Bedeutung einer natürlichen Zahl liegt darin, daß sie bestimmten Axiomen und einem bestimmten Regelkanon entspricht. D.h. jedes Element (der Realität), das sich ebenso verhält, ist eine natürliche Zahl. Vgl. Quine [11], pp. 44-45

   Numbers ...are known only by their laws, the laws of arithmetic, so that any constructs obeying those laws -- certain sets, for instance -- are eligible in turn as explications of number. [...]

   Arithmetic is ...all there is to number: there is no saying absolutely what the numbers are; there is only arithmetic.

   Eine wichtige Unterscheidung liegt zwischen der

   • impliziten Bedeutung, die durch Angabe der Axiome und Regeln festgelegt ist, und der

   • expliziten Bedeutung, die durch die Ausarbeitung des formalen Systems zu Theoremen und deren Beziehungen untereinander `erkannt' wird.

   Bedeutung haben Dinge/Symbole für uns, d.h. ihre Bedeutung ist von unserer Kenntnis abhängig und diese wiederum von der expliziten Kenntnis des gesamten Geflechtes/Netzes (bzw. eines größeren Teils), das die Zeichen und deren Regelwerk erzeugen.

   D.h. man `versteht' die Welt nicht dadurch, daß man eine (hypothetische) Weltformel und ggf. deren Anfangsbedingungen kennt, sondern erst durch das Netz von Folgerungen `versteht' man immer besser, was beispielsweise diese Formel `bedeutet'. Das Verständnis ist also essentiell abhängig von dem Hintergrund, in den etwas eingebettet wird. Daher gibt es auch kein umfassendes Verstehen, sondern stets wird nur eine Teilmenge erfaßt (bzw. konstruiert). (Der Hintergrund besteht zudem nicht nur aus gesichertem Wissen, sondern ggf. auch aus falschen Annahmen.) Ebenso wächst die Kenntnis und damit das Verständnis eines formalen Systems mit dessen Ausarbeitung / Entfaltung.

8. Wenn es für ein formales System mehrere sinnvolle Interpretationen gibt, d.h. Interpretationen, die die Axiome (Theoreme) zu wahren Sätzen machen, so hat man eine gemeinsame Struktur erkannt. Insb. wenn man eine gemeinsame Struktur für verschiedene Bereiche der Welt `entdeckt' hat, so vermutet man, daß diese Struktur nicht zufällig entstanden bzw. vorhanden ist, sondern `geschaffen' wurde. Erst durch eine Ordnung oder Struktur kann Information codiert und dadurch eine Interpretation ermöglicht werden. Auch ein formales System erzeugt eine Ordnung, d.h. Beziehungen zwischen den Symbolen, die dann interpretiert werden kann.

   Haben wir formale System geschaffen, um Ordnungsstrukturen abzubilden, die wir durch die Evolution und unsere Erfahrung mit der Welt bedingt schon intuitiv teilweise erfaßt haben? Durch den Versuch der Formalisierung werden dann auch neue Erkenntnisse generiert. Oder ist es immer so, daß wir zunächst intuitiv (informal) etwas vermutlich Wahres erfassen, das dann im zweiten Schritt ggf. als Theorem eines formalen Systems bewiesen wird? Ich meine, daß beides möglich ist und stattfindet:

   (a) Beweis neue Erkenntnis

   (b) Vermutung Beweis

   Die Interpretation ist in beiden Fällen unentbehrlich.

Ich hoffe, daß trotz der Unfertigkeit meiner Gedanken nicht völlig im Dunkeln geblieben ist, worüber ich mich bemüht habe nachzudenken.