(1) 阅读 (1144)

可计算性逻辑 编辑

词条创建者 匿名用户

可计算性逻辑

编辑

可计算性逻辑(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"的角色互换。


内容由匿名用户提供,本内容不代表vibaike.com立场,内容投诉举报请联系vibaike.com客服。如若转载,请注明出处:https://vibaike.com/167690/

发表评论

登录后才能评论

词条目录
  1. 可计算性逻辑
  2. 可计算性逻辑的语言
  3. 语义学

轻触这里

关闭目录

目录