Loading article…
計算可能性論理（CoL ）は、真理の形式理論である古典論理とは対照的に、計算可能性の体系的な形式理論として論理を再開発するための研究プログラムおよび数学的枠組みです。これは、 2003年にギオルギ・ジャパリゼによって導入され、そのように命名されました。[ 1 ]
古典論理では、論理式は真偽の命題を表します。CoLでは、論理式は計算問題を表します。古典論理では、議論の妥当性は形式のみに依存し、意味には依存しません。CoLでは、妥当性とは常に計算可能であることを意味します。より一般的に言えば、古典論理は、与えられた命題の真偽が、他の命題の集合の真偽から常に導かれる場合を教えてくれます。同様に、CoLは、与えられた問題 Aの計算可能性が、他の与えられた問題B1 ,..., Bnの計算可能性から常に導かれる場合を教えてくれます。さらに、CoLは、B1 , ..., Bnの既知の解から、そのようなAの解（アルゴリズム）を実際に構築するための統一的な方法を提供します。
CoLは、計算問題を最も一般的な意味での対話的意味で定式化します。CoLは、計算問題を、機械が環境に対して行うゲームとして定義します。このような問題は、環境のあらゆる可能な動作に対してゲームに勝つ機械が存在する場合に計算可能です。このようなゲームをプレイする機械は、チャーチ・チューリングのテーゼを対話レベルに一般化します。真理の古典的な概念は、計算可能性の特別な、対話度ゼロのケースであることがわかります。これにより、古典論理はCoLの特別な断片となります。したがって、CoLは古典論理の保守的な拡張です。計算可能性論理は、古典論理よりも表現力、構成力、計算上の意味が優れています。古典論理に加えて、独立性フレンドリー（IF）論理、線形論理および直観主義論理 の特定の適切な拡張も、CoLの自然な断片であることがわかります。[ 2 ] [ 3 ]したがって、「直観主義的真理」、「線形論理的真理」、「IF論理的真理」の意味のある概念は、CoLの意味論から導き出すことができます。
CoLは、何が計算可能でどのように計算できるかという根本的な問いに体系的に答えます。そのため、CoLには、構成的応用理論、知識ベースシステム、計画および行動のためのシステムなど、多くの応用があります。これらのうち、これまで広範に研究されてきたのは、構成的応用理論における応用のみです。CoLに基づく一連の数論は、「クラリスメティクス」と呼ばれ、古典論理に基づく一階ペアノ算術や、有界算術システムなどのその変種に対する、計算論的および複雑性理論的に意味のある代替案として構築されています[4 ] [ 5 ]。
自然演繹やシーケント計算などの従来の証明体系では、 CoLの非自明な断片を公理化するには不十分である。このため、サークエント計算などの代替的でより一般的で柔軟な証明方法の開発が必要となった。[ 6 ] [ 7 ]
CoL の完全な言語は、古典的な一階述語論理の言語を拡張したものです。その論理語彙には、数種類の論理積、論理和、量化子、含意、否定、およびいわゆる再帰演算子があります。このコレクションには、古典論理のすべての論理結合子と量化子が含まれます。この言語には、基本的と一般の2 種類の非論理的原子もあります。基本的原子は、古典論理の原子に他ならず、基本的問題、つまり、真の場合に機械が自動的に勝ち、偽の場合に負ける、動きのないゲームを表します。一方、一般原子は、基本的か非基本的かを問わず、任意のゲームとして解釈できます。意味的にも構文的にも、古典論理は、言語内で一般原子を禁止し、¬、∧、∨、→、∀、∃ 以外のすべての演算子を禁止することによって得られる CoL の断片に他なりません。
ジャパリゼは、CoLの言語は無限に拡張可能であり、さらなる拡張が可能であることを繰り返し指摘してきた。この言語の表現力の高さゆえに、公理化の構築やCoLに基づく応用理論の構築といったCoLの進歩は、通常、この言語の特定の断片に限定されてきた。
CoLのセマンティクスの根底にあるゲームは、静的ゲームと呼ばれます。このようなゲームにはターン順序がなく、他のプレイヤーが「考えている」間でも、プレイヤーは常に動くことができます。しかし、静的ゲームでは、プレイヤーが「考えすぎる」（自分の動きを遅らせる）ことに対してペナルティが課されることはないため、このようなゲームはスピードを競うゲームにはなりません。すべての基本ゲームは自動的に静的であり、一般的なアトムの解釈として許容されるゲームも同様です。
静的ゲームには、機械と環境という2つのプレイヤーが存在する。機械はアルゴリズム的な戦略にしか従えないが、環境の行動には制約がない。各ラン（プレイ）では、どちらか一方のプレイヤーが勝利し、もう一方が敗北する。
CoLの論理演算子は、ゲームに対する演算として理解されます。ここでは、それらの演算の一部を非公式に概観します。簡略化のため、議論の領域は常にすべての自然数の集合、{0,1,2,...}であると仮定します。
否定演算子 ¬は、2 人のプレイヤーの役割を入れ替え、機械による手や勝利を環境による手や勝利に変え、その逆もまた同様です。例えば、チェスが白プレイヤーの視点から見たチェス（ただし引き分けはなし）であるならば、¬チェスは黒プレイヤーの視点から見た同じゲームです。
並列結合∧ ("pand") と並列分離∨ ("por") は、ゲームを並列的に組み合わせます。A ∧ BまたはA ∨ Bの連続は、2 つの結合での同時プレイです。マシンは、両方に勝てばA ∧ Bに勝ちます。マシンは、少なくとも 1 つに勝てばA ∨ Bに勝ちます。たとえば、チェス∨¬チェスは、白と黒でプレイする 2 つのボードで行われるゲームで、マシンのタスクは少なくとも 1 つのボードで勝つことです。このようなゲームは、対戦相手が誰であっても、一方のボードからもう一方のボードに相手の動きをコピーすることで簡単に勝つことができます。
並列含意演算子 → (「pimplication」) は、 A → B = ¬ A ∨ Bで定義されます。この操作の直感的な意味は、 B をAに還元すること 、つまり、攻撃者がBを解く限りAを解くことです。
並列量化子∧ ("pall") と∨ ("pexists") は、∧ xA ( x ) = A (0)∧ A (1)∧ A ( 2)∧... および ∨ xA ( x ) = A (0)∨ A (1)∨ A (2)∨... と定義できます。したがって、これらはA (0)、A (1)、A (2)、... がそれぞれ別のボード上で同時にプレイすることを意味します。マシンは、これらのゲームすべてに勝てば∧ xA ( x ) で勝ち、いくつかに勝てば∨ xA ( x ) で勝ちます。
一方、ブラインド量化子 ∀ ("blall") および ∃ ("blexists") は、シングルボードゲームを生成します。 ∀ xA ( x ) または ∃ xA ( x ) の実行は、Aの単一の実行です。マシンは、そのような実行がxのすべての (または少なくとも 1 つの) 可能な値に対してA ( x )の勝利実行である場合に∀ xA ( x ) (または ∃ xA ( x )) に勝ち、少なくとも 1 つの値に対してこれが真である場合に ∃ xA ( x ) に勝ちます。
これまで説明してきた演算子はすべて、基本的な（動きのない）ゲームに適用した場合、古典的な演算子とまったく同じように振る舞い、同じ原理を検証します。これが、CoLがこれらの演算子に古典論理と同じ記号を使用する理由です。しかし、これらの演算子を非基本的なゲームに適用すると、その振る舞いはもはや古典的ではありません。例えば、pが基本的なアトムでPが一般的なアトムである場合、p → p ∧ pは有効ですが、 P → P ∧ Pは有効ではありません。ただし、排中律P ∨¬ Pは有効のままです。同じ原理は、他の3種類の選言（選択、逐次、トグル）ではすべて無効です。
ゲームAとBの選択論理和 ⊔ ("chor") はA ⊔ Bと表記され、勝つためにはマシンが 2 つの論理和のうちの 1 つを選択し、選択したコンポーネントで勝つ必要があるゲームです。逐次論理和("sor") A ᐁ BはAとして始まり、マシンが「スイッチ」操作を行わない限りAとして終わります。スイッチ操作を行う場合はAは放棄され、ゲームは再開され、Bとして続きます。切り替え論理和("tor") A ⩛ Bでは、マシンはAとBを任意の有限回数切り替えることができます。各論理和演算子には、2 人のプレイヤーの役割を交換することによって得られる双対論理和があります。対応する量化子は、並列量化子の場合と同様に、無限論理和または無限論理和としてさらに定義できます。各種類の論理和は、並列含意 → の場合と同様に、対応する含意演算も誘導します。例えば、選択含意（「chimplication」）A ⊐ Bは、¬ A ⊔ Bと定義されます。
Aの並列再帰(「前再帰」) は、無限並列結合A ∧A∧A∧... として定義できます。逐次 (「s再帰」) およびトグル (「trecurrence」) タイプの再帰も同様に定義できます。
共再帰演算子は無限の選言として定義できます。最も強い種類の再帰である分岐再帰（「brecurrence」）⫰には、対応する論理積はありません。⫰ Aは、Aとして開始および進行するゲームです。ただし、いつでも環境は「複製」操作を行うことが許されており、これにより、 Aの現在の位置の 2 つのコピーが作成され、共通の過去を持つものの将来の展開が異なる可能性のある 2 つの並列スレッドにプレイが分割されます。同様に、環境は任意のスレッドの任意の位置をさらに複製することができ、これにより、Aのスレッドがますます多く作成されます。これらのスレッドは並列にプレイされ、マシンは⫰ Aで勝者となるために、すべてのスレッドでAに勝つ必要があります。分岐共再帰（「cobrecurrence」）⫯ は、「マシン」と「環境」を入れ替えることで対称的に定義されます。
それぞれの再帰は、対応する弱い含意と弱い否定を誘発する。前者はリム含意、後者は反駁と呼ばれる。分岐リム含意（「ブリム含意」）A ⟜ Bは⫰ A → Bに他ならず、Aの分岐反駁（「反駁」）はA ⟜ ⊥であり、⊥ は常に負ける基本ゲームである。他のすべての種類のリム含意と反駁についても同様である。
CoLの言語は、文献で確立された名称の有無にかかわらず、無数の多様な計算問題を体系的に記述する方法を提供する。以下にいくつかの例を示す。
fを単項関数とする。fを計算する問題は、 ⊓ x ⊔ y( y = f ( x ))と表される。CoL のセマンティクスによれば、これは環境が最初の操作 (「入力」) を行い、xの値mを選択するゲームである。直感的には、これは機械にf ( m ) の値を教えるように求めることに相当する。ゲームは⊔ y( y = f ( m )) と続く。今度は機械が操作 (「出力」) を行うことが期待され、yの値nを選択する必要がある。これは、nがf (m )の値であると述べることに相当する。ゲームは、 n = f ( m )という基本的な問題に帰着し、 nが実際にf ( m )の値である場合に限り、機械が勝利する。
p を単項述語とする。このとき、⊓ x ( p ( x )⊔¬ p ( x )) はpの判定 問題を表し、⊓ x ( p ( x )& ᐁ ¬ p ( x )) はpの半判定問題を表し、⊓ x ( p ( x )⩛¬ p ( x )) はpの再帰的近似問題を表す。
pとq を2 つの単項述語とする。このとき、 ⊓ x ( p ( x ) ⊔¬ p ( x )) ⟜ ⊓ x ( q ( x )⊔¬ q ( x )) は、 qをpにチューリング還元する 問題を表す( qがpにチューリング還元可能であるのは、対話型問題 ⊓ x ( p ( x )⊔¬ p ( x )) ⟜ ⊓ x ( q ( x )⊔¬ q ( x )) が計算可能である場合に限る)。⊓ x ( p ( x )⊔¬ p ( x )) → ⊓ x ( q ( x )⊔¬ q ( x )) は、pのオラクルを一度だけ照会できる、より強力なバージョンのチューリング還元に対して同じことを行う。⊓ x ⊔ y ( q ( x )↔ p ( y )) は、多対一で q を p に還元する問題に対しても同様の処理を行います。より複雑な式を用いることで、例えば「半決定問題 r を多対一で qを pに還元する問題にチューリング還元する」など、計算問題に関するあらゆる種類の無名ながらも潜在的に意味のある関係や操作を捉えることができます。機械の動作に時間や空間の制約を課すことで、こうした関係や操作の計算複雑性理論上の対応物も得られます。
CoLの様々な断片に対応する既知の演繹システムは、システム内の問題の証明から解（アルゴリズム）を自動的に抽出できるという共通の特性を持っています。この特性は、これらのシステムに基づくすべての応用理論にも受け継がれています。したがって、与えられた問題の解を見つけるには、それをCoLの言語で表現し、その表現の証明を見つけるだけで十分です。この現象を別の角度から見ると、CoLの式Gをプログラム仕様（目標）と考えることができます。すると、 Gの証明は、より正確には、その仕様を満たすプログラムに翻訳されます。証明自体が検証であるため、仕様が満たされていることを検証する必要はありません。
CoL に基づく応用理論の例としては、いわゆるクラリスメティクスがあります。これらは、1 階ペアノ算術PA が古典論理に基づいているのと同じ意味で CoL に基づく数論です。このようなシステムは通常、PA の保守的な拡張です。通常、すべてのペアノ公理を含み、後継関数の計算可能性を表す⊓ x ⊔ y ( y = x' ) のような 1 つまたは 2 つのペアノ以外の公理を追加します。通常、帰納法や内包法の構成的バージョンなどの 1 つまたは 2 つの非論理的な推論規則も持ちます。このような規則のルーチン的な変更により、1 つ以上の対話型計算複雑性クラスCを特徴付ける健全で完全なシステムを得ることができます。これは、問題がCに属するのは、その問題が理論に証明を持つ場合のみであるという意味です。したがって、このような理論は、アルゴリズム的な解法だけでなく、多項式時間や対数空間で実行される解法など、要求に応じて効率的な解法を見つけるためにも使用できます。すべての明算理論は同じ論理公準を共有しており、非論理公準のみが対象となる複雑性クラスによって異なる点に留意すべきである。同様の目標を持つ他のアプローチ（例えば、限定算術）との顕著な違いは、PAを弱めるのではなく拡張し、PAの完全な演繹力と利便性を維持している点にある。