Albert Visser

Utrecht University

The third Löb condition, provable implies provably provable, is the most interesting of the Löb conditions. It may fail in many circumstances. What remains of provability logic in its absence?

There is an interesting class of theories and proof predicates for which we do have the first two Löb conditions plus Löb’s Rule. We study the logic of these principles in a context where we have a representation of modalised fixed points. There are various ways to add modalised fixed points to a modal logic but, In our talk, we zoom in on the case where we represent the fixed points by having (an appropriate) cyclic syntax. The system we obtain by taking the modal logic K plus Löb’s Rule in cyclic syntax is Cyclic Henkin Logic, CHL.

In our talk we explain how CHL works and how arithmetical interpretations of CHL work. We show that we do have the de Jongh-Sambin-Bernardi Theorem on uniqueness of modalised fixed points. We illustrate that the de Jongh-Sambin algorithm shows that we have cycle elimination in CHL plus the third Löb condition.