ラッセルのパラドックス：傾向と対策 (3.2.3) : ウカシェーヴィチ無限値述語論理 ∀L・・・包括原理の限界

logic

前回は、ウカシェーヴィチ3値論理 L3 において包括原理を仮定した場合、ラッセルのパラドックスだけなら解決できるが、莫少揆のパラドックスにより結局矛盾を導いてしまう、という話を紹介いたしました。今回は、その続きとして、ウカシェーヴィチ3値論理を無限値述語論理 ∀Lまで拡張した場合、包括原理を仮定しても無矛盾であるという話を紹介したいと思います。

連続関数と不動点

さて、莫少揆のパラドックスの最大の理由は、L3の真理値の集合 {0, 0.5, 1} は、否定（y=1-x: ラッセル・パラドックスではこちらのみが問題となる）に関しては不動点を持つが、ならば（z=1-x+y）に関しては不動点を持たないことに原因がありました。莫少揆のパラドックス（有限値論理版）の示すところは、3値だけでなく、任意の有限値論理に関して、ならば（→）をうまく使うことで、不動点を持たないようにすることができるということです。
それでは、真理値をどこまで拡張すればいいのか？ここで注目すべきは、→も否定も真理関数は連続関数だということです。したがって、

ブラウアーの不動点定理
[0,1]区間上の任意の連続関数 f:[0,1]^n→[0,1] は不動点を持つ

から、真理値が[0,1]の実数全体であれば、→などに関して不動点を持つだろう、と想像できます。

ウカシェーヴィチ無限値述語論理 ∀L

