数理逻辑02 推演系统

写在前面

在上一章给出了命题逻辑的语法、语义,公理化的定义,以及一种判定公式是否可满足/永真的算法,但是这还不够,因为:

  1. 并不是所有逻辑都有Decision Procedure,因此这种方法不够普遍
  2. 即使有,在有无穷多的公理时,Decision Procedure很可能没法处理无穷项的公式(算法不一定终止)
  3. 即使终止,Decision Procedure也只能展示一件事情:命题的真值。我们没法得到中间结果,对理解逻辑没有帮助

于是就有了推演系统(Deductive System),这是对推理证明的形式化。同样的,推演系统有很多种,每一个都有自己的语法(公理+推导规则)和语义(对应逻辑的语义)。在命题逻辑中,不同的一致完备推演系统相互等价,这可以看成是对同一个东西的不同解释(模型)。我们所有的推演都是基于语法的推导,而一致性和完备性则是连接了语法和语义的桥梁,它保证了推演系统足够强大又不会出错。

推演系统

包括一组公理集(Set of Axioms)和一组推演规则(Rules of Inference)

证明

一个证明(Proof)指的是一段长度有限的公式序列 \(A_1,A_2\ldots A_n\),其中每个公式 \(A_i,i\in\left\{1\ldots n\right\}\)

  1. 要么是公理
  2. 要么可以由前面的公式+推演规则得到
  3. 要么是前面出现过的公式
  4. 要么是已经证明过的定理

用 \(\vdash A\) 表示 \(A\) 在推演系统中可证明,即存在一个证明使得 \(A\) 是最后出现的公式,称 \(A\) 为一个定理(Theorem)。对于中间出现的公式我们称为引理(Lemma)。

\(\scr G\)

给出 Gentzen 系统的(语法)定义

公理

含有互补对的公式集是公理

推演规则

有两类规则

\[\frac{\vdash U\cup\left\{\alpha_1,\alpha_2\right\}}{\vdash U\cup\left\{\alpha\right\}} \\ \frac{\vdash U\cup\left\{\beta_1\right\}\text{\quad}\vdash U\cup\left\{\beta_2\right\}}{\vdash U\cup\left\{\beta\right\}} \]

一个常见的例子是令 \(\alpha=\alpha_1\vee\alpha_2\),\(\beta=\beta_1\wedge\beta_2\)

在 \(\scr G\) 中,一个证明即是一个由公式集组成的序列。

正确性

\(\scr G\) 的正确性由如下重要定理给出:

设 \(\scr U\) 是一个公式集,\(\scr \bar U\) 定义为 \({\scr\bar U}=\left\{\bar A\mid A\in{\scr U}\right\}\),那么有 \(\vdash {\scr U}\) 当且仅当 \({\scr \bar U}\) 存在closed Semantic Tableaux

该定理的特殊情况是 \({\scr U}=\left\{U\right\}\),此时定理表述为:在 \(\scr G\) 中 \(\vdash U\) 当且仅当 \(\neg U\) 存在closed Semantic Tableaux

证明

先证明充分性,即:若 \(\scr\bar U\) 存在closed Semantic Tableaux \(\scr T\),则 \(\vdash\scr U\)

