补充资料：一阶理论及其元逻辑

    　　数理逻辑所研究的一个重要内容。一阶理论是一种用一阶语言陈述的、并用一阶逻辑的规律作为证明工具的形式系统。一阶逻辑是不包括非逻辑符号和非逻辑公理的一阶理论。其他的一阶理论，在其一阶语言中包括非逻辑符号，并在公理中包括非逻辑公理。元逻辑是关于形式系统的语法和语义的逻辑研究。
　　
　　形式算术系统N 　 形式系统、一阶理论这些抽象概念，可以从形式算术系统N中得到说明。系统N是自然数算术理论的形式化，建立系统 N所用的一阶逻辑是带等词(=)的系统。系统N的初始符号有：联结词和量词符号塡，→，凬；等词符号=；个体变元符号x,y,z,...；个体常元符号 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中的这次出现不是约束的，例如，在公式(凬y)((凬x)F(x)→F(y))中，量词(凬y)的辖域是(凬x)F(x)→F(y)，(凬x)的辖域是F(x)，x和y在(凬y)((凬x)F(x)→F(y))中的两次出现都是约束的。在公式(凬x)F(x)→F(y)中,x两次出现是约束的,y的唯一一次出现则是自由的。个体变元α在A中可以既有约束出现又有自由出现，例如(凬x)F(x)→F(x)。个体变元α在A中是自由(约束)的,如果它在A中有自由（约束）出现。不含有自由 (个体)变元的公式称为闭公式。
　　
　　系统 N的公理：
　　
　　A1,A→(B→A)；
　　
　　A2,(A→(B→C))→((A→B)→(A→C))；
　　
　　A3,(塡A→塡B)→((塡A→B)→A)；
　　
　　A4,(凬α)(A→B)→(A→(凬α)B),
　　其中α在A中没有自由出现；
　　
　　A5,(凬α)→A(a),
　　其中A(α)是公式，a是项,并且a对于在A(α)中的α是自由的，即：如果β 是项a中的一个体变元，那末α在A(α)中的自由出现都不在(凬β)的辖域之中；
　　
　　A6,α=α；
　　
　　A7,α₁=β₁→(α₂=β₂→...(α_n=β_n(→(A(α₁,α₂,...α_n
　　
　　
　　
　　→A(β₁,β₂,...,β_n)))...)；
　　
　　N1,塡(α+1=0)；
　　
　　N2,α+1=β+1→α=β；
　　
　　N3,α+0=α；
　　
　　N4,α+(β+1)=(α+β)+1；
　　
　　N5,α·0=0；
　　
　　N6,α·(β+1)=α·β+α。
　　
　　A1～A7是一般的逻辑公理，其中A6～A7是关于等词的公理；N1～N6是非逻辑公理，或者说是系统 N的特有的公理。这些公理都是用语法变元陈述的，是一些公理模式，而不是单个公理。每一公理模式都代表无穷条公理，如根据A6,x=x,y=y,z=z等等都是公理。用公理模式陈述公理，是为了在推理规则中可以不用代入规则。
　　
　　系统N的推理规则或称变形规则为：
　　
　　R1，分离规则，从A和A→B可以推出B；
　　
　　R2，概括规则，从A(α)可以推出(凬α)A(α)；
　　
　　R3，数学归纳原则,从A(0)和(凬α)(A(α)→A(α+1))可以推出(凬α)A(α)，
　　
　　其中R1、R2是一阶逻辑的规则，R3是 N中特有的规则。
　　
　　所谓定理是指从公理应用推理规则推演出来的公式，或者说，是有证明的公式。一个证明是公式的有穷序列，其中每一公式或者是公理或者是从序列中前面的公式应用推理规则得出的。一个证明也说是它的最后公式的证明。
　　
　　系统 N满足关于形式系统的下述要求：任给一符号，能够机械地检查它是不是 N中的符号；任给一符号的组合，能够机械地检查它是不是 N的一公式；任给一公式可以机械地检查它是不是 N的一个公理；给定一有穷的公式序列，能够机械地检查它是不是 N中的一个正确的证明。
　　
　　一阶理论的语法研究 　元逻辑对形式系统的研究包括语法的和语义的两个方面。形式系统包括形式语言(符号、形成规则)、公理和推理规则三部分。如果只涉及符号、符号组合、公式序列的形状,公式的变形,就是语法方面的研究，叫做语法学。语法研究的一个重要概念是可证明性，即一个公式是不是在系统中可证明的，是不是系统中的定理。语法学研究形式系统的以下几个重要性质：①研究形式系统的一致性。其结果为：如果不是每一公式都是可证明的,或者不存在一个公式A，A和塡A都是可证明的,就说系统是一致的;否则，系统是不一致的。②研究形式系统的完全性。对于一阶逻辑，完全性是指每一普遍有效的公式都是定理；对于其他的一阶理论，如果任一闭公式A,或者A是定理,或者塡A是定理,就说系统是完全的;否则,系统是不完全的。③研究判定问题，即确定是否有一种机械方法对系统中的任意一个公式，用它都能机械地在有穷步内确定它是不是定理。通过语法研究所得到的定理叫做语法元定理。元定理不是系统自身之中的定理，而是关于系统的（性质的）定理。
　　
　　一阶理论的语义研究 　在形式系统的语法研究过程中，是可以不涉及符号和公式的意义的。但是一个形式系统（形式理论）是一个有内容的理论的形式化。在构造一个形式系统,从而把一个有内容的理论形式化时,选取符号是要让它们反映被形式化的理论的概念或指称某种对象的。形成规则关于公式的规定，是要使公式成为被形式化的理论的语句的反映；公理的选择是要使得它们经解释后成为被形式化的理论的真语句。即一个形式系统的符号、公式等等是有预想的解释的，或是从具体理论抽象得来的。一个形式系统可以有不同的解释，预想的解释是它的主要的或标准的解释。关于形式系统的解释以及关于它的公式的意义的研究是语义研究的基本内容。
　　
　　对于一阶理论T的形式语言L的解释，由一个非空的论域D和一赋值系υ组成。赋值系包括以下规定：①对每一个体变元x，υ都赋与一个D中的元为值,记为x^υ。对每一个体常元，在赋值υ下的值是D中的一特定的元。对每一项a，在赋值υ下的值记为a^υ。
　　
　　②　如 R是一个n元谓词符号（常元），则R^υ是D中一特定的n元谓词。
　　
　　③　如果??是一个n元函数符号（运算）,则??^υ是D中一特定的n元运算。如果??是n元函数符号，且a₁,a₂,...,a_n是项，则(??(a₁,a₂,...,a_n))^υ=??^υ(a,a...,a)。
　　
　　④　对于每一公式A,在赋值υ下的值或者为1（真）或者为0(假), 即A^υ的值是1或0；如果A为原子公式R(a₁,...,a_n), (a₁,...,a_n) 所赋之值〈a,...,a〉属于R所赋之值 R^υ，则(R(a₁,...,a_n))之值为1，否则为0。(塡A)^υ之值为1，当且仅当A^υ之值为0；(A凮B)^υ之值为1；当且仅当A^υ之值为0或B之值为1；((凬)Ax)^υ之值为 1, 当且仅当设A的赋值已经给定，用D中的每一个体替代A中的x时，A的值均为1 。在一阶理论T中，由于被断定的开公式如
　　x+y=y+x
　　和其闭公式
　　(凬x)(凬y)(x+y =y +x)
　　可以互相推导，其真假亦相同。因之在探究其值时，可以只考虑闭公式。设 A是理论T的一个闭公式，I是在论域M中对T的一个解释。在此解释下，A成为关于M的一个或真或假的语句 A_I。如 A_I在 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不可能都是可证的。
　　
　　③　完全性定理。凡重言式都是定理，命题演算的每一公式都可变换成一个与之等值的合取范式，每一个重言的合取范式,都可以从可证公式p∨塡p,p→p∨q,p→(q→p∧q),应用分离规则推演出来，即是可证明的。因此，变换成合取范式的原来那个公式是可证明的，即是定理。
　　
　　④　命题演算是可判定的。对于任一公式 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不可满足，即停机问题可以归约到一阶逻辑的判定问题。因此，如果一阶逻辑公式的普遍有效性（可满足性）是可判定的，则停机问题是可解的。但这与停机问题不可解的结果相矛盾，因之一阶逻辑公式的判定问题也是不可解的。除了这个一般性的结果，还有一阶逻辑公式集的子集的判定问题。这通常是用前束范式对公式分类。关于这种分类的判定问题，在下述意义下已几乎完全解决了，即每个前束类或者是可判定的或者是归约类（不可判定的）。这方面的一个重要结果是,具有形式凬xヨ_u凬yA(x,_u,y)的公式,其中仅包含若干二元谓词或一个二元谓词加上若干一元谓词构成了一个关于可满足性的归约类。另外，只包含一元谓词的公式类是可判定的。
　　
　　关于形式数学系统，有如下几个结果：①最早证明并且也是最重要的结果是哥德尔在1931年证明的两个不完全性定理。第一个不完全性定理为：一个满足条件①一致的，②适当丰富，即足以展开一个适量的自然数算术理论的形式系统S，是不完全的。例如，系统N是不完全的。在这样的系统 S中，存在不可判定的语句，即不包含自由个体变元的闭公式 A，A和塡A都是不可证明的。经解释后，根据排中律A与塡A二者之中必有一真，因此，在 S中有一真的但不可证明的语句。并且这样的形式系统 S是不可能完全的，即如果把一个原来不可证的公式作为公理加到 S中，则在新的系统中总又可以构造出另一个闭公式，而且这个闭公式及其否定在这新的系统中都是不可证的。从这个定理还能推得，系统 S的真语句集是不能在 S中定义的，第一个不完全性定理显示了形式系统的固有局限性，表明一个内容丰富的理论是不能完全形式化的。第二个不完全性定理表明，满足上述条件①、②的形式系统S的一致性，是不能在系统S自身中证明的。它同时还表明，D.希尔伯特所提出的证明古典数学一致性的方案是不能实现的。
　　
　　②　关于一致性的结果。W.阿克曼于1924年证明对数学归纳原则加以限制的经典数论的形式系统是一致的。在这方面，最著名的结果是G.根岑于1936年证明经典数论系统 N是一致的。根岑在证明中，放宽了希尔伯特对元逻辑研究所用方法的限制,使用了超穷归纳,超穷归纳是不能在系统 N中形式化的。一致性问题研究的另一个方向，是研究经典数论与直觉主义数论之间的关系。哥德尔在1933年找到了经典数论在直觉主义数论中的一个解释。因此，如果直觉主义数论是一致的，则经典数论也是一致的。哥德尔还在1958年发表了另一个结果，即应用原始递归泛函得到了经典数论语句的一个构造性解释。
　　
　　③　关于判定问题的结果。这类结果包括可判定性的和不可判定性两个方面。关于可判定性的结果有：M.普拉斯伯格证明只有一个加法运算的自然数算术理论是可判定的；塔尔斯基证明初等代数和初等几何是可判定的。不可判定性的结果有：象 N这样的系统的真语句集是不可判定的，没有判定一个语句是否真的机械方法。在象N 这样的系统中，一切递归的或可判定的函数和谓词都是可表示的，而系统的语言中的谓词"真"却不是在系统中可表示的或可定义的，因此，它也不是递归的或可判定的。一个著名的结果是,Ю.В.马季亚谢维奇在1970年证明，希尔伯特第10个问题是不可解的，即丢番图方程p(x₁,...,x_n)=0是否有整数解是不可判定的。
　　

说明：补充资料仅用于学习参考，请勿用于其它任何用途。