Mathematical Logic for Computer Science 读书笔记

事情的前因后果比较复杂，目前的状况是身上一堆没看完的书和没填完的坑，但还是处在开坑的状态中
不过暑假还有一半不是嘛！

在这本书之前还看了一遍THU的《数理逻辑与集合论》。这书实在是太老了，在书上甚至还写着费马大定理仍然是open problem....这不搞笑嘛(掀桌)于是看完了那本又开始看这本

reasoning 推理
formalization 形式化
syntax 语法
semantic 语义的
propositional logic 命题逻辑
pre order 前序
in order 中序
material implication 实质蕴含
substitute A for B 用A替换B
tautology 重言式
deductive systems 推理系统
semantic tableaux 语义表
rules of inferences 推理规则

要区分清楚命题被证明和命题为真

我们主要关心逻辑系统(Logic System)的

1. consistency: 即一致性，命题和它的否定不能同时被证明
2. independence: 公理之间无法互相推出
3. soundness： 所有可被证明命题都为真
4. completeness： 所有真命题都可被证明

Hilbert希望证明数学可以被同时complete和consistent地公理化，但是Godel证明这是做不到的，即consistent的算术公理系统必然存在无法证明的真命题。

The system of logic that can be intepreted by values, functions and relations is called first-order logic(also called predicate logic or predicate calculus)

Modal Logic: 命题真值可以不是真和假，例如{T,F,M}表示一定真、假、可能真。当然也可以用概率来理解

Temporal Logic: Modal Logic的一种，{T,M,F}分别表示"always true","eventually true","false".这在交互式的程序中非常有用，例如OS

如何验证程序的正确性：

1. 首先要形式化定义"正确"为一个命题
2. 然后形式化程序的语义(行为)
3. 在一个形式系统中进行推理，验证程序满足正确性

介绍一种逻辑通常从syntax和semantic层面来说
syntax: 哪些是公式
semantic: 公式的含义(真值如何计算)

这本书对命题公式的定义是从树形结构的角度开始的，我觉得讲得比较清楚

树形结构变为公式的时候必然要损失结构信息，因此书中给出了三种解决(模糊含义)的方案

1. 加括号，这里通常认为所有连接命题的符号地位都是相等的
2. 规定优先级和结合性(左结合/右结合)，即对不同符号的优先级做出区分.奇怪的是书上说一般符号是右结合的

当然也可以用CFG(context free grammar)规定命题公式，就是递归定义~

Polish Notation

就是前序遍历表达式树(运算在元素前),求值就逆序遍历

Structural Induction

由Formulas的结构可知，证明一些相关命题可以通过结构递归来证明其对所有Formula成立

1. 证明原子命题成立
2. 假设命题A成立，证明对( eg A)成立
3. 假设A、B成立，证明A op B成立

Interpretations

一个Formula的Intepretation就是为其所有atoms赋予真值，即一个{all atoms}到{T,F}的函数

Formula F在Interpretation I下的真值叫the value of F under I

Partial Interpretaions

有时只需要带入部分atom的真值，这就是partial的含义

Truth Table

也即真值表.若F有n个atoms，则列2^n列枚举所有Interpretations，计算每种情况下F的真值

Logical Equivalence

若Formula F1 F2在任意Interpretation I下都有I(F1)=I(F2)，则称二者为Logical Equivalence，记作(F_1equiv F_2)

举例：((p ightarrow q)equiv ( eg pvee q))
这告诉我们在证明含变项的命题时需要证明它在任意解释下都成立

(leftrightarrow)和(equiv)的区别

(leftrightarrow)是二元算子，用以连接两个命题，构成一个新的大的命题
(equiv)是一个命题集合上的二元等价关系，两侧的命题看成是分开的两个部分

定理：有 (F_1equiv F_2) 当且仅当 (F_1leftrightarrow F_2)在任意解释下为真
证明：
必要性:(F_1equiv F_2)，故在任意解释I下 (I(F_1)=I(F_2))，即在任意解释I下(I(F_1)leftrightarrow (F_2))为真，即(F_1leftrightarrow F_2)在任意解释下为真

充分性:考虑(leftrightarrow)的真值表：(F_1leftrightarrow F_2)为真当且仅当(F_1=F_2)，即在任意解释下(F_1=F_2)，于是(F_1equiv F_2)

