一阶语义图方法

一种能用来探知是否有满足一给定的有穷的公式集的解释，一给定的公式是否为一给定的有穷公式集的逻辑后承以及一给定的公式是不是常真式的方法。它是一种系统地研究一阶逻辑的方法。一阶语义图方法在20世纪50年代由E．W．贝思、J．欣迪卡以及K．舒提各自独立创立，后经R．M·斯穆里安加以发展和改进。一阶语义图方法与用公理化方法把一阶逻辑构成一个公理系统不同，它没有公理，而只有一组规则。这一点和自然推理系统类似。但它又和自然推理系统不同。它的规则不是用来作推演或证明，而是用来对一给定的公式，构造一个图，以判明此公式是否常真，等等。在陈述语义图方法的规则之前，先说明什么是一个图及其它概念，以及对一给定的公式(有穷的公式集)如何构造一个图。这里讨论的一阶逻辑的语言和一阶逻辑系统F(见一阶逻辑)的相同，初始符号包括，∧，∨，→，，和。

一个图是一些称为结点的元素的集合。每一结点都联系一有穷的公式集合。通常一给定结点就等同于所联系的公式集合。

图的元素(即结点)分成层。每一结点都属于唯一的一层。层用自然数作标号。0层的结点恰好一个，叫做一个图的始点。每一属于n+1层的结点都是一属于n层的唯一的结点的后继。用图式表示出来时，一给定结点的后继就写在它的下面，并且用线段把它和它的后继连接起来。没有后继的结点叫做终点。

一个图如果至少有一d层结点，但没有d+1层的结点，就说这图的深度为d。

一个图的一条枝是结点的有穷序列Φ，Φ，…，，其中Φ是图的始点，并且i=1，…，l，Φ是Φ的后继，而Φ是终点。这个枝就说结束在Φ。显然，对每一终点有唯一的一枝终止于它。

属于一枝的一个结点的公式就说是该枝的公式。属于始点的公式叫做这图的初始公式。

一个图是一偏序集，它的元素(结点)由下面的关系所偏序：每一结点后随它的后继，它的后继的后继，等等。

下面说明给定一有穷公式集Φ如何构造一个图。

首先，如果Φ是任何有穷的公式集，以Φ为唯一结点的图是一对于Φ的图。凡是以Φ为始点的图就是一对于Φ的图。

其次，得到对于Φ的一个图T后，可根据下面的13条规则中任何一条把图T扩展为一新的图T′。在每一情形下，T′包括T的所有结点，并加上一个或两个新的结点。旧的结点间的关系，在T′中与在T中相同。新的结点被指定为T中某个终点的后继。

－规则 如果在T的一终止于结点Φ的枝的公式中间有一个公式A，增加一新的结点｛A｝作为Φ的后继。

∧－规则 如果在T的一终止于结点Φ的枝的公式中间有一个公式A∧B，增加一个新的结点｛A，B｝作为Φ的后继。

∧－规则 如果在T的一终止于结点Φ的枝的公式中间有一个公式(A∧B)，增加两个新的结点｛A｝和｛B｝作为Φ的后继。

∨－规则 如果在T的一终止于结点Φ的枝的公式中间有一个公式A∨B，增加两个新的结点｛A｝和｛B｝作为Φ的后继。

∨－规则 如果在T的一终止于结点Φ的枝的公式中间有一个公式(A∨B)增加一个新的结点｛A，B｝作为Φ的后继。

→－规则 如果在T的一终止于结点Φ的枝的公式中间有一个公式A→B，增加两个新的结点｛A｝和｛B｝作为Φ的后继。

→－规则 如果在T的一终止于结点Φ的枝的公式中间有一个公式(A→B)，增加一个新的结点｛A，B｝作为Φ的后继。

－规则 如果在T的一终止于结点Φ的枝的公式中间有一个公式AB，增加两个新的结点｛A，B｝和｛A，B｝作为Φ的后继。

规则 如果在T的一终止于结点Φ的枝的公式中间有一个公式(AB)，增加两个新的结点｛A，B｝和｛A，B｝，作为Φ的后继。

－规则 如果在T的一终止于结点Φ的枝的公式中间有一个公式xA(x)，增加一个新的结点｛A(x／t)｝，作为Φ的后继(t为任意的项)。

－规则 如果在T的一终止于结点Φ的枝的公式中间有一个公式xA(x)，增加一个新的结点｛A(x／v)}，作为Φ的后继(对v有限制．y在由增加结点A(x／y)加以扩展的这枝的所有前面的公式中都不自由出现。y称为关键变元。)

－规则 如果在T的一终止于结点Φ的枝的公式中间有一个公式xA(x)，增加一个新的结点｛A(x／y)｝(对y有限制，同－规则。)作为Φ的后继。

－规则 如果在T的一终止于结点Φ的枝的公式中间有一个公式xA(x)，增加一个新的结点｛A(x／y)｝，作为Φ的后继。

