演绎定理 范式

发表于

演绎定理

  • 狭谓词演算是一个逻辑系统，其公理和定理都是普遍有效的
    • 其中一部分是蕴涵式，相当于正确的推理的规则或形式

  • 狭谓词演算是一个公理系统

    • 推演的出发点是公理
    • 推演的根据是基本的推演规则
      • 变形规则和推导出的推演规则

有前提的推演：一个应用狭谓词演算的变形规则进行的推演，除了公理以外还以其它非普遍有效公式作为出发点

  • 有前提的推演的形式结构：
  • 从前提 $A_1, A_2, …, A_m$ 可推演的B，当且仅当有一有穷公式序列 $E_1, E_2, …, E_n$，其中每一 $E_k(k = 1, …, n)$ 皆为下列之一：
      1. 一公理或一定理
      1. 一前提 $A_i(1 \leq i \leq m)$
      1. 由本序列在前的一公式或两公式根据变形规则得到
      1. 最后的公式 $E_n$ 为B

狭谓词演算内定理的证明是无前提的推演，证明的最后公式是狭谓词演算的定理

依赖：在一推演中一公式 $E_k$ 依赖于前提A，如果

    1. $E_k$ 即为前提A
    1. $E_k$ 由 $E_i$ 经过变形得到，或由 $E_i$ 和 $E_j$ (i, j < k) 经过变形得到，而 $E_i$ 依赖于A
    1. 只有在以上二情况下 $E_k$ 才依赖于A

自由变项保持不变：前提A里一自由变项保持不变，当且仅当在推演过程中对于自由出现在一切依赖A的公式里的这个变项未曾引用 变项代入 和 前件存在或后件概括

限制的推演：前提里的自由变项保持不变的推演

一般思维的推演都是限制推演
属于狭谓词演算的具体推演里前提中只有具体命题、具体谓词而没有命题变项和谓词变项
即使有自由个体变项也是被用来表示一般性的：可以等同于用全称量词约束起来
如 x+y=y+x <==> (x)(y)(x+y=y+x)

演绎定理：设在狭谓词演算里给定公式 $A_1, A_2, …, A_m(m \not= 0)$，并设 $A = A_1 \bigwedge A_2 \bigwedge … \bigwedge A_m$，如果从A可以推演出公式B，在推演过程中A里的自由变项保持不变，并且 $A \rightarrow B$ 为合式公式，那么 $├ A \rightarrow B$，即 $A \rightarrow B$ 为一定理

证明略…

演绎定理的意义

  1. 狭谓词演算是逻辑系统，是推理和证明的理论基础和工具：一阶谓词演算没有谓词的谓词或二阶谓词乃至二阶以上的谓词，只有个体变项被量词所约束；由狭谓词演算的逻辑符号和理论的个体常项、谓词常项和具体命题表达的一阶数学理论可以公理化和形式化

  2. 通过对狭谓词演算中推演规则和演绎定理的考察可以更明确理解等值和“可互推”两个逻辑关系的区别：两个公式A和B等值，如果A和B同真或同假；两公式A和B可互推，如果根据狭谓词演算的推演规则从A可以推B并且B可以推A。等值的两个公式可以互推，可互推的公式却不必等值

命题演算的完全性中，可证若以非重言式作为公理，则一切公式皆可推出
在命题演算中两个非重言公式皆可互推，但并非任何两个非重言公式都等值。

根据狭谓词演算的概括规则，若A和B可以互推，那么A普遍有效的充要条件是B普遍有效
在以狭谓词演算为逻辑工具的推演中，可以用A替代B或用B替代A
若A和B有更强的等值关系，作为公式的整体，A和B在推导中可以相互替代，作为某公式的一部分也可以相互置换(根据基本置换规则)。

范式 前束范式 $\exists$-前束范式

求谓词逻辑的范式的方法：

  • 谓词逻辑的公式一般都有量词，将量词全部移至公式最前端，每一量词的辖域都延伸至公式末端，得到 $A: \ \ \ \ \ \ Z_1 Z_2 … Z_n B$
    • 其中每个 $Z_i(i = 1, 2, …, n)$都是一个量词，B中不再有量词而只有命题变项、带目式的谓词变项和一些联结词
    • B为A的基式：B可以作为命题演算的公式处理
    • A为前束范式，A前方的一组量词为前束词

前束范式：E是一前束范式当且仅当E中一切量词都未被否定地处于公式最前方且其辖域都延伸至公式的末端。 例如：$(x)(\exists y)(R(x, y) \right R(y, y))$

  • E是D的前束范式，当且仅当E是前束范式且 $├ E \leftrightarrow D$

前束范式存在定理：狭谓词演算的每一公式都有其前束范式。一公式的前束范式不是唯一的

  • 从一公式出发，根据以下步骤必然可以得到其前束范式

    1. 消去被否定的量词，根据
    • $├ ¬(x)F(x) \leftrightarrow (\exists x)¬F(x)$
    • $├ ¬(\exists x)F(x) \leftrightarrow (x)¬F(x)$
    1. 引用约束变项易字规则，将含有相同变项的量词易字，使不同的量词所含的约束变项都是用不同字母表示对的。例如：$(x)F(x) \bigvee (x)G(x)$ 易字为 $(x)F(x) \bigvee (y)G(y)$
    1. 消去某些等值式($\leftrightarrow$)
    1. 依一定的次序作置换将量词逐步前移至公式的最前方并使其辖域都延伸至公式的末端；依据以下定理
    • 关于合取和析取的等值式
    • $├ p \bigvee (x)F(x) \leftrightarrow (x)(p \bigvee F(x))$
    • $├ p \bigvee (\exists x)F(x) \leftrightarrow (\exists x)(p \bigvee F(x))$
    • $├ p \bigwedge (x)F(x) \leftrightarrow (x)(p \bigwedge F(x))$
    • $├ p \bigwedge (\exists x)F(x) \leftrightarrow (\exists x)(p \bigwedge F(x))$
    • 关于蕴涵的等值式
    • $├ p \rightarrow (x)F(x) \leftrightarrow (x)(p \rightarrow F(x))$
    • $├ p \rightarrow (\exists x)F(x) \leftrightarrow (\exists x)(p \rightarrow F(x))$
    • $├ (x)F(x) \rightarrow p \leftrightarrow (\exists x)(F(x) \rightarrow p)$
    • $├ (\exists x)F(x) \rightarrow p \leftrightarrow (x)(F(x) \rightarrow p)$

一公式和其前束范式是可置换的，真假相同

$\exists$-前束范式(司寇伦范式)：$\exists$-前束范式是一前束范式，其中无自由个体变项，至少有一存在量词，且一切存在量词都在全称量词之前。 例如：$(\exists x)(y)(F(x) \rightarrow F(y))$

$\exists$-前束范式的存在定理：谓词演算的每一公式D都有一$\exists$-前束范式E，并且D和E可互推，即D普遍有效是E普遍有效的充分必要条件

证明略…

引用

  1. 《数理逻辑引论》，王宪钧，北京大学出版社