というわけで、真理値が[0,1]の実数であるような、ウカシェーヴィチ多値論理の拡張を考えましょう。

  1. これは真理値として [0,1] 区間の実数全体（[0,1]={x: 0≦x≦1}）をとる。
  2. 論理結合子に関して、以下の二つを持つ。v(A)を、論理式Aの真理値を定める付値とします。このとき
    1. 否定 ¬ に関して: v(¬A)=1-v(A)
    2. A→Bに関して： v(A→B)=min{1, 1-v(A)+v(B)}
    3. 他の論理結合子（∧, ∨, etc.）は否定と→を組み合わせて作成する（A∨B は¬A→Bの略記、などなど）。
  3. v(∀xP(x))=inf{v(P(a): aはモデルのドメインの元}、同様に∃は¬∀¬で定義する。

（多値論理は大体そうですが）これもモデルから論理を定義する形になります。

∀L+包括原理の無矛盾性証明の困難・・・モデル構成編

という訳で、包括原理が ∀Lで矛盾を導かないことを証明しなければならない訳です。 ∀Lはモデルから定義されているので、 ∀L+包括原理のモデルを構成してみせるのが一番早いのだろうと思われます。実際、∀L+包括原理の部分体系の無矛盾性については以下の結果が出ています。

ZFCは以下を証明する*1。

  • Skolem (1957)*2: 量化子を持たない文についてのみ包括原理を認める部分体系（ただしidentity =を持たない言語）は無矛盾である
  • Chang(1963)*3: 以下の形の文についてのみ包括原理を認める部分体系は無矛盾である
    • 文P(y,z)で、yとzは自由変数であり、Pの中で v∈w の形の部分論理式があるときもしvがPの束縛変数ならば v=wが成立するような文である
    • もしくはP(y)の形の文で、Pがいっさいパラメータを持たない形の文である
  • Fenstad(1964) *4: 以下の形の文についてのみ包括原理を認める部分体系は無矛盾である。
    • 文P(y,z)で、yとzは自由変数であり、Pの変数 u は u∈w の形でしかPの中での出現がない

彼らは、ZFCのモデルの中で、組み合わせ原理を使って部分体系のモデルを構成しました。要は、パラメーターを持たないか、パラメーターを持っても特殊な形でしか現れない論理式に関して包括原理を許す集合論は、ZFCでモデルを作ることができる、ということです。
彼らのモデルの問題は、

  • 制限された形の文にのみ包括原理の適用を許す部分体系のモデルしか構成できないこと
  • 「モデル」というくせに、例えば u∈w の形の論理式の真理値は一律同じになってしまうこと：つまり、φ∈ωの真理値も、ω∈φの真理値も一緒になってしまうこと

です。だめじゃん。
モデルを構成する際の困難の原因ですが、何が問題となるかというと、実は∀L+包括原理のモデルには、一般の論理式について以下の二種類の論理式の真理値の決め方があるという点です。論理式 P(x) とターム t について、

  1. call-by-name: P(t) の真理値は t∈{x:P(x)} の真理値として割り振られる
  2. call-by-value: P(t) の真理値は、論理式P(x)の構成に沿って決定される（例：P(x)= (φ∈x)∧(x∈ω)ならば、v(P(t))=min{ v(φ∈x),v(t∈ω)}）

という訳で、モデルを作る際、これらの値が矛盾しないように決めていかなければならないのですが、その辺をそんなにうまく制御できる都合の良い組み合わせ原理なんてあるのでしょうか。

∀L+包括原理の無矛盾性証明の困難・・・証明論的アプローチ編

モデルを作るのが難しい以上、証明論的に∀L+包括原理の体系が無矛盾であることを証明しなければなりません。そのためには ∀Lを、syntactical に形式化してやらなければなりません。ですが、∀Lは元来モデルから定義されたものであるため、その形式化は非常に困難であることが判明しました。

  1. ∀Lは帰納的に公理化不可能であることが証明されています。すなわち、 ∀Lのどんなモデルで真理値が必ず1となる文（1-tautology と呼ばれます）の集合は、帰納的に枚挙可能ではない（Scarpellini 1962 *5 による）。
  2. 従って、形式化する際には、Hilbert style + 無限個の推論ルールを持つ形で形式化するしかありません（Hay 1963*6による）。

ちなみに、「∀Lの形式化」という言葉で意味しているのは、∀Lの1-tautologyをちょうど導出するような、形式的体系のことです。

証明論的アプローチ：Whiteの無矛盾性証明

さて、 ∀L+包括原理の体系の無矛盾性を証明するということは、すなわち、こういう証明論的に非常に面倒な体系について、カット除去が可能であることを証明することです。本当に面倒なのですが、それをやったのがホワイトです。

定理：White (1979) *7
Hは無矛盾である。

（証明）

  1. ∀L+包括原理の体系を、Hayによる無限的に形式化された体系上、規則として包括原理に相当する abstraction rule を付け加えた論理体系を H と名付ける（Hは Hay のHです）。
  2. Hに、Hilbertのτ-termsを付け加えた体系 H1を構成する。
  3. H1の言語上で、自然演繹スタイルの体系 Gを構成する。Gは、normalization proofにより無矛盾であることが示せる（ちなみに、わざわざH1でτ-termsを付け加えた理由は、このnormalizationをうまくいかせるためにあった）。
  4. Gは整合的なので、Gの極大無矛盾な文の集合をとることができる。具体的には、ここでカット除去証明の際にやるように、証明探索樹(proof search tree)の無限パスをとってくればよい。
  5. 任意のH1の定理（ただし閉論理式で書けるもの）はGで証明可能である。従って、もしH1が矛盾しているならば、矛盾を表す論理式は閉論理式で書けるため、Gの定理ともなるはずである。しかし、上で示したように、Gは無矛盾で、モデルを持つ。従って、H1も無矛盾であり、Gのモデルは（閉論理式に関して）H1のモデルになっている。

という訳で、だいぶ遠回りしてですが、無矛盾性が証明されました。（証明終了）

ここで注意してほしいことは、「モデル」といいながら、ここで構成されたのは論理式（1-tautology）の無限集合だ、ということです。∀L は本来モデル（真理値）から定義されているのに、唯一知られているモデルが（証明論的手法で構成された）論理式の無限集合だ、という点にやりきれなさを感じます。

Hとラッセル・パラドックス

無矛盾性がわかりましたので、次は手短にラッセル・パラドックスについて。

  • Hではラッセル集合 R も存在する。
  • R∈R の真理値も ¬(R∈R) の真理値も0.5
  • ラッセル・パラドックスの推論 R∈R→¬(R∈R) の真理値は1、その意味で正しい推論である（1-tautologyである）。

∀Lと縮約規則

では、論理 ∀L は、証明論的な視点からは、どのような特徴があるのでしょうか？まとめると

  • グリシン論理の拡張である：つまりグリシン論理で証明できる定理は全て証明できる。
  • また、古典論理の部分論理である。∀Lが複雑な原因だった「無限的な推論ルール」とは、縮約規則の断片に対応している。
  • つまり、グリシン論理／ ∀L／古典論理の差は、縮約規則がどれだけ含まれているかのみであり、その他の点では同一である。

つまり、図式にまとめると以下のようになります。

　　グリシン論理→→ウカシェーヴィチ無限値述語論理（∀L）→→古典論理
　　（縮約なし）　　　（縮約規則の断片を含む）　　　　　　　　（縮約をフルに含む）

実は、∀Lは、包括原理を仮定しても矛盾を導かない論理の中で、もっとも証明力の強い論理であることが知られています。つまり、縮約規則の断片を無限的な形で入れているため、ここが証明力の極限となっている訳です。この点こそ∀Lの研究の意義です：つまり、真理値上の不動点の重要性だけでなく、
　　　包括原理を仮定して、縮約規則をどこまで強くしたら矛盾がおこるか、そのギリギリのところを教えてくれる
のです。

Hと再帰性・算術の展開

上の結果は、言い換えれば、包括原理でどこまで数学を展開できるか知りたかったら、Hで数学が展開できれば調べればよい、ということです。グリシン論理の時にお話ししましたが、包括原理は再帰定理と同値で、再帰定理は（計算機科学の根幹である）再帰的計算の一般化です。というわけで、Hは、再帰的計算によってどこまで数学が展開できるのか、その限界を指し示すとも言えます。
では、具体的に見ていきましょう。集合論 Hでは、

  1. もちろん外延性公理を仮定すると矛盾が起こる（グリシンのパラドックス）。
  2. 再帰定理が証明できる。
    • 再帰定理によって、自然数全体の集合ωが定義され、その上の演算（足し算／かけ算など）が関係として定義される。
    • しかし、相変わらず関数として定義されるかどうかはまだわかっていない。
  3. 古典論理上の算術と決定的に違う点は、以下の通りである。
    • 数学的帰納法を仮定すると矛盾が導出される（Hajek 2004*8）。
    • っていうかH自身がω-矛盾である。実際、インフォーマルな言い方をすれば、全てのHのモデルにおいて、ωは超準的自然数を持つ*9。ちなみに、この証明は、莫少揆のパラドックスの直接的な応用となります（そのうち、暇があったら補足します）。
    • この結果は、数学的帰納法と一般化された再帰法は、極限において矛盾する、と言い直すことができます。
      • よく知られた結果ですが、タイプ理論等では、再帰オペレーター（recursor）を持ちながら不動点オペレーターを持つ体系を考えることで、再帰法が使えるが数学的帰納法は成立しない体系を作ることができます。
      • 古典論理上のタイプ理論とHで同様な現象が起こるという事実は、古典論理上のタイプ理論での矛盾の導出がどれくらい弱い論理で可能であるかを考察するという視点からも、研究する必要があるのかもしれません。

まとめると

  1. ∀L+包括原理は無矛盾であろう、とスコーレムが1950年代に提唱した。
    • ラッセルのパラドックスは、二値論理上で矛盾を導く。これは真理値上に否定に関する不動点がとれないのが原因。
    • ウカシェーヴィチ3値論理 L3 において包括原理を仮定した場合、莫少揆のパラドックスにより矛盾を導いてしまう。真理値上に→に関する不動点がとれないのが原因。
    • ウカシェーヴィチ論理の真理関数は皆連続であるため、真理値を[0,1]の実数全体に広げると不動点をとることができる。それがウカシェーヴィチ無限値述語論理 ∀Lである。
    • ただし、∀L+包括原理の無矛盾性証明は難しく、1979年にホワイトが証明論的に証明するまで待たねばならなかった。
  2. ∀Lは、古典論理の部分論理であり、グリシン論理の拡張にあたる。
    • そして、∀Lは、包括原理を仮定しても矛盾を導かない論理の中では最も証明力の強い論理である。
    • ∀Lは、包括原理を仮定して、縮約規則をどこまで強くしたら矛盾がおこるか、そのギリギリのところを教えてくれる。
  3. 集合論 H （∀L+包括原理）は、包括原理でどこまで数学を展開できるかの限界を教えてくれる。
    • また、再帰的計算によってどこまで数学が展開できるのか、その限界を指し示すとも言える。
    • Hでは、古典論理上の算術に近いことができるが、一方でω-矛盾であることが知られており、謎が多い。更なる研究が必要であろう。

というわけで今回はこれまで。次回は（いつになるかわかりませんが）ファジイ論理一般のケースのご紹介をしたいと思います。

*1:サーベイとしては C. C. Chang. Infinite valued logic as a basis for set theory. Logic, Methodology and Philosophy of Science (Proc. 1964 Internat. Congr.) pp. 93-100 North-Holland, Amsterdam (1965)を参考のこと。

*2:T. Skolem. Bemerkungen zum Komprehensionsaxiom. Zeitschrift fur mathematische Logik und Grundlagen der Mathematik, 3(1957) pp.1-17

*3:C. C. Chang. The axiom of comprehension in infinite valued logic. Mathematica Scandinavia 13 (1963) pp.9-30

*4:J.E. Fenstad. On the consistency of the axiom of comprehension in the Lukasiewicz infinite-valued logic. Mathematica Scandinavia 14 (1964) pp.65-74

*5:B. Scarpellini. Die Nichtaxiomatisierbarkeit des unendlichwertigen Pradikatenkalkuls von Lukasiewicz. Journal of Symbolic Logic, 27 (1962) pp.159-170

*6:Louise Schmir Hay. Axiomatization of the Infinite-Valued Predicate Calculus. Journal of Symbolic Logic, 28(1) (1963) pp.77-86

*7:Richard B. White. The consistency of the axiom of comprehension in the infinite-valued predicate logic of Lukasiewicz. Journal of Philosophical Logic, 8 (1979) pp.509-534

*8:Petr Hajek. On arithmetic in the Cantor-Lukasiewicz fuzzy set theory. Archive for Mathematical Logic 44(6): 763 - 82.:この論文では、∀Lではなく、似ているが別の体系であるL∀で証明しているため、「hajekがこの事実を証明した」というのは、もしかしたら語弊があるかもしれません。

*9:Shunsuke Yatabe. A note on Hajek, Paris and Shepherdson’s theorem. Logic Journal of IGPL, pp.261-266, vol. 13(2), March 2005.