数学の基礎

　本節では、直観主義論理で（したがって古典論理でも）一般的に成り立つ定理を、自然推論で証明してみましょう。

メタ定理７

P とそれ自身は同値。特に P Þ P は定理。

　P と仮定すれば、( 仮 定 ) により P である。よって ( Þ 導入) により P Þ P である。

メタ定理８

Ø^ は定理。

　メタ定理７で P を ^ とすれば ^ Þ ^ が得られるが、これは Ø^ に他ならない。

メタ定理９

Q が定理なら P Þ Q は定理。

　P と仮定すると、( 増 ) により Q はこの仮定のもとでも定理である。よって ( Þ 導入) により P Þ Q である。

メタ定理10

P が定理なら Q と P Þ Q は同値。

　Q から P Þ Q はメタ定理９。逆は ( Þ 消去) による。

メタ定理11

P が定理なら ^ と ØP は同値。特に ^ と ØØ^ は同値。

　メタ定理10で Q を ^ とすればよい。後半は、これとメタ定理８により明らか。

メタ定理12

^ Þ P は定理。

　^ を仮定すると、( ^ 消去) により P が得られるので、( Þ 導入) により ^ Þ P が導かれる。

メタ定理13

P Þ Q と Q Þ R が定理なら P Þ R は定理。

　P と仮定すると、P Þ Q と ( Þ 消去) により Q が得られ、Q Þ R なので再度 ( Þ 消去) により R が得られる。よって ( Þ 導入) により P Þ R が得られる。

メタ定理14

ØP が定理なら P Þ Q は定理。

　仮定により P Þ ^ が定理で、メタ定理12により ^ Þ Q も定理なので、メタ定理13により結論が得られる。

メタ定理15

(ØP) Ú Q が定理なら P Þ Q は定理。

　ØP のときはメタ定理14により、Q のときはメタ定理９により P Þ Q が得られるので、いずれにせよ（つまり ( Ú 消去) により）結論が得られる。

メタ定理16

P Þ Q が定理なら (Q Þ R) Þ (P Þ R) は定理。

　Q Þ R と仮定すると、メタ定理13により P Þ R である。よって ( Þ 導入) により (Q Þ R) Þ (P Þ R) が得られる。

メタ定理17

P Þ Q が定理なら (ØQ) Þ (ØP) は定理。

　メタ定理16で R を ^ とすればよい。なお、(ØQ) Þ (ØP) を P Þ Q の対偶といいます。

メタ定理18

P Þ {(P Þ Q) Þ Q} は定理。

　P と仮定する。P Þ Q と仮定すると ( Þ 消去) により Q が得られるので、( Þ 導入) により (P Þ Q) Þ Q が得られる。ゆえに ( Þ 導入) により P Þ {(P Þ Q) Þ Q} が得られる。

メタ定理19

P Þ ØØP は定理。

　メタ定理18で Q を ^ とすればよい。

メタ定理20

ØP と ØØØP は同値。

　メタ定理19で P に ØP を代入すれば ØP Þ ØØØP が得られ、メタ定理19の対偶をとれば ØØØP Þ ØP が得られる。

メタ定理21

P と P Ù P と P Ú P はすべて同値。

　P Ú P と仮定する。P のときは P である。よっていずれにせよ P である。
　次に P と仮定すると、( Ù 導入) により P Ù P である。
　最後に P Ù P と仮定すると、( Ù 消去) により P だから、( Ú 導入) により P Ú P である。

メタ定理22	(a)　P Ù Q と Q Ù P は同値。
	(b)　P Ú Q と Q Ú P は同値。

(a)　P Ù Q と仮定すると、( Ù 消去) により P であり、Q でもある。よって ( Ù 導入) により Q Ù P である（逆も同じ）。

(b)　P Ú Q と仮定する。P の場合も Q の場合も、いずれも ( Ú 導入) により Q Ú P であるから、いずれにせよ Q Ú P が成り立つ（逆も同じ）。

