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.

翻译：我们研究了原则φ蕴含□φ（称为“强度”或“完备性原则”），在构造性版本的勒布逻辑中。我们同时考虑了带有必然性算子的模态语言和带有刘易斯箭头的模态语言（其中勒布逻辑被适当调整）下的这一原则。可证性逻辑的核心洞见，如德容-桑宾定理和德容-桑宾-贝尔纳迪定理，在引入强度后呈现简化形式。我们给出了这些简化版本。我们讨论了两个显著系统的语义，并证明了两者的均匀内插性质。此外，我们勾勒了这些系统的算术解释。最后，我们描述了该主题与计算机科学的各种联系。