以下的證明會分成使用（A3）的部分跟將公理（A3）取代為（T1）的部分，用以證明兩者的等價性。

（DNe） Double negation, elimination —
$\vdash \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}$

More information （1）

...

證明（使用A3）
（1） $(\neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}})\Rightarrow [(\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {A}})\Rightarrow {\mathcal {A}}]$ （A3）（2） $\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {A}}$ （I）（3） $(\neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}})\Rightarrow {\mathcal {A}}$ （D2 with 1, 2）（4） $\neg \neg {\mathcal {A}}\Rightarrow (\neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}})$ （A1）（5） $\neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}$ （D1 with 3, 4）

Close

More information （1）

...

證明（使用T1）
（1） $\neg \neg {\mathcal {A}}\Rightarrow (\neg \neg \neg \neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}})$ （A1）（2） $\neg \neg {\mathcal {A}}$ （Hyp）（3） $\neg \neg \neg \neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}$ （MP with 2, 1）（4） $\neg {\mathcal {A}}\Rightarrow \neg \neg \neg {\mathcal {A}}$ （MP with 3, T1）（5） $\neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}$ （MP with 4, T1）（6） ${\mathcal {A}}$ （MP with 2, 5）

Close

（DNi） Double negation, introduction —
$\vdash {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}$

More information （1）

...

證明（使用A3）
（1） $(\neg \neg \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {A}})\Rightarrow [(\neg \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}})\Rightarrow \neg \neg {\mathcal {A}}]$ （A3）（2） $(\neg \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}})\Rightarrow \neg \neg {\mathcal {A}}$ （MP with DNe, 1）（3） ${\mathcal {A}}\Rightarrow (\neg \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}})$ （A1）（4） ${\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}$ （D1 with 2,3）

Close

More information （1）

...

證明（使用T1）
（1） $\neg \neg \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {A}}$ （DNe）（2） ${\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}$ （MP with 1, T1）

Close

上面兩定理表達了雙否定推理上等價於於原公式，參照兩者任一會都以（DN）簡寫。

（T1） Transposition-1 —
$\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}\vdash {\mathcal {B}}\Rightarrow {\mathcal {A}}$

More information （1）

...

證明（使用A3）
（1） $(\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}})\Rightarrow [(\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {A}}]$ （A3）（2） $\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}$ （Hyp）（3） $(\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {A}}$ （MP with 1, 2）（4） ${\mathcal {B}}\Rightarrow (\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})$ （A1）（5） ${\mathcal {B}}\Rightarrow {\mathcal {A}}$ （D1 with 3, 4）

Close

（T2） Transposition-2 —
${\mathcal {B}}\Rightarrow {\mathcal {A}}\vdash \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}$

More information （1）

...

證明（使用T1）
（1） $\neg \neg {\mathcal {B}}\Rightarrow {\mathcal {B}}$ （DN）（2） ${\mathcal {B}}\Rightarrow {\mathcal {A}}$ （Hyp）（3） $\neg \neg {\mathcal {B}}\Rightarrow {\mathcal {A}}$ （D with 1, 2）（4） ${\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}$ （DN）（5） $\neg \neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}}$ （D1 with 3,4）（6） $(\neg \neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}})\Rightarrow (\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}})$ （T1, D）（7） $\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}$ （MP with 5, 6）

Close

注意到（T2）的證明參照了（T1）+（DN），但之前已經證明了（A1）+（A2）+（A3）可以推出（T1）；還有（A1）+（A2）+（T1）也可以推出（DN），所以註明使用（T1）即可。

以上二定理說明 ${\mathcal {B}}\Rightarrow {\mathcal {A}}$ 推理上等價於 $\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}$ ，參照這兩個定理中任一都以（T）表示。

至此，已經可以證明（A1）+（A2）+（T1）可以推出（A3）：

More information

, （1） ...

（T1）可推出（A3）的證明
由MP律顯然有 $\neg {\mathcal {B}},\,(\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\vdash {\mathcal {B}}$ （1） $\neg {\mathcal {B}}\Rightarrow [\,(\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}\,]$ （對上面的定理使用兩次演繹元定理）（2） $\neg {\mathcal {B}}\Rightarrow [\,\neg {\mathcal {B}}\Rightarrow \neg (\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\,]$ （D1 with 1, T2）（3） $(\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {B}})\Rightarrow [\,\neg {\mathcal {B}}\Rightarrow \neg (\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\,]$ （MP with A2, 2）（4） $\neg {\mathcal {B}}\Rightarrow \neg (\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})$ （MP with I, 3）（5） $(\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}$ （MP with T1, 4）（6） $(\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {C}})$ （Hyp）（7） $\neg {\mathcal {B}}\Rightarrow {\mathcal {C}}$ （Hyp）（8） $\neg {\mathcal {C}}\Rightarrow \neg \neg {\mathcal {B}}$ （MP with T2, 7）（9） $\neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {B}}$ （D1 with 6, 8）（10） $\neg {\mathcal {B}}\Rightarrow {\mathcal {B}}$ （D1 with DN, 9）（11） ${\mathcal {B}}$ （MP with 5, 10）

Close

所以綜合以上所述，在有（A1）+（A2）的前提下，公理（T1）等價於公理（A3）。

由（T）可以得到類似於公理（A3）的定理

（A3'） —
${\mathcal {A}}\Rightarrow {\mathcal {B}},\neg {\mathcal {A}}\Rightarrow {\mathcal {B}}\vdash {\mathcal {B}}$

More information （1）

...

證明
（1） $(\neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}})\Rightarrow [(\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow {\mathcal {B}}]$ （A3）（2） $(\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow (\neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}})$ （T, D）（3） $\neg {\mathcal {A}}\Rightarrow {\mathcal {B}}$ （Hyp）（4） $\neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}}$ （MP with 2, 3）（5） $(\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow {\mathcal {B}}$ （MP with 1, 4）（6） $({\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow (\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})$ （T, D）（7） ${\mathcal {A}}\Rightarrow {\mathcal {B}}$ （Hyp）（8） $\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}}$ （MP with 6, 7）（9） ${\mathcal {B}}$ （MP with 5, 8）

Close