Lewis 与 Brouwer 遇强 Löb 逻辑

本文研究了原理$\phi \Rightarrow \square\phi$（称为'强度'或'完备原理'）在Löb逻辑构造版本中的情况。我们同时考虑带有必然算子的模态语言和带有Lewis箭头的模态语言，并对Löb逻辑进行相应调整。证明逻辑的核心见解，如de Jongh-Sambin定理和de Jongh-Sambin-Bernardi定理，在存在强度原理时形式简洁。我们给出这些简化版本。我们讨论了两个显著系统的语义，并为两者证明均匀插值。此外，我们勾勒了这些系统的算术解释。最后，我们描述了我们的研究与计算机科学的各种联系。