用户:C44986054/数理逻辑/一阶逻辑
本篇是数理逻辑的第三章
基本符号
简介
不同于命题逻辑，自一阶逻辑，我们开始关心一段叙述如何组成。
从一般语言叙述的构成来看，如果我们不照惯例，而把所有的东西都说得清清楚楚的话，照理来说一段叙述应该是 "主词+动词+受词"、"主词+动词"、"主词+动词谓语+修饰词"的主要架构，配上动词、主词和受词的修饰语或修饰子句构成的。但数学关心的，只是一个对象有怎么样的状态，则另一个对象会有怎样的状态，也就是"主词+动词谓语+修饰词"的架构配上推理的关系。描述状态不外乎辨识特征，事实上跟定义"集合"的本质，也就是辨别一个群体的共通性做的事是一样的。
一段叙述都有它叙述的对象；比如说「业界(有人)对这个产品有兴趣」、「(所有)外国旅客入境前都要防疫隔离」；逻辑学上，"有人"(更一般的说存在一个人)跟"所有人"(注意到所有外国旅客是不是本国籍且身在我国的所有人的略语)这两个表述叙述对象范围的词语被称为量词(quantifier)。显然外国的旅客不只一个，这就是需要在语意上说明描述范围的变数(variable)，也就是每个变数都有它的取值范围。(外国旅客是从所有人类里取值，找有外国国籍且身在我国的人类)
数理逻辑上，"所有的变数$\displaystyle x$的取值满足合式公式$\mathcal{A}$"以$(\forall x)\mathcal{A}$代表；类似的"存在变数$\displaystyle x$的取值满足合式公式$\mathcal{A}$"以$(\exists x)\mathcal{A}$代表，其实也就是$\neg(\forall x)(\neg\mathcal{A})$。类似的，$(\forall x)\mathcal{A}$就是$\neg(\exists x)(\neg\mathcal{A})$。
要构成一段叙述，我们还需要其他要素；比如说"这个产品"就是一个常数(constant)；有兴趣代表著一种人和产品之间的关系；类似的，外国旅客的"定义"是来自国家和入境旅客的国籍隶属"关系"。在逻辑学上我们用谓词符号(predicate letter)去形式的表示"关系"。
数理逻辑上，两个变数$\displaystyle x$和$\displaystyle y$的谓词符号通常会用$\displaystyle A_{i}^{2}(x,y)$代表；其中$\displaystyle i$提醒我们理论里可能不只一种"关系"，$\displaystyle 2$提醒我们是描述"两者之间的关系"，这是因为关系可以描述到两者以上(比如说三维空间中某一点在某区域内，那这点的三个座标跟这个区域就有"隶属"关系)。只有一个对象的"谓词符号"可以代表隶属于特定群体的关系(也就是固定群体变数的取值)
特别注意到$\displaystyle A_{i}^{2}(x,y)$跟$\displaystyle A_{i}^{2}(y,x)$是不一样的东西，就好比如果甲是乙的父亲的话，反过来乙并不一定是甲的父亲；对某些关系来讲摆放的变数顺序是很重要的，但像是相等、朋友关系等等就不是重要的。
另日常生活中会提到「你的身分」或是「一对夫妻的第一个小孩」这种可以用关系描述的片语。但是这两段片语有个共同的特征；每个人只有一种身分；同样每对夫妻也只有一个第一个小孩；与其描述隶属"关系"，我们反而对独有的那个对应物更有兴趣，一般来说，是不同组变数的取值能对到的唯一值(比如说加法的结果都只有一个)，这在逻辑学上以函数符号(function letter)去形式的代表。
数理逻辑里，一组变数$\displaystyle x_1,x_2,....,x_n$的一个函数符号是以$\displaystyle f_{i}^{n}(x_1,x_2,....,x_n)$代表。
当然一般的叙述还不只有这些，像是「(所有)亲子关系都可以用核酸检定法验证」、「(所有)国家都应该保护它的侨民」这种对"关系"和"变数取值范围"(甚至函数符号)使用量词的叙述。逻辑学上有两种不一样的处理；第一种是把关系、变数取值范围和函数符号都解释为集合(为何如此很快下面"一阶逻辑的语意"一节就会说明)，也就是说，我们需要一个以集合为变数取值的形式理论，称为集合论。另一种方法，是仿造日常语言，直观的把量词扩充到关系和函数符号甚至取值范围，但是这种方法在语意的解释上一样需要集合论，而且语意跟形式理论的联系不是很好，所以第一种方法是大部分数学家常用的方法。虽然一套严谨的集合论是依赖于一套有量词的形式理论，但我们仍然可以先非正式的讨论量词的语意，以此为动机选取逻辑公理。等到有正确的集合论以后，再回过头来严谨讨论一阶逻辑的语意(参见一阶逻辑的模型)。第二种方法我们还是会在附录的二阶逻辑详述，让读者参考。
量词只能施用在变数上的形式理论被称为一阶逻辑(first-order logic)，反之称为高阶逻辑(Higher-order logic)。事实上有另外一种和本篇大异其趣的数理逻辑，是以"函数"对应为基础建构的类型论，类型论就是一种高阶逻辑。
量词
对于$(\forall y)\mathcal{B}$，我们称$\mathcal{B}$是量词$\forall y$的范围(scope)，如果变数$\displaystyle y$出现在量词$\forall y$的范围里，我们称此次出现的$\displaystyle y$是被限制的(bounded)；反之称为自由的(free)。在一段合式公式里，同个变数可能在某个地方自由，但另一个地方是被限制的，如
$\forall y[A^{2}_{1}(x,y)]\Rightarrow A^{1}_{1}(y)$
第一次出现的$\displaystyle y$是被限制的；但第二次出现是自由的。我们说$\displaystyle x$在一条合式公式里都不自由的时候，代表$\displaystyle x$每个地方都被限制，或更有可能是$\displaystyle x$根本没出现过。
$\displaystyle y$完全不在量词$\forall y$的范围时，$(\forall y)\mathcal{B}$跟$\mathcal{B}$在语意上等价。
项
很显然一段"合法"的叙述，单有对象是没有用的，比如说「医生!」、「长孙!」、「独子的身分!」都是一些语意隐晦的叙述。为了更清楚说明这一点，考虑到一般情况下，函数符号是可能被连续施用(比如说二次多项式就是加法跟乘法的连续施用结果)，为此我们定一个新名词，项(term)：
$\displaystyle (1)$变数和常数都是项
$\displaystyle (2)f^{n}_{k}$是一个函数符号，$\displaystyle t_1,t_2,....,t_n$是项，则$\displaystyle f^{n}_{k}(t_1,t_2,....,t_n)$是项。
$\displaystyle (3)$项只能透过以上两点建构出来。
所谓的原子公式(atomic formula)，也就是最基本的一段叙述，型如$\displaystyle A^{n}_{k}(t_1,t_2,....,t_n)$，其中$\displaystyle t_1,t_2,....,t_n$是一组项。也就是形如「医生是(她的)长孙!」「独子的身分是医生!」。而合式公式就是以原子公式为基础，配上命题连接词跟量词组合而成的!
一阶逻辑的语意
本节的目的在于直观的解释新增公理的合理性，而不是给予一阶逻辑的语意(semantics)一套严谨的理论。
虽然从动机上来讲，我们需要小心地确认量词于一般叙述的意义，由此才能设计出让我们满意的一阶逻辑形式理论；但从推演的角度来讲，一阶逻辑的语意只是公理化集合论架构下的附属品(实用角度来讲，一种方便确定一段$\displaystyle wf$是不是定理的办法)，说直接一点，与下面将建构出来的形式理论相容的语意解释不只有一种，就像命题逻辑的形式理论，并没有禁止多值逻辑的语意诠释。
解释
要定义与甲的亲子关系，事实上可以用列举甲的所有儿女来定义。比较数学化的方式，就是用(甲,儿子1)、(甲,儿子2)、....、(甲,女儿1)、(甲,女儿2),....的方法；那全球(针对父亲)的亲子关系就可以写成
(父親1,父親1的兒子1)、(父親1,父親1的兒子2)、....、(父親1,父親1的女兒1)、(父親1,父親1的女兒2)、....
(父親2,父親2的兒子1)、(父親2,父親2的兒子2)、....、(父親2,父親2的女兒1)、(父親2,父親2的女兒2)、....
. . . .
. . . .
. . . .
. . . .
所以说的一般一点，两者之间的关系就是(x,y)这样的二元有序对集合，只不过x和y的取值范围都有限制；像是这个例子就是从"所有人类中取值"，配成(人类A,人类B)这样的有序对；但人类A必须都是男性且生过小孩；而且随意把人类B配在有序对的第二个位置，不见得人类B就是人类A生的。当然除了笨拙地列举去定义亲子关系，我们可以用DNA定序、或是其他"比较聪明"的方法去定义，但这就是另外个故事了，牵涉到满足一段叙述的所有值，怎么组成一个集合；而满足两段不同叙述的两个集合会不会相等的问题。以我们目前的能力还无法严谨的去讨论。
所以关系是所有二元有序对(x,y)构成的集合的一部分(称为子集合)。如果把所有变数取的值聚集起来，组成一个集合，写成$\displaystyle D$，那我们用$\displaystyle D^2$代表所有可能取值的二元有序对所聚集而成的集合。
说的更一般，n个变数之间的关系就是$\displaystyle D^n$──也就是所有可能取值的n元有序对$\displaystyle(x_1, x_2, ...., x_n)$构成的集合──的子集合
同样的道理，我们可以把n个数字的相加表达为$\displaystyle(x_1, x_2, ...., x_n, x_1+x_2+....+x_n)$这样的关系，但从叙述的目的上，我们比较喜欢$D^n\to D$这样的符号提醒自己这是一个对应，是从每个n元有序对对应到一个$\displaystyle D$里的值(一个"够广大"的取值范围要包括加法的结果!)。而更一般的来说，$\displaystyle f_{i}^{n}(x_1,x_2,....,x_n)$就是被解释成$D^n\to D$这样的对应。
如此一来我们就有一套解释一阶逻辑语意的要素：
一个一阶逻辑的解释(interpretation)$\displaystyle M$需要有以下的要素：
(1)所有变数取值的范围，称为论域(domain of discourse)。以$\displaystyle D$代表。
(2)谓词符号$\displaystyle A_{i}^{n}$被解释为某个$\displaystyle D^n$的子集合，以${(A_{i}^{n})}_{M}$代表
(3)函数符号$\displaystyle f_{i}^{n}$被解释成某个从$D^n\to D$的对应规则(也就是函数)，以${(f_{i}^{n})}_{M}$代表
(4)常数$\displaystyle a$被解释成某个属于$\displaystyle D$的固定值，以$\displaystyle a_M$代表
接下来我们说明这些要素如何适当的解释一阶逻辑
变数的解释
穷人类能力所及，我们最多可以讨论跟自然数一样多的变数$\displaystyle x_1, x_2, x_3,....$所以一组变数的取值，就是从$\displaystyle D$取出如$\displaystyle a_1, a_2, a_3,....$这样的序列，以${\{a_i\in D\}}_{i\in\mathbb{N}}$简记， 其中$i\in\mathbb{N}$的意思是$\displaystyle i$是自然数(也就是$\displaystyle i$在自然数集合$\mathbb{N}$里)，$a_i\in D$的意思就是第$\displaystyle i$个变数从$\displaystyle D$取的值是$\displaystyle a_i$。如果论域在上下文很明显的话，我们会把变数取值简记为${\{a_i\}}_{i\in\mathbb{N}}$。
(事实上序列是一个由$\mathbb{N}$到$\displaystyle D$的对应，所以序列也是一个函数；所以也是一个关系，从而更能看成一个二元有序对的集合)
项的解释
所有变数的取值是${\{a_i\}}_{i\in\mathbb{N}}$，在这种情况下项在$\displaystyle D$的对应值如下
(1)变数$\displaystyle x_j$的对应值是$\displaystyle a_j$；常数$\displaystyle a$的对应值是$\displaystyle a_M$
(2)在变数取值${\{a_i\}}_{i\in\mathbb{N}}$下，项$\displaystyle t_1, t_2,....,t_n$的对应值分别是$\displaystyle (t_1)_M, (t_2)_M, ...., (t_n)_M$，那$\displaystyle f^{n}_{k}(t_1,t_2,....,t_n)$在${\{a_i\}}_{i\in\mathbb{N}}$下的对应值是
- $\displaystyle {(f^{n}_{k})}_M[(t_1)_M, (t_2)_M, ...., (t_n)_M]$
注意$\displaystyle f(a_1, a_2,....,a_n)$代表依照函数$\displaystyle f$的对应规则下n元有序对$\displaystyle (a_1, a_2,....,a_n)$所对应的函数值。直观来说，就是输入了n个变数值所得出的"输出值"。一个最简单的输出规则，就是输入$\displaystyle (a_1, a_2,....,a_n)$会输出$\displaystyle a_j$(也就是俗称的第$\displaystyle j$个分量)
逻辑符号的解释
事实上一阶逻辑的合式公式规则，只是多要求：
- 原子公式是$\displaystyle wf$
- $\mathcal{B}$是$\displaystyle wf$，则$(\forall x_i)\mathcal{B}$也是$\displaystyle wf$
如此一来，我们可以依照合式公式规则给所有的$\displaystyle wf$解释：
$\mathcal{B}$和$\mathcal{C}$是$\displaystyle wfs$。$\displaystyle A_{i}^{n}$是n元谓词符号。变数的取值为${\{a_i\}}_{i\in\mathbb{N}}$之下，项$\displaystyle t_1, t_2, ....,t_n$的取值分别为$\displaystyle {(t_1)}_M, {(t_2)}_M, ...., {(t_n)}_M$，则
(1)${\{a_i\}}_{i\in\mathbb{N}}$满足$\displaystyle A_{i}^{n}(\displaystyle t_1, t_2, ....,t_n)$当且仅仅当$\displaystyle ({(t_1)}_M, {(t_2)}_M, ...., {(t_n)}_M)\in {(A_{i}^{n})}_M$ (项对应值组成的有序对，在谓词符号所对应的关系里)
(2)${\{a_i\}}_{i\in\mathbb{N}}$满足$\neg\mathcal{B}$当且仅仅当${\{a_i\}}_{i\in\mathbb{N}}$不满足$\mathcal{B}$ (否定的直观定义)
(3)${\{a_i\}}_{i\in\mathbb{N}}$满足$\mathcal{B}\Rightarrow\mathcal{C}$当且仅仅当${\{a_i\}}_{i\in\mathbb{N}}$不满足$\mathcal{B}$或是${\{a_i\}}_{i\in\mathbb{N}}$满足$\mathcal{C}$ (去除满足$\mathcal{B}$却不满足$\mathcal{C}$的状况)
(4)${\{a_i\}}_{i\in\mathbb{N}}$满足$(\forall x_j)\mathcal{B}$当且仅当所有$i\neq j$则$\displaystyle c_i=b_i$的变数取值${\{c_i\}}_{i\in\mathbb{N}}$满足$\mathcal{B}$ (第$\displaystyle j$个变数在$\displaystyle D$任意取值要为真)
真假值与逻辑
由逻辑符号的语意，我们可以理解合式公式在解释$\displaystyle M$下的"真假"：
(1)合式公式$\mathcal{B}$在$\displaystyle M$为真当且仅仅当每组变数取值都满足$\mathcal{B}$，以符号${\models}_{M}\mathcal{B}$表示。
(2)合式公式$\mathcal{B}$在$\displaystyle M$为假当且仅仅当每组变数取值都不满足$\mathcal{B}$。
(3)$\displaystyle\Gamma$是一组一阶逻辑的$\displaystyle wfs$，如果所有$\displaystyle\Gamma$的$\displaystyle wf$在解释$\displaystyle M$下都是真的，称$\displaystyle M$是$\displaystyle\Gamma$的模型(model)
甚至一些合式公式是不随解释的选取而总是为真，也就是说，他在"逻辑上"就是正确的
如果对于任何解释$\displaystyle M$，${\models}_{M}\mathcal{B}$，称$\mathcal{B}$为逻辑上有效的(logically valid)。反之对于任何解释都为假的$\mathcal{B}$称为逻辑上无效的(logically invalid)或是直称矛盾。
一阶逻辑形式理论里的逻辑定理，依照我的们的期望理当是逻辑上有效的$\displaystyle wf$。其实一阶逻辑的逻辑上有效，就是仿造命题逻辑的恒等式定义的。
类似的，我们也可以定义逻辑上等价和逻辑上推出：
对于合式公式$\mathcal{B}$和$\mathcal{C}$
(1)$\mathcal{B}$在逻辑上推出$\mathcal{C}$当且仅仅当对于任何解释，满足$\mathcal{B}$的变数取值也会满足$\mathcal{C}$
- (也就是当且仅仅当$\mathcal{B}\Rightarrow\mathcal{C}$是逻辑上有效的)
(2)$\mathcal{B}$是一套$\displaystyle wfs$(也就是$\displaystyle\Gamma$)的逻辑结论(logical consequence)，当且仅仅当对于任何解释，满足所有$\displaystyle\Gamma$的$\displaystyle wf$的变数取值，也会满足$\mathcal{B}$。
(3)$\mathcal{B}$在逻辑上等价于$\mathcal{C}$当且仅仅当对于他们逻辑上可以推出彼此
- (也就是当且仅仅当$\mathcal{B}\Leftrightarrow\mathcal{C}$是逻辑上有效的)
重要的逻辑有效式
型式理论
(1)符号：
(a)量词：$\forall$
(b)命题连接词(propositional connectives)：$\neg,\Rightarrow$
(c)标点符号：逗号跟左右括弧。(但为了更方便阅读命题连接词施用的顺序，我们会额外采用中括弧跟大括弧)
(d)一定要有，但最多跟跟自然数一样多的变数符号。变数以小写的任何西方语言字母代表(可能附有上下标或是prime)，如$a,\,\beta',\gamma_3,\,\delta^4,\,\aleph^5_5$
(e)可能有函数符号，可能有常数。但一定会有谓词符号。这些符号都最多可以跟自然数一样多。
- 另外，我们用大写西方字母代表项，如$T,\,\Gamma$。
- 有时候谓词符号和函数符号里有大量的变数，为求简便起见，我们以${\big{<}a_k\big{>}}^{n}_{k=1}$ 代表 $a_1,....,\,a_n$；而项亦采用这个方法，将$T_1,....,\,T_n$简记为${\big{<}T_k\big{>}}^{n}_{k=1}$。
(2)合式公式($\displaystyle wf$)：
(1)所有原子公式是$\displaystyle wf$。
(2)如果$\mathcal{B},\mathcal{C}$是$\displaystyle wf$，$\displaystyle y$是一个变数，则$(\neg\mathcal{B}),(\mathcal{B}\Rightarrow\mathcal{C}),((\forall y)\mathcal{B})$都是$\displaystyle wf$。最外层的括弧，和包住$\forall y$的括弧，如果命题连接词施用的顺序很明显可以不用写。
(3)$\displaystyle wf$只能从上面两点建构出来。
- 没有特别声明的话，我们习惯用草写的大写字母代表$\displaystyle wf$；另外为了辨别方便，我们会对$\displaystyle wf$加上数字上下标或是prime，如${\mathcal{B}}_1$、$\mathcal{B}'$。
(3)公理：
- $\displaystyle (a)$逻辑公理：如果$\mathcal{B},\mathcal{C},\mathcal{D}$是$\displaystyle wf$
(A1)$\mathcal{B}\Rightarrow(\mathcal{C}\Rightarrow\mathcal{B})$
(A2)$[\mathcal{B}\Rightarrow(\mathcal{C}\Rightarrow\mathcal{D})]\Rightarrow[(\mathcal{B}\Rightarrow\mathcal{C})\Rightarrow(\mathcal{B}\Rightarrow\mathcal{D})]$
(A3)$[(\neg\mathcal{B})\Rightarrow(\neg\mathcal{C})]\Rightarrow[(\neg\mathcal{B}\Rightarrow\mathcal{C})\Rightarrow\mathcal{B}]$
(A4)$\displaystyle T$是一个项(里面出现的变数记为$\displaystyle t_j$)；$\displaystyle x$是一个变数。如果在$\mathcal{B}$里面，所有$\displaystyle t_j$的量词的范围里都没有自由的$\displaystyle x$(这个情况称在$\mathcal{B}$项$\displaystyle T$对$\displaystyle x$是自由的)，则
- $[(\forall x)\mathcal{B}(x)]\Rightarrow[\mathcal{B}(T)]$
$\mathcal{B}(T)$代表把$\mathcal{B}$里自由的$\displaystyle x$都取代为$\displaystyle T$
(A5)如果在$\mathcal{B}$里面，都没有自由的$\displaystyle x$则
- $[(\forall x)(\mathcal{B}\Rightarrow\mathcal{C})]\Rightarrow[\mathcal{B}\Rightarrow(\forall x)(\mathcal{C})]$
(A6)若$\mathcal{B}$是公理，则
- $(\forall a_1)(\forall a_2)....(\forall a_n)\mathcal{B}$
也是公理。
(A7)$[(\forall x_1)(\forall x_2)....(\forall x_n)(\mathcal{B}\Rightarrow\mathcal{C})]\Rightarrow[(\forall x_1)(\forall x_2)....(\forall x_n)(\mathcal{B})\Rightarrow(\forall x_1)(\forall x_2)....(\forall x_n)(\mathcal{C})]$
- 关于取代，我们根据(A4)做出以下的符号规定；合式公式表示成$\mathcal{B}(a_1,\,....,\,a_n)$不代表$\mathcal{B}$只有$a_1,\,....,\,a_n$是自由的；这仅仅是因为$\mathcal{B}(T_1,\,....,\,T_n)$代表每个出现自由$a_k$的位置，分别被项$T_k$所取代。
- ex.若以$\mathcal{B}(x,\,y)$代表$(\forall x)[A^{3}_1(x,\,y,\,z)]\Rightarrow(\forall y)[A^{3}_2(x,\,y,\,z)]$，那$\mathcal{B}(T,\,S)$的意思是
- $(\forall x)[A^{3}_1(x,\,T,\,z)]\Rightarrow(\forall y)[A^{3}_2(S,\,y,\,z)]$
- $\displaystyle (b)$真公理(proper axioms)：根据不同理论的需求而订制。
(4)推理规则：如果$\mathcal{B},\mathcal{C}$是$\displaystyle wf$，$\displaystyle x$是一个变数
MP律：$(\mathcal{B}\Rightarrow\mathcal{C})$跟$\mathcal{B}$可以推出$\mathcal{C}$。
其他的逻辑符号如下定义：
$\mathcal{A}\wedge\mathcal{B}:=\neg[\mathcal{A}\Rightarrow\neg(\mathcal{B})]$
$\mathcal{A}\vee\mathcal{B}:=(\neg \mathcal{A})\Rightarrow \mathcal{B}$
$(\exists x)(\mathcal{A}):=\neg[(\forall x)(\neg \mathcal{A})]$
而简写的规则，我们仅需将括弧规则里第二项的施用顺序改成
$\neg,\,\wedge,\,\vee,\,\forall,\,\Rightarrow,\,\Leftrightarrow$
注意到一阶逻辑的形式理论，只要把原子公式视为命题逻辑形式理论里的叙述字母，就可以完全引用之前的元定理。
(A4)是一切取代的最终极基础。所以为了方便起见，套用(T)和(DN)以后，我们可以得到(A4)的"$\exists$"形式：
若于$\mathcal{B}(x)$，$T$对$x$是自由的，则
$\vdash\mathcal{B}(T)\Rightarrow(\exists x)\mathcal{B}(x)$
而应用这个定理的时候，我们一样代称为应用(A4)。
推广律
公理(A7)可以稍加延伸，跟我们的直观连系在一起
元定理(定理的推广律):
$\ulcorner\vdash\mathcal{B}\urcorner\to\ulcorner\vdash(\forall x)\mathcal{B}\urcorner$
| 证明 |
|---|
|
假设$\mathcal{C}_1,\mathcal{C}_2,....,\mathcal{C}_n$就是$\mathcal{B}$的证明，那$\mathcal{C}_1$一定是公理，根据(A6)可以得到$\vdash(\forall x)\mathcal{C}_1$ 若对$\displaystyle i<k$都有$\vdash(\forall x)\mathcal{C}_i$，如果$\mathcal{C}_k$是公理的话显然$\vdash(\forall x)\mathcal{C}_k$；所以我们考虑有$\displaystyle l,m<k$使得 $\mathcal{C}_m:\mathcal{C}_l\Rightarrow\mathcal{C}_k$。 则根据归纳法的假设跟(A7) $\vdash(\forall x)\mathcal{C}_l\Rightarrow(\forall x)\mathcal{C}_k$ 配上$\vdash(\forall x)\mathcal{C}_l$就可以得到$\vdash(\forall x)\mathcal{C}_k$，以此归纳到$\mathcal{C}_n$也就是$\mathcal{B}$，故本元定理得证$\Box$。 |
以下就是最一般情况的推广律。
元定理($\displaystyle GEN$, Rule of Generalization):
$\mathcal{A}_1,\mathcal{A}_2,....,\mathcal{A}_n$里都没有自由的$\displaystyle x$，则
$\ulcorner\mathcal{A}_1,\mathcal{A}_2,....,\mathcal{A}_n\vdash\mathcal{B}\urcorner\to\ulcorner\mathcal{A}_1,\mathcal{A}_2,....,\mathcal{A}_n\vdash(\forall x)\mathcal{B}\urcorner$
| 证明 |
|---|
|
我们对前提条件的数量$\displaystyle n$做归纳。 若$\displaystyle n = 1$，前提条件就是$\mathcal{A}_1\vdash\mathcal{B}$，则根据推论元定理跟定理的推广律，会得到$\vdash(\forall x)(\mathcal{A}_1\Rightarrow\mathcal{B})$，再根据(A6)和MP律，就可以得到$\vdash\mathcal{A}_1\Rightarrow(\forall x)\mathcal{B}$，也就是本元定理要求的结果。 现在假设$\displaystyle n < k$的情况下元定理会成立，若$\mathcal{A}_1,\mathcal{A}_2,....,\mathcal{A}_{k-1}\vdash\mathcal{A}_k\Rightarrow\mathcal{B}$，根据归纳法的假设 $\mathcal{A}_1,\mathcal{A}_2,....,\mathcal{A}_{k-1}\vdash(\forall x)(\mathcal{A}_k\Rightarrow\mathcal{B})$ 配上(A5)，本元定理在$\displaystyle n = k$的情况就可以得到证明，故本元定理得证$\Box$。 |
GEN可以稍加修饰，以适合证明"$\exists$"形式的定理(以后简称 GENe)
元定理：
若$\displaystyle x$在$\displaystyle \Gamma$里的$\displaystyle wfs$里面都不自由，且$\mathcal{C}$里也没有自由的$\displaystyle x$
(1) $\ulcorner\Gamma\vdash\mathcal{A}\Rightarrow\mathcal{B}\urcorner\to\ulcorner\Gamma\vdash(\exists x)\mathcal{A}\Rightarrow(\exists x)\mathcal{B}\urcorner$
(2) $\ulcorner\Gamma\vdash\mathcal{B}\Rightarrow\mathcal{C}\urcorner\to\ulcorner\Gamma\vdash(\exists x)\mathcal{B}\Rightarrow\mathcal{C}\urcorner$
证明提示：使用(T)和(A4)
并有以下直观的选择律
元定理($Rule\ C$, Rule of Choice, 选择律)：
若$t$不曾出现在$\Gamma$和$\mathcal{A}(x)$里，则
$\ulcorner\Gamma\vdash\mathcal{A}(t)\Rightarrow\mathcal{B}\urcorner$且$\ulcorner\Gamma\vdash(\exists x)\mathcal{A}(x)\urcorner$$\to$$\ulcorner\Gamma\vdash(\exists t)\mathcal{B}\urcorner$
| 证明 |
|---|
|
(1)$\mathcal{A}(t)\Rightarrow\mathcal{B}$ (Hyp) (2)$(\exists t)\mathcal{A}(t)\Rightarrow(\exists t)\mathcal{B}$ (GENe) (3)$(\forall t)[\neg\mathcal{A}(t)]\Rightarrow[\neg\mathcal{A}(x)]$ (A4) (4)$(\forall x)\{(\forall t)[\neg\mathcal{A}(t)]\Rightarrow[\neg\mathcal{A}(x)]\}$ (GEN) (5)$(\forall x)(\forall t)[\neg\mathcal{A}(t)]\Rightarrow(\forall x)[\neg\mathcal{A}(x)]$ (MP with 4, A7) (6)$(\forall t)[\neg\mathcal{A}(t)]\Rightarrow(\forall x)[\neg\mathcal{A}(x)]$ (MP with 5, A5) (7)$(\exists x)\mathcal{A}(x)\Rightarrow(\exists t)\mathcal{A}(t)$ (MP with 6, T) (8)$(\exists x)\mathcal{A}(x)\Rightarrow(\exists t)\mathcal{B}$ (D1 with 2, 7) 至此再套上MP律，定理就会得证$\Box$。 |
所以由推广律，很容易证明以下关于"交换性"的定理
(1) $(\forall x)(\forall y)\mathcal{A}\vdash(\forall y)(\forall x)\mathcal{A}$
(2) $(\exists x)(\exists y)\mathcal{A}\vdash(\exists y)(\exists x)\mathcal{A}$
(3) $(\exists x)(\forall y)\mathcal{A}\vdash(\forall y)(\exists x)\mathcal{A}$
注意最后一个定理是一般来说是不能反向的，只要想到"对每个a，都有一个数(也就是-a)，使a+(-a)=0"，但是任取一个a的数(-a)和任意的数b，b+(-a)并不一定会为零。
量词表示的简化
为了让我们的叙述更好阅读，对于变数$\displaystyle x_1,x_2,....,x_n$和任意变数$\displaystyle x,y$、合式公式$\mathcal{B}$、和可被简记为$x\star y$，也就是只有$x$跟$y$完全自由的$\displaystyle A_{i}^{2}(x,y)$，我们定义：
$(\forall x\star y)(\mathcal{B}):=(\forall x)[(x\star y)\Rightarrow\mathcal{B}]$
$(\exists x\star y)(\mathcal{B}):=(\exists x)[(x\star y)\wedge\mathcal{B}]$
$(x_1,x_2,....,x_n\star y):=(x_1\star y)\wedge(x_2\star y)\wedge....\wedge(x_n\star y)$
也就是我们平常的"属于"、"等于"、"大于小于"都可以用这个方式简写
直观上我们比较常说"对所有a属于A且满足....的话....则...."会不会不会跟上面的话简化符号有所抵触呢?为了回答这个问题，首先有以下定理：
(abb)$\vdash[\mathcal{A}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{C})]\Leftrightarrow[(\mathcal{A}\wedge\mathcal{B})\Rightarrow\mathcal{C}]$
| 证明 |
|---|
|
($\Rightarrow$) $\mathcal{A}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{C})\vdash(\mathcal{A}\wedge\mathcal{B})\Rightarrow\mathcal{C}$ (1)$\neg(\mathcal{A}\Rightarrow\neg\mathcal{B})\Rightarrow\mathcal{C}$ (Hyp) (2)$\neg\mathcal{C}\Rightarrow(\mathcal{A}\Rightarrow\neg\mathcal{B})$ (MP with 1, T) (3)$(\neg\mathcal{C}\Rightarrow\mathcal{A})\Rightarrow(\neg\mathcal{C}\Rightarrow\neg\mathcal{B})$ (MP with 2, A2) (4)$\mathcal{A}\Rightarrow(\neg\mathcal{C}\Rightarrow\mathcal{A})$ (A1) (5)$\mathcal{A}\Rightarrow(\neg\mathcal{C}\Rightarrow\neg\mathcal{B})$ (D1 with 3, 4) (6)$(\neg\mathcal{C}\Rightarrow\neg\mathcal{B})\Rightarrow(\mathcal{B}\Rightarrow\mathcal{C})$ (T) (7)$\mathcal{A}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{C})$ (D1 with 5, 6) ($\Leftarrow$) $(\mathcal{A}\wedge\mathcal{B})\Rightarrow\mathcal{C}\vdash\mathcal{A}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{C})$ 注意到$\mathcal{A},\mathcal{B}\vdash\mathcal{A}\wedge\mathcal{B}$，所以$(\mathcal{A}\wedge\mathcal{B})\Rightarrow\mathcal{C},\mathcal{A},\mathcal{B}\vdash\mathcal{C}$。再由推论元定理就可以得证。 |
由此就可以证明以下定理($x\star y$代表$\displaystyle A_{i}^{2}(x,y)$；$x\ast y$代表$\displaystyle A_{j}^{2}(x,y)$)
$\vdash(\forall x\star T)(\forall y\ast S)\mathcal{B}\Leftrightarrow\forall x\forall y\{[(x\star T)\wedge(y\ast S)]\Rightarrow\mathcal{B}\}$
其中$\displaystyle S$是项；$\displaystyle y$不出现在项$\displaystyle T$中
| 证明 |
|---|
|
($\Rightarrow$) $(\forall x\star T)(\forall y\ast S)\mathcal{B}\vdash\forall x\forall y\{[(x\star T)\wedge(y\ast S)]\Rightarrow\mathcal{B}\}$ (1)$\forall x\{(x\star T)\Rightarrow\forall y[(y\ast S)\Rightarrow\mathcal{B}]\}$ (Hyp) (2)$(x\star T)\Rightarrow\forall y[(y\ast S)\Rightarrow\mathcal{B}]$ (MP with 1, A4) (3)$(x\star T)\Rightarrow [(y\ast S)\Rightarrow\mathcal{B}]$ (D1 with 2, A4) (4)$[(x\star T)\wedge(y\ast S)]\Rightarrow\mathcal{B}$ (MP with 3, abb) (5)$\forall x\forall y\{[(x\star T)\wedge(y\ast S)]\Rightarrow\mathcal{B}\}$ (GEN with 4 twice) ($\Leftarrow$) $\forall x\forall y\{[(x\star T)\wedge(y\ast S)]\Rightarrow\mathcal{B}\}\vdash(\forall x\star T)(\forall y\ast S)\mathcal{B}$ (1)$\forall x\forall y\{[(x\star T)\wedge(y\ast S)\Rightarrow\mathcal{B}]$ (Hyp) (2)$[(x\star T)\wedge(y\ast S)]\Rightarrow\mathcal{B}$ (MP with 2, A4 twice) (3)$(x\star T)\Rightarrow [(y\ast S)\Rightarrow\mathcal{B}]$ (MP with 2, abb) (4)$\forall y\{(x\star T)\Rightarrow [(y\ast S)\Rightarrow\mathcal{B}]\}$ (GEN with 3) (5)$(x\star T)\Rightarrow \forall y[(y\ast S)\Rightarrow\mathcal{B}]$ (MP with 4, A5) (6)$\forall x\{(x\star T)\Rightarrow \forall y[(y\ast S)\Rightarrow\mathcal{B}]\}$ (GEN with 5) |
由以上的定理，可以归纳出更多变数状况的简化式，且简化式前面的括弧可以"交换"的条件，是括弧中的项不能出现别的括弧里的变数。
更一般来说，仿照上面的证明，定理可以延伸为
$\vdash(\forall x)[\mathcal{A}\Rightarrow(\forall y)(\mathcal{B}\Rightarrow\mathcal{C})]\Leftrightarrow(\forall x)(\forall y)[(\mathcal{A}\wedge\mathcal{B})\Rightarrow\mathcal{C}]$
其中$\displaystyle y$在$\mathcal{A}$里不是自由的。
这个一般化定理之后将大大减化集合论的定理的推导和表示。
我们可以对"$\exists$"得出类似的定理
$(\exists x)(\exists y)(\mathcal{A}\wedge\mathcal{B}\wedge\mathcal{C})\vdash(\exists x)[\mathcal{A}\wedge(\exists y)(\mathcal{B}\wedge\mathcal{C})]$
但反过来是不对的，因为$\mathcal{A}\wedge(\exists y)\mathcal{D}$不总是能推出$\mathcal{A}\wedge\mathcal{D}$。
等号
若一阶逻辑的型式理论，配有一谓词符号$A^{2}_{i}(x,y)$(简记为$\displaystyle x = y$)，使下列$\displaystyle wfs$为此形式理论的定理：
(E1) $\displaystyle x=x$ (等号的自反性)
(E2) $(x=y)\Rightarrow[\mathcal{B}(x,x)\Rightarrow\mathcal{B}(x,y)]$ (等号的可代换性)
其中在$\mathcal{B}(x,x)$中$\displaystyle y$对$\displaystyle x$是自由的；而$\mathcal{B}(x,y)$是由$\mathcal{B}(x,x)$里一些自由的$\displaystyle x$被取代成$\displaystyle y$而成的
则称这个型式理论是带等号的一阶逻辑(with equality)。把(E1)和(A4)组合起来，很自然的确保"有人一定会跟指定数相等"：
$\vdash(\forall x)(\exists y)(x=y)$
等号的性质
(I) $\vdash T=T$
证明提示：(II) $\vdash (T=S)\Rightarrow(S=T)$
| 证明 |
|---|
|
(1)$(x=y)\Rightarrow[(x=x)\Rightarrow(y=x)]$ (E2) (2)$(x=y)\Rightarrow(y=x)$ (D2 with E1, 1) (3)$\forall x\forall y[(x=y)\Rightarrow(y=x)]$ (GEN) 现在取$\displaystyle x$为不在$\displaystyle T$中的变数；$\displaystyle y$取为不在$\displaystyle S$中的变数。套用两次(A4)，定理就可以得证。$\Box$ |
(III) $\vdash (T=S)\Rightarrow[(S=R)\Rightarrow(T=R)]$
| 证明 |
|---|
|
(1)$(y=x)\Rightarrow[(y=z)\Rightarrow(x=z)]$ (E2) (2)$(x=y)\Rightarrow[(y=z)\Rightarrow(x=z)]$ (D1 with II, 1) (3)$\forall x\forall y\forall z\{(x=y)\Rightarrow[(y=z)\Rightarrow(x=z)]\}$ (GEN) 现在取$\displaystyle x$为不在$\displaystyle T$中的变数；$\displaystyle y$取为不在$\displaystyle S$中的变数；$\displaystyle z$取为不在$\displaystyle R$中的变数。套用三次(A4)，定理就可以得证。$\Box$ |
(E2)的等价条件
元定理：
(E2)等价于要求以下两点
(1)对于不含函数符号、常数的原子公式$\mathcal{B}(x,x)$有
- $x=y\vdash \mathcal{B}(x,x)\Rightarrow \mathcal{B}(x,y)$
- 其中$\mathcal{B}(x,y)$来自于$\mathcal{B}(x,x)$中一个自由的$\displaystyle x$被取代为$\displaystyle y$
(2)对于任意函数符号$\displaystyle f_i^n(x_1,....,x_j,....,x_n)$有
- $x=y\vdash f_i^n(a,....,x,....,b) = f_i^n(a,....,y,....,b)$($\displaystyle x$和$\displaystyle y$摆在同个顺位上)
| 证明 |
|---|
|
从(E2)推理出两点是很显然的，因为(1)是(E2)的特殊情况；而(2)只不过是(E2)的特殊状况套用(D2)而已。 现在我们从这两点推出一般状况的(E2)。 (I)扩张到有含常数的原子公式
(II)扩张到含函数符号的原子公式
(III)一般$\displaystyle wf$的情况
最后，虽然我们以上证明的都是取代一次的状况，但是取代$\displaystyle n$次的情况，可以视为被取代$\displaystyle n-1$次的情况再取代一次；所以我们可以用取代一次的情况归纳到任意数量的取代，故(1)、(2)的要求和(E2)是等价的$\Box$ |
特别注意到如果把$x=y$换成某个符合(E1)、(E2)，$x$和$y$完全自由的$\mathcal{E}(x,\,y)$，也就是以$wf$而不是谓词符号为基础来定义"等号"的话，以上的定理和元定理还是会成立的。这是因为要求$x$和$y$在$wf$完全自由时确保了以(A4)进行代换时，得到和谓词符号完全同样的结果。
比如说，集合论就是以"属于$x$等价于属于$y$"去定义"x等于y"。
唯一性
$(\exists! x)\mathcal{B}(x):=(\exists x)\mathcal{B}(x)\wedge(\forall x)(\forall y)\{[\mathcal{B}(x)\wedge\mathcal{B}(y)]\Rightarrow (x=y)\}$
其中$\displaystyle y$是不出现在$\mathcal{B}(x)$的变数；$\displaystyle \mathcal{B}(y)$是来自于$\mathcal{B}(x)$中自由的$\displaystyle x$都被取代为$\displaystyle y$。
函数符号与唯一性
数学理论常常随著内容的推进，而需要符号上的简化；也就是一套型式理论增加新的符号(函数符号、常数符号)以后，我们仍然希望这个"新"型式理论和原来的型式理论，有同等的效力。具体来说，对每个新系统里的合式公式$\displaystyle\mathcal{B}$，有一个符号上的变换，将$\displaystyle\mathcal{B}$转变为原来系统中的合式公式$\displaystyle\mathcal{B}'$，并满足
(1)$\displaystyle\mathcal{B}$在旧理论内的话，$\displaystyle\mathcal{B}'$就是$\displaystyle\mathcal{B}$。
(2)$\vdash_2\mathcal{B}\Leftrightarrow\mathcal{B}'$
(3)$\ulcorner\,\vdash_2\mathcal{B}\,\urcorner\to\ulcorner\,\vdash_1\mathcal{B}'\,\urcorner$
其中，$\vdash_1$代表旧理论内可以推出；$\vdash_2$代表新理论内可以推出。
读者请自己检验，由(2)可以推出$\ulcorner\,\vdash_1\mathcal{B}'\,\urcorner\to\ulcorner\,\vdash_2\mathcal{B}\,\urcorner$，于是达到了一开始"效力等同"的要求!
直观的动机
"相反数"的存在是仰赖于一个事实──"存在一个唯一的数，和原来的数相加为零"；所以一般来说，如果旧理论可以证明$(\exists!x)\mathcal{B}(a_1,\,....,a_n,\,x)$，那直观上，可以用$\mathcal{B}[a_1,\,....,\,a_n,\,f^{n}_i(a_1,\,....,\,a_n)]$去"定义"一个新的函数符号$f^{n}_i$，去构成一个新的理论。(注意到如果没有$a_k$的话，函数符号就会"退化"成常数)
那新旧理论的$\displaystyle wfs$间要如何做符号转换呢?比如说，"相反数小于零"这个叙述明显是新理论里的叙述；那在旧理论，会把它叙述成"存在一个数，跟原来的数相加起来为零且这个数小于零。所以一般来说，如果在新理论里有形如$\mathcal{C}[....,\,f(T_1,\,....,\,T_n),....]$的$\displaystyle wf$，那在旧理论里，我们应该把它写成$(\exists x)[\mathcal{C}(....,\,x,\,....)\wedge\mathcal{B}(T_1,\,....,T_n,\,x)]$。(注意到不管是新旧理论，相反数唯一性存在性都是个定理)
一个唯一性的定理
以严谨的方式实践我们的动机前，需要一个辅助定理
$(\exists! x)\mathcal{B}(x)\vdash(\exists x)[\mathcal{B}(x)\wedge\mathcal{C}(x)]\Leftrightarrow(\forall x)[\mathcal{B}(x)\Rightarrow\mathcal{C}(x)]$ (aux)
| 证明 |
|---|
|
假设$t$不曾在$\mathcal{B}(x)$和$\mathcal{C}(x)$出现。 ($\Rightarrow$)
($\Leftarrow$)
|
新理论的假设
依照一开始的动机，新理论和旧理论都会满足
$(\exists!x)\mathcal{B}(a_1,\,....,a_n,\,x)$ (U')
其中$\big<a_k\big>^{n}_{k=1}$和$x$在$\mathcal{B}$里是完全自由的。(如此才能以A4与E2进行完全的代换)
但新理论加入了新的函数符号$f^{n}_i$，也就是加入了新公理
$\mathcal{B}[a_1,\,....,a_n,\,f^{n}_i(a_1,\,....,\,a_n)]$ (U)
注意到所有的公理形式都必须和$f^{n}_i$相容，特别是(A4)这个唯一描述项代换的公理。
新理论理当也要是套带等号的形式理论。为此，考虑到(E2)的等价条件必须假设
$a_k=x\vdash f_i^n(a_1,....,\,a_k,....,\,a_n) = f_i^n(a_1,....,\,x,....,\,a_n)$($\displaystyle a_k$被$\displaystyle x$取代)
由此就可以得到新理论下
$\vdash_2 [x=f^{n}_i(a_1,\,....,\,a_n)]\Leftrightarrow\mathcal{B}(a_1,\,....,a_n,\, x)$ (E)
| 证明 |
|---|
|
($\Rightarrow$)
($\Leftarrow$)
|
所以(E)证实了我们的"直观幻想"，跟"函数值"相等的叙述完全可以用$\mathcal{B}$替代。
符号变换
为了证明新旧理论效力等价的条件(2)；我们需要以下定理
$t$在新理论的$\mathcal{A}(t)$里是完全自由的。新理论里的项${\big{<}S_k\big{>}}^{n}_{k=1}$全部不含变数$x$，那
$\vdash_2 \mathcal{A}\big{[}f^{n}_i({\big{<}S_k\big{>}}^{n}_{k=1})\big{]}\Leftrightarrow(\exists x)\big{[}\mathcal{B}\big{(}{\big{<}S_k\big{>}}^{n}_{k=1},\,x\big{)}\wedge \mathcal{A}(x)\big{]}$
证明提示：
($\Rightarrow$)套用(A4)和(U)
($\Leftarrow$)套用上面的(aux)，然后用(A4)代换
这样我们就可以对$f^{n}_i$在原子公式里的数量做归纳，(然后配上GENe)而得出符合条件(2)的符号变换
(1) ${\{A^{m}_j[x_1,....,\,f^{n}_i({\big{<}a_k\big{>}}^{n}_{k=1}),....,\, x_m]\}}^{\prime}\asymp(\exists t)\{A^{m}_j[x_1,....,\,t,....,\, x_m]\wedge\mathcal{B}({\big{<}a_k\big{>}}^{n}_{k=1},\,t)\}$
(2)若$x$于$\mathcal{A}(x)$完全自由，则
- ${\{\mathcal{A}[f^{n}_i({\big{<}S_k\big{>}}^{n}_{k=1})]\}}^{\prime}\asymp(\exists t)\{{[\mathcal{A}(t)]}^{\prime}\wedge{[\mathcal{B}({\big{<}S_k\big{>}}^{n}_{k=1},\,t)]}^{\prime}\}$
注意以上的$t$都必须于变换时首次出现
注意上面的规则(2)可以透过以下的定理，把从变换产生的新量词，递回地提到最外面
$t$和$s$在新理论的$\mathcal{A}(s,\,t)$里是完全自由的。新理论里的项${\big{<}T_k\big{>}}^{m}_{k=1}$和${\big{<}S_k\big{>}}^{n}_{k=1}$都不含变数$x$和$y$，那
$\vdash_2 \mathcal{A}\big{[}f^{n}_i({\big{<}T_k\big{>}}^{m}_{k=1}),\,f^{n}_i({\big{<}S_k\big{>}}^{m}_{k=1})\big{]}\Leftrightarrow(\exists x)(\exists y)[\mathcal{A}(x,\,y)\wedge\mathcal{B}({\big{<}T_k\big{>}}^{m}_{k=1},\,x)\wedge\mathcal{B}({\big{<}S_k\big{>}}^{m}_{k=1},\,y)]$
证明提示：套用(A4)、(U)和(aux)
一般的$wf$只要对$\neg$和$\Rightarrow$的数量做归纳，就会得到
(1)${(\neg\mathcal{A})}^{\prime}\asymp\neg{\mathcal{A}}^{\prime}$
(2)${(\mathcal{A}\Rightarrow\mathcal{C})}^{\prime}\asymp{\mathcal{A}}^{\prime}\Rightarrow{\mathcal{C}}^{\prime}$
(3)${(\forall x\mathcal{A})}^{\prime}\asymp\forall x{\mathcal{A}}^{\prime}$
如此就可以得到一般$wf$下的条件(2)。