标签：01 定义 mathscr 公式 right 命题逻辑 left 数理逻辑 scr
写在前面
第一次看这本书的时候看得比较急，也没有一个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
本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享； 2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关； 3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关； 4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除； 5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。