⟐ 数学の作り方 How to make Mathematics

第10章 非古典・高階の論理

「排中律」を疑うと、別の論理が見えてくる

これまでの論理は古典論理——「φ\varphi か ¬φ\lnot\varphi のどちらかは必ず真」（排中律）を認めてきました。 真理値表を書けば当たり前に見えます。でも「存在する」を「実際に構成してみせる」と読む立場からは、これは自明ではありません。 「φ∨¬φ\varphi\lor\lnot\varphi が真」と言うには、どちらが真かを示せるべきではないか？

この問い直しから生まれるのが直観主義論理です。さらに「必然的に」「可能である」を扱う様相論理、対象だけでなく 性質や集合にも量化する高階論理、真偽の間に段階を認める多値・ファジィ論理——古典論理は唯一の論理ではなく、 目的に応じて選ぶ道具の一つだと分かります。この章は、それぞれがどんな意味論をもち、これまでの完全性・ コンパクト性がどこで保たれ・どこで崩れるかを見ます。

古典論理は数ある論理の一つ。排中律を落とすと直観主義論理、量化を性質へ広げると高階論理——完全性の運命も変わる。

直観主義論理

古典論理と構文はほぼ同じですが、排中律 φ∨¬φ\varphi\lor\lnot\varphi・二重否定除去 ¬¬φ→φ\lnot\lnot\varphi\to\varphi・背理法 RAA を認めない （第2章で「ここが分かれ目」と予告した点）。何を意味するのかは、証明を「構成」と読む次の解釈で明快になります。

定義 BHK解釈（構成的意味）

論理式の“証明”を次のように読む（Brouwer–Heyting–Kolmogorov）： φ∧ψ\varphi\land\psi の証明＝φ\varphi の証明と ψ\psi の証明の組。φ∨ψ\varphi\lor\psi の証明＝どちらかを指定し、その証明を与えること。 φ→ψ\varphi\to\psi の証明＝φ\varphi の証明を ψ\psi の証明へ変換する手続き。∃x φ\exists x\,\varphi の証明＝具体的な対象 aa と φ(a)\varphi(a) の証明の組。 ¬φ:≡φ→⊥\lnot\varphi:\equiv\varphi\to\bot、⊥\bot の証明は無い。

この読み方だと、φ∨¬φ\varphi\lor\lnot\varphi を証明するには「φ\varphi が証明できるか、¬φ\lnot\varphi が証明できるか、いずれかを示す」必要がある。 未解決問題 φ\varphi ではどちらも今は示せない——だから排中律は一般には成り立たない。直観主義論理は 「存在するとは、構成できること」という立場の論理です。その特徴が次の性質に凝縮されます。

定理 直観主義論理の性質

（無矛盾な直観主義理論について）選言特性：⊢φ∨ψ\vdash\varphi\lor\psi なら ⊢φ\vdash\varphi または ⊢ψ\vdash\psi。 存在特性：⊢∃x φ\vdash\exists x\,\varphi なら、ある閉項 tt で ⊢φ[x:=t]\vdash\varphi[x:=t]。

古典論理では成り立たない（⊢φ∨¬φ\vdash\varphi\lor\lnot\varphi でもどちらも導けないことがある）これらが、直観主義では成り立つ。 証明が構成を持つ、というBHKの理念がそのまま定理になっています。この「証明＝プログラム」という見方が、 カリー–ハワード対応（第16章）でプログラミングと論理を一体化させます。意味論はクリプキが与えます。

定義 直観主義のクリプキ意味論

半順序集合 (W,≤)(W,\le)（“情報状態”とその増加）の各点 ww に、成り立つ原子式を単調に（w≤w′w\le w' なら増える方向に）割り当てる。 w⊩φ→ψ  ⟺  w\Vdash\varphi\to\psi \iff すべての w′≥ww'\ge w で（w′⊩φw'\Vdash\varphi ならば w′⊩ψw'\Vdash\psi）。 w⊩¬φ  ⟺  w\Vdash\lnot\varphi\iff すべての w′≥ww'\ge w で w′⊮φw'\not\Vdash\varphi。w⊩∀…w\Vdash\forall\dots も未来の状態を見る。

味噌は →,¬,∀\to,\lnot,\forall が「今と、これから増える情報すべて」を見る点。だから「今 φ\varphi が未確定」なら φ∨¬φ\varphi\lor\lnot\varphi は成り立たない。直観主義論理は、このクリプキ意味論に対して健全かつ完全（一階直観主義論理の完全性）です。 シークエント計算では、LKLK の後件を1つの論理式に制限した LJLJ が直観主義に対応します（右の「または」を許さない＝排中律が出ない）。

様相論理

「必然的に φ\varphi（□φ\Box\varphi）」「可能である（◊φ\Diamond\varphi）」を扱います。同じクリプキの枠組みが、今度は 「可能世界」の意味論として働きます。

定義 様相論理のクリプキ意味論

可能世界の集合 WW と到達可能関係 R⊆W×WR\subseteq W\times W を与える。 w⊩□φ  ⟺  w\Vdash\Box\varphi\iff wRw′wRw' なるすべての w′w' で w′⊩φw'\Vdash\varphi（到達可能な全世界で真＝必然）。 w⊩◊φ  ⟺  w\Vdash\Diamond\varphi\iff ある到達可能 w′w' で w′⊩φw'\Vdash\varphi（＝可能）。

