思维顺序

思维过程是证明过程的逆序，即“要证……只需证……”

先从下往上写出思维过程，再从上到下写出证明过程。

常用公理/定理

公理1：砍头

$A_1:A\to(B\to A)$

“砍头”公理：要证 $B\to A$，只需证 $A$。

运用条件：前后件没有关系，或者后件本身就是永真式

公理2：提前件

$A_2:(A\to(B\to C))\to((A\to B)\to (A\to C))$

“共享前件”公理：可以将共同的前件提取出来

运用条件：需要证明的式子的前后件有共同的前件，那么可以将前件提出来；如果是有共同的后件，可以对每个部分取逆得到共享前件的式子，再使用 $A_2$

定理1：反身

$T_1:\quad\vdash A\to A$

定理2-3：前件互换

$T_2:\quad if \vdash A\to (B\to C), then \vdash B\to (A\to C)$

$T_3:\quad \vdash (A\to (B\to C))\to (B\to (A\to C))$

作用：调换两部分的位置

运用条件：形如$A\to(B\to C)$都行