考虑对 \(\scr T\) 这个树形结构做结构归纳

  1. \(\scr\bar V\) 是 \(\scr T\) 的叶子,则其存在互补对,此时 \(\scr V\) 也存在互补对,因此 \(\scr V\) 是 \(\scr G\) 中的公理,\(\vdash\scr V\)

  2. \(\scr\bar V\) 不是 \(\scr T\) 的叶子,不妨设 \(\scr\bar V\) 中的新增公式为 \(\phi\),分类讨论:

    1. \(\scr\bar V\) 是一个 Semantic Tableaux 上的 \(\alpha\) 推导,则不妨设 \(\phi=\alpha_1\wedge\alpha_2\),则其子树 \(\scr\bar V'\) 根据归纳假设有 \(\vdash\scr V'\),并且有 \(\scr\bar V'=\bar V-\left\{\alpha_1\wedge\alpha_2\right\}\cup\left\{\alpha_1,\alpha_2\right\}\)。

      此时可得 \({\scr V}={\scr V'}\cup\left\{\neg(\alpha_1\wedge\alpha_2)\right\}-\left\{\neg\alpha_1,\neg\alpha_2\right\}\),再根据 \(\scr G\) 中的 \(\alpha\) 推导规则就可得到 \(\vdash\scr V\)。对于 \(\phi\) 为其它情况的证明是类似的。

    2. \(\scr\bar V\) 是一个 Semantic Tableaux 上的 \(\beta\) 推导,则不妨设 \(\phi=\beta_1\vee\beta_2\),则其子树 \(\scr\bar V_1,\bar V_2\) 根据归纳假设有 \(\vdash\scr V_1,\vdash V_2\),并且有 \(\scr\bar V_1=\bar V-\left\{\beta_1\vee\beta_2\right\}\cup\left\{\beta_1\right\},\;\bar V_2=\bar V-\left\{\beta_1\vee\beta_2\right\}\cup\left\{\beta_2\right\}\)。

      此时可得 \({\scr V}={\scr V_1\cup V_2}\cup\left\{\neg(\beta_1\vee\beta_2)\right\}-\left\{\neg\beta_1,\neg\beta_2\right\}\),再根据 \(\scr G\) 中的 \(\beta\) 推导规则就可得到 \(\vdash\scr V\)。对于 \(\phi\) 为其它情况的证明是类似的。

再证明必要性,即:若 \(\vdash \scr U\),那么 \(\scr\bar U\) 存在closed Semantic Tableaux \(\scr T\)

注意到 \(\scr G\) 中的证明本身也有某种树形结构(不过是倒置的),因此也考虑对 \(\scr U\) 做结构归纳

  1. \(\scr U\) 是 \(\scr G\) 中的公理,故存在互补对,此时 \(\scr\bar U\) 也存在互补对,故 \(\scr\bar U\) 必然构造出 \(\scr T\)
  2. \(\scr U\) 经推导而来,不妨记新增公式为 \(\phi\),记 \({\scr U}={\scr U'}\cup\left\{\phi\right\}\)
    1. \(\phi = \alpha_1\vee\alpha_2\),此时记前提(Premise)为 \(\scr U_1=\scr U'\cup\left\{\alpha_1,\alpha_2\right\}\),必然已有 \(\vdash {\scr U_1}\)。根据归纳假设有 \(\scr\bar U_1\) 存在closed Semantic Tableaux,并且有 \({\scr\bar U} = {\scr \bar U_1}\cup\left\{\neg(\alpha_1\vee\alpha_2)\right\}-\left\{\neg\alpha_1,\neg\alpha_2\right\}\),只需要根据Semantic Tableaux中的 \(\alpha\) 推导规则就可以通过 \(\scr\bar U_1\) 的Tableaux来得到 \(\scr\bar U\) 的Tableaux了。其余形式的 \(\phi\) 的证明是类似的。
    2. \(\phi = \beta_1\wedge\beta_2\),此时记前提(Premise)为 \(\scr U_1=\scr U'\cup\left\{\beta_1\right\},U_2=U'\cup\left\{\beta_2\right\}\),必然已有 \(\vdash {\scr U_1},\vdash{\scr U_2}\)。根据归纳假设有 \(\scr\bar U_1\) 和 \(\scr\bar U_2\) 都存在closed Semantic Tableaux,并且有 \({\scr\bar U} = {\scr \bar U_1}\cup{\scr\bar U_2}\cup\left\{\neg(\beta_1\wedge\beta_2)\right\}-\left\{\neg\beta_1,\neg\beta_2\right\}\),只需要根据Semantic Tableaux中的 \(\beta\) 推导规则就可以通过 \(\scr\bar U_1,\bar U_2\) 的Tableaux来得到 \(\scr\bar U\) 的Tableaux了。其余形式的 \(\phi\) 的证明是类似的。

回过头看这个证明,无非是把 \(\scr G\) 中的每个公式集取反后就对应到了 Semantic Tableaux 上,并且可以发现两个系统里的推导规则可以一一对应。再结合对公式集可满足性的定义就会发现,本质上是对整个公式集组成的大公式做了取反,仅此而已。

Soundness & Completeness

在 \(\scr G\) 中,\(\vdash A\) 当且仅当 \(\neg A\) 存在closed Semantic Tableaux 当且仅当 \(\neg A\) 不可满足 当且仅当 \(\models A\)

这样就证完了。只需要建立起 \(\scr G\) 到 \(\scr T\) 的一一对应,就可以利用 \(\scr T\) 的一致完备性得到 \(\scr G\) 的一致完备性,这正是推演证明的一种。

\(\scr H\)

我靠这个花体字实在是太帅了,奈何我怎么都写不出这种感觉。

在 \(\scr H\) 中用大写字母表示命题变元(即可带入任意的命题)

下面给出Hilbert 系统的定义

公理

\[\begin{aligned} \textbf{Axiom 1 } &\vdash A\rightarrow (B\rightarrow A) \\ \textbf{Axiom 2 } &\vdash (A\rightarrow (B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow (A\rightarrow C)) \\ \textbf{Axiom 3 } &\vdash (\neg B\rightarrow\neg A)\rightarrow(A\rightarrow B) \end{aligned} \]

推演规则

只有一条

\[\frac{\vdash A\;\;\;\vdash A\rightarrow B}{\vdash B} \]

也叫做肯定前件(modus ponens),记为MP

对证明的拓展

设 \(\scr U\) 是公式集,\(A\) 是某个公式,则符号 \({\scr U}\vdash A\) 表示 \(\scr U\) 中的公式是证明 \(A\) 的假设

\(\scr H\) 中的证明是一系列形如 \({\scr U_i}\vdash A_i\) 的公式,其中 \(A_i\)

  1. 要么是公理
  2. 要么是已经证明过的引理
  3. \(A_i\in {\scr U_i}\)
  4. 可由已经证明过的定理+MP得到

这一拓展反映的是证明形如“如果 \(A\) 那么 \(B\) ”的命题时,我们可以假设 \(A\) 成立,然后检查 \(B\) 是否可被证明。

衍生规则

虽然只有MP是足够的,但是只用MP就像在裸奔,因此需要包装MP和公理来得到一些更抽象的推演规则。We are now doing composition!

具体可以把这些规则看成是一些语法上的宏,展开就能得到纯MP和公理组成的推演规则。

Deduction Rule

\[\frac{{\scr U}\cup \left\{A\right\}\vdash B}{{\scr U}\vdash A\rightarrow B} \]

这条规则就反映了拓展证明的意图,这条规则保证了我们可以在证明 \(A\rightarrow B\) 时先假设 \(A\),再证明 \(B\)

下面需要证明拓展是sound的,即不会引入原本不能证明的命题。其completeness是显然的。

对 \({\scr U}\cup\left\{A\right\}\vdash B\) 的推导步骤数 \(n\) 作数学归纳法

  1. \(n=1\),此时 \(B\) 一步就得到了,因此 \(B\) 要么是公理,要么是 \(A\),要么是已经证过的定理,下面给出 \(B\neq A\) 的证明:

    \[\begin{aligned} &{\scr U}\vdash B \\ &{\scr U}\vdash B\rightarrow (A\rightarrow B) &\textbf{Axiom 1} \\ &{\scr U}\vdash A\rightarrow B &\text{MP 1, 2} \end{aligned} \]

    故sound

    当 \(A=B\),该命题退化为 \({\scr U}\vdash A\rightarrow A\)

  2. \(n>1\),因此 \({\scr U}\cup\left\{A\right\}\vdash B\) 是一个MP

    不妨设

    \[\begin{aligned} &{\scr U}\cup\left\{A\right\}\vdash C \\ &{\scr U}\cup\left\{A\right\}\vdash C\rightarrow B \end{aligned} \]

    上面两式根据归纳假设有

    \[\begin{aligned} &{\scr U}\vdash A\rightarrow C &\text{Deduction Rule} \\ &{\scr U}\vdash A\rightarrow (C\rightarrow B) &\text{Deduction Rule} \\ &{\scr U}\vdash (A\rightarrow (C\rightarrow B))\rightarrow ((A\rightarrow C)\rightarrow (A\rightarrow B)) &\textbf{Axiom 2} \\ &{\scr U}\vdash (A\rightarrow C)\rightarrow (A\rightarrow B) &\text{MP 2, 3} \\ &{\scr U}\vdash A\rightarrow B &\text{MP 1, 4} \end{aligned} \]

    故sound

Contrapositive Rule

\[\begin{aligned} \frac{{\scr U}\vdash\neg B\rightarrow \neg A}{{\scr U}\vdash A\rightarrow B} \end{aligned} \]

只需要用一下 \(\textbf{Axiom 3}\) 就可以得到的规则,注意这条规则和如下规则的区别:

\[\begin{aligned} \frac{{\scr U}\vdash A\rightarrow B}{{\scr U}\vdash \neg B\rightarrow \neg A} \end{aligned} \]

因为我们目前都只在语法层面操作公式,因此二者是有本质区别的规则,需要分别单独证明

Transitivity Rule

\[\frac{{\scr U}\vdash A\rightarrow B\;\;\;\;\;{\scr U}\vdash B\rightarrow C} {{\scr U}\vdash A\rightarrow C} \]

证明如下:

\[\begin{aligned} & {\scr U}\vdash A\rightarrow B \\ & {\scr U}\vdash B\rightarrow C \\ & {\scr U}\vdash (B\rightarrow C)\rightarrow(A\rightarrow (B\rightarrow C)) &\textbf{Axiom 1} \\ & {\scr U}\vdash A\rightarrow (B\rightarrow C) &\text{MP 2, 3} \\ & {\scr U}\vdash (A\rightarrow (B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow (A\rightarrow C)) &\textbf{Axiom 2} \\ & {\scr U}\vdash (A\rightarrow B)\rightarrow (A\rightarrow C) &\text{MP 4, 5} \\ & {\scr U}\vdash A\rightarrow C &\text{MP 1, 6} \end{aligned} \]

Exchange of antecedent Rule

\[\frac{{\scr U}\vdash A\rightarrow(B\rightarrow C)}{{\scr U}\vdash B\rightarrow (A\rightarrow C)} \]

证明如下:

\[\begin{aligned} & {\scr U}&\vdash& A\rightarrow(B\rightarrow C) \\ & {\scr U}\cup\left\{A\right\}&\vdash& B\rightarrow C &\text{Deduction Rule} \\ & {\scr U}\cup\left\{A,B\right\}&\vdash& C &\text{Deduction Rule} \\ & {\scr U}\cup\left\{B\right\}&\vdash& A\rightarrow C &\text{Deduction Rule} \\ & {\scr U}&\vdash& B\rightarrow(A\rightarrow C) &\text{Deduction Rule} \\ \end{aligned} \]

Double negation Rule

\[\frac{{\scr U}\vdash\neg\neg A}{{\scr U}\vdash A},\;\frac{{\scr U}\vdash A}{{\scr U}\vdash\neg\neg A} \]

证明如下:

引理:

\[\begin{aligned} & \left\{\neg\neg A\right\}&\vdash& \neg\neg A\rightarrow(\neg\neg\neg\neg A\rightarrow \neg\neg A) &\textbf{Axiom 1} \\ & \left\{\neg\neg A\right\}&\vdash& \neg\neg A \\ & \left\{\neg\neg A\right\}&\vdash& \neg\neg\neg\neg A\rightarrow \neg\neg A &\text{MP 1, 2} \\ & \left\{\neg\neg A\right\}&\vdash& \neg A\rightarrow \neg\neg\neg A &\text{Contrapositive Rule} \\ & \left\{\neg\neg A\right\}&\vdash& \neg\neg A\rightarrow A &\text{Contrapositive Rule} \\ & \left\{\neg\neg A\right\}&\vdash& A &\text{MP 2, 5} \\ & &\vdash& \neg\neg A\rightarrow A &\text{Deduction Rule} \end{aligned} \]

因此

\[\begin{aligned} & {\scr U}\vdash \neg\neg A \\ & {\scr U}\vdash \neg\neg A\rightarrow A \\ & {\scr U}\vdash A \end{aligned} \]

另一个的证明是类似的

Reductio ad absurdum

也就是所谓的排中律

\[\frac{{\scr U}\vdash \neg A\rightarrow false}{{\scr U}\vdash A} \]

规定 \(false \overset{def}=A\wedge\neg A\overset{def}=\neg(A\rightarrow A)\),\(true\overset{def}=A\vee\neg A\overset{def}=A\rightarrow A\),注意这是语法上的定义,即两侧可以等价替换。

那么有 \(\vdash \neg false\),且 \(\vdash true\),这个证明是显然的。

关于排中律的"证明":

\[\begin{aligned} & {\scr U}\vdash \neg A\rightarrow false \\ & {\scr U}\vdash \neg false\rightarrow \neg\neg A &\text{Contrapositive Rule} \\ & {\scr U}\vdash \neg false &\text{By Lemma} \\ & {\scr U}\vdash \neg \neg A &\text{MP 2, 3} \\ & {\scr U}\vdash A &\text{Double negation Rule} \end{aligned} \]

在某些逻辑里,\(\vdash A\vee\neg A\) 是可以不成立的。比如说Constructive Logic里就没法通过反证法证明一个东西,你必须提供一个构造才能说明某些存在性。在这里不是重点

先去吃饭,咕咕咕

上一篇:反对失败成功学02。对女孩积极的表达出自己的欲望


下一篇:Go语言02-开发环境与VScode配置