二重否定除去と矛盾の公理の関係に関する一考察
中原

陽

三

A Study on the Relationship between the two Axioms;
the Double Negative Eliminationand the Principle of Explosion
Yozo NAKAHARA
Keywords:

Minimal logic，Double negative elimination，Principle of explosion，Law of excluded middle，Peirce's law，Classical logic，Intuitionistic logic，
NK，NJ

1

はじめに
本稿では、二重否定の除去の公理、矛盾の公理の関係を中心に、排中律、Peirceの法則、古典論理、直観主義論理まで含めて、これらの知られている関係を再精査し、最小論理の観点から統一的に関係を整理する。また、これらの関係に関して、一つの定理を除いたすべてに詳細な証明を付して、これらの関係の詳細を明示する。
構成としては、まず、二重否定の除去の公理、矛盾の公理、排中律、および、Peirceの法則に関する、最小論理からの視点を明確にした６つの定理を挙げ、５つについてはできるだけ詳しい証明を付け、証明を付けなかった１つについては、証明が得られる文献を明示する。さらに、これらの定理から、二重否定の除去の公理、矛盾の公理、排中律、Peirceの法則、古典論理、直観主義論理に関してこれまで知られている関係を得られることを示す。

2準備・記法
本稿では、矛盾命題を表す命題定数を定義 1という記号で示す。

最小論理［ 1 ］（p.56），［ 2 ］をML（minimal logicの略）で表す。さらに、「∀ 論理式 A，（あるいは （矛盾）に関する公理［ 1 ］（p.59））をPE（principle→ A」という内容の矛盾の公理［ 3 ］
of explosionの略）で表し、「∀ 論理式 A，￢￢ A → A」という内容の二重否定の除去の公理［ 3 ］（あるいは二重否定の除去の法則［ 1 ］（p.57））をDNE（double negative eliminationの略）で表し、「∀ 論理式 A，B，（（A→ B） → A） → A」という内容のPeirceの公理［ 3 ］（あるいはPeirceの法則「∀ 論理式 A，B，A ∨￢ A」という内容の排中律［ 1 ］（p.56）,［ 4 ］［1］（p.72）），をPeirceで表し、（VI.論理の形式化）をLEM（law of excluded middleの略）で表す。

－ 211 －

さらにまた、これらを組み合わせた論理体系を、それぞれ、ML ＋ PE、ML ＋ PE ＋ DNEなどで表す。
定義 2

任意の論理式の集合Γ=｛A1，A2，A3,・・・｝、任意の論理式 A 、任意の論理体系 Lに対し、
Γ ├L A（VI.論理の形式を、L において A がΓから証明可能（演繹可能）であることと定義し［ 5 ］,［ 4 ］化）、ΓをΓ├L A の前提、A をΓ ├L A の結論と呼ぶ。また、├L A が成立する時、 A を L のTheorem、任意の論理式 A、任意の論理体系と呼ぶ。同様に、任意の論理式の集合Γ=｛A1，A2，A3,・・・｝

Lに対し、
ΓL

A

を、L において A がΓから証明不可能（演繹不可能）であることと定義し［ 6 ］、ΓをΓ
前提、A をΓ
注意 1

LL

A のA の結論と呼ぶ。

定義 2 は、Γがない場合を含めての定義である。すなわち、可能（演繹可能）であることを意味する。同様に、

LL

A は、L において A が証明

A は、L において A が証明不可能（演繹不可能）であることを意味する。
定義 3

任意の論理体系L1，L2に対し、L1=L2で、L1とL2の論理体系が等しい（証明できるTheoremが等しい）ことを表す。
注意 2

古典論理のゲンツェンによる体系 NK は、NK = ML + PE + LEM を満たし、直観主義論理（p.60）,［ 4 ］（VII.自然演繹（その体系 NJ は、NJ = ML + PE を満たすことが知られている［ 1 ］の１））。
また、NJ ではPeirceの法則を証明できないが、古典論理では証明できることも知られている［ 7 ］。

3６つの定理とその証明
本節では、定理 1 ～６を挙げ、定理 2 以外に対してできるだけ詳しい証明を付ける（定理 2 の証

明は［ 1 ］に詳しい）。
なお、定理 1 の証明は、［ 1 ］の証明をまとめた。定理 3 、補題 1 、補題 2 、補題 3 、および、その証明は独自に与えた。定理 4 、補題 4 、補題 5 、および、その証明も、独自に与えたものである
が、定理 4 の証明は、考えているときに［ 8 ］も見て参考にした。ただし、同じ方針となっているか未確認である。定理 5 、定理 6 は、［ 1 ］を参考に独自に与えたものであるが、証明は［ 1 ］とほぼ同様にまとめた。
定理 1任意の論理式 A に対して├ML（（￢￢ A → A） → （→ A））

