私が直観主義論理を擁立するたった1つの理由

本題に入る前に

最初に明確にしておきたいのですが、私は古典論理における背理法や排中律の正しさを疑っているわけでは全くありません。
直観主義論理を擁護するとしたらこの路線かなあと思いましたので記事にしてみました。

古典論理とは？

古典論理は素朴には命題を扱う論理です。
古典論理では、命題は真であるか偽であるかが確定するものとして扱います。
むしろそれが命題の定義でもあり、命題は（真と偽の2値の）真理値の別名であるとさえ言えます。
これにより、真理表はただちに正当化されます。
例えば、「$P$でない」が偽のとき、「$P$である」は真です。
したがって、もちろん排中律は成り立ちますし、背理法も成り立ちます。ここを疑う余地は全くありません。

命題は日本語や英語などの自然言語で記述されることがあります。
ここで重要なのは、命題は自由変数を含まないという観察です。

例えば、「自然数$n$は偶数である」というのは古典論理の命題ではありません。
「自然数$2$は偶数である」は命題で、これは真ですし、
「自然数$9$は偶数である」も命題で、これは偽です。
したがって、「自然数$n$は偶数である」というのは$n$の値によって真にもなりますし、偽にもなります。
このように自由変数を含む主張は真偽が定まるものではないため、命題と呼ぶ代わりに命題関数と呼ばれます。

命題関数はそのすべての自由変数を何か具体的なものに置き換えたり、量化することによって命題にすることができます。
先ほどの例では$n$に$2$や$9$といった具体的な数を代入して命題にしました。
量化の例を挙げると、「すべての自然数$n$について$n$は偶数である」というのは命題です。それは偽であり、その反例は$n = 1$です。

古典論理では命題が関心の対象なので、しばしば命題を記号化します。
例えば、「$P$かつ$Q$」を$P \land Q$、「すべての$x$について$P(x)$が成り立つ」を$\forall x. P(x)$などと書き、すべての命題を記号で記述します。
ここから更に進んで、記号化された命題から意味を取り去り、文法だけが規定されている単なる記号列を考え、これを論理式と言います。
自由変数を含まない論理式を飽和論理式、自由変数を含む論理式を不飽和論理式と言い、意味を考えるとこれらは命題と命題関数にそれぞれ対応します。

構文論おさらい

論理式は意味を伴わない単なる構文上の式ですが、命題の

• 変数$x, y, z, \ldots$
• 関数$f, g, h, \ldots$（引数の個数$n \geq 0$がそのそれぞれに予め定められている）
  • 引数の個数$0$の関数を定数と呼ぶ。
• 述語$P, Q, R \ldots$（引数の個数$n \geq 0$がそのそれぞれに予め定められている）

などの記号から始めて、帰納的に項、原子論理式、論理式の順に文法を定めるのが通例です。

細かい定義は省略しますが、大雑把に以下の通りです。

• 項は（述語を使わずに形成される）文法的に正しい式のことです。
  • 数論で言えば$42$や$n$、$5 \times 8$、$3 - (m + 4)$などが該当します。
• 原子論理式は（後で）命題や命題関数として意味を持たせられる最小の式のことです。
• 論理式は（後で）命題や命題関数とする式のことです。

論理式を定義する際は、原子論理式から始めて、論理接続詞$\lnot, \land, \lor, \Rightarrow$や量化記号$\forall, \exists$で組み合わせることで帰納的に定義されます。

意味論おさらい

論理式は単なる記述ですが、自由変数を含まない論理式（すなわち飽和論理式）は命題となることを意図して定義された式であり、これに真理値を割り当てることで意味論が展開されます。

真理値の集合を$\mathbf{2} = \{ T, F \}$とします。
飽和な原始論理式全体の集合を$\mathrm{SatAtom}$とすると、飽和な原始論理式$\phi$を命題として解釈してその真理値を割り当てる関数

$$ I \colon \mathrm{SatAtom} \to \mathbf{2} $$

を考えることができます。これは解釈関数と呼ばれます。

2つの飽和論理式$\phi$と$\psi$について、構文的な定義により$\phi \land \psi$も飽和論理式になりますが、これにも真理値を割り当てることができるべきです。
$\land$は「かつ」を表したいので、例えば$I(\phi) = T, I(\psi) = T$のときは$I(\phi \land \psi) = T$としたいです。
ここで重要なことは、$I(\phi \land \psi)$の値は真理値$I(\phi)$と$I(\psi)$にのみ依存すべきであって、論理式$\phi$や$\psi$そのものがどのように形成されているかに直接依存すべきでないという観察です。
つまり、$\land$の意味の解釈$\hat{\land}$と言うのは、単に2つの真理値の直積から真理値への関数と見なせるべきです。

