命题逻辑：语法

形式系统

0. Q: 如何理解“形式（演绎）系统中有关符号的一切行为和性质不依赖符号特定的意义和具体的性质”？用常微分方程的形式幂级数解举例阐述。
   A: 提示：形式上规定针对幂级数可以逐项求微分或积分，而不考虑收敛性。这里的演算都是形式上、符号上的，不一定符合幂级数的实际数学含义。
1. 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})$是公式。
   注：当然也可以采用前缀表达式，从而不需要引入括号。
   注：形式系统$L$中的字符$\to$和$\sim$是抽象的记号，我们并不天然地认为它们代表了用真值表或布尔函数定义的“具体”的连接符$\to ,\sim$. 但是$L$的公理模式和推理规则实际上从某种程度上阐述了$\to ,\sim$的意义。
2. Q: 说“$L$的公理只有三条”有何不准确之处？
   A: $L$应当说有三个公理模式。每个公理模式中的$\mathcal{A},\mathcal{B}$等都可以代表任意公式（命题形式），从而有无数条公理。
   当然，也可以引入替换规则，从而共有四条公理（而非公理模式）。
3. Q: $L$中的公理模式和演绎规则有什么密切的联系？
   A: 可以发现所有的公理模式都是$\mathcal{A}\to \mathcal{B}$形式。因此如果另已知$\mathcal{A}$，就可以通过分离规则得到直接后承$\mathcal{B}$. 这体现了两者的密切关系。
4. Q: 形式证明中的公式序列中的公式可能是哪两种？
   A: 或者是一条公理（即公理模式代入具体公式后得到的公式）。或者是由序列中位于前面的两公式应用分离规则的直接后承。
5. Q: 依据形式证明的定义，能否在$L$中证明$L$的公理？
   A: 按照定义，$L$中的公理自然也是$L$中的定理。证明是只含有自身的序列。
   注：公理是没有经过证明，但被当作不证自明的命题。这和“在$L$中证明公理”是两个方面的东西。
6. Q: 从什么集合的演绎就是证明？
   A: 空集（或：包含若干条公理的集合）
   注：从集合$\Gamma$的演绎和从$\Gamma \cup {\Gamma }^{\prime }$的演绎（其中${\Gamma }^{\prime }$中所有公式都是公理）依据定义是相同的。
   注：因此$\mathcal{A}$是$L$中定理可以简记为$\varnothing {⊢}_L\mathcal{A},{⊢}_L\mathcal{A},⊢\mathcal{A}$.
7. 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）
8. Q: 抽象出7.的过程，可以得到一条（），其具有推理规则的效果，可以帮助简化证明。
   A: 元定理。（关于对象语言形式系统的结果）
9. Q: 斜形证明中何时增加行首空格？
   A: 使用MP时。
10. 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 \mathcal{A}\mathcal{A}$.
    $\to \to \sim \mathcal{B}\to \to \sim \mathcal{A}\sim \mathcal{B}\to \mathcal{B}\mathcal{A}\to \to \sim \mathcal{B}\to \sim \mathcal{A}\sim \mathcal{B}\to \sim \mathcal{B}\to \mathcal{B}\mathcal{A}$.

演绎定理

0. Q: 叙述演绎定理（的正向），并针对 Γ ∪ { A } \Gamma\cup\{\mathscr A\} Γ∪{ A}到$\mathcal{B}$的演绎序列中只有一个公式的情况做出分类证明。
   A: 若 Γ ∪ { A } ⊢ L B \Gamma \cup\{\mathscr A\}\vdash_L\mathscr B Γ∪{ A}⊢L​B，则$\Gamma {⊢}_L(\mathcal{A}\to \mathcal{B})$.
   若演绎序列只有一个公式，则$\mathcal{B}$是公理或$\Gamma$中元素时用一次L1即可。而$\mathcal{B}$就是$\mathcal{A}$时回忆上一节10.
1. Q: 接上，如果$\mathcal{B}$不是以上三种情况，那么它一定是（）而得的。那么根据归纳，一定有$\Gamma {⊢}_L$（）和$\Gamma {⊢}_L$（）。于是在（）和（）的演绎序列后加上几步（要使用L2）即得待求的（）的演绎序列。
   A: 由 Γ ∪ { A } \Gamma \cup \{\mathscr A\} Γ∪{ A}（通过更少步演绎得到的）两条公式根据MP，$\mathcal{A}\to \mathcal{C}$，$\mathcal{A}\to (\mathcal{C}\to \mathcal{B})$，$\mathcal{A}\to \mathcal{C}$，$\mathcal{A}\to (\mathcal{C}\to \mathcal{B})$，$\mathcal{A}\to \mathcal{B}$
