经典可实现性中的存在性见证提取及通过否定翻译的方法

我们展示了如何使用Krivine的经典可实现性（其中经典证明被解释为带有call/cc控制算子的lambda项）从经典证明中提取存在性见证。我们首先回顾了经典可实现性的基本框架（在经典二阶算术中），并展示了如何用原始数字扩展它以加速计算。然后，我们展示了如何在此框架中执行见证提取，讨论了依赖于存在公式形状的几种技术。特别地，我们证明了在Sigma01情况下，Krivine的见证提取方法通过一个合适的否定翻译简化为Friedman的方法，从而得到直觉主义二阶算术。最后，我们讨论了使用call/cc而非否定翻译的优势，特别是从实现的角度来看。