 Löb axiom implies positive introspection

ID: lob-axiom-implies-positive-introspection

The Löb axiom

□ (□ A \to A) \to □ A

over normal modal logic already implies

□ X \to □□ X

. Put

C = □ X \land X

. Distribution gives

□ C \to □ X

, hence

X \to (□ C \to C)

. Necessitation and distribution give

□ X \to □ (□ C \to C)

; the Löb axiom gives

□ C

, which implies

□□ X

 New to topics? Read the docs here!