可证明性逻辑

可证明性逻辑是一种模态逻辑，其中的盒式（或必然性）运算符被解释为”可以证明”。其目的是为了捕捉一个合理的丰富的形式理论的证明谓词的概念，如Peano算术。

有许多可证明性逻辑，其中一些在§参考文献中提到的文献中有所涉及。基本系统一般被称为GL（代表哥德尔-罗布）或L或K4W（W代表基础良好）。它可以通过在逻辑K(或K4)中加入Löb定理的模态版本得到。也就是说，GL的公理是经典命题逻辑的所有同义词加上以下形式之一的所有公式。分布公理。□(p→q)→(□p→□q)；Löb公理。□(□p→p)→□p。推理的规则是模态推理。从p→q和p得出q的结论；必然性。从⊢{displaystyle{vdash}，p得出q的结论。

GL模型是由RobertM.Solovay在1976年开创的。从那时起，直到他在1996年去世，该领域的主要启发者是GeorgeBoolos。SergeiN.Artemov,LevBeklemishev,GiorgiJaparidze,DickdeJongh,FrancoMontagna,GiovanniSambin,VladimirShavrukov,AlbertVisser等人对该领域做出了重大贡献。

可解释性逻辑和Japaridze的多模态逻辑是可证明性逻辑的自然延伸。