数理逻辑学习笔记[1] 命题逻辑的形式系统

本文主要是介绍数理逻辑学习笔记[1] 命题逻辑的形式系统，希望对大家解决编程问题提供一定的参考价值，需要的开发者们随着小编来一起学习吧！

2 命题逻辑：语法

2.1 形式系统

形式系统

0. Q: 如何理解“形式（演绎）系统中有关符号的一切行为和性质不依赖符号特定的意义和具体的性质”？用常微分方程的形式幂级数解举例阐述。
   A: 提示：形式上规定针对幂级数可以逐项求微分或积分，而不考虑收敛性，从而给出常微分方程的形式幂级数解。
   这里的演算都是形式上、符号上的，不一定符合幂级数的实际数学含义。
1. Q: 语言、公理、规则和理论计算机中的哪些计算模型有联系？试举例。
   A: 如语言、规则和半Thue过程有类似之处。每次应用规则可能用前面的若干条已证明的定理但具体用哪条并未指定类似于非确定图灵机(DTM)。等等。
2. Q: 命题演算形式系统$L$中的形式语言${\mathcal{L}}_0$由哪两部分构成？
   A: 一个（可能无穷）的符号集$\sim ,\to ,(,),p_1,p_2,\cdots$，以及一个合式公式（well-formed formulas）集。
   注：回忆 { ∼ , → } \{\sim,\to\} {∼,→}是完备集。
   合式公式集是递归定义的。即$p_i$是公式；且对于公式$\mathcal{A},\mathcal{B}$，有$(\sim \mathcal{A})$和$(\mathcal{A}\to \mathcal{B})$是公式。
   注：当然也可以采用前缀表达式，从而不需要引入括号。
3. Q: 上面的符号集中的符号$\sim$和函数 f : { 0 , 1 } → { 0 , 1 } ; f ( 0 ) = 1 , f ( 1 ) = 0 f:\{0,1\}\to\{0,1\};f(0)=1,f(1)=0 f:{0,1}→{0,1};f(0)=1,f(1)=0有什么联系？
   A:
   形式系统$L$中的字符$\to$和$\sim$是抽象的记号，我们并不天然地认为它们代表了用真值表或布尔函数定义的“具体”的连接符$\to ,\sim$. 但是$L$的公理模式和推理规则实际上从某种程度上符合了$\to ,\sim$的意义。
4. Q: 说“$L$的公理只有三条”有何不准确之处？
   A: $L$有三个公理模式。每个公理模式中的$\mathcal{A},\mathcal{B}$等都可以代表任意公式（命题形式），从而有无数条公理。
   当然，也可以引入替换规则，这样可以只使用三条公理而不用前面说的“公理模式”了。
5. Q: $L$中的公理模式和演绎规则有什么密切的联系？
   A: 可以发现所有的公理模式都是$\mathcal{A}\to \mathcal{B}$形式。因此如果另已知$\mathcal{A}$，就可以通过分离规则得到直接后承$\mathcal{B}$. 这体现了两者的密切关系。

形式证明

0. Q: 形式证明中的公式序列中的公式可能是哪两种？
   A: 或者是一条公理（即公理模式代入具体公式后得到的公式）。或者是由序列中位于前面的两公式应用分离规则的直接后承。
1. Q: 依据形式证明的定义，能否在$L$中证明$L$的公理？
   A: 按照定义，$L$中的公理自然也是$L$中的定理。证明是只含有自身的序列。
   注：公理是没有经过证明，但被当作不证自明的命题。这和“在$L$中证明公理”是两个方面的东西。
2. Q: 从什么集合的演绎就是证明？
   A: 空集（或：包含若干条公理的集合）
   注：从集合$\Gamma$的演绎和从$\Gamma \cup {\Gamma }^{\prime }$的演绎（其中${\Gamma }^{\prime }$中所有公式都是公理）依据定义是相同的。
   注：因此$\mathcal{A}$是$L$中定理可以简记为$\varnothing {⊢}_L\mathcal{A},{⊢}_L\mathcal{A},⊢\mathcal{A}$.
3. Q: 使用前缀表达式（前置式），在$L$中构造$\mathcal{A},\to \mathcal{B}\to \mathcal{A}\mathcal{C}⊢\to \mathcal{B}\mathcal{C}$的演绎。
   A:
   (1)$\mathcal{A}$（假设）
   (2)$\to \mathcal{B}\to \mathcal{A}\mathcal{C}$（假设）
   (3)$\to \mathcal{A}\to \mathcal{B}\mathcal{A}$（L1）
   (4)$\to \mathcal{B}\mathcal{A}$（(1)(3)MP）
   (5)$\to \to \mathcal{B}\to \mathcal{A}\mathcal{C}\to \to \mathcal{B}\mathcal{A}\to \mathcal{B}\mathcal{C}$（L2）
   (6)$\to \to \mathcal{B}\mathcal{A}\to \mathcal{B}\mathcal{C}$（(2)(5)MP）
   (7)$\to \mathcal{B}\mathcal{C}$（(4)(6)MP）
4. Q: 抽象出上述过程，可以得到一条（），其具有推理规则的效果，可以帮助简化证明。
   A: 元定理。（关于对象语言形式系统的结果。区分与形式证明得到的具体的“定理”）
5. Q: 斜形证明中何时增加行首空格？
   A: 提示：画有向无环图，看经过的边数量。
6. Q: 在证明元定理$⊢\to \mathcal{A}\mathcal{A}$和$⊢\to \sim \mathcal{B}\to \mathcal{B}\mathcal{A}$时，所使用的隐含分配（L2）分别具体是什么？
   A: 可能的答案：
   $\to \to \mathcal{A}\to \to \mathcal{A}\mathcal{A}\mathcal{A}\to \to \mathcal{A}\to \mathcal{A}\mathcal{A}\to$

这篇关于数理逻辑学习笔记[1] 命题逻辑的形式系统的文章就介绍到这儿，希望我们推荐的文章对编程师们有所帮助！

---