Beweisbarkeitslogik/Widerspruchsfreiheit als Fixpunkt/Aufgabe/Lösung

Wegen Kontraposition genügt es,

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

zu zeigen, wobei wir die einzelnen Implikationen getrennt zeigen. Aus einem Widerspruch folgt Beliebiges, also

$\vdash \bot \rightarrow \neg \Box \bot .$

Nach Fakt  (1) folgt

$\vdash \Box \bot \rightarrow \Box \neg \Box \bot .$

Eine Instanz des Löb-Axioms ist

$L\vdash \Box (\Box \bot \rightarrow \bot )\rightarrow \Box \bot .$

Das Widerspruchsaxiom ergibt

$\vdash \neg \Box \bot \wedge \Box \bot \rightarrow \bot ,$

was wir als

$\vdash \neg \Box \bot \rightarrow (\Box \bot \rightarrow \bot )$

schreiben. Mit Fakt  (1) erhalten wir

$\vdash \Box \neg \Box \bot \rightarrow \Box (\Box \bot \rightarrow \bot ).$

Der Kettenschluss liefert

$L\vdash \Box \neg \Box \bot \rightarrow \Box \bot .$

Zur gelösten Aufgabe