2. Q: 通过演绎定理可以证明HS（假言三段论）也能起到推理规则的作用。而通过HS和（）（填公理模式）可以得到$⊢\sim \mathcal{A}\to (\mathcal{A}\to \mathcal{B})$，再用演绎定理得到（）。说出该事实的实际含义。
   A: L1和L3，$\sim \mathcal{A},\mathcal{A}⊢\mathcal{B}$. 自相矛盾的题设可以推出一切结论。
   注：可以发现$\sim \mathcal{A},\mathcal{A}$都写到$⊢$左边后，顺序可以调换。从而马上得到$⊢\mathcal{A}\to (\sim \mathcal{A}\to \mathcal{B})$
3. Q: 为了证明$⊢(\sim \mathcal{A}\to \mathcal{A})\to \mathcal{A}$，我们考虑对2.中的$\sim \mathcal{A}⊢\mathcal{A}\to \mathcal{B}$应用（）（填公理模式），得到：在已知条件$(\sim \mathcal{A}\to \mathcal{A})$时，对于一切公式$\mathcal{B}$都有$(\sim \mathcal{A}\to \mathcal{B})$可以（）。把$\mathcal{B}$替换为$\sim (\sim \mathcal{A}\to \mathcal{A})$，就得到了$\sim \mathcal{A}\to \mathcal{A}⊢\sim \mathcal{A}\to \sim (\sim \mathcal{A}\to \mathcal{A})$. 接下来（）就证明了结论。
   A: L2，被演绎得到，用L3及演绎定理再划去左侧集合中重复的元素$\sim \mathcal{A}\to \mathcal{A}$.
4. Q: 在形式证明的简略形式中，可以省略指明替换、MP和演绎定理。即：实际书写时行右边的括号标注不再只能是(m)(n)(MP)或(Ln)的形式。而有可能是（）（说出在简略形式中可能出现但在非简略形式中被认为不规范的一些括号标注）。省略演绎定理在实际书写中能带来什么便利？
   A: (m)(Ln)形式，(m)(Ln)(HS)形式，等等。
   注意：省略了MP。
   注意：不用单起一行写(Ln)（即：省略了替换）。
   例：
   (1)$\sim \sim \mathcal{A}⊢\sim \mathcal{A}\to \sim \sim \sim \mathcal{A}$
   (2)$\sim \sim \mathcal{A}⊢\sim \sim \mathcal{A}\to \mathcal{A}$(1)(L3)(HS)
   省略演绎定理可以减少括号和$\cdot$的使用，把$⊢$当成区分优先级的工具。
5. Q: 用简略形式证明$\mathcal{A}\to \mathcal{B}⊢\sim \mathcal{B}\to \sim \mathcal{A}$. 尝试解释为什么不把前式作为公理模式。
   A:
   (1)$\sim \sim \mathcal{A}⊢\sim \sim \sim \sim \mathcal{A}\to \sim \sim \mathcal{A}$(L1)
   (2)$\sim \sim \mathcal{A}⊢\sim \mathcal{A}\to \sim \sim \sim \mathcal{A}$(1)(L3)(HS)
   (3)$\sim \sim \mathcal{A}⊢\sim \sim \mathcal{A}\to \mathcal{A}$(2)(L3)(HS)
   (4)$\sim \sim \mathcal{A}⊢\mathcal{A}$(演绎定理，此行其实可以省略)
   (5)$\sim \sim \sim \mathcal{A}⊢\sim \mathcal{A}$(替换，当然替换可以不写)
   (6)$\mathcal{A}⊢\sim \sim \mathcal{A}$(5)(L3)(MP，当然MP可以不写)
   (7)$\mathcal{A}\to \mathcal{B},\sim \sim \mathcal{A}⊢\mathcal{A}\to \mathcal{B}$(假设)
   (8)$\mathcal{A}\to \mathcal{B},\sim \sim \mathcal{A}⊢\mathcal{B}$(4)(7)(MP，当然MP可以不写)
   (9)$\mathcal{A}\to \mathcal{B},\sim \sim \mathcal{A}⊢\sim \sim \mathcal{B}$(8)(6)
   注：从不同角度讲（采用不同的公式集$\Gamma$），(9)可以看成(MP)也可以看成(HS). 通过演绎定理转换即可得到“不同角度”。
   (10)$\mathcal{A}\to \mathcal{B}⊢\sim \mathcal{B}\to \sim \mathcal{A}$(9)(L3)(HS)
   不选取(10)作为公理模式，一个可能的原因是公理模式(L3)可以去除$\sim$，而(10)反过来添加$\sim$，不能合理应用。
