Cyclic Henkin Logic

Abstract

In this paper, we study Cyclic Henkin Logic CHL, a logic that can be described as provability logic without the third L\"ob condition, to wit, that provable implies provably provable (aka principle 4). The logic CHL does have full modalised fixed points. We implement these fixed points using cyclic syntax, so that we can work just with the usual repertoire of connectives. The main part of the paper is devoted to developing the logic on cyclic syntax. Many theorems, like the multiple fixed point theorem, become matter of course in this context. We submit that the use of cyclic syntax is of interest even for the study of classical L\"ob's Logic. We show that a version of the de Jongh-Sambin algorithm can be seen as one half of a synonymy between the theory GL^\circ, i.e.\ CHL plus the third L\"ob Condition, and ordinary L\"ob's Logic GL. Our development illustrates that an appropriate computation scheme for the algorithm is guard recursion. We show how arithmetical interpretations work for the cyclic syntax. In an appendix, we give some further information about the arithmetical side of the equation.