写在前面

第一次看这本书的时候看得比较急，也没有一个big picture的把握，所以在细节上面耗费了很多时间....现在算是重构一次笔记了

我们知道，形式逻辑是对推理的形式化（mathematical logic formalizes resoning），为了描述推理我们有各种各样的逻辑系统。对于一个逻辑系统，最关键的就是它的语法（Syntax）和语义（Semantics）。其中语法决定了逻辑系统中讨论的对象长什么样，而语义决定了我们如何解释这些逻辑系统中被研究的对象。

比如说我们有研究命题的命题逻辑（Propositional Logic）、包含了函数 算术的一阶逻辑（First Order Logic）、对真值进行扩充得到的模态逻辑等等。这些逻辑的区别就在于它们的语法和语义（当然应用也不一样，这是废话）。

同时，在熟悉这些逻辑系统的同时，还要分清什么是我们的研究对象。因为逻辑在研究推理的形式化，因此需要区分什么是逻辑系统中的形式化推理（研究对象），什么是我们对于研究对象的推理。后者被成为元逻辑、元语言，前者就是对象逻辑、对象语言了。所有的对象逻辑都应根据相应的逻辑系统的定义赋予其含义，而在元语言的层面则可以随意一些，就是正常的平时推理。

本书是写给CSer的数理逻辑教材，因此会专门讲不同逻辑系统中的一类算法（Decision Procedure）的构造和正确性证明，这些是纯数不太感兴趣的东西，也是这本书多出来的东西。同时在看的时候，还要尤其注意什么是基础、什么是组合构造方法、这些逻辑对哪些东西做了抽象，这三板斧应该刻在DNA里。

废话不多说

命题逻辑

命题逻辑是比较常见易懂的逻辑，它主要关心在给出若干基本命题（atoms）之后，如何通过组合小命题来获得大命题、如何给组合命题递归地赋予含义（Compositionality），因此用树形结构来展示这样的命题构造就是很自然的了。

语法

给出BNF

\[{stmt = atom\;|\;(\neg\;stmt)\;|\;(stmt_1\;op\;stmt_2)} \]

为了方便，引入语法符号 \(\top,\bot\)，规定任意解释下都有 \({\mathscr I}(\bot)=F,{\mathscr I}(\top)=T\)

注意，我们给出这样的定义之后，无穷多项的公式就不存在了（回忆BNF的推导序列是有限的）

通常记所有公式组成的集合为 \(\mathscr F\)

语义

定义公式 \(A\) 的一个解释 \(\mathscr I\) 为一个函数 \(U_A\mapsto \left\{T,F\right\}\)，其中 \(U_A\) 为公式 \(A\) 中包含的所有原子所组成的集合

通过 \({\mathscr I}(A_1)\) 和 \({\mathscr I}(A_2)\) 给出 \({\mathscr I}(A_1\;op\;A_2)\) ，以此来定义命题构造子（别人都叫他运算符，但我更喜欢这么说）\(op\) 的含义

若在某个解释 \(\scr I\) 下公式 \(A\) 满足 \({\scr I}(A)=T\)，我们就说 \(A\) 是可满足的（satisfiable），此时的 \({\scr I}\) 是 \(A\) 的一个模型（Model）

若在任意解释 \({\scr I}\) 下公式 \(A\) 满足 \({\scr I}(A)=T\)，我们就说 \(A\) 是永真的（valid），记作 \(\models A\)

类似可以定义永假的（即不可满足的 unsatisfiable）、可假的（fasifiable）记作 \(\not\models A\)，在某些操作下这四种性质可以互相转化

需要注意的是，我们在命题逻辑中讨论的全都是命题变元（语法上的公式），而赋予其真值是解释做的事情（语义上的含义）。这也是为什么我没有通过给“运算符”列真值表来定义，这里的定义完全是基于解释的。

定义和定理

公式组成的集合的解释

记 \({\scr U}=\left\{A\right\}\) 为公式的集合（在这里我们忽略无穷集，因为对于无穷的二元运算没有定义）

若在某个解释 \({\scr I}\) 下有 \({\scr I}(A)=T\) 对 \({\scr U}\) 中的每个公式都成立，则称 \({\scr U}\) 是可满足的

若在任意解释 \({\scr I}\) 下都存在 \({\scr U}\) 中的某个公式 \(A\) 使得 \({\scr I}(A)=T\)，则称 \({\scr U}\) 是不可满足的

容易发现这个定义就是在讨论 \(\bigwedge_{A\in {\scr U}} A\) 在解释 \({\scr I}\) 下的真值

运算符

一个 \(n\) 元运算实际上是 \(\left\{T,F\right\}^n\mapsto \left\{T,F\right\}\) 的一个函数，因此有 \(\scr F\) 上的本质不同的 \(n\) 元运算有 \(2^{2^n}\) 种。