が成立する。すなわち、任意の論理式 A に対し、最小論理の推論規則のみを用いて（￢￢ A → A）→（→ A）を証明できる。

－ 212 －

二重否定除去と矛盾の公理の関係に関する一考察
注意 3

定理 1 より、最小論理において、二重否定除去の公理から矛盾の公理を導けることがわかる。
このことから、あるいは定理 1 から直接、

ML + DNE = ML + DNE + PE

が成立することがわかる。
ＰＲＯＯＦ（定理 1 ）．
［ 1 ］のp.58～p.59をまとめると、次の証明図を得る；

q.e.d.
定理 2最小論理の範囲で、矛盾の公理から二重否定除去の公理を導くことはできない［ 1 ］。よって、最小論理の推論規則だけで「任意の論理式 A において（→ A）→（￢￢ A → A）」を証明できない。すなわち、∃ 論理式 A,ML→ A）→（￢￢ A → A））（（が成立する。
定理 3

任意の論理式 A に対して├ML（（（ A →）→ A）→ A）→（（→ A）→（￢￢A → A））

が成立する。
注意 4（

定理 3 より、最小論理の推論規則とPeirceの法則を用いて、「任意の論理式 A に対して、→ A）→（￢￢ A → A）を証明できる」ことがわかる。よって、最小論理とPeirceの法則の範囲で、矛盾の公理から二重否定除去の公理が導けることがわかる。
このことからML + Peirce + PE = ML + Peirce + PE + DNE



が成立することがわかる。従って、より、

ML + Peirce + PE = ML + Peirce + DNEが成立する。

－ 213 －



ＰＲＯＯＦ（定理 3 ）．



ただし、X =（（（ A →）→ A）→ A）→（（￢ A → A）→ A）とする。

X が成立すること（├ML X が成立すること）は、以下の補題 1 ， 2 ， 3 より得られるが、その概略は以下のとおり；
補題 2 は補題 1 より得られる。この補題 2 の式における A、B、C、D をそれぞれ A－、￢ A、A、Aと置き換えて得られる式と、補題 3 の式に対して、「→－除去」を行う。
q.e.d.
注意 5定理 1 の上記証明では、├ML X が必要であり、そのために補題 1 から 3 を用意した。ただし、├ML X とは少し違う├ML（（（A →）→ A）→ A）→（（￢A → A）→ ￢￢A）

は、すぐに示せる。以下にその証明図を付しておく；


補題 1

任意の論理式 A、B、C に対して、├ML（（（A → B）∧（B → A））→（（（A → C）→（B → C））∧（（B → C）→（A → C））））が成立する。

－ 214 －二重否定除去と矛盾の公理の関係に関する一考察
ＰＲＯＯＦ（補題 1 ）．
下記証明図が得られる；


ただし、X2は、下記の証明図を表すものとする；

q.e.d.
なお、上記証明において、X2は、証明図全体を記載する十分なスペースがないために導入したにすぎない。ちなみに証明図全体は以下のようになる（元原稿では、少し縮小した図となっている）
；

注意 6

通常の数学で用いられている古典論理の範囲で、補題 1 の式における├ML の結論（├MLより右の部分）は、意味的にはほぼ明らかであるし、トートロジー（tautology）であることを真理表から厳密に確認することもできる。さらに、トートロジーであることから、古典論理の完全性より、古典論理の範囲で証明できることもわかる。ただし、補題 1 で主張しているのは、古典論理の範囲ではなく、最小論理の範囲で式における├ML の結論を証明できることである。

－ 215 －

補題 1 を 2 度使うことで、次の補題 2 が得られる。
補題 2

任意の論理式 A、B、C、D に対して、├ML（（（A → B）∧（B → A））→（（（（A → C）→ D）→（（B → C）→ D））∧（（（B → C）→ D）→（（A → C）→ D））））
が成立する。
言い換えると、最小論理の推論規則のみを用いて、「任意の論理式 A，B，C，D において、式における├ML の結論（すなわち、（（A → B）∧（B → A））→（（（（A → C）→ D）→（（B → C）→ D））∧（（（B → C）→ D）→（（A → C）→ D））））」を証明できる。
ＰＲＯＯＦ（補題 2 ）．証明図のA，B，Cをそれぞれ次のように置き換える；

