可实现性

可实现性是可用来处理关于公式的信息而不是关于公式的证明的那部分证明论。^[1]自然数n被称为实现了自然数算术的语言中一个陈述。其他逻辑和数学陈述也是可实现的，假如提供了解释合式公式一种方法，而不用借助达成这些公式的证明。

起源

斯蒂芬·科尔·克莱尼在1945年介入了可实现性的概念，寄希望于它成为直觉逻辑推理的忠实典范，^[2]但这个设想最初由Rose反证了一个可实现的命题公式的例子，它在直觉演算中是不可证明的。^[3]可实现性似乎由于它的复杂度而难于公理化，但它可以通过高阶Heyting算术（HA）来达成。

后来发展

改进可实现性^[4]使用有类型lambda演算作为语言实现者。改进可实现性是展示马尔科夫原理在直觉逻辑中不可推导的一种方式。正相反，它允许构造性的证实前提的独立性原理：${\displaystyle (\neg A\rightarrow \exists x\;P(x))\rightarrow \exists x\;(\neg A\rightarrow P(x))}$ 。

相对可实现性^[5]是非必需可计算的数据结构的递归或递归可枚举元素的直觉主义分析，比如在实数在数字计算机系统上只能近似表示的时候在所有实数上的可计算的运算。

计算机科学应用

改进可实现性证实了实施于某些证明辅助工具比如Coq中的“证明提取”过程。

引用

• Birkedal, Lars; Jaap van Oosten. Relative and modified relative realizability. 2000.  引文使用过时参数coauthors (帮助); 外部链接存在于|title= (帮助)

• 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.  引文使用过时参数coauthors (帮助), pp. 95-112.

• Oosten, Jaap van. Realizability: An Historical Essay. 2000.  外部链接存在于|title= (帮助)

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

注释

1. Oosten, pp. 3-5
2. Kleene (1945)
3. Rose
4. Kreisel
5. Birkedal