実現可能性

数理論理学において、実現可能性とは、構成的証明を研究し、そこから追加情報を抽出するために使用される証明理論における一連の方法である。 ^{[1]形式理論の}式は、「実現者」と呼ばれるオブジェクトによって「実現」され、実現者に関する知識が式の真実性に関する知識を与える。実現可能性には多くのバリエーションがあり、正確にどのクラスの式を研究し、どのオブジェクトが実現者であるかは、バリエーションごとに異なる。

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

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

クリーネの実現可能性のオリジナル版では、自然数をヘイティング算術の式の実現子として使用している。いくつかの表記法が必要である。まず、固定された原始的な再帰的ペアリング関数を使用して、順序付きペア ( n、m ) を単一の数として扱う。次に、各自然数nに対して、 φ _{n は}インデックスnを持つ計算可能な関数である。次の節は、自然数nと式Aの間の「 n はA を実現する」という関係をヘイティング算術の言語で定義するために使用される。これはクリーネの 1945 年の実現可能性関係として知られる。^[2]

• 任意の数n は、 s = tが真である場合に限り、原子式s = tを実現します。したがって、すべての数は真の方程式を実現し、偽の方程式を実現する数はありません。
• ペア ( n、m ) が式A ∧ B を実現するのは、 n がA を実現し、m がB を実現する場合のみです。したがって、連言の実現子は、連言の実現子のペアです。
• ペア ( n、m ) が式A ∨ Bを実現するのは、次の条件が満たされる場合のみです。nは 0 または 1 であり、nが 0 の場合、 m はA を実現します。 nが 1 の場合、 m はB を実現します。したがって、選言の実現子は、明示的に選言の 1 つ ( nを使用) を選択し、それに対する実現子 ( mを使用) を提供します。
• 数n が式A → B を実現するのは、 A を実現するすべてのmに対してφ _n ( m )がB を実現する場合のみです。したがって、含意の実現子は、仮説の任意の実現子を取り、結論の実現子を生成する計算可能な関数に対応します。
• ペア ( n , m ) が式 (∃ x ) A ( x ) を実現するのは、 m がA ( n )の実現子である場合のみです。したがって、存在式の実現子は、量指定子の明示的な証拠と、その証拠でインスタンス化された式の実現子を生成します。
• 数n が式 (∀ x ) A ( x ) を実現するのは、すべてのmに対してφ _n ( m ) が定義され、A ( m ) を実現する場合のみです。したがって、普遍的なステートメントの実現子は、各mに対して、 mでインスタンス化された式の実現子を生成する計算可能な関数です。

この定義により、次の定理が得られる: ^[3]

A をHeyting 算術 (HA) の文とします。HA が A を証明する場合、nがA を実現するようなnが存在します。

一方、実現可能ではあるがHAでは証明できない古典的な定理（命題式スキームさえも）があり、これはローズによって初めて確立された事実です。^[4]そのため、実現可能性は直観主義的推論を正確に反映するものではありません。

この方法をさらに分析すると、HAが「選言と存在の性質」を持っていることが証明できる。^[5]

• HAが文(∃ x ) A ( x )を証明する場合、HAがA ( n )を証明するnが存在する。
• HA が文A ∨ B を証明する場合、 HA はAを証明するか、 HA はB を証明します。

ハロップの公式を使用すると、さらに多くのこのような特性が得られます。

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

${\displaystyle (A\rightarrow \exists x\;P(x))\rightarrow \exists x\;(A\rightarrow P(x))}$。

相対的実現可能性^{[6]は、必ずしも計算可能ではないデータ構造の}計算可能または計算可能列挙可能要素の直観主義的分析であり、例えば、実数がデジタルコンピュータシステム上で近似値しか取れない場合の、すべての実数に対する計算可能な演算などである。

古典的実現可能性はクリヴィン^[7]によって導入され、実現可能性を古典論理に拡張した。さらに、ツェルメロ-フランケル集合論の公理を実現する。コーエンの強制の一般化として理解され、集合論の新しいモデルを提供するために使用された。^[8]

線形実現可能性は、実現可能性技術を線形論理に拡張したものです。この用語はSeiller ^[9]によって造られ、相互作用モデルの幾何学、^[10] ルディックス、^{[11]相互作用グラフモデル[12]}などのいくつかの構造を包含しています。

実現可能性は、一見非構成的な数学的証明から具体的な「プログラム」を抽出するために証明マイニングで使用される方法の 1 つです。実現可能性を使用したプログラム抽出は、 Coqなどの一部の証明支援ツールに実装されています。

• カリー・ハワード書簡
• 弁証法の解釈
• ハロップ式

• ビルケダル、ラース。ヤープ・ファン・オーステン (2000)。相対的および修正された相対的実現可能性。
• Kreisel G. (1959)。「有限型の構成的関数による解析の解釈」、A. Heyting 編『数学における構成性』、北ホラント、pp. 101–128。
• Kleene, SC (1945). 「直観主義的数論の解釈について」. Journal of Symbolic Logic . 10 (4): 109–124. doi :10.2307/2269016. JSTOR  2269016.
• Kleene, SC (1973)。「実現可能性: 回顧的調査」Mathias, ARD、Hartley Rogers (1973) より。ケンブリッジ数学論理夏期学校: 1971 年 8 月 1 日から 21 日までイギリス/ケンブリッジで開催。ベルリン: Springer。ISBN 3-540-05569-X。、95～112ページ。
• ヴァン・オーステン、ヤープ (2000)。実現可能性: 歴史的エッセイ。
• Rose, GF (1953). 「命題計算と実現可能性」.アメリカ数学会誌. 75 (1): 1–19. doi : 10.2307/1990776 . JSTOR  1990776.

• 実現可能性 実現可能性と関連トピックに関する最近の論文へのリンクのコレクション。