arXiv · 2404.11969
Lewis and Brouwer meet Strong L\"ob
Abstract
We study the principle phi implies box phi, known as `Strength' or `the Completeness Principle', over the constructive version of L\"ob'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\"ob'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.
Explore related subjects
Keep this discovery
Albert Visser, Tadeusz Litak. 2024-04-18. Lewis and Brouwer meet Strong L\"ob. https://arxiv.org/abs/2404.11969
Cite the original work for its findings. Save a collection to share your selection of sources.