$$ \hat{\land} \colon \mathbf{2} \times \mathbf{2} \to \mathbf{2} $$

$$ \begin{align*} T \space\hat{\land}\space T &= T \\ T \space\hat{\land}\space F &= F \\ F \space\hat{\land}\space T &= F \\ F \space\hat{\land}\space F &= F \\ \end{align*} $$

あるいは次のように真理表を書くのが一般的かもしれません。

$$ \begin{array}{cc|c} \phi & \psi & \phi \land \psi \\ \hline T & T & T \\ T & F & F \\ F & T & F \\ F & F & F \\ \end{array} $$

実際、$\lor$（「または」を表す記号）などの他の論理演算子も同様に、真理値を使ってその解釈が定義されます。

命題関数と量化

飽和論理式は真理値を割り当てることで命題の真偽の判断と対応付けることができました。
同様に、不飽和論理式は命題関数と対応します。

自由変数$x$を含む論理式$\phi$に対して、その$x$に項$t$を代入した後の論理式を$\phi[x := t]$で表すこととします。

唯一の自由変数$x$を含む不飽和論理式$\phi$があるとします。（変数$x$自体は複数個含んでいても良いが、変数の種類としては$x$ただ1種類という意味）
変数を含まない項$t$で代入すると、$\phi[x := t]$は飽和論理式になるので真理値を割り当てることができます。
あるいは、$\forall$で束縛すると飽和論理式$\forall x. \phi$になります。
この意味は「すべての$x$について$\phi$である」です。

仮に変数$x$の動く範囲が項$a, b, c$の3つだったとすると、以下の真理表を書くことができます。

$$ \begin{array}{ccc|c} \phi[x := a] & \phi[x := b] & \phi[x := c] & \forall x. \phi \\ \hline T & T & T & T \\ T & T & F & F \\ T & F & T & F \\ T & F & F & F \\ F & T & T & F \\ F & T & F & F \\ F & F & T & F \\ F & F & F & F \\ \end{array} $$

この量化記号に関しても、先ほどの論理演算子と同じ観察が言えます。
つまり、$I(\forall x. \phi)$の値は真理値$I(\phi[x := a]), I(\phi[x := b]), I(\phi[x := c])$にのみ依存すべきであって、論理式$\phi$そのものがどのように形成されているかに直接依存すべきでないということです。

本題

無限領域の量化

ここで問題になってくるのが、無限の領域に対する量化です。
最も単純な例が自然数でしょう。

真理値$I(\forall x. \phi)$を考える際に、先ほどは$x$が取り得る値が3通りである場合を具体的に考察しましたが、$x$が例えば自然数全体を動く場合はどうでしょうか。
自然数は無数に存在するので、すべての場合の真理値を列挙することは不可能です。

例えば、

「自然数$n$について

$$ 1 + 2 + \cdots + n = \frac{n(n+1)}{2} $$

が成り立つ。」

という主張を$P(n)$とします。
※本来はすべてを記号的に書くべきかもしれませんが、ここで論理式を書くことは話の本筋から外れるため割愛します。
この$P(n)$は自由変数$n$を含むので命題関数です。
命題ではないので$P(n)$に真理値が定まるわけではありませんが、$n$が何か具体的な自然数に定まればそれは命題になって真理値が定まります。

さて、ここで変数$n$を全称量化して、

「すべての自然数$n$について$P(n)$が成り立つ。」

とすればこれは古典論理の命題と言って良いでしょう。

しかし、これが真であることを示すには、$P(1), P(2), P(3), \ldots$の真理値を個別に求めるしかありません。
なぜならば、論理式の真理値は、その中の原始論理式に割り当てられた真理値と論理演算子の意味によって定まるからです。
もし途中で真理値$F$が出ればこの手続きを切り上げて、$\forall n. P(n)$は偽であると結論付けることができますが、（皆さんご存じの通り）この命題は真ですので、この手続きは無限に続くことになります。
それはつまり真偽を定めることができるとは言い切れないことを意味します。この意味で$\forall n. P(n)$は常に古典論理の命題であるとは限りません。

