実現可能性 (論理学)

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

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

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

例：自然数による実現可能性

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

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

この定義により、次の定理が得られるテンプレート:Sfn：

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

一方で、実現されるがHAで証明可能でない論理式が存在する。この事実はローズによってテンプレート:要検証テンプレート:Sfn。

このメソッドのさらなる解析は、HAが選言文特性とテンプレート:日本語版にない記事リンクを持つことの証明に使われるテンプレート:Sfn。

• もしHAで $\mathrm{\exists }x.A(x)$ が証明できるなら、 HAで テンプレート:Math が証明できるような自然数 テンプレート:Mvar が存在する。
• HAで $A\vee B$ が証明できるなら、HAで テンプレート:Mvar が証明できるか、またはHAで テンプレート:Mvar が証明できる。

その後の展開

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

$(A\to \mathrm{\exists }x.P(x))\to \mathrm{\exists }x.(A\to P(x))$ .

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

応用

実現可能性はテンプレート:定訳なしで使用される方法の 1 つであり、一見非構成的な数学的証明から具体的な「プログラム」を抽出する。 Coqなどのいくつかのテンプレート:日本語版にない記事リンクには、実現可能性を使用したプログラム抽出が実装されている。

関連項目

• カリー・ハワード同型対応
• テンプレート:仮リンク
• テンプレート:仮リンク

参考資料

• テンプレート:Cite journal
• テンプレート:Cite journal
• Kleene, S. C. (1973). "Realizability: a retrospective survey" from テンプレート:Cite bookCambridge Summer School in Mathematical Logic : held in Cambridge/England, August 1–21, 1971. Berlin: Springer. ISBN <bdi>3-540-05569-X</bdi>., pp. 95–112.
• Kreisel G. (1959). "Interpretation of Analysis by Means of Constructive Functionals of Finite Types", in: Constructivity in Mathematics, edited by A. Heyting, North-Holland, pp. 101–128.
• テンプレート:Cite journal
• テンプレート:Cite journal

外部リンク

• Realizability Jaap van Oostenによる、実現可能性および関連トピックに関する論文へのリンクのコレクション。