  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.
