Fixpunkttheorem – Wikipedia

Das Fixpunkttheorem (auch Fixpunktsatz oder Diagonalisierungslemma) ist ein Satz in der mathematischen Logik zur Beschreibung selbstreferenzieller Aussagen in formalen Theorien. Es wurde von Kurt Gödel 1931 zur Konstruktion seines Beweises der Unvollständigkeit logischer Systeme, die so ausdrucksstark sind, dass man damit die natürlichen Zahlen axiomatisieren kann, verwendet und damit implizit bewiesen, allerdings nicht explizit unter diesem Namen erwähnt. Das Theorem leitet sich von dem Diagonalisierungslemma ab, das so in Anlehnung an das Diagonalisierungsargument von Georg Cantor genannt wird.

Die formalisierte Objektsprache ist hierbei die Prädikatenlogik erster Stufe mit den Peano-Axiomen. Das Fixpunkttheorem besagt, dass es für jedes (einstellige) Prädikat eine Aussage gibt, die sich selbst dieses Prädikat zuschreibt. Diese Form der Selbstreferenz für das von ihm konstruierte Beweisbarkeitsprädikat Bew(x) ist – neben der objektsprachlichen Darstellung der Metasprache durch Gödelisierung – die Grundlage seines Beweises, indem gezeigt wird, dass der Satz „Dieser Satz ist nicht beweisbar“ bewiesen werden kann, was zum Widerspruch führt (Details s. dort).^[1][2]

Sei ${\displaystyle \varphi (x)}$ eine prädikatenlogische Formel mit der freien Variablen ${\displaystyle x}$. Dann existiert der prädikatenlogische Satz ${\displaystyle \psi }$ mit

${\displaystyle \psi \longleftrightarrow \varphi (\ulcorner \psi \urcorner )\quad }$, wobei ${\displaystyle \ulcorner \psi \urcorner }$ die Gödelnummer von ${\displaystyle \psi }$ ist.

Damit ist es möglich, in der Prädikatenlogik den Satz ${\displaystyle \varphi (\ulcorner \psi \urcorner )}$ zu bilden, der etwas über einen prädikatenlogischen Satz ${\displaystyle \psi }$ in seiner numerischen Repräsentation ausdrückt, d. h. metasprachliche Beziehungen können in der Objektsprache formuliert werden. Die Objektsprache sagt also etwas über sich selbst aus.^[3]

Alfred Tarski veröffentlichte 1936 sein Undefiniertheitstheorem, welches besagt, dass es in bestimmten formalen Systemen nicht möglich ist, ein Wahrheitsprädikat zu definieren. Die Beweisführung ist dabei ähnlich über die sog. Tarski-Sätze, selbstreferenzielle Sätze der Form: „ich bin ein Element von M“ für eine Menge M. Wählt man für M die Menge aller falschen Sätze eines Systems, führt die Konstruktion eines Tarski-Satzes zu einem Widerspruch bei der Definition dieser Menge. Daraus lässt sich folgern, dass die Menge aller wahren Sätze eines Systems nicht innerhalb dieses Systems definierbar ist.^[4]

Modallogische Instanzen^[5]

A(p)	Fixpunkt B
${\displaystyle \Box p}$	${\displaystyle \top }$
${\displaystyle \neg \Box p}$	${\displaystyle \neg \Box \bot }$
${\displaystyle \Box \neg p}$	${\displaystyle \Box \bot }$
${\displaystyle \Box p\rightarrow q}$	${\displaystyle \Box q\rightarrow q}$
${\displaystyle \Box (p\rightarrow q)}$	${\displaystyle \Box q}$
${\displaystyle q\lor \Box p}$	${\displaystyle \top }$[Anm. 1]
↑ Da schon ${\displaystyle \Box p}$ eine Tautologie ergibt.

In der Modallogik wird das Beweisbarkeitsprädikat von Gödel als Notwendigkeitszeichen ${\displaystyle \Box }$ (sprich Box) aufgefasst. Damit ergibt sich folgender Beweis des Fixpunkttheorems:

Ist ${\displaystyle A(p)}$ eine Formel, in der ${\displaystyle p}$ nur im Skopus einer Box vorkommt, dann gibt es eine Formel ${\displaystyle B}$, in der ${\displaystyle p}$ nicht vorkommt und keine Aussagenvariablen vorkommen, die nicht schon in ${\displaystyle A}$ vorkommen, so dass gilt:

${\displaystyle \vdash _{GL}B\longleftrightarrow A(p)}$.

Dabei heißt ${\displaystyle B}$ Fixpunkt von ${\displaystyle A(p)}$, GL steht für Gödel-Löb, eine Modallogik, die um den Satz von Löb als Axiom erweitert ist.

• Gödelscher Unvollständigkeitssatz
• Kalkül
• Beweis (Logik)

Wikibooks: Mathematik: Logik – Lern- und Lehrmaterialien

Wikibooks: Mathe für Nicht-Freaks: Aussagenlogik – Lern- und Lehrmaterialien

• Volker Beeh: Wahrheit, Theoremheit, Beweisbarkeit und die entsprechenden „Lügner-Sätze“. In: Zeitschrift für Sprachwissenschaft. 7,2 (1988), 151–172.
• Graeme Forbes: Logic, philosophy of. In: E. Craig (Hrsg.): Routledge Encyclopedia of Philosophy. London 1998. Geschichtliches auch zur Modallogik.
• Peter H. Starke: Logische Grundlagen der Informatik. Umfangreiches Skript, das auch als PDF downloadbar ist, HU Berlin.
• Michael Pucher: Formale Wahrheitstheorien nach Alfred Tarski (PDF), übersichtliche Diplomarbeit zur Thematik
• Alfred Tarski: The Concept of Truth in Formal Systems. 1936 (thatmarcusfamily.org PDF).

1. ↑ Jesús Padilla Gálvez: Wahrheit und Selbstrückbezüglichkeit. In: Journal for General Philosophy of Science. März 1991, Band 22, S. 111–132.
2. ↑ Hans-Jürgen Heringer, Georg Stötzel (Hrsg.): Sprachgeschichte und Sprachkritik: Festschrift für Peter von Polenz zum 65. De Gruyter Berlin, New York 1993, S. 38 ff.
3. ↑ Boolos: The Logic of Provability. Cambridge University Press 1993, Kapitel 1–3.
4. ↑ Wolfgang Stegmüller (Hrsg.): Selbstreferenz, Tarski-Sätze und die Undefinierbarkeit der arithmetischen Wahrheit. Springer Verlag Berlin, Heidelberg 1984 S. 375 f.
5. ↑ Boolos: The Logic of Provability. Cambridge University Press 1993, S. 104.