Realizability (original) (raw)

• Browse using
• Formats
• Faceted Browser
• Sparql Endpoint

数理論理学において実現可能性（realizability）とは、構成的証明から追加情報を抽出するために使用される方法の集まりである。形式理論の論理式は「実現子」（realizer）と呼ばれるオブジェクトによって「実現」され、実現子の持つ情報が論理式の真理値についての情報を提供する。実現可能性には多くのバリエーションがあり、どの論理式のクラスが研究され、どのようなオブジェクトが実現子であるかは、それらバリエーションごとに異なる。 実現可能性は、直観主義論理のの形式化と見なせる。実現可能性を考えるとき、「証明」についての観念（BHK解釈では未定義のまま）は「実現子」についての形式的な観念に置き換えられる。ほとんどのバリエーションにおいて実現可能性は、研究対象の形式体系で証明可能なステートメントはすべて実現可能であるという定理から始まる。ただし、実現子は論理式について通常、形式的証明が直接提供するよりも多くの情報を提供する。 実現可能性は、直観主義的証明可能性への洞察を与えるだけでなく、直観主義理論におけると（英語: Disjunction and existence properties）の証明や、プルーフマイニングのように証明からプログラムの抽出のために適用できる。また、実現可能性トポス（realizability topos）を介したトポス理論とも関連している。