公理集合

共三条公理，或者说「公理模式」：

公理 1：加前件

$$ A\to(B\to A) $$

公理 2：拆后件

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

公理 3：逆否（1）

$$ (\neg A\to\neg B)\to(B\to A) $$

推理规则

分离规则

$$ r_{mp}: \frac{A, A\to B}{B} $$

或者写成公式串的形式：

$$ A, A\to B, B $$

基本定理

定理 1：反身

一个命题公式是蕴含它自己的。

$$ \vdash_{PC}A\to A $$

• 证明

定理 2：前件互换（演绎形式）