第一节 逻辑

一般来说，逻辑包括语言、演绎系统和语义。语言是合式公式的集合，而公式是有穷长的字符串。推演系统是证明的集合，证明是公式集Ф和公式ϕ之间的有序对，推演本身是证明的序列。如果存在从Ф到ϕ的推演，则ϕ是Ф的推演后承；如果ϕ是空集的推演后承，则ϕ是定理。如果不存在公式ϕ，使得ϕ和﹁ϕ都是Ф的推演后承，则Ф是一致的。如果合式公式的集合和推演的集合是递归的，则推演系统是能行的；如果推演系统是能行的，则定理集是递归可枚举的。语义是模型的集合，而模型是论域和解释的集合。语义后承是由满足关系定义的，满足关系与赋值密切相关。如果任给赋值s，M都满足ϕ，则M是ϕ的模型；如果任给赋值s，M都满足Ф的成员，则M是Ф的模型。如果满足Ф的任意模型和赋值也满足ϕ，则ϕ是Ф的语义后承；如果ϕ是空集的语义后承，则ϕ是有效的。ϕ是有效的，当且仅当ϕ的全称闭包是有效的。如果存在满足Ф的成员的模型和赋值，则Ф是可满足的。ϕ是可满足的，当且仅当ϕ的存在闭包是可满足的。如果定理都是逻辑真理，并且推演后承是语义后承，则逻辑是可靠的；如果逻辑真理是定理，并且语义后承是推演后承，则逻辑是完全的。

二阶逻辑是在扩张一阶逻辑的基础上得到的，不同的扩张方式可以得到不同的二阶逻辑。下面分别介绍自由变元逻辑、标准二阶逻辑和分支二阶逻辑。[1]

自由变元逻辑是在一阶逻辑的基础上增加关系变元和函数变元而得到的。除一阶逻辑的形成规则外，还包括如下形成规则：

如果f是n元函数变元并且t1，…，tn是项，则ft1，…，tn是项。

如果R是n元关系变元并且t1，…，tn是项，则Rt1，…，tn是原子公式。

如果语言只包含关系变元，不包含函数变元，则可以用n+1元关系变元表示n元函数变元；如果语言只包含一元关系变元，不包含多元关系变元，则可以用n元组表示n元关系变元。

标准二阶逻辑是在自由变元逻辑的基础上增加二阶量化而得到的。除自由变元逻辑的形成规则外，还包括如下形成规则：

如果ϕ是公式并且R是关系变元，则∀Rϕ是公式。

如果ϕ是公式并且f是函数变元，则∀fϕ是公式。

与一阶逻辑的情况类似，可以用二阶全称量词定义二阶存在量词：

∃Rϕ=：﹁∀R﹁ϕ

∃fϕ=：﹁∀f﹁ϕ

另外，在标准二阶逻辑中，等词是可以定义的：

（t=s）=：∀X（Xt↔Xs）

也就是说，在标准二阶逻辑中，等词是可以通过定义引入的；换言之，带等词的标准二阶逻辑和不带等词的标准二阶逻辑没有实质性区别。

分支二阶逻辑是在标准二阶逻辑的基础上为每个关系变元增加下标，它表示关系变元的层次，例如X0，…，Xn。分支二阶逻辑一般不包括带下标的函数变元。

标准二阶逻辑的公理系统是在一阶逻辑公理系统的基础上增加如下关于二阶量词的公理：

∀Xϕ（X）→ϕ（T），其中T对X代入自由，或者T是关系常项

从ϕ→Ψ推出ϕ→∀XΨ（X），其中X不在ϕ中自由出现。

∀fϕ（f）→ϕ（h），其中h对f代入自由，或者h是函数常量

从ϕ→Ψ推出ϕ→∀fΨ（f），其中f不在ϕ中自由出现。

在此基础上还增加关于关系的概括公理：

∃R∀x1…∀xn（Rx1…xn↔ϕ（x1，…，xn）），其中R不在ϕ（x1，…，xn）中自由出现。

它断定，任意可表达公式都可以断定一个关系的存在。还可以增加关于函数的概括公理：