メタ定理23	(a)　(P Ù Q) Ù R と P Ù (Q Ù R) は同値。
	(b)　(P Ú Q) Ú R と P Ú (Q Ú R) は同値。

(a)　(P Ù Q) Ù R と仮定すると、( Ù 消去) により P Ù Q および R が得られ、再度 ( Ù 消去) により P と Q が成り立つ。よって ( Ù 導入) により Q Ù R が、従って再度 ( Ù 導入) により P Ù (Q Ù R) が成り立つ（逆も同様）。

(b)　(P Ú Q) Ú R と仮定する。
　P Ú Q の場合、P と仮定すると ( Ú 導入) により P Ú (Q Ú R) が成り立ち、今度は Q と仮定すると ( Ú 導入) により Q Ú R なので再度 ( Ú 導入) により P Ú (Q Ú R) が成り立つので、いずれにせよ P Ú (Q Ú R) が成り立つ。
　一方 R の場合は ( Ú 導入) により Q Ú R なので、再度 ( Ú 導入) により P Ú (Q Ú R) が成り立つ。
　よって、いずれにせよ P Ú (Q Ú R) が成り立つ（逆も同様）。

　本メタ定理により、今後メタ定理23の (a) や (b) の左辺を記述するとき、括弧を省略することにします。

メタ定理24	(a)　(P Ù Q) Ú R と (P Ú R) Ù (Q Ú R) は同値。
	(b)　(P Ú Q) Ù R と (P Ù R) Ú (Q Ù R) は同値。

(a)　(P Ù Q) Ú R と仮定する。P Ù Q の場合は ( Ù 消去) により P と Q が成り立つので ( Ú 導入) により P Ú R と Q Ú R が得られ、従って ( Ù 導入) により (P Ú R) Ù (Q Ú R) が成り立つ。一方 R の場合は ( Ú 導入) により P Ú R と Q Ú R が成り立つので、( Ù 導入) によりやはり (P Ú R) Ù (Q Ú R) が成り立つ。よっていずれにせよ (P Ú R) Ù (Q Ú R) が成り立つ。

　逆に、(P Ú R) Ù (Q Ú R) と仮定すると、( Ù 消去) により P Ú R と Q Ú R が得られる。
　ここでまず P の場合を考える。更に Q である場合は ( Ù 導入) により P Ù Q なので、( Ú 導入) により (P Ù Q) Ú R であり、一方 R の場合は ( Ú 導入) により (P Ù Q) Ú R なので、いずれにせよ (P Ù Q) Ú R である。
　次に R の場合を考えると、( Ú 導入) により (P Ù Q) Ú R である。
　よって、いずれにせよ (P Ù Q) Ú R が成り立つ。

(b)　(P Ú Q) Ù R と仮定すると、( Ù 消去) により P Ú Q と R が成り立つ。ここで P の場合は ( Ù 導入) により P Ù R が得られるので、( Ú 導入) により (P Ù R) Ú (Q Ù R) が得られ、Q の場合は ( Ù 導入) により Q Ù R が得られるので ( Ú 導入) により (P Ù R) Ú (Q Ù R) が得られるので、いずれにせよ (P Ù R) Ú (Q Ù R) が成り立つ。

　逆に、(P Ù R) Ú (Q Ù R) と仮定する。まず P Ù R の場合は、( Ù 消去) により P と R が成り立つので、( Ú 導入) により P Ú Q となり、( Ù 導入) により (P Ú Q) Ù R が成り立つ。また Q Ù R の場合は、( Ù 消去) により Q と R が成り立つで ( Ú 導入) により P Ú Q となり、( Ù 導入) により (P Ú Q) Ù R が成り立つ。よっていずれにせよ (P Ú Q) Ù R が成り立つ。

