Lewis and Brouwer meet Strong Löb
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866916212001210368 |
|---|---|
| author | Visser, Albert Litak, Tadeusz |
| author_facet | Visser, Albert Litak, Tadeusz |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_11969 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Lewis and Brouwer meet Strong Löb Visser, Albert Litak, Tadeusz Logic Logic in Computer Science {03B45, 03F45, 03F50, 03F55 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. |
| title | Lewis and Brouwer meet Strong Löb |
| topic | Logic Logic in Computer Science {03B45, 03F45, 03F50, 03F55 |
| url | https://arxiv.org/abs/2404.11969 |