6. Q: 回忆2.中我们得到过$\mathcal{A},\sim \mathcal{A}⊢\mathcal{B}$. 为了把它写成$⊢\sim \mathcal{A}\wedge \mathcal{A}\to \mathcal{B}$形式，我们定义合取$\mathcal{A}\wedge \mathcal{B}$表示$\sim (\mathcal{A}\to \sim \mathcal{B})$. 因此，我们希望由$\mathcal{A},\mathcal{B}⊢\mathcal{C}$推出$⊢\sim (\mathcal{A}\to \sim \mathcal{B})\to \mathcal{C}$. 如何作此推理？你可以直接使用5.中的(6)(10).
   A:
   (1)$\mathcal{A}⊢\mathcal{B}\to \mathcal{C}$(演绎定理)
   (2)$\mathcal{A}⊢\sim \mathcal{C}\to \sim \mathcal{B}$(1)(5.中的(10))(HS)
   (3)$\mathcal{A},\sim \mathcal{C}⊢\sim \mathcal{B}$(演绎定理)
   (4)$\sim \mathcal{C}⊢\mathcal{A}\to \sim \mathcal{B}$(演绎定理)
   (5)$\sim \mathcal{C}⊢\sim \sim (\mathcal{A}\to \sim \mathcal{B})$(4)(5.中的(6))(HS)
   (6)$\sim (\mathcal{A}\to \sim \mathcal{B})⊢\mathcal{C}$(5)(L3)
   （最后一行用演绎定理推出$⊢\sim (\mathcal{A}\to \sim \mathcal{B})\to \mathcal{C}$可以省略）

形式系统的性质

0. Q: $L$中公式集不一致为什么等价于公式集能$⊢$一切公式？
   A: 回忆上一节2.
   并且注意：公式集不一致的定义是能同时$⊢\mathcal{A}$和$⊢\sim \mathcal{A}$，所以能推出一切公式的公式集当然是不一致的。
1. Q: 平凡性和一致性有什么联系和区别？
   A: 一致性可以作为公式集的性质。如果一切不一致的公式集都能推出一切公式，那么说明形式系统具有平凡性。特别地，$L$具有平凡性。
   注：当然，我们也考察形式系统是否具有一致性。之后我们会证明$L$是一致的，这其实就相当于所有公理作为公式集具有一致性。
2. Q: 不一致公式集和真值指派有何关系？
   A: 不一致公式集没有模型，即一切指派都不能使得不一致公式集中公式全部为真。（通过反证法和不一致公式集的定义可以说明）
3. Q: 如何理解“平凡性对数学是合理的，但对数学之外则不合理”？
   A: 提示：比如银行管理系统不能因为一个偶然的错误就让任意人取任意钱。这涉及对错误和异常的处理方法等。
4. Q: ${\mathcal{L}}_0$中公式集的极大一致和一致有什么关系？举一个数学中的对象进行类比说明。
   A: 极大一致的公式集是一致的，但加入任何一条新的公式就不再一致了。类比线性空间的一组基是线性无关的，但加入任何一个新的向量就不再线性无关了。
5. Q: 为了证明${\mathcal{L}}_0$中极大一致的公式集$\Gamma$一定对于任意公式$\mathcal{A}$有$\mathcal{A}\in \Gamma$或$\sim \mathcal{A}\in \Gamma$，可以说明一旦 Γ ∪ { ∼ A } \Gamma\cup\{\sim\mathscr A\} Γ∪{ ∼A}不一致，那么（）$\in \Gamma$. 如何做此推理？
   A:
   (1)$\Gamma ,\sim \mathcal{A}⊢\mathcal{B}$(假设)
   (2)$\Gamma ,\sim \mathcal{A}⊢\sim \mathcal{B}$(假设)
   (3)$\Gamma ,\mathcal{B}⊢\mathcal{A}$(2)(L3)
   (4)$\Gamma ⊢\sim \mathcal{A}\to \mathcal{A}$(1)(3)(HS)
   (5)$\Gamma ⊢\sim \mathcal{A}\to (\sim \mathcal{B}\to \sim \mathcal{A})$(L1)
   (6)$\Gamma ⊢\sim \mathcal{A}\to (\mathcal{A}\to \mathcal{B})$(5)(L3)(HS)
   (7)$\Gamma ,\sim \mathcal{A}\to \mathcal{A}⊢\sim \mathcal{A}\to \mathcal{B}$(6)(L2)
   (8)$\Gamma ⊢\sim \mathcal{A}\to \mathcal{B}$(4)(7)
   (9)$\Gamma ⊢\sim \mathcal{A}\to \sim (\sim \mathcal{A}\to \mathcal{A})$(8)
   (10)$\Gamma ,\sim \mathcal{A}\to \mathcal{A}⊢\mathcal{A}$(9)(L3)
   (11)$\Gamma ⊢\mathcal{A}$(4)(10)
   最后，由于$\Gamma$极大一致，且$\Gamma ⊢\mathcal{A}$，故$\mathcal{A}\in \Gamma$.（否则， Γ ∪ { A } \Gamma \cup \{\mathscr A\} Γ∪{ A}是$\Gamma$的真超集，且是一致的，矛盾）
