Fixed point theorem of provability logic — LessWrong