可证性解释

用可证性来解释模态词。对模态词作这样的解释起源于K．哥德尔于1933年发表的论文《直觉主义命题演算的一个解释》，对A．海廷建立的直觉主义逻辑演算给出了可证性的解释。他引进了一元联结词B，把“p是可证”的记为Bp，并对古典命题演算附加下列公理和规则：

从命题A可推出命题BA。

由此他得到一个与正规模态系统S4等价的系统，给出了海廷系统的一个解释。模态逻辑的可证性解释尽管起源得早，但在20世纪70年代前一直没有得到认真的研究，直到1975年前后才在意大利、荷兰、美国、保加利亚、捷克斯洛伐克、苏联、西德、以色列等国家展开了广泛的研究，建立了可证性逻辑系统GL和一些重要的定理。

可证性概念的有些性质与通常认为必然性概念所应具有的性质相似，而另一些性质则很不一致，构造模态系统GL的动机就是要给出可证性概念的公理刻划。系统GL的初始符号包括命题变项p、q、r…，命题常项、⊥，联结词、∧、∨、以及模态词□；它的公理包括所有重言式和所有形如□A□□A或□(AB)(□A□B)的命题；它的推理规则是下列3条规则：

假言推理规则：从AB和A可推出B；

必然概括规则：从A可推出□A；

罗比规则：从□AA可推出4。简言之，GL就是正规模态系统K4加上罗比规则。GL也可以通过在系统K4中附加公理模式□(□AA)□A而得。GL与皮亚诺算术系统PA(或策尔梅罗－弗兰克尔集论系统ZF)的精确联系是：假定PA的陈述p、q、……以某种方式与命题字母p、q、……相联系，用对应的陈述p、q、……分别替代命题A中的p、q……并且把其中的模态号□解释为PA中的可证性谓词，所得到的结果是PA的一个陈述A；那么，若B在系统GL中可从A、……A推出，并且……、都是在系统PA中可证明的，则B也是在PA中可证明的。R．S．M索罗维(solovay)和其他一些逻辑学家得到的一个重要定理说，如果B在系统GL中不是可推导的，那么B在系统PA中就不是可证的，因此，一模态命题B是在GL中可推导的当且仅当B是在PA中可证明的。模态系统GL是可判定的，也就是说可以机械地来确定一命题在GL中是不是可推导的，这跟系统PA和ZF是完全不同的。有关GL的另一个重要定理是不动点定理。称一命题A(P)为模态于命题字母p的，当且仅当，p在A(p)中的每一出现都在模态号□的辖域内。D．H．德炯(Jongh)和G．萨姆宾(Sambin)的不动点定理断言，如果命题A(p)模态于p，那么有一个除了A(p)中非p的命题字母外不含其它命题字母的命题B使得，p≡A(p)在GL中可推导当且仅当p≡B在GL中可推导。这样的B被称为A(p)的不动点，意思是说B为“等式”(p≡A(p))的一个解。并且，在下述意义上，解是唯一的：如果B’是另一个解，那末B≡B’在GL中是可推导的。p≡A(p)在GL中可推导相当于说p在GL中“可以用自己来定义”，而p≡B在GL中可推导则相当于说p在GL中“可以不用自己来定义”，因此不动点定理的实质是说GL中的自指定义可以归结为非自指的定义。

模态逻辑与形式系统理论之间许多其它联系也都在研究之中，许多问题还有待解决。不过，模态逻辑可证性解释的研究已经使人们知道了关于可证性的最重要的东西。