6. Q: 极大一致子集唯一吗？为什么？
   A: 不一定。设$\Gamma$是一致但不完备的公式集（即$\Gamma$不能推出$\mathcal{A}$也不能推出$\sim \mathcal{A}$），则 Γ ∪ { A , ∼ A } \Gamma\cup \{\mathscr A,\sim\mathscr A\} Γ∪{ A,∼A}的极大一致子集就不唯一。空集是一个平凡的$\Gamma$的例子。
   具体地， Γ ∪ { A } \Gamma\cup\{\mathscr A\} Γ∪{ A}是 Γ ∪ { A , ∼ A } \Gamma\cup \{\mathscr A,\sim\mathscr A\} Γ∪{ A,∼A}的一致子集，否则参考5.，有$\sim \mathcal{A}\in \Gamma$，矛盾。
   且 Γ ∪ { A , ∼ A } \Gamma\cup \{\mathscr A,\sim\mathscr A\} Γ∪{ A,∼A}本身不一致显然。因此 Γ ∪ { A } \Gamma\cup\{\mathscr A\} Γ∪{ A}是 Γ ∪ { A , ∼ A } \Gamma\cup \{\mathscr A,\sim\mathscr A\} Γ∪{ A,∼A}的极大一致子集。同理 Γ ∪ { ∼ A } \Gamma\cup\{\sim\mathscr A\} Γ∪{ ∼A}也是。
7. Q: 由于6.，我们有两种定义“极大一致推理”的方式，即：$\Gamma {⊢}_{MCS}\mathcal{A}$当且仅当一切$\Gamma$的极大一致子集都${⊢}_L\mathcal{A}$. 或$\Gamma {⊢}_{MCS}\mathcal{A}$当且仅当存在一个$\Gamma$的极大一致子集能${⊢}_L\mathcal{A}$.
   对于这两种定义，极大一致推理${⊢}_{MCS}$分别是否具有平凡性和单调性？
   A: 无论哪种定义方式，不一致的$\Gamma$都不一定能推出一切公式。比如6.中 Γ ′ : = Γ ∪ { A , ∼ A } \Gamma':=\Gamma\cup \{\mathscr A,\sim\mathscr A\} Γ′:=Γ∪{ A,∼A}不一致，其所有极大一致子集是 Γ 1 : = Γ ∪ { A } \Gamma_1:=\Gamma\cup\{\mathscr A\} Γ1​:=Γ∪{ A}和 Γ 2 : = Γ ∪ { ∼ A } \Gamma_2:=\Gamma\cup\{\sim\mathscr A\} Γ2​:=Γ∪{ ∼A}显然。
   注：原因是${\Gamma }^{\prime }$本身不是一致子集，且$\Gamma$的任意真子集一定是前述两极大一致子集${\Gamma }_1,{\Gamma }_2$之一的子集。
   则${\Gamma }^{\prime }$无论在哪种极大一致推理的定义下，都不能推出一切公式（只要$\Gamma$非空，例如是单元素集 { p } \{p\} { p}. 论证单元素集 { p } \{p\} { p}的一致性可以参考下一期中证明公理的独立性以及证明一致性定理）。
   对于第一种定义方式，没有单调性。比如考虑前述${\Gamma }_1\subset {\Gamma }^{\prime }$.，则${\Gamma }^{\prime }$的一个极大一致子集${\Gamma }_2$就不能推出$\mathcal{A}$.
   对于第二种定义方式，有单调性。因为如果${\Gamma }^{\ast }$是$\Gamma$的极大一致子集，那么${\Gamma }^{\ast }$是 Γ ∪ { A } \Gamma\cup\{\mathscr A\} Γ∪{ A}的一致子集，从而${\Gamma }^{\ast }$或者 Γ ∗ ∪ { A } \Gamma^*\cup\{\mathscr A\} Γ∗∪{ A}之一一定是 Γ ∪ { A } \Gamma\cup\{\mathscr A\} Γ∪{ A}的极大一致子集。从而单调性容易说明。