A ←（A → B）
B ←（B → C）

C ← Dすると、成立する証明図を得る（証明図の A，B，C をそれぞれどのような論理式に置き換えても、得られる証明図は成立するためである）が、これを、その証明図に含まれるブロックY3、Y4、Y5を用いて以下のように表記する；

Y3→ －導入 1
Y4 → Y5

ただし、

Y3＝得られる証明図のうち、結論行（最後の行）のすぐ上の横棒線より上の部分
Y4＝（（（A → C）→（B → C））∧（（B → C）→（A → C）））



Y5＝（（（（A → C）→ D）→（（B → C）→ D））∧（（（B → C）→ D）→（（A → C）→ D）））である。
また、補題 1 の証明図を、この証明図に含まれるブロックY1、Y2、Y4を用いて以下のように表記する；

Y1→ －導入 1Y2 → Y4



ただし、

Y1＝証明図のうち、結論行（最後の行）のすぐ上の横棒線より上の部分
Y2＝（A → B）∧（B → A）



Y4＝式のY4である。
成立する証明図、より、以下の証明図が成立する。ただし、図中の仮定番号 2 は、式、が表す元の証明図の中に現れたものとは関係ないものとする；－ 216 －

二重否定除去と矛盾の公理の関係に関する一考察
q.e.d.
補題 3

任意の論理式 A に対して、├ML（（（A →）→￢ A）∧（￢ A →（A →）））

が成立する。
ＰＲＯＯＦ（補題 3 ）．



q.e.d.
定理 4

任意の論理式 A、B に対して、├ML（（A ∨￢ A）→（（￢￢B → B）→（（（A → B）→ A）→ A）））

が成立する。
注意 7

定理 4 よりML ＋ DNE ＋ LEM = ML ＋ DNE ＋ LEM ＋ Peirceが成立することがわかる。
定理 4 の証明のため、まず、以下の補題 4 、補題 5 を証明する；
補題 4

任意の論理式 A、B に対して、├ML（￢ A →（（￢￢ B → B）→（（（A → B）→ A）→ A）））

が成立する。
ＰＲＯＯＦ（補題 4 ）．

Y6、Y7を以下のように置く；
1￢A→ － 導入
Y6 ＝
￢ B → ￢ A



－ 217 －

Y6、Y7より次の証明図が得られる；

q.e.d.
補題 5

任意の論理式 A、B に対して、├ML（A →（（￢￢B → B）→（（（A → B）→ A）→ A）））

が成立する。
ＰＲＯＯＦ（補題 5 ）．

q.e.d.
ＰＲＯＯＦ（定理 4 ）．補題 4 の証明図（一つにまとめたもの）をY8、補題 5 の証明図をY9と置く。

Y8、Y9より、以下の証明図が得られる；

q.e.d.
定理 5

任意の論理式 A に対して、├ML（（A ∨￢ A）→（（→ A）→（￢￢A → A）））

が成立する。
注意 8

定理 5 よりML ＋ PE ＋ LEM ＝ ML ＋ PE ＋ LEM ＋ DNEが成立することがわかる。
ＰＲＯＯＦ（定理 5 ）．
［ 1 ］（p.57））と同じ方針による完全な証明を以下に与える；
まず、Y10、Y11を次のように置く；－ 218 －



二重否定除去と矛盾の公理の関係に関する一考察

Y10、Y11より、以下の証明図が得られる；

q.e.d.
定理 6

任意の論理式 A に対して、├ML（（￢￢（A ∨￢A）→（A ∨￢A））→（A ∨￢A））

ML ＋ DNE ＝ ML ＋ DNE ＋ LEM

が成立する。
注意 9

定理 6 よりが成立することがわかる。
ＰＲＯＯＦ（定理 6 ）．
［ 1 ］（p.58））と同じ方針による完全な証明を以下に与える；

q.e.d.

－ 219 －

4

既知の関係の導出
本節では、二重否定の除去の公理、矛盾の公理、排中律、Peirceの法則、古典論理、および、直観主義論理に関する既知の関係が、前節で挙げた６つの定理から定理 8 として導出されることを示す。
定理 7

前節の定理から、それぞれ次のような関係式が得られる；

定理 2 から、

ML ＋ PE ≠ ML ＋ PE ＋ DNE