∀R（∀x1…∀xn∃！yRx1…xny→∃f∀x1…∀xnRx1…xnfx1…xn）

它断定，任意满足特定条件的关系都可以断定一个函数的存在。标准二阶逻辑的概括公理也被称为非直谓概括公理。另外，还可以增加选择公理：

∀R（∀x1…∀xn∃yRx1…xny→∃f∀x1…∀xnRx1…xnfx1…xn）

它断定，如果存在满足特定条件的y，则存在一个函数f，它可以挑选出这样的y。

标准二阶逻辑不需要关于等词的公理，因为根据等词的定义可以推出关于等词的公理，其中需要用到概括公理。

对于自由变元逻辑，因为它没有二阶量化，所以无法在其中表达概括公理。但是可以在其中表达如下代入规则：

从ϕ（X）推出ϕ（Ψ（x）），其中Ψ对X在ϕ中代入自由。[2]

它断定，任意可表达公式都可以替换自由关系变元。还可以增加如下函数变元消除规则：

从ϕ推出ϕ*，其中ϕ*是用关系变元替换ϕ中的函数变元所得到的结果。

事实上，由于没有二阶量化，自由变元逻辑中的所有自由变元都被前束全称量词约束，也就是说，ϕ（X）相当于∀Xϕ（X），﹁ϕ（X）相当于∀X﹁ϕ（X），ϕ（X）→Ψ（X）相当于∀X（ϕ（X）→Ψ（X））。

可以对标准二阶逻辑的概括公理进行某种限制，例如直谓概括公理：

∃X∀x（Xx↔ϕ（x）），其中ϕ（x）不包含二阶量词。

也就是说，只有自由变元逻辑的公式可以断定一个关系的存在。包括直谓概括公理的二阶逻辑被称为直谓二阶逻辑。直谓二阶理论是一阶理论的保守扩张。

在分支二阶逻辑中，可以增加分支直谓概括公理：

∃Xi∀x（Xix↔ϕ（x）），其中Xi的层次高于ϕ（x）中出现的变元的层次。

另外，还可以增加还原公理：

∀Xn∃Y0∀x（Y0x↔Xnx）

它断定，任给n层关系，都存在一个与之等价的0层关系。

二阶逻辑的语义包括标准语义和非标准语义，其中非标准语义又分为亨金语义和一阶语义。

标准模型是M≤D，I＞，其中D是一阶变元的取值范围，是二阶变元的取值范围，I是解释。令s是赋值。项t的指称记为d（t）。满足关系⊨的定义是：

如果d（t）∈s（X），则M，s⊨Xt。

如果任给与s合同（除X外）的s′，都有M，s′⊨ϕ，则M，s⊨∀Xϕ。

如果任给与s合同（除f外）的s′，都有M，s′⊨ϕ，则M，s⊨∀fϕ。

如果任给s，M，s⊨ϕ，则M是ϕ的模型。如果任给M，任给s，都有M，s⊨ϕ，则ϕ是标准有效的。如果存在M，存在s，使得M，s⊨ϕ，则ϕ是标准可满足的。如果任给M，任给s，如果M，s⊨Ф，则M，s⊨ϕ，则ϕ是Ф的标准后承。

满足关系之于标准二阶逻辑正如拟满足关系之于自由变元逻辑。拟满足关系的定义是：

如果任给与s合同（除二阶变元外）的s′，都有M，，则M，。

显然，M，当且仅当M，s⊨∀Xϕ（X）。拟有效、拟可满足和拟后承的定义与标准有效、标准可满足和标准后承的定义类似。

亨金模型是HM≤D，D，f，I＞，其中D是一阶变元的取值范围，D是关系变元的取值范围，f是函数变元的取值范围，I是解释。令s是亨金模型的赋值。亨金满足关系⊨H的定义是：

如果d（t）∈s（X），则HM，s⊨HXt

如果任给与s合同（除X外）的s′，HM，s′⊨Hϕ，则HM，s⊨H∀Xϕ

如果任给与s合同（除f外）的s′，HM，s′⊨Hϕ，则HM，s⊨H∀fϕ

