 GL fixed point for a provability implication

ID: gl-fixed-point-for-a-provability-implication

The Löb axiom gives

□ F \to □ q

q \to F

, necessitated and distributed, gives

□ q \to □ F

. Thus

□ F \leftrightarrow □ q

, and replacing the antecedent in

□ F \to q

gives exactly

F

. Setting

q = ⊥

produces a negative-provability fixed point, provably equivalent to

\neg □ ⊥

 New to topics? Read the docs here!