メタ定理25	(a)　P Ù ^ と ^ は同値。
	(b)　P Ú ^ と P は同値。
	(c)　P Ù Ø^ と P は同値。
	(d)　P Ú Ø^ と Ø^ は同値。

(a)　P Ù ^ と仮定すると、( Ù 消去) により ^ が得られる。逆に ^ と仮定すると ( ^ 消去) により P Ù ^ が成り立つ。

(b)　P と仮定すると、( Ú 導入) により P Ú ^ が得られる。逆に P Ú ^ と仮定すると、P のときは ( 仮 定 ) により P であり、^ のときは ( ^ 消去) により P なので、いずれにせよ P が成り立つ。

(c)　P Ù Ø^ と仮定すると、( Ù 消去) により P が得られる。逆に P と仮定すると、これとメタ定理８と ( Ù 導入) により P Ù Ø^ が成り立つ。

(d)　メタ定理８と ( Ú 導入) により P Ú Ø^ が得られる。これとメタ定理８により同値性は明らかである。

メタ定理26

P Ú Q と ØQ が成り立てば P が成り立つ。

　P の場合は ( 同 一 ) により P であり、Q の場合は ØQ と矛盾するので (弱Ø消去) によりやはり P である。よって、いずれにせよ P である。

メタ定理27

P Þ (Q Þ R) と (P Ù Q) Þ R と Q Þ (P Þ R) はすべて同値。

　１番目と２番目の同値性がわかればメタ定理22 (a) により２番目と３番目の同値性がわかるので、１番目と２番目の同値性だけ証明すればよい。
　P Þ (Q Þ R) と仮定する。更に P Ù Q を仮定すると、( Ù 消去) により P と Q が成り立つので、まず ( Þ 消去) により Q Þ R が、再度 ( Þ 消去) により R が得られる。ゆえに ( Þ 導入) により (P Ù Q) Þ R が成り立つ。
　逆に (P Ù Q) Þ R と仮定する。ここで P を仮定すると、更に Q を仮定すれば ( Ù 導入) により P Ù Q が成り立ち、従って ( Þ 消去) により R が成り立つので、( Þ 導入) により Q Þ R が成り立つ。ゆえに ( Þ 導入) により P Þ (Q Þ R) が成り立つ。

メタ定理28

P Þ (ØQ) と Ø(P Ù Q) と Q Þ (ØP) はすべて同値。

　メタ定理27で R を ^ とすればよい。

メタ定理29

Ø(P Ù ØP) は定理。

　メタ定理28で Q に ØP を代入し、メタ定理19を用いればよい。

メタ定理30	(a)　R Þ (P Ù Q) と (R Þ P) Ù (R Þ Q) は同値。
	(b)　(P Ú Q) Þ R と (P Þ R) Ù (Q Þ R) は同値。
	(c)　(P Þ Q) Ú R が成り立てば P Þ (Q Ú R) が成り立つ。また P Ú ØP か R Ú ØR のどちらかが成り立てば逆も成り立つ。
	(d)　(Ø P) Ú (Ø Q) が成り立てば Ø (P Ù Q) が成り立つ。また P Ú ØP と Q Ú ØQ が共に成り立てば逆も成り立つ。

(a)　R Þ (P Ù Q) と仮定する。更に R を仮定すると ( Þ 消去) により P Ù Q が得られ、( Ù 消去) により P と Q が成り立つ。ゆえに ( Þ 導入) により R Þ P と R Þ Q が得られ、( Ù 導入) により (R Þ P) Ù (R Þ Q) が成り立つ。
　逆に (R Þ P) Ù (R Þ Q) と仮定すると、( Ù 消去) により R Þ P と R Þ Q が得られる。そこで R を仮定すると、( Þ 消去) により P と Q が得られるので ( Ù 導入) により P Ù Q が得られる。よって ( Þ 導入) により R Þ (P Ù Q) が成り立つ。

