Modallogik/K/Phantasiearmutsaxiom und K-Umkehrung/Fakt/Beweis

Beweis

Von (1) nach (2). Aus den aussagenlogischen Tautologien

$\vdash \beta \rightarrow (\alpha \rightarrow \beta )$

und

$\vdash \neg \alpha \rightarrow (\alpha \rightarrow \beta )$

ergeben sich mit Fakt  (1) die Ableitungen

$\vdash \Box \beta \rightarrow \Box (\alpha \rightarrow \beta )$

und

$\vdash \Box \neg \alpha \rightarrow \Box (\alpha \rightarrow \beta ).$

Das Phantasiearmutsaxiom liefert

$\Gamma \vdash \Diamond \neg \alpha \rightarrow \Box \neg \alpha$

und über den Kettenschluss

$\Gamma \vdash \Diamond \neg \alpha \rightarrow \Box (\alpha \rightarrow \beta ).$

Daher gilt

$\Gamma \vdash (\Diamond \neg \alpha \vee \Box \beta )\rightarrow \Box (\alpha \rightarrow \beta ),$

was eben

$\Gamma \vdash (\Box \alpha \rightarrow \Box \beta )\rightarrow \Box (\alpha \rightarrow \beta )$

bedeutet.

Von (2) nach (1). Aus der aussagenlogischen Tautologie

$\vdash (\alpha \rightarrow \neg \alpha )\rightarrow \neg \alpha$

ergibt sich mit Fakt  (1) direkt

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

Die Umkehrung des ${}K$-Axioms mit ${}\beta =\neg \alpha$ liefert

$\Gamma \vdash (\Box \alpha \rightarrow \Box \neg \alpha )\rightarrow \Box (\alpha \rightarrow \neg \alpha ).$

Eine einfache aussagenlogische Überlegung zeigt ferner

$\vdash \Diamond \neg \alpha \rightarrow (\Box \alpha \rightarrow \Box \neg \alpha ).$

Der doppelte Kettenschluss liefert

$\Gamma \vdash \Diamond \neg \alpha \rightarrow \Box \neg \alpha .$

Da diese Beziehung für jedes ${}\neg \alpha$ gilt, gilt es nach Fakt  (5) überhaupt für jede Aussage.

Aus (1) folgt (3). Das ${}K$-Axiom liefert

$\vdash \Box (\alpha \rightarrow \neg \beta )\rightarrow (\Box \alpha \rightarrow \Box \neg \beta )$

und das Phantasiearmutsaxiom liefert

$\Gamma \vdash \Diamond \alpha \rightarrow \Box \alpha .$

Dies zusammen ergibt

$\Gamma \vdash \Box (\alpha \rightarrow \neg \beta )\rightarrow (\Diamond \alpha \rightarrow \Box \neg \beta ).$

Wir schreiben dies als

$\Gamma \vdash \Box (\neg \alpha \vee \neg \beta )\rightarrow (\neg \Diamond \alpha \vee \Box \neg \beta ).$

Durch Kontraposition bedeutet dies

$\Gamma \vdash (\Diamond \alpha \wedge \neg \Box \neg \beta )\rightarrow \Diamond (\alpha \wedge \beta ).$

Von (3) nach (1). Wir betrachten den Spezialfall

$\Gamma \vdash \Diamond \alpha \wedge \Diamond \neg \alpha \rightarrow \Diamond (\alpha \wedge \neg \alpha ).$

Durch Kontraposition ist dies

$\Gamma \vdash \Box \neg (\alpha \wedge \neg \alpha )\rightarrow \neg (\Diamond \alpha \wedge \Diamond \neg \alpha )$

und durch eine aussagenlogische Umstellung

$\Gamma \vdash \Box (\neg \alpha \vee \alpha )\rightarrow (\neg \Diamond \alpha \vee \neg \Diamond \neg \alpha ).$

Aus der aussagenlogischen Tautologie

$\vdash \neg \alpha \vee \alpha$

folgt mit der Nezessisierungsregel

$\vdash \Box (\neg \alpha \vee \alpha )$

und somit

$\Gamma \vdash \neg \Diamond \alpha \vee \neg \Diamond \neg \alpha$

mit Modus ponens. Dies bedeutet

$\Gamma \vdash \Diamond \alpha \rightarrow \Box \alpha .$

Zur bewiesenen Aussage