【ノート・メモ】 有限の立場における排中律について

はじめに

以下、竹内外史・八杉満利子著「数学基礎論  増補版」（共立出版株式会社）より、有限の立場における排中律に関するメモ。

排中律が成り立たない理由

• 有限の立場における'対象'は、有限個の記号およびその有限個の組み合わせ（図形と呼ばれる）に関し、それらを帰納的に組み合わせることで得られる無限の図形。例えば自然数のすべては1,1+1,1+1+1,…のように逐次構成する。
• 以下、有限の立場における、すべて$\forall$、存在$\exists$、およびそれらの否定$\lnot$の定義：

• 「${\mathscr U}(x)$をみたす$x$が存在する」という命題を$\exists x{\mathscr U}(x)$で表す。また「すべての$x$について${\mathscr U}(x)$が成立する」という命題を $\forall x {\mathscr U}(x)$で表す

• 先述のとおり、有限の立場では$\lnot \exists x{\mathscr U}(x)$は考えにくいので$\forall x \lnot {\mathscr U}(x)$で定義する。 これは厳密な意味は等価でないので
  $$ \exists x{\mathscr U}(x) \lor\lnot \exists x{\mathscr U}(x) $$
  は必ずしも頭から主張できない

• 存在に関する命題において排中律が成立しない具体例（以下教科書より引用）：

${\mathscr U}(x)$の特別な場合として、例えば有限の立場において定義される関数$f(x)$をとって$f(x)=1$なるもの（※方程式の意味で解釈せよ）を考えてみよう。この場合$\exists x(f(x)=1)$とは$f(x)=1$を満たす$x$を具体的に作る方法を知っていることを意味している。また$\lnot\exists x(f(x)=1)$は$\forall x\lnot(f(x)=1)$を意味している。すなわち、どんな$a$が与えられても$f(a)=1$でないことを主張するものである。明らかに$\forall x\lnot(f(x)=1)$でないとしても$f(x)=1$なる$x$を求める具体的な方法を知るわけにはゆかないのである。この具体的な方法を知るまでは$\exists x(f(x)=1)$が主張できないのであるから、言葉の定義に従えば、われわれは
$$ \exists x{\mathscr U}(x) \lor\lnot \exists x{\mathscr U}(x) $$
が頭からどんな${\mathscr U}(x)$をとっても成立することを主張することができない。もしある${\mathscr U}(x)$についてこれが成立するというときには、この${\mathscr U}(x)$についてこのことを証明してみせなければならないわけである。すなわち排中律を頭から用いることができず、用いる場合にはその個々の場合について証明しなければならないわけである。

• $\lnot\forall x {\mathscr U}(x)$とは「$\forall x{\mathscr U}(x)$と仮定して矛盾を生じる」ことなので、$\lnot \forall x {\mathscr U}(x)$を主張するときは$\forall x {\mathscr U}(x)$を仮定して矛盾を導いてみせなければならない。それまでは$\lnot \forall x{\mathscr U}(x)$を主張できないので、やはり
  $$ \forall x {\mathscr U}(x)\lor\lnot \forall x {\mathscr U}(x) $$
  を頭から成立することを主張できない（つまりは上記の定義の下では、$\lnot\forall x{\mathscr U}(x)$は$\forall x{\mathscr U}(x)$の厳密な意味での逆ではない）。用いたいときにはその個々の場合について証明しなければならない

• $\exists x\lnot {\mathscr U}, \lnot\forall x {\mathscr U}, \forall x \lnot {\mathscr U}$の関係性（以下教科書より引用）：

いま、もし$\exists x \lnot {\mathscr U}(x)$が成立するならば、具体的な反例によって$\forall x {\mathscr U}(x)$が否定された、すなわち$\forall x {\mathscr U}(x)$を仮定すれば矛盾が生じることが証明されたことになるから、明らかに
$$ \exists x\lnot{\mathscr U}(x)\rightarrow \lnot \forall x {\mathscr U}(x) $$
が成立するわけであるが、この逆は頭から主張することができない。なぜならば'$\forall x {\mathscr U}(x)$を仮定して矛盾が生じる'ことをいえたとしても、$\lnot {\mathscr U}(x)$なる$x$を具体的に求める方法は何もまだ与えられておらず、この方法が与えられるまでは$\exists x \lnot{\mathscr U}(x)$を主張することができないからである。また、この逆を頭から主張できないことは、定義として
$$ \lnot \exists x {\mathscr U}(x)\leftrightarrow \forall x \lnot {\mathscr U}(x) $$
が常に主張できることと比べて注意されねばならない。

Heyting arithmetic (HA)における排中律

直観論理では、式の右辺にはformulaがたかだか1個。これが場合わけを禁ずることになり、排中律が成立しない。よって${\mathscr U}\lor \lnot {\mathscr U}$を主張するためには、どちらかが真であることを証明しなければならない。かつ直観論理では${\mathscr U}(x)$を証明するためには、そのような$x$を実際に提出できなければならないので、単に「このような$x$があるはずだ」ではダメ。そのため${\mathscr U}\lor \lnot {\mathscr U}$は頭から主張することはできない。

HAでも一般には排中律は証明されない。しかし、quantifier-freeなformulaについては、式の右辺の制限がないので、排中律が成り立つ。 quantifier-freeなformulaは有限の立場で真偽決定可能。ゆえに$A$がquantifier-freeならば$A$が真であるか$\lnot A$が真であるか常に具体的な方法で決定でき、したがって${\mathscr U}\lor \lnot {\mathscr U}$が主張できる。