亨金有效、亨金可满足和亨金后承的定义与标准有效、标准可满足和标准后承的定义类似。拟亨金满足关系之于亨金满足关系⊨H正如拟满足关系之于标准满足关系⊨。

如果D是D上的所有关系，f是D上的所有函数，则亨金模型HM被称为完整模型FM。令M是标准模型，FM是相应的完整模型。完整模型和标准模型之间存在如下关系：

任给公式ϕ，任给赋值s，M，s⊨ϕ当且仅当FM，s⊨Hϕ。

亨金语义和标准语义之间存在如下关系：如果ϕ是亨金有效的，则ϕ是标准有效的；如果ϕ是标准可满足的，则ϕ是亨金可满足的；如果ϕ是Ф的亨金后承，则ϕ是Ф的标准后承。

一阶模型是FOM≤D，D，f，＜I，p，a＞＞，其中D是一阶变元的取值范围，D是关系变元的取值范围，F是函数变元的取值范围，I是解释，p是D×D的子集，即“谓述”关系的解释，a是从D×f到D的函数，即“应用”函数的解释。令s是一阶模型的赋值，令t的指称是d（t）。如果f是函数变元，则f（t）的指称是a（d（t），s（f））。一阶满足关系⊨FO的定义是：

如果（d（t），s（X））∈p，则FOM，s⊨FOXt。

如果任给与s合同（除X外）的s′，FOM，s′⊨FOϕ，则FOM，s⊨FO∀Xϕ。

如果任给与s合同（除f外）的s′，FOM，s′⊨FOϕ，则FOM，s⊨FO∀fϕ。

一阶有效、一阶可满足和一阶后承的定义与标准有效、标准可满足和标准后承的定义类似。

令t在亨金模型下和一阶模型下的指称都是d（t）。令f（t）在亨金模型下的指称是dH（f（t）），f（t）在一阶模型下的指称是dFO（f（t））。令sH是亨金模型的赋值，sFO是一阶模型的赋值。关于项，有如下关系：

dH（f（t））=dFO（f（t））当且仅当a（dFO（t），sFO（f））=sH（f）（dH（t））

关于原子公式，有如下关系：

FOM，s⊨FOXt

当且仅当（d（t），s（X））∈p

当且仅当d（t）∈s（X）

当且仅当HM，s⊨HXt

一阶模型和亨金模型之间存在如下关系：

任给亨金模型HM，都存在一阶模型FOM，任给亨金模型的赋值s，都存在一阶模型的赋值s′，使得任给公式ϕ，HM，s⊨Hϕ当且仅当FOM，s′⊨FOϕ。

任给一阶模型FOM，都存在亨金模型HM，任给一阶模型的赋值s，都存在亨金模型的赋值s′，使得任给公式ϕ，FOM，s⊨FOϕ当且仅当HM，s′⊨Hϕ。

亨金语义和一阶语义之间存在如下关系：ϕ是一阶有效的当且仅当ϕ是亨金有效的；ϕ是一阶可满足的当且仅当ϕ是亨金可满足的；ϕ是Ф的一阶后承当且仅当ϕ是Ф的亨金后承。

与二阶逻辑相关的元理论包括：可靠性、紧致性、Löwenheim-Skolem性质、完全性、范畴性。

标准语义对于标准二阶逻辑是可靠的：

令Ф和ϕ分别是标准二阶逻辑的公式集和公式。如果ϕ是Ф的推演

后承，则ϕ是Ф的标准后承。

类似的结论也适用于自由变元逻辑和拟语义。注意，在验证概括公理时，需要在元语言层面假定公理集合论的分离公理。

算术的语言包括：0（零）、s（后继函数）、+（加法函数）、×（乘法函数）。算术的公理包括：

∀x（sx≠0）

∀x（x+0=x）

∀x（x×0=0）

∀x∀y（sx=sy→x=y）

∀x∀y（x+sy=s（x+y））

∀x∀y（x×sy=x×y+x）

∀X（X0∧∀x（Xx→Xsx）→∀xXx）

