実現可能性 (論理学)のソースを表示

{{翻訳直後|1=[https://en.wikipedia.org/w/index.php?oldid=971135357]|date=2021年6月}}

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

実現可能性は、[[直観主義論理]]の{{仮リンク|ブラウワー-ハイティング-コルモゴロフ解釈|en|Brouwer–Heyting–Kolmogorov interpretation|label=BHK解釈}}の形式化と見なせる。実現可能性を考えるとき、「証明」についての観念（BHK解釈では未定義のまま）は「実現子」についての形式的な観念に置き換えられる。ほとんどのバリエーションにおいて実現可能性は、研究対象の形式体系で証明可能なステートメントはすべて実現可能であるという定理から始まる。ただし、実現子は論理式について通常、形式的証明が直接提供するよりも多くの情報を提供する。

実現可能性は、直観主義的証明可能性への洞察を与えるだけでなく、直観主義理論における[[選言文特性]]と{{日本語版にない記事リンク|存在文特性|en|Disjunction and existence properties}}の証明や、{{定訳なし|en|プルーフマイニング|link=Proof mining}}のように証明からプログラムの抽出のために適用できる。また、実現可能性トポス（{{Lang|en|realizability topos}}）を介した[[トポス (数学)|トポス理論]]とも関連している。

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

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

この定義により、次の定理が得られる{{Sfn|van Oosten|2002|p=245}}：

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

一方で、実現されるが'''HA'''で証明可能でない論理式が存在する。この事実はローズによって{{要検証|初めて示された|date=2021年6月}}{{Sfn|Rose|1953}}。

このメソッドのさらなる解析は、'''HA'''が[[選言文特性]]と{{日本語版にない記事リンク|存在文特性|en|Disjunction and existence properties}}を持つことの証明に使われる{{Sfn|van Oosten|2002|p=244}}。

* もし'''HA'''で <math>\exists x.A(x)</math> が証明できるなら、 '''HA'''で {{Math|''A''(''n'')}} が証明できるような自然数 {{Mvar|n}} が存在する。
* '''HA'''で <math>A\lor B</math> が証明できるなら、'''HA'''で {{Mvar|A}} が証明できるか、または'''HA'''で {{Mvar|B}} が証明できる。

== その後の展開 ==
[[ゲオルク・クライゼル|クライゼル]]は、[[型付きラムダ計算]]を実現子の言語として使用する、'''修正実現可能性'''（{{Lang|en|modified realizability}}）を導入した。修正実現可能性は、{{仮リンク|マルコフの原理|en|Markov's principle}}が直観主義論理では導き出せないことを示す 1 つの方法である。一方で、以下に示す前提の独立性の原則を構成的に正当化することができる：

: <math>(A \rightarrow \exists x.P(x)) \rightarrow \exists x.(A \rightarrow P(x))</math> .

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

== 応用 ==
実現可能性は{{定訳なし|en|プルーフマイニング|link=Proof mining}}で使用される方法の 1 つであり、一見非構成的な数学的証明から具体的な「プログラム」を抽出する。 [[Coq]]などのいくつかの{{日本語版にない記事リンク|定理証明支援系|en|Proof assistant|label=証明支援系|preserve=1}}には、実現可能性を使用したプログラム抽出が実装されている。

== 関連項目 ==

* [[カリー＝ハワード同型対応|カリー・ハワード同型対応]]
* {{仮リンク|ダイアレクティカ解釈|en|Dialectica interpretation}}
* {{仮リンク|ハロップ式|en|Harrop formula}}

== 脚注 ==
{{Reflist}}

== 参考資料 ==

* {{Cite journal|last=Birkedal|first=Lars|last2=van Oosten|first2=Jaap|year=2002|title=Relative and modified relative realizability|journal=Annals of Pure and Applied Logic|volume=118|pages=115-132|ref=harv|DOI=10.1016/S0168-0072(01)00122-1|ISSN=0168-0072}}
* {{Cite journal|last=Kleene|first=S. C.|year=1945|title=On the interpretation of intuitionistic number theory|journal=Journal of Symbolic Logic|volume=10|issue=4|pages=109–124|DOI=10.2307/2269016|JSTOR=2269016}}
* Kleene, S. C. (1973). "Realizability: a retrospective survey" from {{Cite book|last=Mathias|first=A. R. D.|last2=Hartley Rogers|title=Cambridge Summer School in Mathematical Logic : held in Cambridge/England, August 1–21, 1971|year=1973|location=Berlin|publisher=Springer|isbn=3-540-05569-X}}<cite class="citation book cs1" id="CITEREFMathiasHartley_Rogers1973">''Cambridge Summer School in Mathematical Logic : held in Cambridge/England, August 1–21, 1971''. Berlin: Springer. </cite><cite class="citation book cs1" id="CITEREFMathiasHartley_Rogers1973">[[ISBN]]&nbsp;<nowiki><bdi>3-540-05569-X</bdi></nowiki>.</cite>, pp.&nbsp;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.&nbsp;101–128.
* {{Cite journal|last=van Oosten|first=Jaap|year=2002|title=Realizability: a historical essay|journal=Mathematical Structures in Computer Science|volume=12|pages=239-263|publisher=Cambridge University Press|ref=harv|DOI=10.1017/S0960129502003626|ISSN=0960-1295}}
* {{Cite journal|last=Rose|first=G. F.|year=1953|title=Propositional calculus and realizability|journal=Transactions of the American Mathematical Society|volume=75|issue=1|pages=1–19|ref=harv|DOI=10.2307/1990776|JSTOR=1990776}}

== 外部リンク ==

* [http://www.math.uu.nl/people/jvoosten/realizability.html Realizability] Jaap van Oostenによる、実現可能性および関連トピックに関する論文へのリンクのコレクション。

{{DEFAULTSORT:しつけんかのうせい}}
[[Category:構成主義 (数学)]]
[[Category:証明論]]
[[Category:数学に関する記事]]