Modallogik/K/Paradoxe Axiomenschemata/Textabschnitt

Einen modallogischen Ausdruck nennen wir paradox, wenn er, wenn man alle darin auftretenden ${}\Box$ (und somit auch alle ${}\Diamond$) weglässt, einen aussagenlogischen Widerspruch ergibt. Ein modallogisches Axiomenschema heißt paradox, wenn es davon eine paradoxe Instanz gibt.

Definition

Das modallogische Axiomenschema

$\Box \alpha \leftrightarrow \neg \alpha$

nennt man Antiaxiom.

Wenn das Antiaxiom gilt, so ist auch

$\Diamond \alpha \leftrightarrow \neg \Box \neg \alpha \leftrightarrow \neg \neg \neg \alpha \leftrightarrow \neg \alpha \leftrightarrow \Box \alpha ,$

das Antiaxiom ist also ideologisch. In einer ${}K$-Modallogik führt das Antiaxiom zu einem Widerspruch, da ja dann zu einer aussagenlogischen Tautologie ${}\alpha$ wegen der Nezessisierungsregel auch ${}\Box \alpha$ und somit der Widerspruch ${}\neg \alpha$ gilt. Wenn man dagegen das Antiaxiom auf Aussagenvariablen beschränkt, also

$\Box p\leftrightarrow \neg p$

betrachtet, so ergibt sich ein sinnvolles ${}K$-System.

Definition

Das modallogische Axiomenschema

$\Box (\Box \alpha \rightarrow \alpha )\rightarrow \Box \alpha$

nennt man Löb-Axiom.

Bemerkung  

Für das Ableitungsprädikat

${}\alpha (y)=\exists x(\delta _{\Gamma }(x,y))\,$

zu einer die Peano-Arithmetik umfassenden entscheidbaren Satzmenge ${}\Gamma$ gilt neben den in Bemerkung angeführten Eigenschaften auch der Satz von Löb, nämlich

$\alpha (GN(\alpha (GN(s))\rightarrow s))\rightarrow \alpha (GN(s)).$

Wenn man

${}\Box s=\alpha (GN(s))\,$

setzt, so kann man dies als

$\Box (\Box s\rightarrow s)\rightarrow \Box s$

schreiben, es liegt also genau das Löb-Axiom vor (daher der Name des Axioms). Unter der modallogischen Beweisbarkeitslogik versteht man die ${}K$-Modallogik, die durch das Löb-Axiom gegeben ist (das Transitivitätsaxiom lässt sich daraus ableiten, siehe Fakt). Es handelt sich um eine paradoxe Modallogik, in der man die Unvollständigkeit nachbbilden kann.

Es sei ${}\bot =p\wedge \neg p$ (gesprochen Falsum) eine Abkürzung für einen Widerspruch. Im Kontext der Beweisbarkeitslogik bedeutet dann ${}\neg \Box \bot$ die Nichtableitbarkeit eines Widerspruchs, also die Widerspruchsfreiheit des Systems. Aus dem Löb-Axiom (also der ${}K$-Modallogik ${}L$, die durch das Löbaxiom gegeben ist) lässt sich ableiten, dass diese Widerspruchsfreiheit ein Fixpunkt der Nichtableitbarkeit ist, d.h. es gilt

$L\vdash \neg \Box \neg \Box \bot \leftrightarrow \neg \Box \bot ,$

siehe Aufgabe. Dies bedeutet insbesondere, dass weder ${}\Box \bot$ noch ${}\neg \Box \bot$ aus ${}L$ ableitbar ist (die Widerspruchsfreiheit des Systems ergibt sich aus Fakt  (6)). Insbesondere ist dieses Ableitungssystem unvollständig, was dem ersten Gödelschen Fixpunktsatz entspricht. Darüber hinaus ist die letzte Unableitbarkeit gerade die Aussage des zweiten Gödelschen Fixpunktsatzes, den man also so modallogisch nachbilden kann (die Hauptarbeit liegt aber darin, zu zeigen, dass das arithmetische Ableitungsprädikat das Löb-Axiom erfüllt).