数学的帰納法を使えば良いのでは？と思われるかもしれませんが、それも上記と同じ理由で不可能です。
「すべての自然数$n$について$P(n) \implies P(n+1)$」が成り立つことを示そうにも、結局$P(1) \implies P(2), P(2) \implies P(3), \ldots$の真理値を個別に求める羽目になります。これは終わりません。

ここでは全称量化$\forall x. \phi$を例に挙げましたが、存在量化$\exists x. \phi$でも同じことが言えます。（そのような$x$が存在しない場合は無限ループに陥る）

普段の数学では

恐らく、「そんなことはおかしい」と思うはずです。個別の場合を全通り確かめずとも真であることは分かるはずですね。

「すべての自然数$n$について

$$ 1 + 2 + \cdots + n = \frac{n(n+1)}{2} $$

が成り立つ。」

という命題は、普段は無限なんて気にせずに証明しているはずですから。
そして、もちろんその通りです。この命題は無限の議論に踏み込まずとも証明できます。

証明の例を挙げます。

ここで、証明中に自由変数$k$が登場していることに気づくでしょうか。
本質的に、変数$k$をわざわざ用意せずとも、変数$n$のまま議論できるはずです。
普段の数学では「すべての$x$について$P(x)$が成り立つ」と言うときに、その個別の事例$a, b, c, \ldots$について$P(a), P(b), P(c), \ldots$の真偽を逐一確認しているわけではなく、単に自由変数を含む命題関数$P(x)$に対して証明を考えているわけです。

この意味で、命題関数のことを自由変数命題、その証明を自由変数証明と呼ぶことができるでしょう。
私たちは普段、$\forall x. P(x)$という命題に取り組む際は、個別の命題$P(a)$に対してではなく、自由変数命題$P(x)$に対して"成り立つかどうか"を考えています。
そして、その自由変数命題が成り立つかどうかというのは、その自由変数$x$を何か具体的な項に代入して命題$P(a)$を作るときに、任意の項$a$で代入しても$P(a)$が成り立つことが分かることを言います。

古典論理に戻って

さて、古典論理に戻りましょう。

無限の領域に量化された命題を考える上で、自由変数命題（命題関数）やその自由変数証明という考え方が重要であることが分かりました。
しかし、古典論理で真理値を割り当てられるものはあくまでも命題であり、自由変数命題ではありません。

意味論のおさらいで何度か述べたように、飽和論理式$\phi$に対する真理値の割り当ては、$\phi$の構文的な形式ではなく、その中の原始論理式に割り当てられた真理値および論理演算子の意味にのみ依存しなければならないからです。
$\phi$の構文的な形式に依存してはならないという制約のため、古典論理で自由変数命題が成り立つかどうかという議論を正当化することはできません。
この意味で、量化された命題を古典論理で扱うときは、その領域は有限でなければならないと言えるでしょう。
これはつまり、例えば「すべての自然数について……」という命題を扱うことができないということです。少なくとも議論を正当化できません。（あるいは古典論理に依拠しないメタ的な視点での正当化が必要）
かなり不便なことですが致し方ありません。どこかに良い解決方法は無いものか……

直観主義論理

そこで現れるのが直観主義論理です。

直観主義論理では「命題とは真であるか偽であるかが定まるものである」という真理値としての命題の定義を捨て、その代わりに「命題とはそれが真であるかどうかを判断できるものであり、命題が真であるとはその証明を実際に構成して説明できることである」というように定義します。
もちろん、この後には証明の構成とは何か？という説明が必要ですが今回は割愛します。

これにより何が変わるかと言うと、命題には真偽を定めなければならないという古典論理の制約が無くなるため、自由変数命題も命題として扱うことができるようになります。つまり、"自由変数命題が真である"ということを議論できるようになります。
そして、自由変数命題の証明とはまさしく自由変数証明のことです。
このように、構成の観点から普段私たちが数学をする際に行っている無限の領域に対する量化を正当化することができます。

ただし、古典論理を捨てる代償もあり、直観主義論理の命題の定義では「命題の真偽が定まる」とは限らなくなってしまうため、特に命題の否定の意味が古典論理から大きく変わってしまいます。
これにより、古典論理では"命題の定義より明らか"であった排中律であったり背理法であったりが一般には成り立たなくなる……というのは有名な話です。
しかし、排中律を捨てるか無限領域での量化を捨てるかを選ぶとすれば私は前者を選ぶでしょう。