Provability Logic and Modalised Fixed Points

Abstract: My talk is an introduction to classical provability logic with an emphasis on the fixed point calculation. Our treatment is slightly different from the usual one. We start with the logic K4 + fixed points. We show that this logic has `fixed point elimination’. For this aim we use a form of the multiple fixed points theorem. The result of eliminating the fixed point operator is Löb's Logic GL. We will also discuss arithmetical interpretations of GL.

Date and Time: 29 September 2020, 7pm Beijing time (1pm Dutch time)

Speaker: Prof. Albert Visser (University of Utrecht, Netherlands)