(b)　(P Ú Q) Þ R と仮定する。P を仮定すると、( Ú 導入) により P Ú Q が成り立つので ( Þ 消去) により R が得られ、従って ( Þ 導入) により P Þ R が成り立つ。同様に、Q を仮定すると、( Ú 導入) により P Ú Q が成り立つので ( Þ 消去) により R が得られ、従って ( Þ 導入) により Q Þ R が成り立つ。ゆえに ( Ù 導入) により (P Þ R) Ù (Q Þ R) が成り立つ。
　逆に (P Þ R) Ù (Q Þ R) と仮定すると、( Ù 消去) により P Þ R と Q Þ R が得られる。ここで P Ú Q と仮定する。P の場合は ( Þ 消去) により R が得られ、Q の場合も ( Þ 消去) により R が得られるので、いずれにせよ R が得られる。従って ( Þ 導入) により (P Ú Q) Þ R が得られる。

(c)　P を仮定する。P Þ Q のときは ( Þ 消去) により Q が得られるので ( Ú 導入) により Q Ú R が得られ、R のときも ( Ú 導入) により Q Ú R が得られるので、いずれにせよ Q Ú R が得られる。
　逆に P Þ (Q Ú R) が成り立つとする。
　P を仮定すると、( Þ 消去) により Q Ú R が成り立ち、Q のときはメタ定理９により P Þ Q が、したがって ( Ú 導入) により (P Þ Q) Ú R が成り立ち、R のときも ( Ú 導入) によりこれが成り立つので、( Ù 消去) によりいずれにせよこれが成り立つ。
　また ØP を仮定すると、メタ定理14により P Þ Q が、したがって ( Ú 導入) により (P Þ Q) Ú R が成り立つ。
　ゆえに P Ú ØP が成り立つときは、いずれにせよ (P Þ Q) Ú R が成り立つ。
　次に R を仮定すれば、( Ú 導入) により (P Þ Q) Ú R が成り立つ。
　また、ØR を仮定すると、更に P を仮定したとき、( Þ 消去) により Q Ú R が成り立つが、ØR なのでメタ定理26により Q が成り立つので、( Þ 導入) により P Þ Q が、したがって ( Ú 導入) により (P Þ Q) Ú R が成り立つ。
　ゆえに R Ú ØR が成り立つときも、いずれにせよ (P Þ Q) Ú R が成り立つ。

(d)　(Ø P) Ú (Ø Q) を仮定し、更に P Ù Q を仮定する。(Ù 消去) により P と Q が成り立つが、Ø P を仮定しても Ø Q を仮定しても矛盾するので、(Ú 消去) によりいずれにせよ矛盾し、Ø (P Ù Q) が成り立つ。
　逆は、(Ú 消去) による P と Ø P による場合分けと、Q と Ø Q による場合分けの組合せを考えると、P と Q の組合せ以外の場合は Ø P か Ø Q のどちらかが成り立ち、P と Q の組合せの場合は (Ù 導入) により P Ù Q が得られて矛盾するので、いずれにせよ (Ø P) Ú (Ø Q) が成り立つ。

メタ定理31

Ø(P Ú Q) と (ØP) Ù (ØQ) と Ø((ØP) Þ Q) と Ø((ØQ) Þ P) はすべて同値。

　第１式と第２式の同値性はメタ定理30 (b) で R を ^ とすればよい。
　第２式を仮定すると、( Ù 消去) により ØP と ØQ が成り立つ。ここで (ØP) Þ Q を仮定すると、( Þ 消去) により Q が得られ、これと ØQ が矛盾するので、( Ø 導入) により 第３式が得られる。
　最後に P Ú Q を仮定すると、メタ定理26により、仮定 ØP から Q が得られるので、( Þ 導入) により (ØP) Þ Q が得られる。ゆえに ( Þ 導入) により (P Ú Q) Þ {(ØP) Þ Q} が得られる。ゆえにこれの対偶と第３式から ( Þ 消去) により第１式が得られる。
　以上で第１〜第３式の同値性が示されたので、第１式又は第２式の P と Q に関する対称性により、これらと第４式の同値性が得られる。

