可靠性和完全性(提纲).doc

第七章 可靠性和完全性（提纲）1. 可靠性与完全性现在逻辑基本上都是采用如下结构：形式语言语义 语法语义与语法的关系形式语言：从初始符号出发，形成主要对象公式。（可能需要一些其它辅助对象，如在一阶逻辑，就有项的概念）。公式是一种特殊的符号串（由初始符号组成的符号串）。语义：给出某种结构，通过某种定义，定义出刻画逻辑规律的有效式。（如在一阶逻辑，我们从结构和赋值出发，给出解释、公式在解释下的真值，用在所有解释下都真定义出有效式）。有效式是一种特殊的公式，所有有效式的集合是全体公式的一个子集。语法：由公理和推导规则组成。按某种标准的方法给出证明序列和内定理。（可以有一些推广的概念，最重要的是推演）。有效式是一种特殊的公式，所有内定理的集合是全体公式的一个子集。语义与语法的关系：最重要的有两个，可靠性和完全性。7.1.1定义 可靠性 所有的内定理都是有效式。7.1.2定义 完全性 所有的有效式都是内定理。2. 一阶推演系统的可靠性可靠性有标准的证明方法：1. 证明每个公理都是有效的。2. 证明推导规则保持有效性不变。3. 归纳证明证明序列中的每个公式都是有效式，所以内定理是有效式。7.2.1引理(1) s(jy) = T当且仅当（如果s(j) = T，则s(y) = T）。(2) s(j1jny) = T 当且仅当（如果s(j1) = T, , s(jn) = T，则s(y) = T）。证 (1) 由定义得s(jy) = T当且仅当 s(j) = F或s(y) = T。s(j) = F或s(y) = T就是（如果s(j) = T，则s(y) = T）。所以，s(jy) = T当且仅当（如果s(j) = T，则s(y) = T）。(2) 对n作归纳。1. n = 1。由(1)得s(j1y) = T 当且仅当（如果s(j1) = T，则s(y) = T）。2. n = k+1。j1jk+1y也就是j1jk(jk+1y)，由归纳假设s(j1jk(jk+1y) = T 当且仅当（如果s(j1) = T, , s(jk) = T，则s(jk+1y) = T）。由(1)得s(jk+1y) = T 当且仅当（如果s(j k+1) = T，则s(y) = T）。所以，s(j1jny) = T 当且仅当（如果s(j1) = T, , s(jn) = T，则s(y) = T）。7.2.2引理(1) 如果s(jy) = T且s(j) = T，则s(y) = T。(2) 如果s(jy) = T且s(j) = T，则s(y) = T。证 (1) 如果s(jy) = T，则s(j) = F或s(y) = T，又s(j) = T，所以s(y) = T。7.2.3定理 一阶推演系统的公理都是有效式。证A1 jyj。任给解释s，如果s(j) = T, s(y) = T，则s(j) = T。由定理7.2.1(2)，任给解释s，都有s(jyj) = T。A2 (jyq)(jy)jq。任给解释s，如果s(jyq) = T, s(jy) = T, s(j) = T，则由s(j) = T和s(jyq) = T得s(yq) = T，由s(j) = T和s(jy) = T得s(y) = T，再由s(y) = T和s(yq) = T得s(q) = T。由定理7.2.1(2)，任给解释s，都有s(jyq)(jy)jq) = T。A3 (jy)(jy)j任给解释s，如果s(jy) = T, s(jy) = T，则用反证法证明s(j) = T。假设s(j) = F，则s(j) = T，由s(j) = T和s(jy) = T得s(y) = T，由s(j) = T和s(jy) = T得s(y) = T，所以s(y) = F。s(y) = T和s(y) = F，矛盾。由定理7.2.1(2)，任给解释s，都有s(jy)(jy)j) = T。A4 xjj(t / x)，在j中t对x代入自由。任给解释s，如果s(xj) = T，则任给aA，都有sx, a(j) = T，取a = s(t)，由代入引理得s(j(t / x) = sx, a(j) = T。由定理7.2.1(2)，任给解释s，都有s(xjj(t / x) = T。A5 x(jy)(xjxy)。任给解释s，如果s(x(jy) = T, s(xj) = T，则任给aA，都有sx, a(jy) = T且sx, a(j) = T，所以任给aA，都有sx, a(y) = T，因此s(xy) = T。由定理7.2.1(2)，任给解释s，都有s(x(jy)(xjxy) = T。A6 jxj，x不是j的自由变项。任给解释s，如果s(j) = T，则任给aA，由合同引理得sx, a(j) = s(j) = T，所以s(xj) = T。由定理7.2.1(2)，任给解释s，都有s(jxj) = T。7.2.4定理 一阶推演系统的推导规则保持有效性不变。(1) 如果jy和j都是有效式，则y也是有效式。(2) 如果j是有效式，则xj也是有效式。证(1) 任给解释s，因为jy和j都是有效式，所以s(jy) = T且s(j) = T，因此s(y) = T。这就证明了任给解释s，都有s(y) = T，所以y是有效式。(2) 任给解释s，任给aA，因为j是有效式，所以sx, a(j) = T，因此s(xj) = T。这就证明了任给解释s，都有s(xj) = T，所以xj是有效式。7.2.5定理 一阶推演系统可靠性定理一阶推演系统的内定理都是有效式。证 设j是内定理，j1, , jn（=j）是它的证明序列，归纳证明任给k（1kn），jk都是有效式，当k = n时，就是说j是有效式。1. ji是公理，由定理7.2.3得ji是有效式。2.1 存在j, kin，使得jk = jjji。由归纳假设得jj和jk = jjji都是有效式，由定理7.2.4(1)得ji是有效式。2.2 存在ji，存在变项x，使得ji = x jj。由归纳假设得jj是有效式，由定理7.2.4(2)得ji = x jj是有效式。7.2.6补充 A7和A8是有效式。证A7 t t。任给解释s，如果s(t) = s(t)，所以s(t t)。A8 t s(j(t / x)j(s / x)。任给解释s，如果s( t s) = T, s(j(t / x) = T，则s(t) = s(s)，取a = s(t) = s(s)，则由代入引理得s(j(s / x) = sx, a(j) = s(j(t / x) = T。由定理7.2.1(2)，任给解释s，都有s( t s(j(t / x)j(s / x) = T。7.2.7补充 带等词的一阶推演系统可靠性定理带等词的一阶推演系统的内定理都是有效式。证 略。3. 和谐和极大和谐7.3.1定义 和谐 F是公式集。如果存在公式j，使得F | j且F | j，则称F是不和谐的。否则称F是和谐的。由定义，F是和谐的条件是：不存在公式j，使得F | j且F | j。7.3.2定理 和谐集等价条件(1) F是不和谐的 当且仅当（任给公式q，都有F | q）。(2) F是和谐的 当且仅当（存在公式q，使得F |/ q）。证 (1) 如果（任给公式q，都有F | q），当然存在公式j，使得F | j且F | j。如果存在公式j，使得F | j且F | j，则任给公式q，由j, j | q得F | q。(2) 由(1)直接可得。7.3.3定理 和谐集的性质(1) 单调性 F Y。如果F是不和谐，则Y也是不和谐的。所以如果Y是和谐的，则F也是和谐的。(2) 有限性 F是和谐的 当且仅当 F的每个有限子集是和谐的。(3) F |/ j 当且仅当 Fj是和谐的。(4) F |/ j 当且仅当 Fj是和谐的。证 (1) 如果F是不和谐，则任给公式q，都有F | q，所以任给公式q，都有Y | q，因此Y是不和谐的。(2) 证明：F是不和谐的 当且仅当 存在F的有限子集Y是不和谐的。设F是不和谐的，则存在公式j，使得F | j且F | j。取F到j的推演序列为j1, , jn，令F1 = j1, , jnF，则F1是F的有限子集且F1 | j，类似地存在有限F的有限子集F2，使得F2 | j。所以存在F的有限子集Y = F1F2，使得Y | j且Y |j，因此存在F的有限子集Y，使得Y是不和谐的。设存在F的有限子集Y是不和谐的，由单调性得F是不和谐的。(3) 证明：F | j 当且仅当 Fj是不和谐的。设F | j，则Fj | j，又Fj | j，所以Fj是不和谐的。设Fj是不和谐的，则Fj | j，由演绎定理得F | jj，由jj | j得F | j。(4) 类似于(3)，留给读者。7.3.4定义 极大和谐 F是和谐的公式集。如果任给公式jF，都有Fj是不和谐的，则称F是极大和谐的。7.3.5定理 极大和谐集的性质 F是极大和谐的公式集。(1) 推演封闭性 如果F | j，则jF。(2) 内定理封闭性 如果j是内定理，则jF。(3) 分离规则 如果jF且jyF，则yF。(4) jF 当且仅当 jF。(5) jyF 当且仅当 jF或yF。证 (1) 反证法。如果jF，则Fj是不和谐的，由定理7.3.3(4)得F | j，又F | j，所以F是不和谐的，矛盾。(2) 如果j是内定理，则由5.3.1(1)得F | j，由(1)得jF。(3) 如果jF且jyF，则F | y，由(1)得yF。(4) 如果jF，由F的和谐性得jF。jF如果jF，则Fj是不和谐的，由定理7.3.3(4)得F | j，由(1)得jF。(5) 如果jyF，分两种情况证明jF或yF。情况1，jF。显然有jF或yF。情况2，jF。由(3)得yF，也有jF或yF。如果jF或yF，则分两种情况证明jyF。情况1，jF。由(4)得jF，因为j(jy)是内定理，所以j(jy)F，再由(3)得jyF。情况2，yF。类似情况1，由内定理y(jy)。由(4)和(5)得：(4) jF 当且仅当 jF。(5) jyF 当且仅当 jF且yF。7.3.6推论 F是极大和谐的公式集。(1) jyF 当且仅当 jF且yF。(2) jyF 当且仅当 jF或yF。证 (1) jyF 当且仅当 (jy)F 当且仅当 jyF 当且仅当 jF且yF 当且仅当 jF且yF。(2) jyF 当且仅当 jyF 当且仅当 jF或yF 当且仅当 jF或yF。4. Hintikka集7.4.1定义 Hintikka集 F是公式集。如果任给存在公式$xyF，都存在项t，使得y(t/x)F，则称F是Hintikka集。7.4.2定理 极大和谐Hintikka集存在定理F是有限公式集，则存在极大和谐的Hintikka集Y，使得F Y。证 注意，我们的语言是可数的，所以全体公式也是可数的，将全体公式排成序列：j1, , jn, ，任给n，归纳定义有限Fn如下：(1) F0 = F。(2) Fk+1分三种情况定义如下：2.1 Fkjk不和谐。令Fk+1 = Fk。2.2 Fkjk和谐，jk不是$xy形式。令Fk+1 = Fkjk。2.3 Fkjk和谐，jk = $xy。取不在Fkjk出现的变元y（这是可以做到的，因为Fkjk是有限公式集），令Fk+1 = (Fkjk)y(y/x)。令Y =Fn | nN。证明一：每个Fn都是和谐的。(1) F0 = F是和谐的。(2) Fk+1分三种情况证明如下：2.1 Fkjk不和谐。由归纳假设，Fk是和谐的，所以Fk+1 = Fk是和谐的。2.2 Fkjk和谐。令Fk+1 = Fkjk和谐的。2.3 Fkjk和谐，jk = $xy。反证法。假设Fk+1 = (Fkjk)y(y/x)是不和谐的，则Fkjk | y(y/x)。由概括规则得Fkjk | yy(y/x)（注意y不是Fkjk的自由变项）。由内定理 | yy(y/x)xy得yy(y/x) | xy，所以Fkjk | xy由内定理 | xy$xy 得xy | $xy，所以Fkjk | xy。这就是Fkjk | jk，由演绎定理得Fk | jkjk。再由内定理 | (jkjk)jk得jkjk | jk，所以Fk | jk，因此Fkjk不和谐，矛盾。证明二：Fn Fn+1，所以Fn | nN是单调的。显然。证明三：Y =Fn | nN是和谐的。反证法。如果Y =Fn | nN是不和谐的，则存在Y的有限子集y1, , ys，存在公式q使得y1, , ys | qq。因为y1, , ys Fn | nN，所以存在Fn1, , Fns，使得y1Fn1, , ysFns，取Fn1, , Fns中最大的集合Fnt（这个最大集合的存在是由Fn | nN的单调性保证的），则y1, , ys Fnt，所以Fnt | qq，因此Fnt不和谐，矛盾。证明四：Y =Fn | nNHintikka集。任给存在公式$xyY，$xy一定是某个jn，因为Yjn = Y和谐，所以Fnjn和谐（注意Fnjn是Yjn的子集）。由定义2.3，存在变项y，使得y(y/x)Fn+1。所以，存在变项y，使得y(y/x)Y。5. 一阶推演系统的完全性7.5.1定义 可满足(1) j是公式。如果存在解释s，使得s(j) = T，则称j是可满足的。(2) F是公式集。如果存在解释s，使得任给公式jF，都有s(j) = T，则称F是可满足的，记为s(F) = T。7.5.2引理(1) j可满足 当且仅当 j不是有效的。(2) F是公式集。如果F可满足，则任给公式jF，j都是可满足的。证 略。注意，任给公式jF，j都是可满足的，并不保证F是可满足的。完全性是说：任给公式j，如果j是有效式，则j是内定理。等价地说：任给公式j，如果j不是内定理，则j不是有效式。完全性证明思路：(1) j不是内定理，则j和谐。（在定理7.3.3(3)中取F为空集）(2) 将j扩