可证明性逻辑

编辑
本词条由“匿名用户” 建档。
可证明性逻辑是一种模态逻辑,其中的盒式(或必然性)运算符被解释为"可以证明"。其目的是为了捕捉一个合理的丰富的形式理论的证明谓词的概念,如Peano算术。 有许多可证明性逻辑,其中一些在§参考文献中提到的文献中有所涉及。基本系统一般被称为GL(代表哥德尔-罗布)或L或K4W(W代表基础良好)。它可以通过在逻辑K(或K4)中加入Löb定理的模态版本得到。也就是说,GL的公理是经典命题逻辑的所有同义词...

可证明性逻辑

编辑

可证明性逻辑是一种模态逻辑,其中的盒式(或必然性)运算符被解释为"可以证明"。其目的是为了捕捉一个合理的丰富的形式理论的证明谓词的概念,如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的多模态逻辑是可证明性逻辑的自然延伸。

内容由匿名用户提供,本内容不代表vibaike.com立场,内容投诉举报请联系vibaike.com客服。如若转载,请注明出处:https://vibaike.com/171317/

(1)
词条目录
  1. 可证明性逻辑
  2. 可证明性逻辑的例子
  3. 可证明性逻辑的历史
  4. 可证明性逻辑的概论

轻触这里

关闭目录

目录