在结构归纳法中我们需要讨论所有形式的公式（即，在每一种运算下产生的所有公式），非常麻烦。一种想法是找出尽可能基本的运算，在此之上构造剩余的运算。

定义运算 \(\circ\) 能被 \(O=\left\{\circ_1,\circ_2\ldots\circ_n\right\}\) 表示，当且仅当对于任意 \(\scr F\) 中的公式 \(A,B\)，都有 \(A\circ B=C_X\circ_Y C_X\cdots C_X\)

其中 \(C_X\in\left\{A,B\right\}\)，\(\circ_Y\in O\)

特殊地，对于单目运算符 \(\sim\)，我们修改定义为 \(\sim A=A\circ_Y A\cdots A\)，其中 \(\circ_Y\in O\)

定义运算集 \(O\) 是完备的（Adequate），当且仅当所有运算都可被 \(O\) 表示。学过数电都知道 NAND和NOR 可以搭出所有电路，在逻辑系统中也有这样的性质，证明只需要简单的构造一下就好了。常用的完备集是 \(\left\{\wedge,\vee,\neg\right\}\)

定理：二元运算的最小完备集只可能是 \(\uparrow\) 或 \(\downarrow\)，即NAND或NOR。具体的证明可以看后面的习题合辑（如果我没有咕咕咕的话）

等价、逻辑后承

定义 \(\mathscr F\) 上的二元关系 \(\equiv\) 逻辑等价（Logical Equivalence）为：

\(A_1\equiv A_2\) 当且仅当在任意解释下，有 \({\mathscr I}(A_1)={\mathscr I}(A_2)\)

定义逻辑后承（Logical Consequence）的含义为：

\({\scr U}\models A\) 当且仅当在所有使得 \({\scr U}\) 可满足的解释 \(\scr I\) 下，都有 \({\scr I}(A)=T\)

我个人觉得也可以叫语义后承

\(A\leftrightarrow B\) 永真当且仅当 \(A\equiv B\)

\(\bigwedge_{A\in {\scr U}}A\rightarrow B\) 永真 当且仅当 \({\scr U}\models B\)

这两个定理实际上是为命题逻辑系统中的语法符号作出了解释，即我们可以用一些逻辑系统内部满足的性质来代替元语言的描述

子公式、替换

子公式仍然是 \(\scr F\) 上的二元关系，在不影响上下文理解的时候，我们将把 \(A\) 是 \(B\) 的子公式简记作 \(A\subseteq B\)

子公式的严格定义可以通过公式作为树结构导出，只需要照抄子树的定义就好

同样在树结构上操作，我们可以将一棵子树替换为另一棵子树，在公式中就表现为将一段子公式替换为另一个公式，记作 \(A\left\{B\leftarrow C\right\}\)，其中 \(B\subseteq A\)，解释为 把 \(A\) 中的所有子公式 \(B\) 替换为公式 \(C\)

若 \(B\equiv C\) 且 \(B\subseteq A\)，则有 \(A\left\{B\leftarrow C\right\}\equiv A\) 成立

具体的证明可以通过对树形结构来归纳做。

文字、互补对

这个翻译很怪

对于原子 \(p\)，我们把 \(p\) 和 \(\neg p\) 称为一对文字（Literals），其中 \(p\) 是正文字（Positive），\(\neg p\) 是负的（Negative）

同一个原子的两个文字组成一对互补对（Complementary Pair）

若公式集 \({\scr U}\) 存在一对互补对，即存在 \(p,\neg p\in {\scr U}\)，当且仅当 \({\scr U}\) 不可满足

这是由定义即得的。互补对定理使得我们可以构造出一种正确的Decision Procedure

理论

若公式集 \(\scr F\) 在 \(\models\) 二元关系下满足封闭性，则称 \(\scr F\) 是一个理论（Theory），\(\scr F\) 中的公式为定理（Theorem）

对于一个理论 \(\scr F\)，若存在 \(\scr U\subseteq F\) 使得 \({\scr F=}\left\{A|{\scr U}\models A\right\}\)，则称 \(\scr F\) 是可公理化的（Axiomatizable），\(\scr U\) 是 \(\scr F\) 的一组公理。

需要注意的是，这里对公理集的大小没有限制。考虑皮亚诺公理系统，我们对自然数集中的每个元素都作出了公理化的定义，因此皮亚诺公理系统的公理集合实际上是由一个Axiom Scheme产生的，我们把这个单独的Scheme作用到每个元素上就得到了无穷多个公理。

标签：01,定义,mathscr,公式,right,命题逻辑,left,数理逻辑,scr
来源： https://www.cnblogs.com/jjppp/p/15059118.html