実現可能性 (論理学)

数理論理学において実現可能性（）とは、構成的証明から追加情報を抽出するために使用される方法の集まりである。形式理論の論理式は「実現子」（）と呼ばれるオブジェクトによって「実現」され、実現子の持つ情報が論理式の真理値についての情報を提供する。実現可能性には多くのバリエーションがあり、どの論理式のクラスが研究され、どのようなオブジェクトが実現子であるかは、それらバリエーションごとに異なる。
実現可能性は、直観主義論理のの形式化と見なせる。実現可能性を考えるとき、「証明」についての観念（BHK解釈では未定義のまま）は「実現子」についての形式的な観念に置き換えられる。ほとんどのバリエーションにおいて実現可能性は、研究対象の形式体系で証明可能なステートメントはすべて実現可能であるという定理から始まる。ただし、実現子は論理式について通常、形式的証明が直接提供するよりも多くの情報を提供する。
実現可能性は、直観主義的証明可能性への洞察を与えるだけでなく、直観主義理論における選言文特性との証明や、のように証明からプログラムの抽出のために適用できる。また、実現可能性トポス（）を介したトポス理論とも関連している。
例：自然数による実現可能性.
クリーネによるオリジナル版の実現可能性の定義は、の論理式の実現子として自然数を用いる。自然数 と式 の間の関係「 が"" を実現する」を、ハイティング算術の言語で定義する。 ただし以下において、順序対 はある固定された有効な対関数を使うことで単一の数値として扱う。また、各自然数 に対して はインデックス の計算可能関数（すなわち、何らかの方法で列挙された計算可能関数の列formula_1における 番目の関数）である。
この定義により、次の定理が得られる：
一方で、実現されるがHAで証明可能でない論理式が存在する。この事実はローズによって。
このメソッドのさらなる解析は、HAが選言文特性とを持つことの証明に使われる。
その後の展開.
クライゼルは、型付きラムダ計算を実現子の言語として使用する、修正実現可能性（）を導入した。修正実現可能性は、が直観主義論理では導き出せないことを示す 1 つの方法である。一方で、以下に示す前提の独立性の原則を構成的に正当化することができる：
相対的実現可能性は、実数に対する計算可能な操作のような、必ずしも計算可能ではないデータ構造に対する再帰的または再帰的列挙可能な要素の直観主義的な分析である。 
応用.
実現可能性はで使用される方法の 1 つであり、一見非構成的な数学的証明から具体的な「プログラム」を抽出する。 Coqなどのいくつかのには、実現可能性を使用したプログラム抽出が実装されている。