Substitution

logical equivalent是为了substitution做准备
首先要定义Subformula

Subformula

考虑Formula的树形结构，F'是F的Subformula当且仅当F'是F的子树
若F'!=F，则称为Proper Subformula

记A是一个formula，B是A的subformula，C是任意一个formula
则把操作(Aleft{Bleftarrow C ight})记为 substitute C for B in A,含义是用C换掉A中的B(注意顺序)

定理：对于substitution (A'=Aleft{Bleftarrow C ight})，若 (Bequiv C)，则有(Aequiv A')
证明：对表达式树的深度作归纳即可，base case是A中所有的B

substitution通常用于简化求值某些复杂formulas

Equivalences

常见的等价有很多，这里就不放了

Operators

重要性质：是否adequate，即是否能表示出所有可能的运算符号
n元运算op实际上可以看成是({T,F}^nmapsto {T,F})的函数，故n元运算总共有(2^{2^n})种

我们称二元运算(circ)由运算集(S=left{circ_1,ldots,circ_n ight})定义当且仅当
任意形如(A_1circ A_2)的公式都存在(A)可由(A_1,A_2)经(S)中的运算得到，且(Aequiv A_1circ A_2)。

事实上定义的符号是冗余的，例：
(Aleftrightarrow B=(Aleftarrow B)wedge(Bleftarrow A))
(Aleftarrow Bequiv eg Avee B)
(Awedge B= eg( eg Avee eg B))
(Auparrow T= eg(Awedge T)= eg A)
( eg Auparrow eg B= eg( eg Awedge eg B)=Avee B)
于是实际上只需要与非(nand)、或非(nor)的其中一个就可以表示出所有的符号

定理：若二元运算(circ)可表示出所有的二元运算和( eg)，则(circ)只能为(uparrow)或(downarrow)

想了挺久，书上给的提示2没有看懂，自己捣鼓了一下

不妨取(A=T)，则根据符号可被表示的定义有(F= eg Aequiv Acirc Acircldotscirc A=left(Acirc Acircldotscirc A ight)circ A)
我们claim对于(circ)运算必有(Tcirc T=F)
反证：假设(Tcirc T=T)，则上述式子根据左结合性有(F=T)，矛盾。故(Tcirc T=F)

同理可证(Fcirc F=T)。这说明(circ)只可能是(uparrow)、(downarrow)、(Acirc B= eg A)、(Acirc B= eg B)

考虑一个任意的二元运算op，则根据符号可被表示的定义有(A op Bequiv C_1circ C_2circldotscirc C_n)，其中(C_i=A)或(C_i=B)。而根据投影的定义，必然有(C_icirc C_j= eg C_i)或(C_icirc C_j= eg C_j)，这说明(A op B=A)或(A op B=B)或(A op B= eg A)或(A op B= eg B)，即(op)也是投影。这与op的任意性矛盾。

因此能表示出所有二元运算和( eg)的二元运算只能是(uparrow)和(downarrow)

Formula Semantics

A is a Formula

1. A is satisfiable iff (exists I), I(A)=T.此时称I是F的一个model
2. A is unsatisfiable iff (forall I), I(A)=F
3. A is valid iff (forall I)，I(A)=T,valid formula也叫做tautology,记作(models A)
4. A is falsifiable iff (exists I),I(A)=F,记作( otmodels A)

类似可以定义formula sets的语义(可满足/不可满足/永真/永假)

给定一个公式集合F的子集U，判断命题(Ain U)的真假的算法被称为decision procedure for U
利用真值表很容易写出satisfiability的一个decision procedure，并且可以用它来判断上述四种情况

Logical Consequnce

U是公式集，A是公式，若在任意使得U成立的解释I下都有I(A)=T(U的model都是A的model)，则称A是U的logical consequence,记作(Umodels A)

同样，( ightarrow)是公式的二元算子，用以连接两个公式得到新的公式
而(models)是元语言中的一个概念的符号(a symbol for a concept in the metalanguage)，是用来描述一阶语言的"语言用词"

类似(Aequiv B)当且仅当(Aleftrightarrow B)是永真式
定理：(Amodels B)当且仅当((wedge A_i) ightarrow B)是永真式，即(Amodels B)当且仅当(models ((wedge A_i) ightarrow B))