在应用这13条规则中任何一条把T扩展为T′时，与所应用的规则相应那个公式就说是该次应用使用了的。在规则(规则)的一次特定的应用中使用的变元y叫做该次应用的关键变元。这些规则可以用图式表示如下：

从图T扩展成T′，T的一个枝就扩展成一更长的枝，或者扩展并分裂成两个更长的枝。T的其它枝都保持不变。

一个图的一个枝称为封闭的，如果有一原子公式A使得A和A都是该枝的公式。所涉及的公式A和A就说是用来封闭该枝的。在封闭的枝的下面打一个×号。一个对于Φ的图称为Φ的一个反驳，如果它的所有的枝都是封闭的。反驳Φ就是构造Φ的一个反驳。

上面的13条规则具有这样的性质，T中的一枝，即这个枝中的所有公式的集合，如果是可满足的，即有一个解释使该枝的公式都真，那么应用一个规则把该枝扩展为一新枝后，那个解释同样使新枝中的公式都真，在把该枝分裂成两个新枝的情况，那个解释至少使其中一个新枝中的公式都真。例如，应用－规则时，是在一枝中增加公式A，A与A同真假，使A为真的解释自然也使A为真。在应用一个规则使一枝扩展为两个新枝的情况，如应用→－规则，一个新枝是在公式A→B下面增加公式A，另一新枝是在A→B的下面增加公式B。公式A→B在A假或B真时为真，使公式A→B为真的解释，必定使公式A→B，A或者使A→B，B为真，即至少有一新枝，在使该枝原来的公式都真的那个解释下，它的所有公式都真。所以，作为一个图的始点的有穷公式集Φ，如果它是可满足的，那么在一个以Φ为始点而构造的图中，至少有一枝是可满足的。在一个封闭的枝中，同时包含有原子公式A及其否定A(实际上不必一定是原子公式，任何公式也一样)，因此封闭的枝是不可满足的。一个反驳的每一枝都封闭，都不可满足，因而作为始点的公式集是不可满足的。所以，一个以有穷公式集Φ为始点而构造的图，如果每一枝都封闭，就表明Φ是不可满足的，该图就是对Φ的一个反驳。任一公式A，A是常真的，当且仅当A不可满足。所以，若能构造｛A｝的一个反驳，就表明A是常真的。设Φ为一有穷公式集，若公式A为Φ的逻辑后承，即ΦA，则每一满足Φ的解释必满足A，因而没有一个解释满足Φ∪｛A｝。因此，通过构造一个对于Φ∪｛A｝的反驳，就能表明A是Φ的逻辑后承。

对命题逻辑部分而言，只有前9个规则，语义图方法提供了一个确定一公式A是不是重言式，和确定公式A是不是有穷公式集Φ的重言后承的一个判定方法。因为应用关于联结词的9个规则构造语义图时，把图中的一个枝扩展为一新枝时，增加的公式都是前面公式的子公式，有穷公式集的子公式数目是有穷的，语义图的构造必定在有穷步内结束。实际上，这个方法要比真值表方法快速有效，比真值表方法更优美。对于谓词逻辑，语义图方法当然没有提供判定任一公式是否常真的判定方法。因为已经证明谓词逻辑是不可判定的，不存在一个判定方法，任给一公式总能用它机械地在有穷步内确定此公式是否常真。但是，对一常真公式，要在公理系统中证明它是定理，或在自然推理系统中证明它是不用前提可推演的，要比构造此一公式的否定的一个反驳，更困难。因为证明是探索性的，没有一定的步骤可循，而构造一个语义图相对说来是相当机械的。

和一阶逻辑的公理系统或自然推理系统一样，语义图方法也具有协调性、可靠性和完全性。设Φ是一有穷的公式集，A是一公式。下面3个条件是等价的：①ΦA；②Φ┝A；③Φ，A是可驳的。

可以通过增加一个规则来加强语义图方法。

规则EM 如果Φ是图T的任何终点，A是任何公式，增加两个结点｛A｝和｛A｝作为Φ的后继。公式A是通过应用EM－规则而引入。因为任何解释满足A或A(排中律)，如果以Φ为终点的枝是可满足的，则应用EM一规则后有一枝是可满足的。利用这个规则可以更快得到反驳。但是这个规则原则上是多余的，不把它看作是语义图方法的规则。有一条EM－规则消去定理：给定一个应用了EM－规则的Φ的反驳，可以构造一个Φ的不应用EM－规则的反驳。因此，不把EM规则看作语义图方法的规则，但是在构造反驳时可以使用它。

语义图方法与G·根岑的系统有深刻的内在联系。实质上，语义图方法是根岑的方法的对偶。根岑的方法是系统地探求树形的证明，而语义图方法是系统地探求倒树形的反驳。根岑的证明树上的一个结点大致相当于一个图中的一枝。对于语义图的消去定理相当于(事实上等阶于)根岑的著名的主定理(hauptsatz)。