2024/04/18 by Albert Visser, Visser, Albert, Tadeusz Litak +1
Computer Science · #03F45 #03F50 #03F55 #Computability, Logic, AI Algorithms #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #{03B45
paper · pdf · doi:10.48550/arxiv.2404.11969
openalex publication_date 2024/04/18 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.