证明充分性：右侧永真，因此在任意解释下为真，因此在所有使得((wedge A_i))为真的解释下(B)都为真，这恰好就是(Amodels B)的定义
必要性：由反证法，假设右侧不是永真式，则存在解释I'使得(I'(wedge A_i)=T)而(I'(B)=F)，这与logical consequence的定义矛盾。故右侧永真

与简单的imply符号相比，logical consequence更复杂也更贴合实际(以若干定理/公理为真作为前提出发，得到若干定理)

Theory

若公式集F在logical consequence运算下满足封闭性，则称F为一个theory，F中的公式为theorem

若存在F的子集U使得(F=left{;Amid Umodels A; ight})，则称F是axiomatizable的，且U是F的axioms。若U有限，则F是finitely axiomatizable
书上33页有一句暂时看不懂的话，先放着

Semantic Tableaux

首先介绍complementary pair(互补对)的概念
literal是原子或原子的否定。对原子p而言，(p)是positive literal,( eg p)是negative literal
对于命题A而言，(A)与( eg A)互为互补对

semantic tableaux的出发点就是把公式A拆成A中的literals，即讨论哪些literals为真时A可满足，然后检查这些literals是否存在complementary pair

定理：公式可满足当且仅当不存在complementary pairs的literals set：
存在cp->任意解释都不满足literals set中的literals为T->公式不可满足，矛盾;
不存在cp->则令ls中的literals为T->这个解释是well defined的->A为T可满足;

流程

说白了一个tableau就是从公式A开始，每次取出优先级最低的运算op把A分成A1和A2
若op是(wedge)，则A1和A2都要为真(才能保证A可满足)，此时把A拆分成A1和A2
若op是(vee)，则A1或A2有一个为真就行了，此时造两个分支儿子分别讨论A1为真/A2为真
这样造出来的树形结构就是一个tableau，树上的叶子就是一个literal set，A可满足当且仅当存在没有complementary pair的叶子。并且若A的所有叶子都有compelmentary pair，则称A是close的，否则就是open的。就这么简单

有限性

算法的有限性证明要用到势能函数W(x)=3b(x)+n(x)，b和n分别为表达式x中二元符号和( eg)的数量。只需要证明随着深度递增，势函数单调递减，且叶子的势函数为0或2即可
或者先把A化成(wedge)范式，那么随着深度递增符号数量就是单调递减的了，这样也可以证明

正确性

正确性的证明包括两步:

1. soundness:所有closed formula都是不可满足的
2. completeness:所有不可满足的公式的任意一种tableau都是close的

1的证明可以对树高进行归纳，用上closed formula的所有子树都是closed formula->所有子树都不可满足，然后分类讨论(wedge)和(or)两种情况

2的证明可以化为证明 若公式存在open tableau，则公式可满足.把open leaf到根的路径上的节点并起来得到集合S,用结构归纳法证明S在叶子的所有literals为真的解释下为真(因此可满足)，且A也在S中，因此A可满足.

Deductive Proofs

也就是演绎证明.在之前的定理有(Umodels A)当且仅当(models (wedge U_i) ightarrow A)，因此我们似乎可以利用decision procedures来判断这个等价命题的真值来证明公理U下的一个命题A，但是我们很少直接这么做，因为：

1. U可能是无穷集,对于formulas with infinite terms的真值还没有做出定义
2. 并非所有逻辑都像命题逻辑一样存在decision procedures(并非所有逻辑都能判断一个命题是否可满足)
3. 有时推理过程中出现的intermediate results(中间结果)无法被认识，因为decision procedures只会给出最后的真值
4. 认识推理过程有利于我们认识公理和定理的关系，从而提出猜想

这一段写得蛮好，算是解决了俺之前看别的书的一大疑问，好评！

Deductive Systems

一个deductive system是一个二元组(U,R)，分别表示set of axioms(公理集合)和inference rules(推理规则)

A Proof

一个Proof是A Sequence Of Formulas(一段公式的有限有序序列)，其中每个公式要么是公理，要么可以由序列中它之前的所有公式(或某些公式)推出

对于长度为n的proof P，我们称An(最后一个公式)为theorem，P是An的一个proof，并且称An is provable，记作(vdash A_n)

有关(vdash)和(models)的区别可以看这个写得很好的回答

引入proof可以解决上面提到的四个问题：

1. Proof序列长度有限，虽然公理可以有无穷多个，但是只有有限多的公理能出现在一个证明中。
2. 虽然可能没有decision procedure，但是我们可以check(检查)一段给定的Proof是否正确
3. Proof显式地说明了每一条公理、定理的作用
4. 已被证明的定理可以用于后续证明

Gentzen System (mathscr{G})

axioms: a set of literals containing a complementary pair.
inference rules:

在Gentzen System中，从axioms出发证明命题A的过程可以看成是倒过来的树形结构，并且和对A造出的Semantic Tableau形态是一样的。

在ST中，每个节点内的子公式都是(wedge)的关系(即都为真->根才可满足)

而在GS中，每个节点内的子公式都是(vee)的关系(即每个节点的公式集取否定后就变成了ST)，因此axioms是永真的(包含互补对)

下面(vdash)的讨论都限定在Gentzen System中

定理：(vdash A)则(models A)

也即是GS soundness的证明。我们同样可以对树形结构进行归纳得到：

显然只需要证明( eg,wedge,vee)三种运算符的规律即可

(alpha)规则就是(vee)对(wedge)的逆分配律。由于两个子公式(A_1veeleft(vee U_1 ight))和(A_2veeleft(vee U_2 ight))都为真，所以((A_1veeleft(vee U_1 ight))wedge (A_2veeleft(vee U_2 ight)))仍然为真，经逆分配律就得到((A_1wedge A_2)vee(vee U_1)vee(vee U_2))为真

(eta)规则就是(vee)的结合律。由于(A_1vee A_2vee U)为真，因此((A_1vee A_2)vee U=Avee U)为真

定理：(models A)则(vdash A)

也即是GS completeness的证明。

由(models A)，( eg A)不可满足。构造( eg A)的semantic tableau T，T一定是closed tableau

将T的每一节点取反，这样就得到了在GS中对(A)的proof。

why?

1. T的每个叶子都close，因此都存在complementary pair，取反后仍然存在CP，满足axiom的定义
2. 仔细比对即可发现对应的拆分法则在取反意义下是相等的。

综上就有(vdash Aiff models A)

扩展到公式集(S)上，易得(vdash Siff (forall xin S)(vdash x)iff(forall xin S)(models x)iff models S)

这就为下面的定理做了铺垫

定理：(vdash A)当且仅当( eg A)存在一个closed tableau

(vdash A)当且仅当(models A)当且仅当( eg A)不可满足当且仅当( eg A)存在closed tableau

更进一步地，定理：(vdash S)当且仅当(overline S)存在closed tableu。这里(S)是公式集

记(P(x))表示(x)存在closed tableau

(vdash Siffmodels Siff(forall xin S)(models x)iff(forall xin S)(P( eg x))iff(forall xinoverline S)(P(x)))

那么只需要把(overline S)中的所有元素的closed tableau取出来，两两合并回去就得到(overline S)的closed tableau了

书上给的流程是先用归纳法证明最后一个定理，然后直接用closed tableau得到(vdash A)和(models)的关系。这里的证明是自己写的，希望没有什么大问题吧....

Hilber System (mathscr{H})

在(mathscr{G})中公理是非常简单的(包含CP的公式集)，而推理规则很多
在(mathscr{H})中则刚好反过来，公理很多，而推理规则只有一条

下面出现的大写字母都表示一个公式

公理包括
(vdash (A ightarrow (B ightarrow A)))
(vdash (A ightarrow (B ightarrow C)) ightarrow((A ightarrow B) ightarrow(A ightarrow C)))
(vdash (A ightarrow B) ightarrow ( eg B ightarrow eg A))

推理规则(又被称为分离规则)
公式(B)可由(A)及(A ightarrow B)推出

我们知道logical equivlalence在substitution后保持整个公式等值，因此证明的关键在于巧妙地作substitution....

axiom scheme & theorem scheme

在给出的公理中存在命题变元，因此所谓三条公理实际上各自代表了一类(无穷多)公理。因此这三条实际上是axiom shcemes(公理模式)
同理还有theorem schemes，也是一类定理的代表

extension of proofs

回顾一下上面的定义：

一个Proof是A Sequence Of Formulas(一段公式的有限有序序列)，其中每个公式要么是公理，要么可以由序列中它之前的所有公式(或某些公式)推出

对于长度为n的proof P，我们称An(最后一个公式)为theorem，P是An的一个proof，并且称An is provable，记作(vdash A_n)​

这里给出新的定义：

记(U)是公式集，(A)是公式，(Uvdash A)仍然表示(A)是(U)的语义后承。但我们把这个记号的含义拓展为：(U)是证明(A)成立时，作为假设成立的那些前提

此时一个Proof是一段形如(U_ivdash phi_i)的公式有限有序序列，其中(U_isubseteq U)，(phi_i)要么是公理(此时(U_i=emptyset))、要么(phi_iin U_i)、要么可以用(phi_{i'},phi_{i''})，(i',i''<i)通过分离规则得到、要么是前面证明过的定理

我们拓展proof定义的目的在于formalize一种叫derived rules的方法来证明一类形如(A ightarrow B)的公式。即通过假设(A)成立来通过推理规则得到(B)

也就是将证明(vdash A ightarrow B)化为证明(Avdash B)
之所以能这么做，是因为(mathscr{H})既sound又complete
因此有(Avdash BRightarrow Amodels BRightarrowmodels A ightarrow BRightarrowvdash A ightarrow B)

然后书上给了一大堆衍生的公式及证明...这里就不抄书了

有几个练习，写一下

Commutative (vdash Avee Bleftrightarrow Bvee A)

只需证明一侧，另一侧同理

(left{; eg A ightarrow B; ight}vdash eg A ightarrow B)

(left{; eg A ightarrow B; ight}vdash eg B ightarrow A)

(vdash ( eg A ightarrow B) ightarrow( eg B ightarrow A))

(vdash (Avee B) ightarrow(Bvee A))​​​​

Weakening1 (vdash A ightarrow(Avee B))​​​
(left{;A; ight}vdash A ightarrow ( eg B ightarrow A))​​

(left{;A; ight}vdash A)

(left{;A; ight}vdash eg B ightarrow A)

(left{;A; ight}vdash eg A ightarrow B)​​

(left{;A; ight}vdash Avee B)​​

(vdash A ightarrow(Avee B))

Weakening2 (vdash (A ightarrow B) ightarrow((Cvee A) ightarrow(Cvee B)))

(left{;A ightarrow B, eg C ightarrow A; ight}vdash eg C ightarrow A)​

(left{;A ightarrow B, eg C ightarrow A; ight}vdash A ightarrow B)

(left{;A ightarrow B, eg C ightarrow A; ight}vdash eg C ightarrow B)

(left{;A ightarrow B, eg C ightarrow A; ight}vdash Cvee B)​

(left{;A ightarrow B; ight}vdash( eg C ightarrow A) ightarrow(Cvee B))

(left{;A ightarrow B; ight}vdash(Cvee A) ightarrow(Cvee B))​

(vdash (A ightarrow B) ightarrow((Cvee A) ightarrow(Cvee B)))

Associativity (vdash (Avee B)vee Cleftrightarrow Avee(Bvee C))

只需证明(vdash (Avee B)vee C ightarrow Avee(Bvee C))，另一侧同理

(left{; eg A ightarrow( eg B ightarrow C), eg A; ight}vdash eg A)

(left{; eg A ightarrow( eg B ightarrow C), eg A; ight}vdash eg A ightarrow( eg B ightarrow C))

(left{; eg A ightarrow( eg B ightarrow C), eg A; ight}vdash eg B ightarrow C)

(left{; eg A ightarrow( eg B ightarrow C), eg A; ight}vdash eg C ightarrow B)

(left{; eg A ightarrow( eg B ightarrow C); ight}vdash eg A ightarrow( eg C ightarrow B))

(left{; eg A ightarrow( eg B ightarrow C); ight}vdash eg C ightarrow( eg A ightarrow B))​

(left{; eg A ightarrow( eg B ightarrow C); ight}vdash eg ( eg A ightarrow B) ightarrow C)​

(vdash( eg A ightarrow( eg B ightarrow C)) ightarrow( eg ( eg A ightarrow B) ightarrow C))​

(vdash(Avee(Bvee C)) ightarrow((Avee B)vee C))​​​​​​

有了这三个就可以很方便地证明(mathscr{H})的completeness和soundness了