面白いのは、RR に条件を課すと、成り立つ公理が変わること。公理と関係の性質が対応します： TT（□φ→φ\Box\varphi\to\varphi）  ⟺  R\iff R 反射的、44（□φ→□□φ\Box\varphi\to\Box\Box\varphi）  ⟺  R\iff R 推移的、 55（◊φ→□◊φ\Diamond\varphi\to\Box\Diamond\varphi）  ⟺  R\iff R ユークリッド的。反射＋推移＝S4（証明可能性・時相論理）、 反射＋推移＋対称＝S5（形而上的必然性）。様相論理は完全性・コンパクト性を保ち（有限モデル性をもつ体系も多く決定可能）、 知識・時間・義務・プログラム検証（動的論理）など応用が広い。ゲーデルの証明可能性述語（第13章）は S4 的な様相 □\Box として振る舞います。

高階論理

一階では対象にしか量化できませんでした。二階論理は「すべての性質 PP について」と、性質（＝対象の集合）にも量化します。

例 二階論理の表現力

自然数の帰納法「∀P (P(0)∧∀n(P(n)→P(n+1))→∀n P(n))\forall P\,\big(P(0)\land\forall n(P(n)\to P(n+1))\to\forall n\,P(n)\big)」は、PP に量化する二階の文。 これで自然数構造 N\mathbb N を同型を除いて一意に特徴づけられる（第二階ペアノ算術は圏論的＝モデルが本質的に1つ）。 一階では超準モデルを排除できなかった（第8章）のに、二階では標準の N\mathbb N だけを切り出せる。実数体の完備性 （上限の存在）も二階の文で、R\mathbb R を一意に特徴づける。

強力ですが、代償は重い。標準的な意味論（“すべての性質”を領域のすべての部分集合とする）のもとで、二階論理は：

定理 高階論理は完全性・コンパクト性を失う

標準意味論の二階論理には、妥当な文全体を導く帰納的な完全証明体系が存在しない（不完全）。コンパクト性も レーヴェンハイム–スコーレムも成り立たない。

理由は表現力の裏返しです。N\mathbb N を一意に特徴づけられるということは、算術の全真理を二階の妥当性に埋め込めるということ。 もし完全な証明体系があれば算術の真理が枚挙できてしまい、第13章の不完全性に反する。「モデルを一意に絞る力」と 「証明体系の完全性」は両立しない——一階論理の“無力さ”（第8章）は、完全性という良さの裏面だったのです。 これが一階論理を数学の標準の土台に据える理由になります。

多値・ファジィ論理

真偽の二値を緩め、真理値を {0,1}\{0,1\} でなく [0,1][0,1] や有限個の値にとる論理もあります。

注意 多値・ファジィ論理

ファジィ論理では真理値を [0,1][0,1] にとり、「背が高い」のような程度を扱う（∧\land を min⁡\min や積、¬\lnot を 1−x1-x で解釈）。 3値論理（真・偽・未定義）は部分関数や未定義を扱うのに使われる。これらは古典論理の一般化で、 制御・データベース・言語の意味論などで応用される。排中律 φ∨¬φ\varphi\lor\lnot\varphi はふつう成り立たない （真理値 0.50.5 なら max⁡(0.5,0.5)=0.5≠1\max(0.5,0.5)=0.5\ne1）。

つまずきポイント

注意 よくある誤解

  • 直観主義は「排中律が偽」ではない。 排中律を一般には認めない（証明の道具から外す）だけ。¬¬(φ∨¬φ)\lnot\lnot(\varphi\lor\lnot\varphi) は直観主義でも成り立つ。「偽」と「証明できない」は別。
  • 高階論理の不完全性は不完全性定理とは別物だが同根。 二階論理に完全な体系が無いのは、標準意味論が強すぎるため。ヘンキン意味論（“性質”を制限）に変えれば一階に還元でき完全になる。
  • 様相 □\Box は真理値関数でない。 □φ\Box\varphi の真偽は φ\varphi の真偽だけでは決まらず、到達可能世界を見る。真理値表では扱えない。

この章のまとめ

  • 直観主義論理は排中律・二重否定除去を認めず、証明を構成と読む（BHK）。選言特性・存在特性をもち、クリプキ意味論で完全。LJLJ（後件1つ）に対応し、カリー–ハワード（第16章）へ繋がる。
  • 様相論理は □◊\Box\Diamond をクリプキの可能世界＋到達可能関係で解釈。公理と RR の性質が対応（T/S4/S5）。完全性を保つ。
  • 高階論理は性質にも量化でき N,R\mathbb N,\mathbb R を一意に特徴づける代償に、完全性・コンパクト性・LS を失う。表現力と完全性は両立しない——一階論理を標準に据える理由。多値・ファジィ論理は真理値を [0,1][0,1] 等に広げる。

証明論を終え、次章から視点を変えます。「機械的に計算できるとは何か」——計算可能性理論（チューリング機械・λ計算）へ進みます。