查看“︁可实现性”︁的源代码

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

==起源==

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

==后来发展==

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

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

==计算机科学应用==

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

==引用==

* {{cite book en| last = Birkedal | first = Lars | coauthors = Jaap van Oosten | year = 2000 | title = [http://www.itu.dk/people/birkedal/papers/relmrr.ps.gz Relative and modified relative realizability]}}

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

* {{cite journal en| last = Kleene | first = S. C. | year = 1945 | title = On the interpretation of intuitionistic number theory | journal = Journal of Symbolic Logic | volume = 10 | pages = 109-124}}

* Kleene, S. C. (1973). "Realizability: a retrospective survey" from {{cite book | last = Mathias | first = A. R. D. | coauthors = Hartley Rogers | title = Cambridge Summer School in Mathematical Logic : held in Cambridge/England, August 1-21, 1971 | year = 1973 | location = Berlin | publisher = Springer | id = ISBN 354005569X}}, pp. 95-112.

* {{cite book en| last = Oosten | first = Jaap van | year = 2000 | title = [http://www.math.uu.nl/people/jvoosten/realizability/history.ps.gz Realizability: An Historical Essay]}}

* {{cite journal en| last = Rose | first = G. F. | year = 1953 | title = Propositional calculus and realizability | journal = Transactions of the American Mathematical Society | volume = 75 | pages = 1-19}}

==注释==
<references/>

[[Category:证明论]]