放一个将 “使用演绎定理的证明” 转写为直接证明的算法: 

假定我们现在已经有了 Γ∪{p} |- q 的证明序列 (q_1,q_2,…,q_n=q) , 想要写出一个 Γ |- {p→q} 的证明序列. 我们知道直接证明的定义虽然是链式的, 但它实际上有着如同二叉树的结构: 从最后的结论往前回溯, 每一个公式要么是由它之前的两个公式 MP 得到, 要么是一个公理/条件. 所以我们可以把证明序列 {q_n} 写成 (非完全) 二叉树的形式. 以下是一个示例:

显然, 在没有条件 p 时, q_i 不一定都为真, 但 p→q 是一定为真的, 所以我们把这个二叉树中的所有 q_i 改为 p→q_i . 现在只剩下两个问题: 1. 每一个叶子上的 p→q_i 如何得到; 2. 已知 q_i 与 q_j 通过 MP 得到 q_k , 如何用 p→q_i 和 p→q_j 得到 p→q_k.

我们首先回答第二个问题: 由于 q_{i,j,k} 是一个满足 MP 所需形式的三元组, q_j 一定形如 q_i→q_k (或者相反, 但这里 q_i 和 q_j 地位是相同的, 无需另外讨论) . 我们可以先用 q_i→q_k 结合公理模式 L1 通过 MP 得到 p→(q_i→q_k) , 再用公理模式 L2 写出 (p→(q_i→q_k))→((p→q_i)→(p→q_k)) , 连续 MP 两次得到 p→q_k (下文中将这整个过程称为 “衍生 MP” ) .

对问题一的回答是容易的: 对于每一个在原证明中处于叶子的 q_i , 如果 q_i 本身是公理或者属于 Γ, 依然可以直接写出; 如果 q_i 本身就是条件 p , 则可以背诵一套经典的内定理 p→p 的证明.

最后, 注意到对条件 p 的引入采用 “一滴血原则” , 即对于某个中间公式 q_i , 只有当它或者它的引理证明中用到 p 时才转写成 p→q_i ; 如果 q_i 在没有条件 p 时也成立, 那么直接照搬原证明中对它的证明序列即可. 但是, 如果发现它紧跟着的下家需要转写, 也需要再用 L1 把它变成 p→q_i 以便后文证明. (例如下图的 q_6 对 q_7 的作用.)

由此我们得到新证明的二叉树 (注意在这个二叉树中, 每一次推导使用的是衍生 MP 而非 MP, 所以写出来的公式数量会多很多) :

下面我们展示一个具体的例子 ∅ |- ((p→q)→r)→(q→r). 在这个例子中我们使用了两次演绎定理, 那么往回转写两次即可.

连续演绎定理拉回两次, 我们改为证 {(p→q)→r,q} |- r . 这个题的直接证明是容易的:

① q 条件

② q→(p→q) 公理L1

③ p→q ①②MP

④ (p→q)→r 条件

⑤ r ③④MP

现在进行第一层转写, 即试图写出 {(p→q)→r} |- q→r 的直接证明.

我们回顾证明序列的每一个公式, 在前面添加上 “q→…” 试图重现整个证明. 注意到 ③ 做如此改写后形如 q→(p→q) , 本身就是一个公理, 没有必要再从改写后的 ①② 推出. 所以我们先写出 ③' : q→(p→q) 随时备用.

再看④, 由于 (p→q)→r 本身是条件, ④' q→((p→q)→r) 可以联合 L1 做一次 MP 轻松得到. 我们把这个过程列出来:

① (p→q)→r 条件

② ((p→q)→r)→(q→((p→q)→r)) 公理L1

③ q→((p→q)→r) ①②MP

再拿出我们准备好的 ③' :

④ q→(p→q) 公理L1

现在, 上述 ③ 和 ④ 已经具备 L2 所需的形式, 可以开始衍生 MP :

⑤ (q→((p→q)→r))→((q→(p→q))→(q→r)) 公理L2

⑥ (q→(p→q))→(q→r) ③⑤MP

⑦ q→r ④⑥MP

现在开始第二层转写, 即直接证明原给命题. 我们分析上述序列的二叉树结构: ①②MP③, ③⑤MP⑥, ④⑥MP⑦. 这里用到条件的本质上只有①, 并且注意到 ①→③ 实际上形如公理 (就是②) , 所以没必要再去转写 ①→① 和 ①→② , 直接先准备好 ①→③, 然后列出⑤⑦, 用一次 L1 做出 ①→⑤ 和 ①→⑦ , 连续 “衍生 MP" 两次即可.

总结一下: 这里我们给出了一个在直接证明题目中 “先使用演绎定理寻找思路, 再转写消除演绎定理痕迹” 的工具. 

需要注意两点: 

1. 我们偷渡出来的工具只有演绎定理一条, 不包括反证律, 二次否定等, 用这些二级结论找到的思路需要寻求别的方法合法化; 

2. 尽管这种算法可以直接证明任何命题, 但我们没有必要机械地照搬算法的每一步, 而是可以随时注意转写出来的哪一步本身就形如公理, 从而不必再转写其上层; 也没有必要一上来就用算法库库抄, 可以先自己想想思路, 划归到一个形式简单, 但证不出来的引理后, 再用算法来处理这个引理, 或许会更节省时间.

最后建议考前看到这条的同学, 如果想要在考试时使用这种方法, 最好还是自己找几个公式来练一下手. 读过了算法及其证明并不代表理解乃至熟练了整个算法思想, 如果没有手操经验, 考场上可能会在某一步不知道自己此刻要干什么耽误时间.

考试的时候一般可以直接skip掉直接证明，因为就是证不出来。

一定要记得打印老师的PPT的最后一个part，那里面有谓词推理的格式要求和示例，而这一部分书上是没有的，考试最后一题还必考这个推理，如果没打印就只能像当时考试坐在我旁边的同学一样面对最后一个题想半天一个字也写不出来，最后无奈像沙摩柯一样弃牌了。

至于老师的讲课，确实是听不下去，so这学期全程没听过课，作业也没做明白过，全是用gpt帮忙写的。最后考试一天速通的，拿到3.7也可以接受。