実現可能性 (論理学)

数理論理学において実現可能性（）とは、構成的証明から追加情報を抽出するために使用される方法の集まりである。形式理論の論理式は「実現子」（）と呼ばれるオブジェクトによって「実現」され、実現子の持つ情報が論理式の真理値についての情報を提供する。実現可能性には多くのバリエーションがあり、どの論理式のクラスが研究され、どのようなオブジェクトが実現子であるかは、それらバリエーションごとに異なる。

実現可能性は、直観主義論理のの形式化と見なせる。実現可能性を考えるとき、「証明」についての観念（BHK解釈では未定義のまま）は「実現子」についての形式的な観念に置き換えられる。ほとんどのバリエーションにおいて実現可能性は、研究対象の形式体系で証明可能なステートメントはすべて実現可能であるという定理から始まる。ただし、実現子は論理式について通常、形式的証明が直接提供するよりも多くの情報を提供する。

実現可能性は、直観主義的証明可能性への洞察を与えるだけでなく、直観主義理論における選言文特性との証明や、のように証明からプログラムの抽出のために適用できる。また、実現可能性トポス（）を介したトポス理論とも関連している。

例：自然数による実現可能性クリーネによるオリジナル版の実現可能性の定義は、の論理式の実現子として自然数を用いる。自然数と式の間の関係「がを実現する」を、ハイティング算術の言語で定義する。ただし以下において、順序対はある固定された有効な対関数を使うことで単一の数値として扱う。また、各自然数に対してはインデックスの計算可能関数（すなわち、何らかの方法で列挙された計算可能関数の列における番目の関数）である。

自然数が原子論理式を実現するとは、が真であることと同値。従って、任意の自然数は恒真な等式を実現し、また矛盾した等式を実現する自然数はない。順序対が論理式を実現するとは、がを実現して、かつがを実現することと同値。つまり、連言の実現子とはそれを構成する各式の実現子の対である。順序対が論理式を実現するとは、が 0 または 1 で、かつが 0 ならばはを実現して、が 1 ならばはを実現することと同値。従って、選言の実現子はそれを構成する式のどちらかを明示的に（で）指してその実現子を（で）提供するものである。自然数が論理式を実現するとは、を実現する任意のについてがを実現することと同値である。従って、含意の実現子は仮定となる式の実現子を引数に取って帰結となる式の実現子を返す計算可能関数とみなせる。順序対が論理式を実現するとは、がの実現子であることと同値である。すなわち、存在文の実現子はその存在量化についての明示的な証拠を、それに裏打ちされた論理式の実現子と共に提供する。自然数が論理式を実現するとは、任意のについてが定義されていて、かつがを実現することと同値である。従って、全称文の実現子は自然数に対してそれによるインスタンスの実現子を提供する計算可能関数とみなせる。

この定義により、次の定理が得られる：

をハイティング算術 (HA) の文とする。HAでが証明できるならば、HAでを実現するような自然数が存在することが証明できる。

一方で、実現されるがHAで証明可能でない論理式が存在する。この事実はローズによって。

このメソッドのさらなる解析は、HAが選言文特性とを持つことの証明に使われる。

もしHAでが証明できるなら、 HAでが証明できるような自然数が存在する。 HAでが証明できるなら、HAでが証明できるか、またはHAでが証明できる。

その後の展開クライゼルは、型付きラムダ計算を実現子の言語として使用する、修正実現可能性（）を導入した。修正実現可能性は、が直観主義論理では導き出せないことを示す 1 つの方法である。一方で、以下に示す前提の独立性の原則を構成的に正当化することができる：

相対的実現可能性は、実数に対する計算可能な操作のような、必ずしも計算可能ではないデータ構造に対する再帰的または再帰的列挙可能な要素の直観主義的な分析である。

応用実現可能性はで使用される方法の 1 つであり、一見非構成的な数学的証明から具体的な「プログラム」を抽出する。 Coqなどのいくつかのには、実現可能性を使用したプログラム抽出が実装されている。

実現可能性 (論理学)

Źródło i licencja