3.5形式推演--3.6前束范式 (2)

形式可推演用∑表示任何公式集，即∑⊆Form(L)。∑∪{A}可以记为∑，A。∑∪∑’可以记为∑，∑’。若∑={A1,A2,A3,…}，则∑可以记为A1,A2,A3,…。∑├A表示A由∑形式可推演（形式可证明）的。其中，∑为前提，A为结论。├不是L中符号。∑├A不是公式。A├┤B表示“A├B并且B├A”，并称A和B是语法等值的。一阶逻辑的推演规则（一）共11+6条，A，B，C为公式(Ref)A├A(+)若∑├A，则∑，∑’├A(﹁-)若∑，﹁A├B，∑，﹁A├﹁B，则∑├A(→-)若∑├A→B，∑├A，则∑├B(→+)若∑，A├B，则∑├A→B(∧-)若∑├A∧B，则∑├A，∑├B(∧+)若∑├A，∑├B，则∑├A∧B(∨-)若∑，A├C，∑，B├C，则∑，A∨B├C(∨+)若∑├A，则∑├A∨B，∑├B∨A(↔-)若∑├A↔B，∑├A，则∑├B若∑├A↔B，∑├B，则∑├A(↔+)若∑，A├B，∑，B├A，则∑├A↔B一阶逻辑的推演规则（二）(∀-)若∑├∀xA(x)，则∑├A(t)(∀+)若∑├A(u)，u不在∑中出现，则∑├∀xA(x)(∃-)若∑，A(u)├B，u不在∑，B中出现，则∑，∃xA(x)├B(∃+)若∑├A(t)，则∑├∃xA(x)，其中A(x)是在A(t)中把t的某些（不一定全部）出现替换成x而得。(≡-)若∑├A(t1)，∑├t1≡t2，则∑├A(t2)，其中A(t2)是在A(t1)中把t1的某些（不一定全部）出现替换成t2而得。(≡+)Ф├u≡u(∀-)(∃+)得到∀xA(x)├A(t)├∃xA(x)(∀+)若∑├A(u)，u不在∑中出现，则∑├∀xA(x)(∃-)若∑，A(u)├B，u不在∑，B中出现，则∑，∃xA(x)├B证明过程常常用到A(u)，u不在∑中出现形式推演的定义定义3.5.1：A是在一阶逻辑中由∑形式可推演（形式可证明）的，记为∑├A，当且仅当∑├A能有限次使用一阶逻辑中形式推演规则生成。这是一个归纳定义。关于归纳证明。一个有限序列∑1├A1，∑2├A2，…，∑n├An被称为∑n├An的形式证明。其中，∑k├Ak（1≤k≤n）由使用某一推演规则而生成。定理3.5.2：(iii)∀xA(x)├┤∀yA(y)(iv)∃xA(x)├┤∃yA(y)(v)∀x∀yA(x,y)├┤∀y∀xA(x,y)(vi)∃x∃yA(x,y)├┤∃y∃xA(x,y)(vii)∀xA(x)├∃xA(x)与(i),(ii)易由规则推出(viii)∃x∀yA(x,y)├∀y∃xA(x,y)证(viii):∀yA(u,y)├A（u，v）取不在x，y中出现的u，v。∀yA(u,y)├∃xA（x，v）（∃+）∀yA(u,y)├∀y∃xA（x，y）（∀+）∃x∀yA(x,y)├∀y∃xA(x,y)（∃-）证明：¬∀xA(x)├┤∃x(¬A(x))定理3.5.3(i)证：先证¬∀xA(x)├∃x(¬A(x))。(1)¬A(u)├¬A(u)u不在A(x)中出现(Ref)(2)¬A(u)├∃x(¬A(x))(∃+)(1)(3)¬∃x(¬A(x))，¬A(u)├∃x(¬A(x))(+)(2)(4)¬∃x(¬A(x))，¬A(u)├¬∃x(¬A(x))(∈)(5)¬∃x(¬A(x))├A(u)(¬-)(3)(4)(6)¬∃x(¬A(x))├∀xA(x)(∀+)(5)(7)¬∀xA(x)，¬∃x(¬A(x))├∀xA(x)(+)(6)(8)¬∀xA(x)，¬∃x(¬A(x))├¬∀xA(x)(∈)(9)¬∀xA(x)├∃x(¬A(x))(¬-)(7)(8)再证∃x(¬A(x))├¬∀xA(x)。(1)∀xA(x)├∀xA(x)(Ref)(2)∀xA(x)├A(u)u不在A(x)中出现(∀-)(1)(3)﹁A(u)，∀xA(x)├A(u)(+)(2)(4)﹁A(u)，∀xA(x)├﹁A(u)(∈)(5)﹁A(u)├﹁∀xA(x)(﹁+)(3)(4)(6)∃x(¬A(x))├¬∀xA(x)(∃-)(5)证明：∀x(A(x)→B(x))├∀xA(x)→∀xB(x)Th3.5.4(i)证：(1)∀x(A(x)→B(x))├∀x(A(x)→B(x))(Ref)(2)∀x(A(x)→B(x))├A(u)→B(u)(∀-)(1)u不在A(x)和B(x)中出现(3)∀x(A(x)→B(x))，∀xA(x)├A(u)→B(u)(+)(2)(4)∀x(A(x)→B(x))，∀xA(x)├∀xA(x)(∈)(5)∀x(A(x)→B(x))，∀xA(x)├A(u)(∀-)(4)(6)∀x(A(x)→B(x))，∀xA(x)├B(u)(→-)(3)(5)(7)∀x(A(x)→B(x))，∀xA(x)├∀xB(x)(∀+)(6)(8)∀x(A(x)→B(x))├∀xA(x)→∀xB(x)(→+)(7)证:∀x(A(x)→B(x))├∃xA(x)→∃xB(x)Th3.5.4(ii)证：(1)∀x(A(x)→B(x))├∀x(A(x)→B(x))(Ref)(2)∀x(A(x)→B(x))├A(u)→B(u)(∀-)(1)u不在A(x)和B(x)中出现(3)∀x(A(x)→B(x))，A(u)├A(u)→B(u)(+)(2)(4)∀x(A(x)→B(x))，A(u)├A(u)(∈)(5)∀x(A(x)→B(x))，A(u)├B(u)(→-)(3)(4)(6)∀x(A(x)→B(x))，A(u)├∃xB(x)(∃+)(5)(7)∀x(A(x)→B(x))，∃xA(x)├∃xB(x)(∃-)(6)(8)∀x(A(x)→B(x))├∃xA(x)→∃xB(x)(→+)(7)证:∀x(A(x)→B(x)),∀x(B(x)→C(x))├∀x(A(x)→C(x))Th3.5.4(iii)证：(1)∀x(A(x)→B(x))├∀x(A(x)→B(x))(Ref)(2)∀x(A(x)→B(x))├A(u)→B(u)(∀-)(1)u不在A(x)、B(x)和C(x)中出现(3)∀x(A(x)→B(x))，∀x(B(x)→C(x))，A(u)├A(u)→B(u)(+)(2)(4)∀x(A(x)→B(x))，∀x(B(x)→C(x))，A(u)├A(u)(∈)(5)∀x(A(x)→B(x))，∀x(B(x)→C(x))，A(u)├B(u)(→-)(3)(4)(6)∀x(A(x)→B(x))，∀x(B(x)→C(x))，A(u)├∀x(B(x)→C(x))(∈)(7)∀x(A(x)→B(x))，∀x(B(x)→C(x))，A(u)├B(u)→C(u)(∀-)(6)(8)∀x(A(x)→B(x))，∀x(B(x)→C(x))，A(u)├C(u)(→-)(5)(7)(9)∀x(A(x)→B(x))，∀x(B(x)→C(x))├A(u)→C(u)(→+)(8)(10)∀x(A(x)→B(x))，∀x(B(x)→C(x))├∀x(A(x)→C(x))(∀+)(9)证明：Th3.5.4(iv)A→∀xB(x)├┤∀x(A→B(x))。x不在A中出现。证：先证A→∀xB(x)├∀x(A→B(x))。(1)A→∀xB(x)，A├A→∀xB(x)(∈)(2)A→∀xB(x)，A├A(∈)(3)A→∀xB(x)，A├∀xB(x)(→-)(1)(2)(4)A→∀xB(x)，A├B(u)(∀-)(3)u不在A和B(x)中出现(5)A→∀xB(x)├A→B(u)(→+)(4)(6)A→∀xB(x)├∀x(A→B(x))(∀+)(5)再证∀x(A→B(x))├A→∀xB(x)。(1)∀x(A→B(x))，A├∀x(A→B(x))(∈)(2)∀x(A→B(x))，A├A→B(u)(∀-)(1)u不在A和B(x)中出现(3)∀x(A→B(x))，A├A(∈)(4)∀x(A→B(x))，A├B(u)(→-)(2)(3)(5)∀x(A→B(x))，A├∀xB(x)(∀+)(4)(6)∀x(A→B(x))├A→∀xB(x)(→+)(5)Thm3.5.4(vi)证:∀xA(x)→B├┤∃x[A(x)→B]分析：“├”∀xA(x)→B，¬∃x[A(x)→B]├矛盾i.e.¬∃x[A(x)→B]├∀x¬(A(x)→B)├¬(A(u)→B)├A(u),¬B├∀xA(x)“┤”∃x[A(x)→B],¬(∀xA(x)→B)├矛盾¬(∀xA(x)→B)├∀xA(x)，¬B├A(u)∃x[A(x)→B]├A(u)→BThm3.5.5合取的形式推演（i）A∧∀xB(x)├┤∀x[A∧B（x）],x不在A中出现.（ii）A∧∃xB(x)├┤∃x[A∧B（x）],x不在A中出现.（iii）∀xA(x)∧∀xB(x)├┤∀x[(A(x)∧B（x）]（iv）∃x[(A(x)∧B（x）]├∃xA(x)∧∃xB(x)（v）Q1(x)A(x)∧Q2yB(y)├┤Q1(x)Q2y(A(x)∧B(y),x不在B(y)中出现,y不在A(x)中出现.Thm3.5.6析取的形式推演（i）A∨∀xB(x)├┤∀x[A∨B（x）],x不在A中出现.（ii）A∨∃xB(x)├┤∃x[A∨B（x）],x不在A中出现.（iii）∀xA(x)∨∀xB(x)├∀x[(A(x)∧B（x）]（iv）∃x[(A(x)∨B（x）]├┤∃xA(x)∨∃xB(x)（v）Q1(x)A(x)∨Q2yB(y)├┤Q1(x)Q2y(A(x)∨B(y),x不在B(y)中出现,y不在A(x)中出现.Thm3.5.7等值的形式推演（i）∀x(A(x)↔B(x))├∀xA(x)↔∀xB(x)（ii）∀x(A(x)↔B(x))├∃xA(x)↔∃xB(x)（iii）∀x(A(x)↔B(x)),∀x(B(x)↔C(x))├∀x(A(x)↔C(x))（iv）∀x(A(x)→B(x)),∀x(B(x)→A(x))├┤∀x(A(x)↔B(x))证明：A(t1)，t1≡t2├A(t2)（定理3.5.8(i)）证：(1)A(t1)，t1≡t2├A(t1)(∈)(2)A(t1)，t1≡t2├t1≡t2(∈)(3)A(t1)，t1≡t2├A(t2)(≡-)(1)(2)证明：Ф├t≡t（定理3.5.8(ii)）证：(1)Ф├u≡u(≡+)(2)Ф├∀x(x≡x)(∀+)(1)(3)Ф├t≡t(∀-)(2)证明：t1≡t2├t2≡t1（定理3.5.8(iii)）证：(1)Ф├t1≡t1(已证)(2)t1≡t2├t1≡t1(+)(1)(3)t1≡t2├t1≡t2(Ref)(4)t1≡t2├t2≡t1(≡-)(2)(3)证明：A(t)├┤∀x(x≡t→A(x))（定理3.5.8(v)）证：先证A(t)├∀x(x≡t→A(x))(1)A(t)，u≡t├A(t)(∈)u不在A(t)中出现。(2)A(t)，u≡t├u≡t(∈)(3)u≡t├t≡u(已证)(4)A(t)，u≡t├t≡u(Tr)(2)(3)(5)A(t)，u≡t├A(u)(≡-)(1)(4)(6)A(t)├u≡t→A(u)(→+)(5)(7)A(t)├∀x(x≡t→A(x))(∀+)(6)再证∀x(x≡t→A(x))├A(t)(1)∀x(x≡t→A(x))├∀x(x≡t→A(x))(Ref)(2)∀x(x≡t→A(x))├t≡t→A(t)(∀-)(1)(3)Ф├t≡t(≡+)(4)∀x(x≡t→A(x))├t≡t(+)(3)(5)∀x(x≡t→A(x))├A(t)(→-)(2)(4)重要结论¬∃x¬A(x)├┤∀xA(x)├A(t)├A(u)├∃xA(x)├┤¬∀x¬A(x)¬∃xA(x)├┤¬∀xA(x)┤¬A(t)┤¬A(u)┤¬∃xA(x)├┤¬∀xA(x)∀x(A(x)→B(x))，A(u)├B(u)A(u)├A(u)注意u不在左端公式出现，不能使用(∃-）得不到∃xA(x)├A(u)同理也得不到A(u)├∀xA(x)(∀+）也不能使用基本的推理公式基本的推理公式(x)P(x)(