Cyclic Henkin Logic

TL;DR

This paper introduces Cyclic Henkin Logic (CHL), a provability logic without the L"ob condition, utilizing cyclic syntax for fixed points, and explores its properties, algorithms, and arithmetical interpretations.

Contribution

It develops a novel cyclic syntax framework for CHL, demonstrating fixed point theorems, connections to classical L"ob's Logic, and arithmetical interpretations, expanding the understanding of provability logics.

Findings

Cyclic syntax simplifies fixed point theorems.

CHL relates to classical L"ob's Logic via the de Jongh-Sambin algorithm.

Guard recursion is key to the computation scheme.

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.