Beweisbarkeitslogik/Widerspruchsfreiheit als Fixpunkt/Aufgabe

Es sei ${}\Gamma$ die durch das Löb-Axiom gegebene ${}K$-Modallogik, also die Beweisbarkeitslogik. Wir setzen

${}\bot :=p\wedge \neg p\,$

(als Abkürzung für einen Widerspruch). Zeige, dass

$\Gamma \vdash \neg \Box \neg \Box \bot \leftrightarrow \neg \Box \bot$

ableitbar ist.

Zur Lösung, Alternative Lösung erstellen