资源描述：
《可靠性和完全性(提纲)》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。
1、第七章可靠性和完全性（提纲）1.可靠性与完全性现在逻辑基本上都是采用如下结构：形式语言语义语法语义与语法的关系形式语言：从初始符号出发，形成主要对象——公式。（可能需要一些其它辅助对象，如在一阶逻辑，就有项的概念）。公式是一种特殊的符号串（由初始符号组成的符号串）。语义：给出某种结构，通过某种定义，定义出刻画逻辑规律的有效式。（如在一阶逻辑，我们从结构和赋值出发，给出解释、公式在解释下的真值，用在所有解释下都真定义出有效式）。有效式是一种特殊的公式，所有有效式的集合是全体公式的一个子集。语法：由公
2、理和推导规则组成。按某种标准的方法给出证明序列和内定理。（可以有一些推广的概念，最重要的是推演）。有效式是一种特殊的公式，所有内定理的集合是全体公式的一个子集。语义与语法的关系：最重要的有两个，可靠性和完全性。7.1.1定义可靠性所有的内定理都是有效式。7.1.2定义完全性所有的有效式都是内定理。2.一阶推演系统的可靠性可靠性有标准的证明方法：1.证明每个公理都是有效的。2.证明推导规则保持有效性不变。3.归纳证明证明序列中的每个公式都是有效式，所以内定理是有效式。7.2.1引理(1)s(j®y)
3、=T当且仅当（如果s(j)=T，则s(y)=T）。(2)s(j1®…®jn®y)=T当且仅当（如果s(j1)=T,…,s(jn)=T，则s(y)=T）。证(1)由定义得s(j®y)=T当且仅当s(j)=F或s(y)=T。s(j)=F或s(y)=T就是（如果s(j)=T，则s(y)=T）。所以，s(j®y)=T当且仅当（如果s(j)=T，则s(y)=T）。(2)对n作归纳。1.n=1。由(1)得s(j1®y)=T当且仅当（如果s(j1)=T，则s(y)=T）。2.n=k+1。j1®…®jk+1®y也
4、就是j1®…®jk®(jk+1®y)，由归纳假设s(j1®…®jk®(jk+1®y))=T当且仅当（如果s(j1)=T,…,s(jk)=T，则s(jk+1®y)=T）。由(1)得s(jk+1®y)=T当且仅当（如果s(jk+1)=T，则s(y)=T）。所以，s(j1®…®jn®y)=T当且仅当（如果s(j1)=T,…,s(jn)=T，则s(y)=T）。77.2.2引理(1)如果s(j®y)=T且s(j)=T，则s(y)=T。(2)如果s(j®y)=T且s(j)=T，则s(y)=T。证(1)如果s(
5、j®y)=T，则s(j)=F或s(y)=T，又s(j)=T，所以s(y)=T。7.2.3定理一阶推演系统的公理都是有效式。证A1j®y®j。任给解释s，如果s(j)=T,s(y)=T，则s(j)=T。由定理7.2.1(2)，任给解释s，都有s(j®y®j)=T。A2(j®y®q)®(j®y)®j®q。任给解释s，如果s(j®y®q)=T,s(j®y)=T,s(j)=T，则由s(j)=T和s(j®y®q)=T得s(y®q)=T，由s(j)=T和s(j®y)=T得s(y)=T，再由s(y)=T和s(y
6、®q)=T得s(q)=T。由定理7.2.1(2)，任给解释s，都有s((j®y®q)®(j®y)®j®q)=T。A3(Øj®y)®(Øj®Øy)®j任给解释s，如果s(Øj®y)=T,s(Øj®Øy)=T，则用反证法证明s((j)=T。假设s(j)=F，则s(Øj)=T，由s(Øj)=T和s(Øj®y)=T得s(y)=T，由s(Øj)=T和s(Øj®Øy)=T得s(Øy)=T，所以s(y)=F。s(y)=T和s(y)=F，矛盾。由定理7.2.1(2)，任给解释s，都有s((Øj®y)®(Øj®Øy
7、)®j)=T。A4"xj®j(t/x)，在j中t对x代入自由。任给解释s，如果s("xj)=T，则任给aÎA，都有sx,a(j)=T，取a=s(t)，由代入引理得s(j(t/x))=sx,a(j)=T。由定理7.2.1(2)，任给解释s，都有s("xj®j(t/x))=T。A5"x(j®y)®("xj®"xy)。任给解释s，如果s("x(j®y))=T,s("xj)=T，则任给aÎA，都有sx,a(j®y)=T且sx,a(j)=T，所以任给aÎA，都有sx,a(y)=T，因此s("xy)=T。由定
8、理7.2.1(2)，任给解释s，都有s("x(j®y)®("xj®"xy))=T。A6j®"xj，x不是j的自由变项。任给解释s，如果s(j)=T，则任给aÎA，由合同引理得sx,a(j)=s(j)=T，所以s("xj)=T。由定理7.2.1(2)，任给解释s，都有s(j®"xj)=T。7.2.4定理一阶推演系统的推导规则保持有效性不变。(1)如果j®y和j都是有效式，则y也是有效式。(2)如果j是有效式，则"xj也是有效式。证(1)任给解释s，因为j®y和j都是有效式，所以s(j
