证明技巧：思路图
使用公理系统时，证明的「构思过程」与证明的「书写过程」大相径庭。思考过程往往从最后一步开始，逐步规约。来看两个例子
传递律的证明
\[A\rightarrow B, B\rightarrow C\vdash A\rightarrow C \]Thinking & Writing...
换位律的证明
\[\vdash(A\rightarrow(B\rightarrow C))\rightarrow (B\rightarrow(A\rightarrow C) ) \]Thinking & Writing...
证明技巧：待定公式法
E1
证明
\[\vdash \neg\neg P\rightarrow P \]容易想到应该用公理3，我们希望干这件事：
\[\begin{aligned} ??? &\rightarrow \neg \neg P\\ &\Downarrow\\ \neg P &\rightarrow\ ???\\ &\Downarrow\\ ??? &\rightarrow P \end{aligned} \]显然，我们需要一个公式\(???\)带着\(\neg\neg P\)来回转。那我们不妨令\(???=\neg\neg R\)，从而
\[\neg\neg P\rightarrow(\neg\neg R\rightarrow \neg\neg P) \qquad \mathscr A_1 \]对\(\neg\neg R\rightarrow \neg\neg P\)用两次公理3，得到\(R\rightarrow P\)，再用一次公理2，借助传递律和MP规则得
\[(\neg\neg P\rightarrow R) \rightarrow (\neg\neg P\rightarrow P) \]我们令\(\vdash \neg\neg P\rightarrow R\)，显然可以取
\[\neg\neg P\rightarrow R \equiv \neg\neg P\rightarrow(Q\rightarrow \neg\neg P) \]于是可以回头构造证明
E2
证明
\[\vdash (A\rightarrow\neg A)\rightarrow \neg A \]显然我们可以用\(\vdash (\neg A\rightarrow A)\rightarrow A\)和\(\vdash (P\rightarrow Q)\rightarrow (\neg Q\rightarrow \neg P)\)快速解决这个题。
不过，如果我们从\(\neg A\)开始构造证明呢？
我们不妨设可以得到\(\neg\neg R\rightarrow \neg A\)
证明技巧：识别死胡同
我们的公理系统具有可靠性，也就是说，在语义层面
-
它只能从永真的公式推演到永真的公式，不能从永真的公式推出不永真的公式
-
它推出的公式中，后件可满足的情况一定比前件多，后件不可满足的情况一定比前件少，前件可满足时后件一定可满足。
-
简而言之，它只能使结论/后件的永真性不断变强，不能使其变弱
所以，如果你发现以下情况，那说明你的证明思路是错的
-
如果你想要证明一个(满足前提条件时)不是永真的公式，那你应该考虑给这个公式增加一些前件，或者调整它的结构，把它变成永真式
例如，如果见到\(B\rightarrow(A\rightarrow C)\)，那说明你走错路了
-
如果你想要通过证明\(A\rightarrow B\)来证明\(B\)，或者想要通过\(R\rightarrow(A\rightarrow B)\)来证明\(R\rightarrow B\)，但\(A\)并不是一个永真公式，那么除非你确定你有特殊方法做到这件事，否则你的\(A\)就太弱了，需要改成一个永真公式
例如，使用待定公式法时，设\(P\rightarrow(R\rightarrow Q)\)，想得到\(P\rightarrow Q\)，这时\(R\)通常必须是永真的
-
简言之，如果\(A\prec B\)，那么你既不能借助\(A\)推演出\(B\)，也不能借助\(R\rightarrow(A\rightarrow B)\)推演出\(R\rightarrow B\)。这种情况下，你应该加强\(A\)，使得\(A\succcurlyeq B\)