可實現性

可實現性是可用來處理關於公式的信息而不是關於公式的證明的那部分證明論。自然數n被稱為實現了自然數算術的語言中一個陳述。其他邏輯和數學陳述也是可實現的，假如提供了解釋合式公式一種方法，而不用藉助達成這些公式的證明。

起源

史蒂芬·科爾·克萊尼在1945年介入了可實現性的概念，寄希望於它成為直覺邏輯推理的忠實典範，但這個設想最初由Rose反證了一個可實現的命題公式的例子，它在直覺演算中是不可證明的。可實現性似乎由於它的複雜度而難於公理化，但它可以通過高階Heyting算術（HA）來達成。

後來發展

改進可實現性使用有類型lambda演算作為語言實現者。改進可實現性是展示馬爾科夫原理在直覺邏輯中不可推導的一種方式。正相反，它允許構造性的證實前提的獨立性原理：$(\neg A\rightarrow \exists x\;P(x))\rightarrow \exists x\;(\neg A\rightarrow P(x))$。

相對可實現性是非必需可計算的資料結構的遞歸或遞歸可枚舉元素的直覺主義分析，比如在實數在數字計算機系統上只能近似表示的時候在所有實數上的可計算的運算。

計算機科學應用

改進可實現性證實了實施於某些證明輔助工具比如Coq中的「證明提取」過程。

引用

• Birkedal, Lars; Jaap van Oosten. Relative and modified relative realizability. 2000. 

• 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.

• Kleene, S. C. On the interpretation of intuitionistic number theory. Journal of Symbolic Logic. 1945, 10: 109–124. 

• Kleene, S. C. (1973). "Realizability: a retrospective survey" from Mathias, A. R. D.; Hartley Rogers. Cambridge Summer School in Mathematical Logic : held in Cambridge/England, August 1-21, 1971. Berlin: Springer. 1973. ISBN 354005569X.  , pp. 95-112.

• Oosten, Jaap van. Realizability: An Historical Essay. 2000. 

• Rose, G. F. Propositional calculus and realizability. Transactions of the American Mathematical Society. 1953, 75: 1–19.