Cyclic Henkin Logic

We present a general version of the second incompleteness theorem G2. In this version we consider certain predicates semi-numerating the axiom set of the given theory that do not necessarily support the verification of the third Löb Condition: provable implies provably provable.
Cyclic Henkin Logic (CHL) is a provability logic that is valid for arithmetical interpretations whenever the conditions for the above version of G2 apply. The logic is, in first approximation, K plus Löb’s Rule plus Fixed Points. The logic has many good properties. For example, the de Jongh-Sambin-Bernardi Theorem holds in the CHL. We realise the idea of `Fixed Points’ by employing a syntax on cyclic graphs. We will sketch how this works and briefly indicate how arithmetical interpretation of a graph works (even modulo bisimulation). CHL turns out to be mutually interpretable with the mu-Calculus plus the minimal Henkin Fixed Point. As a consequence, one has, for example, a completeness theorem for CHL in finite acyclic Kripke models and uniform interpolation.