メタ定理32

ØØ(P Ú ØP) が成り立つ。

　Ø(P Ú ØP) と仮定すると、メタ定理31により (ØP) Ù (ØØP) が成り立つので、( Ù 消去) により ØP と ØØP が得られ矛盾する。ゆえに ( Ø 導入) により ØØ(P Ú ØP) が得られる。

メタ定理33

P Ú ØP が成り立てば、P と ØØP は同値。

　メタ定理26の Q に ØP を代入すれば (ØØP) Þ P が得られるので、これとメタ定理19から結論が得られる。

メタ定理34

Ø(P Þ Q) と (ØØP) Ù (ØQ) と Ø((ØP) Ú Q) はすべて同値。

　第２式と第３式の同値性は、メタ定理31の P に ØP を代入したものから明らかだから、第１式と第２式の同値性だけを示せばよい。
　そこで、まず Ø(P Þ Q) と仮定する。ØP と仮定するとメタ定理14により P Þ Q が得られて矛盾するので ( Ø 導入) により ØØP が得られ、Q と仮定すると、メタ定理９により P Þ Q が得られて矛盾するので ( Ø 導入) により ØQ が得られる。ゆえに ( Ù 導入) により第２式が得られる。
　逆に第２式を仮定すると、( Ù 消去) により ØØP と ØQ が得られるが、更に P Þ Q と仮定すると、その対偶 (ØQ) Þ (ØP) と ( Þ 消去) により ØP が得られて ØØP と矛盾するので、( Ø 導入) により Ø(P Þ Q) が得られる。

　以下の証明では、推論規則として何を用いたかを一々書かないことにします。

メタ定理35	(a)　"xP Þ $xP は定理。
	(b)　$x$yP と $y$xP は同値。
	(c)　"x"yP と "y"xP は同値。
	(d)　$x"yP Þ "y$xP が成り立つ。
	(e)　($xP) Ú ($xQ) と $x(P Ú Q) は同値。
	(f)　("xP) Ù ("xQ) と "x(P Ù Q) は同値。

(a)　x は自由変数と仮定してよい（以下でも同様）。"xP と仮定すると P が得られるので、$xP が成り立つ。

(b)　x と y は相異なる自由変数と仮定してよい（以下でも同様）。$x$yP と仮定し、$yP であるような x を取り、P であるような y を取ると、$xP が成り立ち、従って $y$xP が成り立つ。逆も同じ。

(c)　"x"yP と仮定すると、"yP が成り立つので P が成り立つ。x は任意なので、"xP が成り立ち、y も任意なので "y"xP が成り立つ。逆も同じ。

(d)　$x"yP と仮定し、"yP であるような x を取ると、P が成り立つので $xP が成り立つ。y は任意なので "y$xP が成り立つ。

(e)　($xP) Ú ($xQ) と仮定する。$xP のときは、P となる x を取ると、P Ú Q となるので $x(P Ú Q) が成り立つ。$xQ のときも同様。
　逆に $x(P Ú Q) と仮定し、P Ú Q となる x を取ると、P のときは $xP となるので ($xP) Ú ($xQ) が成り立つ。Q のときも同様。

