命题逻辑（蕴涵）
MP
规则1（MP）：
↗#1 对任意公式 $A,B$ ，$A \imp B \mand A \mimp B$ 。
#2 对任意公式 $A_1,A_2,\cdots,A_n,B$ ，$A_1 \imp A_2 \imp \cdots \imp A_n \imp B \mand A_1 \mand A_2 \mand \dots \mand A_n \mimp B$ 。
↗#1 对任意公式 $A,B$ ，$A \imp B \mand A \mimp B$ 。
#2 对任意公式 $A_1,A_2,\cdots,A_n,B$ ，$A_1 \imp A_2 \imp \cdots \imp A_n \imp B \mand A_1 \mand A_2 \mand \dots \mand A_n \mimp B$ 。
注：为了表述方便，该规则一般在引用其他定理的时候默认使用。
〔证明规则1〕
#1：即分离规则MP。
#2：连续使用MP可得：
$A_1 \imp A_2 \imp A_3 \imp \cdots \imp A_n \imp B \mand A_1 \mand A_2 \mand A_3 \mand \dots \mand A_n $
$\mimp A_2 \imp A_3 \imp \cdots \imp A_n \imp B \mand A_2 \mand A_3 \mand \dots \mand A_n$
$\mimp A_3 \imp \cdots \imp A_n \imp B \mand A_3 \mand \dots \mand A_n$
$\vdots$
$\mimp A_n \imp B \mand A_n$
$\mimp B$ 。〔规则1证毕〕
#1：即分离规则MP。
#2：连续使用MP可得：
$A_1 \imp A_2 \imp A_3 \imp \cdots \imp A_n \imp B \mand A_1 \mand A_2 \mand A_3 \mand \dots \mand A_n $
$\mimp A_2 \imp A_3 \imp \cdots \imp A_n \imp B \mand A_2 \mand A_3 \mand \dots \mand A_n$
$\mimp A_3 \imp \cdots \imp A_n \imp B \mand A_3 \mand \dots \mand A_n$
$\vdots$
$\mimp A_n \imp B \mand A_n$
$\mimp B$ 。〔规则1证毕〕
$\imp$ 左引入
↗定理1（ $\imp$ 左引入）：对任意公式 $A,B$ ，$A \imp (B \imp A)$ 。
$\imp$ 对 $\imp$ 左插入
↗定理2（ $\imp$ 对 $\imp$ 左插入）：对任意公式 $A,B$ ，$(A \imp (B \imp C)) \imp ((A \imp B) \imp (A \imp C))$ 。
同一律
↗定理3（同一律）：对任意公式 $A$ ，$A \imp A$ 。
〔证明定理3〕
〔定理3证毕〕
$$\begin{aligned}
\s{1} A \imp ((A \imp A) \imp A) &&([\href{#ili}{\text{\text{$\imp$}左引入}}])\\
\s{2} (A \imp (A \imp A)) \imp (A \imp A) &&([\href{#iils}{\text{\text{$\imp$}对\text{$\imp$}左插入}}]1)\\
\s{3} A \imp (A \imp A) &&([\href{#ili}{\text{\text{$\imp$}左引入}}])\\
\s{4} A \imp A &&([2]3)
\end{aligned}$$
$\imp$ 对 $\imp$ 左引入
↗定理4（ $\imp$ 对 $\imp$ 左引入）：对任意公式 $A,B,C$ ，$(B \imp C) \imp ((A \imp B) \imp (A \imp C))$ 。
〔证明定理4〕
〔定理4证毕〕
$$\begin{aligned}
\s{1} (A \imp (B \imp C)) \imp ((A \imp B) \imp (A \imp C)) &&([\href{#iils}{\text{\text{$\imp$}对\text{$\imp$}左插入}}])\\
\s{2} (B \imp C) \imp ((A \imp (B \imp C)) \imp ((A \imp B) \imp (A \imp C))) &&([\href{#ili}{\text{\text{$\imp$}左引入}}]1)\\
\s{3} ((B \imp C) \imp (A \imp (B \imp C))) \imp ((B \imp C) \imp ((A \imp B) \imp (A \imp C))) &&([\href{#iili}{\text{\text{$\imp$}对\text{$\imp$}左引入}}]2)\\
\s{4} (B \imp C) \imp (A \imp (B \imp C)) &&([\href{#ili}{\text{\text{$\imp$}左引入}}])\\
\s{5} (B \imp C) \imp ((A \imp B) \imp (A \imp C)) &&([3]4)
\end{aligned}$$
$\imp$ 对 $\imp$ 左置换
↗定理5（ $\imp$ 对 $\imp$ 左置换）：对任意公式 $A,B,C$ ，$(A \imp (B \imp C)) \imp (B \imp (A \imp C))$ 。
〔证明定理5〕
〔定理5证毕〕
$$\begin{aligned}
\s{1} (A \imp (B \imp C)) \imp ((A \imp B) \imp (A \imp C)) &&([\href{#iils}{\text{\text{$\imp$}对\text{$\imp$}左插入}}])\\
\s{2} ((A \imp (B \imp C)) \imp (A \imp B)) \imp ((A \imp (B \imp C)) \imp (A \imp C)) &&([\href{#iils}{\text{\text{$\imp$}对\text{$\imp$}左插入}}]1)\\
\s{3} ((A \imp B) \imp ((A \imp (B \imp C)) \imp (A \imp B))) \\
& \imp ((A \imp B) \imp ((A \imp (B \imp C)) \imp (A \imp C))) &&([\href{#iili}{\text{\text{$\imp$}对\text{$\imp$}左引入}}]2)\\
\s{4} (A \imp B) \imp ((A \imp (B \imp C)) \imp (A \imp B)) &&([\href{#ili}{\text{\text{$\imp$}左引入}}])\\
\s{5} (A \imp B) \imp ((A \imp (B \imp C)) \imp (A \imp C)) &&([3]4)\\
\s{6} (B \imp (A \imp B)) \imp (B \imp ((A \imp (B \imp C)) \imp (A \imp C))) &&([\href{#iili}{\text{\text{$\imp$}对\text{$\imp$}左引入}}]5)\\
\s{7} B \imp (A \imp B) &&([\href{#ili}{\text{\text{$\imp$}左引入}}])\\
\s{8} B \imp ((A \imp (B \imp C)) \imp (A \imp C)) &&([6]7)\\
\s{9} (B \imp (A \imp (B \imp C))) \imp (B \imp (A \imp C)) &&([\href{#iils}{\text{\text{$\imp$}对\text{$\imp$}左插入}}]8)\\
\s{10} ((A \imp (B \imp C)) \imp (B \imp (A \imp (B \imp C)))) \\
& \imp ((A \imp (B \imp C)) \imp (B \imp (A \imp C))) &&([\href{#iili}{\text{\text{$\imp$}对\text{$\imp$}左引入}}]9)\\
\s{11} (A \imp (B \imp C)) \imp (B \imp (A \imp (B \imp C))) &&([\href{#ili}{\text{\text{$\imp$}左引入}}])\\
\s{12} (A \imp (B \imp C)) \imp (B \imp (A \imp C)) &&([10]11)
\end{aligned}$$
$\imp$ 对 $\imp$ 右逆引入
↗定理6（ $\imp$ 对 $\imp$ 右逆引入）：对任意公式 $A,B,C$ ，$(A \imp B) \imp ((B \imp C) \imp (A \imp C))$ 。
〔证明定理6〕
〔定理6证毕〕
$$\begin{aligned}
\s{1} (B \imp C) \imp ((A \imp B) \imp (A \imp C)) &&([\href{#iili}{\text{\text{$\imp$}对\text{$\imp$}左引入}}])\\
\s{2} (A \imp B) \imp ((B \imp C) \imp (A \imp C)) &&([\href{#iilp}{\text{\text{$\imp$}对\text{$\imp$}左置换}}]1)
\end{aligned}$$
$\imp$ 传递
规则2（ $\imp$ 传递）：
↗#1 对任意公式 $A,B,C$ ，$A \imp B \mand B \imp C \mimp A \imp C$ 。
#2 对任意公式 $A_1,A_2,\cdots,A_n$ ，$A_1 \imp A_2 \mand A_2 \imp A_3 \mand \cdots \mand A_{n-1} \imp A_n \mimp A_1 \imp A_n$ 。
↗#1 对任意公式 $A,B,C$ ，$A \imp B \mand B \imp C \mimp A \imp C$ 。
#2 对任意公式 $A_1,A_2,\cdots,A_n$ ，$A_1 \imp A_2 \mand A_2 \imp A_3 \mand \cdots \mand A_{n-1} \imp A_n \mimp A_1 \imp A_n$ 。
〔证明 $\imp$ 传递〕
#1：
#2：连续使用#1可得：
$A_1 \imp A_2 \mand A_2 \imp A_3 \mand A_3 \imp A_4 \mand \cdots \mand A_{n-1} \imp A_n $
$\mimp A_1 \imp A_3 \mand A_3 \imp A_4 \mand \cdots \mand A_{n-1} \imp A_n $
$\mimp A_1 \imp A_4 \mand \cdots \mand A_{n-1} \imp A_n $
$\vdots$
$\mimp A_1 \imp A_{n-1} \mand A_{n-1} \imp A_n$
$\mimp A_1 \imp A_n$ 。〔 $\imp$ 传递证毕〕
#1：
$$\begin{aligned}
\s{1} A \imp B &&(\text{前提})\\
\s{2} B \imp C &&(\text{前提})\\
\s{3} A \imp C &&([\href{#iirvi}{\text{\text{$\imp$}对\text{$\imp$}右逆引入}}]1,2)
\end{aligned}$$
$A_1 \imp A_2 \mand A_2 \imp A_3 \mand A_3 \imp A_4 \mand \cdots \mand A_{n-1} \imp A_n $
$\mimp A_1 \imp A_3 \mand A_3 \imp A_4 \mand \cdots \mand A_{n-1} \imp A_n $
$\mimp A_1 \imp A_4 \mand \cdots \mand A_{n-1} \imp A_n $
$\vdots$
$\mimp A_1 \imp A_{n-1} \mand A_{n-1} \imp A_n$
$\mimp A_1 \imp A_n$ 。〔 $\imp$ 传递证毕〕
凡可说的都可被清楚的说，凡不可说的则应当保持沉默。― Ludwigittgenstein, 《逻辑哲学论》