从真理到可计算性 I

最近发起的称为可计算性逻辑的方法是一种交互式计算的形式理论。关于该主题的综合在线资源请参见 http://www.cis.upenn.edu/~giorgi/cl.html 。本文给出了演绎系统 CL3 的可靠性与完备性证明，该系统对可计算性逻辑中最基本的一阶片段（称为有限深度、基本基片段）进行了公理化。该结果的潜在应用领域包括交互式计算理论、构造性应用理论、知识库系统、资源受限规划与行动系统。本文是自包含的，因为它重新介绍了所有相关定义以及主要动机。