が得られる。
定理 1 から、注意 3 の式が得られる。
定理 3 から、注意 4 の式が得られる。
定理 4 から、注意 7 の式が得られる。
定理 5 から、注意 8 の式が得られる。
定理 6 から、注意 9 の式が得られる。
ＰＲＯＯＦ（定理 7 ）ほぼ明らかである。
q.e.d.
定理 8以下の関係式が成立する；

NK ＝ ML＋ DNE

＝ ML ＋ PE ＋ DNE

＝ ML ＋ PE ＋ LEM

＝ ML ＋ PE ＋ Peirce＝ ML ＋ PE ＋ DNE ＋ LEM ＋ Peirce＝MJ＋ DNE

＝MJ＋ LEM＝MJ＋ Peirce＝MJ＋ DNE ＋ LEM ＋ Peirce＋ PE≠ MLＰＲＯＯＦ（定理 8 ）定理 7 で得られた関係式および注意 2 に示した２つの関係式より得られるが、詳細は以下のとおり；
まず、定理 7 で得られた関係式のうち、式、、、、から以下の関係式が成立する。

－ 220 －

二重否定除去と矛盾の公理の関係に関する一考察

ML ＋ DNE ＋ LEM＝ML ＋ PE＋ LEM ＋ DNE＝ML ＋ DNE＋ PE（by）

（by）




＝ML ＋ DNE （by）＝ML ＋ DNE＋ LEM （by）＝ML ＋ DNE＋ LEM ＋Peirce（by）＝ML ＋ DNE＋ LEM ＋Peirce＋PE（by）

（by）

＝ML ＋ Peirce ＋ PE＋DNE＝ML ＋ Peirce ＋ PE （by）

これらと、注意 2 に示した２つの関係式

NK ＝ML ＋ PE＋ LEM

NJ ＝ML ＋ PE

より、定理 8 の最後の式以外が成立する。最後の式は、定理 7 の式と上記式から成立する。
q.e.d.

5

あとがき
本稿では、二重否定の除去の公理、矛盾の公理の関係を中心に、排中律、Peirceの法則、古典論理、直観主義論理まで含めて、これらの知られている関係を再精査し、最小論理の観点から統一的に関係を整理した。また、これらの関係に関して、一つの定理を除いたすべてに詳細な証明を付して、これらの関係の詳細を明示した。
構成としては、まず、二重否定の除去の公理、矛盾の公理、排中律、および、Peirceの法則に関する、最小論理からの視点を明確にした６つの定理を挙げ、５つについてはできるだけ詳しい証明を付け、証明を付けなかった１つについては、証明が得られる文献を明示した。さらに、これらの定理から、二重否定の除去の公理、矛盾の公理、排中律、Peirceの法則、古典論理、直観主義論理に関してこれまで知られている関係を得られることを示した。

参考文献［ 1 ］前原昭二．記号論理入門（日評数学選書）.日本評論社，第１版第４刷， 8 1970.

［ 2 ］基礎現代文化学 基礎演習１論理学 第 4 回 担当 矢田部俊介，（URLの最終確認は2009.10.28）．
http://staff.aist.go.jp/shunsuke.yatabe/kyoto_04_090512.pdf.

．数理解析［ 3 ］廣川佐千男，亀山幸義，馬場謙介.λc計算とλp計算との対応（計算理論とその応用）研究所講究録，Vol.992，pp.167.174，19970500.

－ 221 －

［ 4 ］高崎金久．Introduction to mathematical logic，（URLの最終確認は2009.10.28）．
http://www.math.h.kyoto-u.ac.jp/.~takasaki/edu/logic/index.html#lectures.

［ 5 ］村井哲也，深海悟.様相論理.日本ファジィ学会誌，Vol.7，No.1，pp.3-18，19950215.

［ 6 ］Yuichi Komori. Syntactical investigations into bi logic and bb’
i logic．Studia Logica，
Vol.53，No.3，pp.397-416，1994.

［ 7 ］古 森 雄 一 . 部 分 構 造 論 理（ 特 に ，b c k 論 理 ）へ の 招 待 ，（ U R L の 最 終 確 認 は 2 0 0 9 . 1 0 . 2 8 ）．
http://www.math.s.chiba-u.ac.jp/~komori/jyugyou/suuriron.pdf.

［ 8 ］y a o . パ ー ス の 法 則 の 証 明（ y a h o o ! j a p a n 知 恵 袋 ），（ U R L の 最 終 確 認 は 2 0 0 9 . 1 0 . 3 0 ）．
http://detail.chiebukuro.yahoo.co.jp/qa/question_detail/q1110663361.

－ 222 －