可计算性逻辑

可计算性逻辑(CoL)是一个研究计划和数学框架，旨在将逻辑重新发展为一个系统的可计算性形式理论，与作为真理形式理论的经典逻辑相反。它是由GiorgiJaparidze在2003年提出并如此命名的。在经典逻辑中，公式代表真/假语句。在CoL中，公式代表计算问题。在经典逻辑中，一个公式的有效性只取决于它的形式，而不取决于它的意义。在CoL中，有效性意味着总是可计算的。更一般地说，经典逻辑告诉我们，当一个给定的语句的真理总是来自于一组给定的其他语句的真理。类似地，CoL告诉我们，当一个给定的问题A的可计算性总是从其他给定的问题B1,...,Bn的可计算性而来时。此外，它还提供了一种统一的方法，从任何已知的B1,...,Bn的解中实际构造出这样一个A的解(算法)。CoL在其最一般的互动意义上制定了计算问题。CoL将计算问题定义为一个机器与环境的博弈。如果有一台机器能够在环境的每一种可能的行为中赢得游戏，那么这样的问题就是可计算的。这样的游戏机将丘吉尔-图灵论推广到互动层面。真理的经典概念被证明是可计算性的一个特殊的、零互动度的案例。这使得古典逻辑成为CoL的一个特殊片段。因此，CoL是经典逻辑的一个保守的扩展。可计算性逻辑比经典逻辑更具表达性、建设性和计算意义。除了经典逻辑，有利于独立的(IF)逻辑以及线性逻辑和直觉逻辑的某些适当的扩展也被证明是CoL的自然片段。因此，有意义的直觉性真理、线性逻辑真理和中频逻辑真理的概念可以从CoL的语义中导出。

CoL系统地回答了什么可以被计算以及如何计算的基本问题；因此CoL有很多应用，比如构造性应用理论、知识库系统、计划和行动的系统。在这些应用中，到目前为止只有在建构性应用理论中的应用被广泛探索：一系列基于CoL的数论，被称为clearithmetics，被构建为在计算和复杂性理论上有意义的替代基于古典逻辑的Peano算术及其变体，如有界算术系统。传统的证明系统，如自然演绎和序列微积分，不足以对CoL的非微观片段进行公理化。这就需要开发其他更普遍、更灵活的证明方法，如圆周率计算。

CoL的完整语言扩展了经典一阶逻辑的语言。它的逻辑词汇有几种连接词、非连接词、量词、暗示、否定和所谓的递归运算符。这个集合包括经典逻辑的所有连接词和量词。该语言也有两种非逻辑原子：基本原子和一般原子。基本原子，除了经典逻辑的原子之外，还代表基本问题，即没有任何动作的游戏，当真时机器自动获胜，当假时机器自动失败。另一方面，一般原子可以被解释为任何游戏，无论是基本的还是非基本的。在语义和句法上，古典逻辑不过是CoL的片段，通过在其语言中禁止一般原子，禁止除¬,∧,∨,→,∀,∃之外的所有运算符得到。Japaridze多次指出，CoL的语言是开放式的，可以进一步扩展。由于这种语言的可表达性，CoL的进展，如构建公理化或建立基于CoL的应用理论，通常只限于该语言的一个或另一个适当的片段。

CoL语义学的基础游戏被称为静态游戏。这种游戏没有回合顺序；一个玩家总是可以在其他玩家思考时移动。然而，静态游戏从来不会因为玩家思考时间过长而受到惩罚（延迟自己的行动），所以这种游戏从来不会成为速度的竞争。所有的基本游戏都自动是静态的，因此允许成为一般原子的解释的游戏也是如此。在静态游戏中，有两个玩家：机器和环境。机器只能遵循算法策略，而对环境的行为没有任何限制。每一次运行（游戏）都是由其中一个玩家获胜，另一个玩家失败。CoL的逻辑运算符被理解为对游戏的操作。这里我们非正式地调查了其中的一些操作。为了简单起见，我们假设话语域总是所有自然数的集合。{0,1,2,...}.否定(not)的操作¬是将"1"和"2"的角色互换。