Beweisbarkeitslogik/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.