[科普中国]-一阶理论及其元逻辑

一阶理论是一种用一阶语言陈述的、并用一阶逻辑的规律作为证明工具的形式系统。一阶逻辑是不包括非逻辑符号和非逻辑公理的一阶理论。

定义数理逻辑所研究的一个重要内容1。一阶理论是一种用一阶语言陈述的、并用一阶逻辑的规律作为证明工具的形式系统。一阶逻辑是不包括非逻辑符号和非逻辑公理的一阶理论。其他的一阶理论，在其一阶语言中包括非逻辑符号，并在公理中包括非逻辑公理。元逻辑是关于形式系统的语法和语义的逻辑研究。
形式算术系统N形式系统、一阶理论这些抽象概念，可以从形式算术系统N中得到说明。系统N是自然数算术理论的形式化，建立系统 N所用的一阶逻辑是带等词(=)的系统。系统N的初始符号有：联结词和量词符号塡，→，凬；等词符号=；个体变元符号,,,…；个体常元符号 0,1；函数符号+，·；括号(,)。在初始符号中没有用到谓词变元和函数变元，其中个体常元和函数符号是非逻辑符号，其余的是逻辑符号。

形成规则系统 N的形成规则有项形成规则和公式的形成规则两类。项形成规则：①一个体常元是一项，一个体变元是一项；②如果a,b是项，则a+b和a·b是项；③只有适合①和②两条的是项。公式的形成规则：①如 a,b是项，则a=b是公式，称为原子公式；②如果A,B是公式,α是一个体变元，则塡A,A→B,(凬α)A(α)是公式；③只有适合①、②两条的是公式。在这些形成规则中出现的符号a,b,A,B和α，不是系统N中的符号，而是描述或陈述系统N时所使用的另一个称为元语言中的符号。a，b表示任一项，α表示任一个体变元，A,B表示任一公式。这些符号称为语法变元。A(α)表示α在A中出现（也可以不出现）。

一阶理论的语法研究元逻辑对形式系统的研究包括语法的和语义的两个方面。形式系统包括形式语言(符号、形成规则)、公理和推理规则三部分。如果只涉及符号、符号组合、公式序列的形状,公式的变形,就是语法方面的研究，叫做语法学。语法研究的一个重要概念是可证明性，即一个公式是不是在系统中可证明的，是不是系统中的定理。语法学研究形式系统的以下几个重要性质：①研究形式系统的一致性。其结果为：如果不是每一公式都是可证明的,或者不存在一个公式A，A和塡A都是可证明的,就说系统是一致的;否则，系统是不一致的。②研究形式系统的完全性。对于一阶逻辑，完全性是指每一普遍有效的公式都是定理；对于其他的一阶理论，如果任一闭公式A,或者A是定理,或者塡A是定理,就说系统是完全的;否则,系统是不完全的。③研究判定问题，即确定是否有一种机械方法对系统中的任意一个公式，用它都能机械地在有穷步内确定它是不是定理。通过语法研究所得到的定理叫做语法元定理。元定理不是系统自身之中的定理，而是关于系统的（性质的）定理。

一阶理论的语义研究在形式系统的语法研究过程中，是可以不涉及符号和公式的意义的。但是一个形式系统（形式理论）是一个有内容的理论的形式化。在构造一个形式系统,从而把一个有内容的理论形式化时,选取符号是要让它们反映被形式化的理论的概念或指称某种对象的。形成规则关于公式的规定，是要使公式成为被形式化的理论的语句的反映；公理的选择是要使得它们经解释后成为被形式化的理论的真语句。即一个形式系统的符号、公式等等是有预想的解释的，或是从具体理论抽象得来的。一个形式系统可以有不同的解释，预想的解释是它的主要的或标准的解释。关于形式系统的解释以及关于它的公式的意义的研究是语义研究的基本内容。
对于一阶理论T的形式语言L的解释，由一个非空的论域D和一赋值系υ组成。赋值系包括以下规定：①对每一个体变元，υ都赋与一个D中的元为值,记为。对每一个体常元，在赋值υ下的值是D中的一特定的元。对每一项a，在赋值υ下的值记为a。
② 如 R是一个n元谓词符号（常元），则R是D中一特定的n元谓词。
③ 如果ƒ是一个n元函数符号（运算）,则ƒ是D中一特定的n元运算。如果ƒ是n元函数符号，且a,a,…,a是项，则(ƒ(a,a,…,a))=ƒ(a,a…,a)。
④ 对于每一公式A,在赋值υ下的值或者为1（真）或者为0(假), 即A的值是1或0；如果A为原子公式R(a,…,a), (a,…,a) 所赋之值〈a,…,a〉属于R所赋之值 R，则(R(a,…,a))之值为1，否则为0。(塡A)之值为1，当且仅当A之值为0；(A凮B)之值为1；当且仅当A之值为0或B之值为1；((凬)A)之值为 1, 当且仅当设A的赋值已经给定，用D中的每一个体替代A中的时，A的值均为1 。在一阶理论T中，由于被断定的开公式如

x+y=y+x

和其闭公式

(凬x)(凬y)(x+y =y +x)

