Abstract:

The third Löb Condition L3, to wit *provable* implies *provably provable*, is the most problematic of Löb's three conditions. There are theories and representations of the axiom set such that either we do not know how to verify L3 or we can actually show that it fails. Still, in many circumstances where L3 is lacking, both Gödel’s Second Incompleteness Theorem and the de Jongh-Sambin-Bernardi Theorem on the uniqueness of fixed points still hold.

In this talk, we study Cyclic Henkin Logic. In this logic we do have Löb’s Rule but we do not have L3. We cannot define modalised fixed points in the purely modal language, since the de Jongh-Sambin Theorem on explicit fixed points fails. There are several ways of adding fixed points to the language: as constants, using a variable-binding fixed point operator and by adopting a cyclic syntax. Cyclic Henkin Logic embodies the choice for a cyclic syntax. This choice is arguably the most beautiful one.

The talk is an introduction to CHL. We will explain the syntax and prove some basic facts.If time allows, we will how CHL can be viewed as a fragment of the mu-Calculus.