相干谓词逻辑

相干逻辑的量词理论。相干谓词逻辑是跟古典谓词逻辑很不相同的，古典谓词逻辑的一元谓词部分是可判定的，但相干谓词逻辑的一元谓词部分却是不可判定的。

在相干命题逻辑系统E和R中附加有关量词的公理和规则，就得到相应的量词系统EQ和RQ。具体的做法如下。首先，按通常的方式定义出一阶公式的概念。为方便起见，将可数无穷多个个体变项分成二个无穷子类。一类是约束变项，以x，y，z，…等表示之；另一类是自由变项(有时也称为参变项)，以a，b，c，…等表示之。约束变项不得在公式中有不约束的出现。量词和可以互相定义，因此只须取其中之一为初始符号。这里，取为初始的，定义为。为得到相干谓词逻辑，可以附加下列有关量词的公理和规则：

①xA→A(a／x)，(-消去)

②x(A→B)→(A→xB)，(-引入)

③x(A∨B)→A∨xB，(限制)

④从A(a／x)可推出xA。(全称概括)

通常要求公理模式②和③中的x不得在A中自由出现，现在由于规定约束变项不得在公式中自由出现，这一要求也就自动得到满足。公理模式③是将合取∧对于析取∨的分配律从有穷情形推广到无穷情形的结果。如果语言中含有函项符号，那未公理模式(1)就应当改成xA→A(t／x)，这里t是任意的项。

为得到相干谓词逻辑而附加的公理和规则，除了上述那一组外，还有其它各种可能。其中最经济的要算下述的一组，只由一个公理模式和一个规则组成：

①xA→A(a／x)，

②从A→B∨C(a／x)可推出A→B∨xC；

②中的a不得在A或B中出现。相干命题逻辑的克里普克式关系语义可以很自然地推广到相应的相干谓词逻辑上，但所带来的完全性问题却是比较复杂的。就相干命题逻辑系统R而言，为R－构架中各元素配上同一个个体域就可建立起RQ的语义，RQ相对于这样的语义是可靠的，即，RQ的每一个定理在这语义下都是有效的。但是，RQ相对于这样的不变个体域语义却是不完全的。