可以互相推导，其真假亦相同。因之在探究其值时，可以只考虑闭公式。设 A是理论T的一个闭公式，I是在论域M中对T的一个解释。在此解释下，A成为关于M的一个或真或假的语句 A。如 A在 M中为真，则称〈M,I〉为A 的一个模型。设∑为理论 T的一个闭公式集，〈M,I〉是∑的模型,当且仅当〈M,I〉是∑中每一公式的模型。如〈M,I〉是理论T的公理集的模型,则称〈M,I〉为理论T的模型。一组有模型的公式又称为可满足的。
形式系统 N的标准解释，是取自然数域为论域，个体常元 0和1分别解释为自然数域中的 0和1，函数符号+与·解释为通常的加和乘。
真、假、赋值、可满足性、模型等等都是语义概念。从语义学考虑，一个形式系统如果至少有一个模型，那末它就是一致的，如果每一真的公式都是可证明的，该形式系统就是完全的。对于判定问题，就是研究是否有一种机械的方法，能判定任意公式是不是真的。
元逻辑也研究语法和语义之间的关系。例如语法概念可证性和语义概念真理性，在20世纪30年代以前的数学中一般都是相混同的，K.哥德尔和A.塔尔斯基在元逻辑方面的工作证明，真理性是不能等同于可证性的。
元逻辑的一些重要结果 元逻辑在命题演算、一阶逻辑以及一阶数学理论等方面已有若干重要的结果。命题演算的元逻辑结果有：①可靠性定理。根据这条定理，命题演算的定理都是重言式即常真的。
② 一致性定理。命题演算是一致的，对任一公式A及其否定塡A,若其一是重言式,则另一必是常假的。根据可靠性定理，A和塡A不可能都是可证的。
③ 完全性定理。凡重言式都是定理，命题演算的每一公式都可变换成一个与之等值的合取范式，每一个重言的合取范式,都可以从可证公式∨塡,→∨,→(→∧),应用分离规则推演出来，即是可证明的。因此，变换成合取范式的原来那个公式是可证明的，即是定理。
④ 命题演算是可判定的。对于任一公式 A是否为重言式，是不是定理，都是可判定的。用真值表方法或求合取范式的方法，都能机械地在有穷步内判定一公式是否为重言式，因而是不是定理。
命题演算的重要元逻辑问题，可以说都已得到肯定的解决，留下的一个新的有兴趣的问题是寻找判定一公式是否为重言式的快速判定方法。
关于一阶逻辑的重要的元逻辑结果有：①可靠性定理，即凡定理都是普遍有效的。
② 一致性定理。一阶逻辑是一致的。若取只有一个个体a的集为论域，凬αA(α)即为A(a)，而所有量词全部消去。于是，所有的公式都可看作是命题演算的公式。因此，对任一公式A，不可能A和塡A都可证。
③ 完全性定理。一阶逻辑在语义意义下是完全的，即凡普遍有效的公式都是定理。完全性定理还有一个更强的形式，即每一一致的公式集都有模型，都是可满足的。这一更强形式的完全性定理也称强完全性。根据完全性定理，如果塡A不是定理，则塡A不普遍有效，因此，A是可满足的。说一公式A是一致的,即从A不可能推出两个矛盾的公式， 不外是意谓塡A不是定理。所以，如果A是一致的，那末A是可满足的。这样，对于一阶逻辑来说，语义概念的普遍有效性、可满足性，与语法概念的可证性和一致性，是相互符合的。
④ 紧致性定理。一个公式集г是有模型的,当且仅当它的每一有穷子集是有模型的。根据一个比较容易证明的定理，公式集г是一致的,当且仅当它的每一有穷子集是一致的。紧致性定理能直接从完全性定理推出。
⑤ 勒文海姆-司寇伦定理,简称LS定理。该定理表明,如一公式或一公式集有模型,则它有一可数模型。LS定理是L.勒文海姆、T.司寇伦证明的。从哥德尔对完全性定理的原来证明能直接推出LS定理。LS定理还有由塔尔斯基改进了的形式。LS定理的直接证明方法，为模型论以及集合论中相对一致性和独立性的证明，提供了一个非常有用的工具。紧致性定理和LS定理是模型论的基础性定理。
⑥ 判定问题的结果。A.图林和A.丘奇在1936年分别证明了一阶逻辑是不可判定的，即不存在判定一个一阶逻辑的公式是否普遍有效（可满足）或是否可证的机械方法。图林证明，图林机的停机问题，即任一图林机从空白带开始计算是否最后停机是不解的（见图林机器理论）。他又证明对于一台图林机T是否停机的问题,可用一阶逻辑的一个公式 A表达，使得T停机当且仅当A不可满足，即停机问题可以归约到一阶逻辑的判定问题。因此，如果一阶逻辑公式的普遍有效性（可满足性）是可判定的，则停机问题是可解的。但这与停机问题不可解的结果相矛盾，因之一阶逻辑公式的判定问题也是不可解的。除了这个一般性的结果，还有一阶逻辑公式集的子集的判定问题。这通常是用前束范式对公式分类。关于这种分类的判定问题，在下述意义下已几乎完全解决了，即每个前束类或者是可判定的或者是归约类（不可判定的）。这方面的一个重要结果是,具有形式凬ヨ凬A(,,)的公式,其中仅包含若干二元谓词或一个二元谓词加上若干一元谓词构成了一个关于可满足性的归约类。另外，只包含一元谓词的公式类是可判定的。

本词条内容贡献者为:

杜强 - 高级工程师 - 中国科学院工程热物理研究所