上述公理所构成的理论被称为二阶算术。如果把二阶算术表述在自由变元逻辑中，则需要去掉最后一条公理前面的全称量词，称其为自由变元算术。下面的结论说明，二阶算术唯一地刻画了自然数结构：

令M1≤D1，I1＞和M2≤D2，I2＞分别是模型。令01、02，s1、s2，+1、+2，×1、×2分别是零、后继函数、加法函数、乘法函数在M1和M2下的解释。如果M1和M2都是二阶皮亚诺算术的模型，则M1和M2是同构的，也就是说，存在从D1到D2的函数f，使得f（01）=02，任给D1中的a和b，f（s1a）=s2a，f（a+1b）=f（a1）+2f（b1），f（a×1b）=f（a1）×2f（b1）。

上述结论是由戴德金证明的。根据二阶算术的同构性，标准二阶逻辑的标准语义不具有Löwenheim-Skolem性质。由于二阶逻辑的表达力强于一阶逻辑，二阶逻辑可以刻画“有穷”和“无穷”，所以标准二阶逻辑的标准语义也不具有紧致性。类似地，同构性、非Löwenheim-Skolem性以及非紧致性也适用于自由变元逻辑和拟语义。另外，根据哥德尔不完全性定理，一阶算术的真理集不是递归可枚举的，而二阶算术包含一阶算术，因此二阶算术的真理集也不是递归可枚举的，也就是说，存在真但是不可证的标准二阶逻辑的语句。因此，标准语义对于标准二阶逻辑是不完全的。如果把自由变元逻辑的关系变元和函数变元改写为非逻辑符号，则自由变元逻辑变成一阶逻辑。因此，拟语义对于自由变元逻辑是完全的。但是自由变元算术的拟后承集也不是递归可枚举的。

对于标准二阶逻辑，亨金模型不是可靠的，因为它可能不满足概括公理或选择公理。类似地，亨金模型对于自由变元逻辑也不是可靠的。如果亨金模型满足概括公理和选择公理，则称其为忠实于标准二阶逻辑；如果亨金模型拟满足代入规则和函数变元消除规则，则称其为忠实于自由变元逻辑。由此可以得到可靠性和完全性：

令Ф和ϕ分别是标准二阶逻辑的公式集和公式。如果ϕ是Ф的推演后承，则任何满足Ф的忠实的亨金模型也满足ϕ。

如果任何满足Ф的忠实的亨金模型也满足ϕ，则ϕ是Ф的推演后承。

与标准模型不同，在亨金模型中不能定义等词。在标准模型中，任给元素a∈D，都存在它的单元集；根据∀X（Xt↔Xs），{a}可以把t和s识别为相同的。但是在亨金模型中，有可能，所以∀X（Xt↔Xs）不能把t和s识别为相同的。如果任给赋值s，如果M，s⊨∀X（Xx↔Xy），则x和y的赋值相同，则称亨金模型M是等词标准的。由此可以得到紧致性：

如果任意Ф的有穷子集在忠实的（等词标准的）亨金模型中都是可满足的，则Ф在忠实的（等词标准的）亨金模型中是可满足的。

令HM′≤D′，D′，F′，I′＞是HM≤D，D，f，I＞的亨金子模型[3]。令k是从HM′到HM的函数。如果任给P∈D′，都有k（P）∈D并且P=k（P）∩D′，任给g∈F′，都有k（g）∈f并且g=k（g）|D′[4]，则称k是对应函数。令s是赋值。sk是新的赋值，sk与s在一阶变元上合同；任给关系变元R，如果s把P赋值给R，则sk把k（P）赋值给R；任给函数变元f，如果s把g赋值给f，则sk把k（g）赋值给R。由此可以得到Löwenheim-Skolem性质：

如果HM≤D，D，f，I＞是亨金模型，则存在亨金子模型HM′≤D′，D′，F′，I′＞和对应函数k使得：（1）D′、D′和F′都是可数无穷的；（2）任给公式集Ф和HM′上的赋值s，HM′，s⊨HФ当且仅当HM，sk⊨HФ。

类似地，向上的Löwenheim-Skolem性质也成立。