(f)　("xP) Ù ("xQ) と仮定する。"xP なので、P が成り立ち、"xQ なので、Q が成り立つ。ゆえに P Ù Q が成り立ち、x は任意なので "x(P Ù Q) が成り立つ。
　逆に "x(P Ù Q) と仮定すると、P Ù Q が成り立つので P と Q が成り立つ。x は任意なので "xP と "xQ が成り立ち、したがって ("xP) Ù ("xQ) が成り立つ。

メタ定理36	x を Q に現れない自由変数とする。このとき
	(a)　Q Þ ("xP) と "x(Q Þ P) は同値。
	(b)　($xP) Þ Q と "x(P Þ Q) は同値。
	(c)　($xP) Ù Q と $x(P Ù Q) は同値。
	(d)　($xP) Ú Q と $x(P Ú Q) は同値。
	(e)　("xP) Ù Q と "x(P Ù Q) は同値。
	(f)　("xP) Ú Q Þ "x(P Ú Q) が成り立つ。また、Q Ú ØQ が成り立つときは、逆 "x(P Ú Q) Þ ("xP) Ú Q も成り立つ。

(a)　Q Þ ("xP) と仮定する。任意に x を取り、Q を仮定すると、"xP が得られ、P が得られるので Q Þ P が成り立つ。x は任意なので "x(Q Þ P) が成り立つ。
　逆に "x(Q Þ P) と仮定する。ここで Q と仮定し、任意に x を取ると Q Þ P が成り立つので P が得られるが、x は任意なので、"xP が得られる。よって Q Þ ("xP) が成り立つ。

(b)　($xP) Þ Q と仮定する。ここで任意に x を取り、更に P を仮定すると、$xP が得られるので Q が成り立つ。ゆえに P Þ Q が得られ、x は任意だから "x(P Þ Q) が成り立つ。
　逆に "x(P Þ Q) と仮定する。ここで $xP と仮定し、P を満たす x を取ると P Þ Q が成り立つので Q が得られる。よって ($xP) Þ Q が成り立つ。

(c)　($xP) Ù Q と仮定すると、$xP と Q が得られる。P を満たす x を取ると、P Ù Q が得られ、$x(P Ù Q) が成り立つ。
　逆に $x(P Ù Q) と仮定し、P Ù Q を満たす x を取ると、P と Q が得られ、$xP が成り立つので ($xP) Ù Q が成り立つ。

(d)　($xP) Ú Q と仮定する。$xP が成り立つ場合は、P となる x を取ると、P Ú Q が成り立つので $x(P Ú Q) が得られる。また Q の場合には P Ú Q が得られるので $x(P Ú Q) が成り立ち、いずれにせよ $x(P Ú Q) が成り立つ。
　逆に $x(P Ú Q) と仮定する。P Ú Q を満たす x を取ると、P の場合は $xP が成り立ち、($xP) Ú Q が得られる。また Q の場合は ($xP) Ú Q が成り立つ。よっていずれにせよ ($xP) Ú Q が成り立つ。

(e)　("xP) Ù Q と仮定すると、"xP と Q が得られ、任意に x を取ると P が得られる。ゆえに P Ù Q が得られ、x は任意だから "x(P Ù Q) が成り立つ。
　逆に "x(P Ù Q) と仮定すると、任意に取った x に対して P Ù Q が、従って P が得られ、x は任意なので "xP が得られる。また P Ù Q から Q が得られる。したがって ("xP) Ù Q が成り立つ。

(f)　("xP) Ú Q と仮定する。"xP の場合は、任意に取った x に対して P が得られるので P Ú Q が成り立つが、x は任意なので "x(P Ú Q) が得られる。一方 Q の場合は、任意に取った x に対して P Ú Q が成り立つので、やはり x の任意性により "x(P Ú Q) が得られる。よっていずれにせよ "x(P Ú Q) が得られ、("xP) Ú Q Þ "x(P Ú Q) が成り立つ。
　次に Q Ú ØQ が成り立つとし、"x(P Ú Q) と仮定する。Q の場合は当然 ("xP) Ú Q が成り立つ。また ØQ の場合は、任意に取った x に対して P Ú Q が成り立つのでメタ定理26により P が成り立つ。x は任意なので "xP が成り立ち、従って ("xP) Ú Q が成り立つ。

メタ定理37	(a)　"x(ØP) と Ø$xP は同値。
	(b)　$x(ØP) Þ Ø"xP が成り立つ。
	(c)　"xP Þ Ø$x(ØP) が成り立つ。
	(d)　$xP Þ Ø"x(ØP) が成り立つ。

(a)　メタ定理36 (b) で Q に ^ を代入すればよい。

(b)　$x(ØP) と仮定し、更に "xP と仮定する。ØP となる x を取ると、この x に対しても P であることに反する。

(c)　(b) とメタ定理28から明らか。

(d)　(a) とメタ定理28から明らか。

メタ定理38	ØØP を P' 、ØØQ を Q' と書くと、
	(a)　P' Ù Q' と Ø((ØP) Ú (ØQ)) と Ø(P Þ (ØQ)) と Ø(Q Þ (ØP)) と ØØ(P Ù Q) はすべて同値。
	(b)　P' Þ Q' と (ØQ) Þ (ØP) と Ø(P Ù ØQ) と P Þ ØØQ と ØØ((ØP) Ú Q) と ØØ(P Þ Q) はすべて同値。
	(c)　"xP' と Ø$x(ØP) は同値。

(a)　メタ定理34で Q に ØQ を代入すると第１〜第３式の同値性がわかり、メタ定理28の否定をとれば第３〜第５式の同値性がわかる。

(b)　第１式を仮定すると、その対偶により (ØØØQ) Þ (ØØØP) が得られ、メタ定理20とメタ定理５により第２式が得られる。逆に第２式の対偶から第１式が得られる。
　また、メタ定理28で Q に ØQ を代入すれば、第２〜第４式の同値性がわかる。
　また、メタ定理28で P に ØØQ を代入すれば、第１式と Ø((ØØP) Ù ØQ) の同値性がわかり、メタ定理34の否定により、これと第５、第６式との同値性がわかる。

(c)　メタ定理37 (a) で P に ØP を代入すればよい。

　さて、次の推論規則を排中律といいます：

(排中律)

P Ú ØP

　メタ定理32とメタ定理33により、古典論理の推論規則 (Ø消去) は (排中律) に置き換えてもよいことがわかります。
　また、特定の命題 P に対して P Ú ØP が成り立つとき、P について排中律が成り立つといいます。次のメタ定理は、論理接続詞については排中律が“遺伝”し、その結果多くの“古典論理的な”命題が成立することを示しています。

メタ定理39	P と Q に対して共に排中律が成り立てば、
	(a)　P Ù Q , P Ú Q , P Þ Q , ØP についても排中律が成り立つ。
	(b)　ØØP と P は同値。
	(c)　P Ù Q と Ø((ØP) Ú (ØQ)) と Ø(P Þ (ØQ)) と Ø(Q Þ (ØP)) はすべて同値。
	(d)　Ø(P Ù Q) と (ØP) Ú (ØQ) と P Þ (ØQ) と Q Þ (ØP) はすべて同値。
	(e)　P Ú Q と Ø((ØP) Ù (ØQ)) と (ØP) Þ Q と (ØQ) Þ P はすべて同値。
	(f)　P Þ Q と (ØQ) Þ (ØP) と Ø(P Ù ØQ) と (ØP) Ú Q はすべて同値。
	(g)　Ø(P Þ Q) と P Ù ØQ は同値。
	(h)　P Þ (Q Ú R) と (P Þ Q) Ú R は同値。
	(i)　(P Þ Q) Ú (Q Þ P) は定理である。
	(j)　"xP と Ø$x(ØP) は同値。
	(k)　x が Q に現れない自由変数なら、("xP) Ú Q と "x(P Ú Q) は同値。

　その証明ですが、(a) については、P の場合と ØP の場合に分け、更に Q の場合と ØQ の場合に分けて考えれば十分です。
　まず P と Q が成り立つ場合は P Ù Q が成り立ちます。それ以外の場合は、例えば ØP のときは、メタ定理14とメタ定理28により Ø(P Ù Q) が導けます。ØQ の場合も同様です。
　次に P か Q のいずれかが成り立つ場合は P Ú Q が成り立ちます。それ以外の場合は ØP と ØQ が共に成り立つので、メタ定理31により Ø(P Ú Q) が導けます。
　また、ØP か Q のいずれかが成り立つ場合は、メタ定理９とメタ定理14により P Þ Q が成り立ちます。それ以外の場合は P と ØQ が共に成り立つので、メタ定理19とメタ定理34により Ø(P Þ Q) が導けます。
　最後に ØP については、メタ定理19とメタ定理５により (ØØP) Ú ØP が成り立ちます。

　(b) は、仮定とメタ定理33から得られます。
　(c) は (b) とメタ定理38 (a) から得られます。
　(d) は (c) の否定と (a),(b) から得られます。
　(e) はメタ定理31の否定と (a),(b) から得られます。
　(f) は (a),(b) とメタ定理38 (b) から得られます。
　(g) は (f) の否定と (a),(b) から得られます。
　(h) は仮定とメタ定理30 (c) から得られます。
　(i) の命題は、(f) により {(ØP) Ú Q} Ú {(ØQ) Ú P)} と同値であり、これはまたメタ定理22 (b) とメタ定理23 (b) により {(ØP) Ú P} Ú {(ØQ) Ú Q)} と同値なので、仮定により定理であることがわかります。
　(j) は (b) とメタ定理38 (c) から得られます。
　(k) は仮定とメタ定理36 (f) から得られます。

　さて、次の推論規則を帰謬法又は背理法といいます：

(帰謬法)

ØP├ Q ØP├ ØQ ————— P

　(帰謬法) の前提と (Ø導入) から ØØP が得られますから、(Ø消去) を使うと P が得られ、(帰謬法) が導かれます。逆に ØØP を仮定すると、ØP├ ØP と ØP├ ØØP が得られますから、(帰謬法) を使うと P が得られ、これは (Ø消去) が成り立つことを意味します。
　すなわち古典論理の推論規則 (Ø消去) は (帰謬法) に置き換えることも可能です。

　また、古典論理のもとで、P と ØP が成り立つとき、勝手な命題 Q に対し、前節メタ定理３により ØQ├ P と ØQ├ ØP が成り立つので、(帰謬法) により Q が得られます。これは (弱Ø消去) に他なりません。

　以上の点に注意し、古典論理で成り立つ定理（定理番号に * を付けて区別することにします）をいくつか挙げてみます。

メタ定理40*	古典論理では、メタ定理39の (a)~(k) が無条件で成り立つのに加え、次が成り立つ：
	(a)　Ø"xP と $x(ØP) は同値。
	(b)　$xP と Ø"x(ØP) は同値。
	(c)　$x($xP Þ P) は定理である。

　実際、(a) はメタ定理39 (j) の否定とメタ定理39 (b) から得られます。
　(b) はメタ定理37 (a) の否定とメタ定理39 (b) から得られます。
　(c) の命題は、メタ定理39 (f) により $x{(Ø$xP) Ú P} と同値であり、これはまたメタ定理36 (d) により (Ø$xP) Ú $xP と同値ですから、排中律により定理であることがわかります。

　メタ定理39 (c),(f),(j) により、古典論理では、論理記号 Ù と Þ と " は、Ø と Ú と $ を使って定義できることがわかります。
　また、メタ定理39と40の各項目は、直観主義論理ではいずれも無条件では成り立たないことが知られています（付録９参照）。特に、メタ定理39 (h),(i),(k) とメタ定理40 (c) は、当の命題に含まれている論理記号 Þ，Ú，"，$ に関する推論規則だけでは証明できず、当該命題に現れない Ø に対する推論規則 (Ø消去) を本質的に使って証明されています。言い換えると、推論規則 (Ø消去) は、当該論理記号 Ø の意味を規定するという以上の役割を果たしています。