的一阶谓词演算

一致性的问题谓词微积分是相对简单的。世界可能会假定只有一个对象一个。在这种情况下,普遍量化和存在量化的句子(∀x)一个(x)和(∃x)一个(x)减少到简单的句子一个(一个),所有量词可以消除。它可能很容易地确认,减少后,所有定理的微积分成为重言式(即。命题演算的定理)。如果F是任何谓词,等一个句子“每个x是F并不是每个x是F”即:(∀x)F(x)·∼(∀x)F(x)——然后减少到“一个既一个而不是,一个”- - -一个(一个)·∼一个(一个)——不是同义反复;因此,原句不是一个定理;因此,没有矛盾可以是一个定理。如果F是简单的,那么F和一个都是一样的。如果F是复杂的,包含(∀y)或(∃z)等。一个获得的结果吗迭代消除(∀的变换y)等。事实上,它不仅可以被证明是相当直接,微积分是一致的而且其所有定理都是有效的。

微积分的发现是完整和不可判定的更深刻的发现其一致性。1930年哥德尔证明了其完整性;建立了它的不可判定性与教会和1936年图灵完全不同的方法。考虑到一般的发展发生了1936年,它的不可判定性也遵循从定理的另一种方式X哥德尔的1931年的论文。

微积分的完整性意味着每个有效的句子是一个定理。由此可见,如果∼一个不是一个定理,然后∼一个是无效的;,因此,一个是可以满足的;也就是说,it has an interpretation, or a model. But to say that一个只不过意味着∼是一致的吗一个不是一个定理。因此,从完整性,如果它遵循一个是一致的,那么一个是可以满足的。因此,语义的概念有效性和可满足性与可微性的语法概念和一致一致性。

的Lowenheim-Skolem定理

发现的完整性密切相关定理Lowenheim-Skolem定理(1915、1920),命名利奥波德Lowenheim德国教师和Skolem说,如果一个句子(或一个正式的系统)模型,它有一个可数或可列举的模型(即。,一个模型whose members can be matched with the positive integers). In the most direct method of proving this theorem, the logician is provided with very useful tools in model theory and in studies on relative consistency and independence in集理论。

在谓词微积分有一些减少或标准定理。是一个有用的例子前束的标准形式:每个句子都可以简化为一个等价的句子表达的前束form-i.e。这样的一种形式,所有量词出现在开始。这张表格显示的中心思想特别有用的一些Lowenheim-Skolem定理的证明。

作为一个例子,前束的形式可能会考虑一个简单的模式,”对于每一个x,有一些y这样x熊(任意)关系米来y”;也就是说,

(3)(∀x)(∃y)米xy。

如果现在(3)与一个非空的域模型D那么,从集合论(一个原则公理的选择),存在一个函数f的x写f(x),挑出x一个相应的y。因此,“为每一个x,x熊的关系米来f(x)”;也就是说,

(4)(∀x)米xf(x)。

如果一个现在有对象吗D,那么可数子域名{一个,f(一个),f(f(一个)],。}已经包含足够的对象来满足(4),因此为了满足(3)。因此,如果(3)有任何模型,它有一个可数模型,这实际上是一个原始的子模型。

一个替代证明,1922年由Skolem避免吸引集理论的原则,已经被证明是有用的也建立微积分的完整性。而不是使用函数f和之前一样,一个可以任意用1。从方程(3)是正确的,必须有一些对象y这样1熊数量关系米来y,或者象征性的米1y,其中的一个y可称为2。当这个过程是无限重复,一个获得

(5)米12;米12·米23;米12·米23·米34;。,

所有这一切都是真实的在给定的模型。的论点是基本的,因为每个实例一个仅仅认为从“存在一些吗y这样n是米的y”即:(∃y)米ny——“让一个这样的y是n+ 1。“因此,每一个成员在一些模型(5)是正确的。然后就有可能推断出(5)的所有成员同时适用于一些model-i.e。,有一些的分配方式真理值其原子部分,这样所有的成员(5)将是正确的。因此,因此,(3)在一些可数模型是正确的。

的完备性定理

哥德尔原始证据的完整性密切相关,第二个定理证明。可能又会考虑所有的句子(5)不包含更多的量词。如果他们都是可以满足的,那么,它们同时可以满足的,(3)模型。另一方面,如果(3)没有模型,它的一些terms-say米12·。·米89 -不可以满足的;也就是说,their negations are重言式(命题演算的定理)。因此,∼米12∨。∨∼米89是一个无谓的重复,这是一个事实如果1 2。,9取而代之的是变量,如r,年代、。z;因此,∼米r年代∨。∨∼米yz在谓词演算,作为一个同义反复表达通常制定,是一个定理。然后易于使用的通常规则谓词演算推导还声明,“存在一个x这样,每一个y,x不是米的y”;也就是说,(∃x)(∀y)∼米xy。换句话说,(3)的否定是谓词演算的一个定理。因此,如果(3)没有模型,那么它的否定是谓词演算的一个定理。最后,如果一个句子是有效的(即。,if its negation has no model), then it is itself a theorem of the predicate calculus.

的不可判定性定理和减少课程

鉴于完备性定理,它遵循的任务决定是否任何句子都是谓词演算的一个定理是等价的决定是否任何句子都是有效的还是它的否定是可以满足的。

图灵的方法证明了这类问题不可判定的特别提示。曾经的概念机械过程结晶,这绝对是相对容易找到吗无法解决的problems-e.g。,停止的问题,它要求每一个图灵机它是否会停止的问题,从一个空白的磁带。换句话说,每个图灵机操作以预定的方式给出了根据最初(输入)磁带;现在我们考虑一个空白磁带的特殊情况和特殊问题机器是否最终会停止。这无限类的问题(对每台机器)是无法解决的。

图灵的方法表明,每一个这样的问题一个图灵机可以由一个句子表达的谓词演算,这样机器就会停止当且仅当这句话不可以满足的。因此,如果有一个决策过程有效性(或可满足性)的谓词演算的句子,然后停止的问题是可以解决的。

近年来(1962),图灵的配方改进,所需要的是相对简单的句子形式(∀x)(∃y)(∀z)米xyz开始时,所有量词;也就是说,米不包含更多的量词。因此,考虑到停止问题的不可解性,因此,即使对句子的简单的类谓词演算的量词∀∃∀,决策问题是无法解决的。此外,证据的方法也产生了一个程序,每个句子的谓词演算可以与上面给出的简单的形式。因此,类的∀∃∀句子形式“减少类。”(也有其他各种减少类)。