実現可能性 (論理学)

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

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

実現可能性は、直観主義的証明可能性への洞察を与えるだけでなく、直観主義理論における選言文特性と存在文特性（英語: Disjunction and existence properties）の証明や、プルーフマイニングのように証明からプログラムの抽出のために適用できる。また、実現可能性トポス（realizability topos）を介したトポス理論とも関連している。

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

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

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

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

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

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

このメソッドのさらなる解析は、HAが選言文特性と存在文特性（英語: Disjunction and existence properties）を持つことの証明に使われる。

• もしHAで $\exists x.A(x)$ が証明できるなら、 HAで A(n) が証明できるような自然数 n が存在する。
• HAで $A\lor B$ が証明できるなら、HAで A が証明できるか、またはHAで B が証明できる。

その後の展開

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

$(A\rightarrow \exists x.P(x))\rightarrow \exists x.(A\rightarrow P(x))$ .

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

応用

実現可能性はプルーフマイニングで使用される方法の 1 つであり、一見非構成的な数学的証明から具体的な「プログラム」を抽出する。 Coqなどのいくつかの証明支援系（英語: Proof assistant）には、実現可能性を使用したプログラム抽出が実装されている。

関連項目

• カリー・ハワード同型対応
• ダイアレクティカ解釈
• ハロップ式

参考資料

• Birkedal, Lars; van Oosten, Jaap (2002). “Relative and modified relative realizability”. Annals of Pure and Applied Logic 118: 115-132. doi:10.1016/S0168-0072(01)00122-1. ISSN 0168-0072. 
• Kleene, S. C. (1945). “On the interpretation of intuitionistic number theory”. Journal of Symbolic Logic 10 (4): 109–124. doi:10.2307/2269016. JSTOR 2269016. 
• Kleene, S. C. (1973). "Realizability: a retrospective survey" from Mathias, A. R. D.; Hartley Rogers (1973). Cambridge Summer School in Mathematical Logic : held in Cambridge/England, August 1–21, 1971. Berlin: Springer. ISBN 3-540-05569-X Cambridge 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.
• van Oosten, Jaap (2002). “Realizability: a historical essay”. Mathematical Structures in Computer Science (Cambridge University Press) 12: 239-263. doi:10.1017/S0960129502003626. ISSN 0960-1295. 
• Rose, G. F. (1953). “Propositional calculus and realizability”. Transactions of the American Mathematical Society 75 (1): 1–19. doi:10.2307/1990776. JSTOR 1990776. 

外部リンク

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