Lewis and Brouwer meet Strong Löb

Abstract

We study the principle phi implies box phi, known as `Strength' or `the Completeness Principle', over the constructive version of Löb's Logic. We consider this principle both for the modal language with the necessity operator and for the modal language with the Lewis arrow, where Löb's Logic is suitably adapted. Central insights of provability logic, like the de Jongh-Sambin Theorem and the de Jongh-Sambin-Bernardi Theorem, take a simple form in the presence of Strength. We present these simple versions. We discuss the semantics of two salient systems and prove uniform interpolation for both. In addition, we sketch arithmetical interpretations of our systems. Finally, we describe the various connections of our subject with Computer Science.