首页> 外文期刊>Journal of Symbolic Logic >Towards applied theories based on computability logic
【24h】

Towards applied theories based on computability logic

机译:基于可计算性逻辑的应用理论

获取原文
获取原文并翻译 | 示例
           

摘要

Computability logic (CL) is a recently launched program for redeveloping logic as a formal theory of computability, as opposed to the formal theory of truth that logic has more traditionally been. Formulas in it represent computational problems, "truth" means existence of an algorithmic solution, and proofs encode such solutions. Within the line of research devoted to finding axiomatizations for ever more expressive fragments of CL, the present paper introduces a new deductive system CL12 and proves its soundness and completeness with respect to the semantics of CL. Conservatively extending classical predicate calculus and offering considerable additional expressive and deductive power, CL12 presents a reasonable, computationally meaningful, constructive alternative to classical logic as a basis for applied theories. To obtain a model example of such theories, this paper rebuilds the traditional, classical-logicbased Peano arithmetic into a computability-logic-based counterpart. Among the purposes of the present contribution is to provide a starting point for what, as the author wishes to hope, might become a new line of research with a potential of interesting findings-an exploration of the presumably quite unusual metatheory of CL-based arithmetic and other CL-based applied systems.
机译:可计算性逻辑(CL)是最近启动的程序,用于将逻辑重新开发为可计算性的形式理论,这与逻辑传统上的形式形式真理理论相反。其中的公式表示计算问题,“真相”表示算法解的存在,并且证明对这些解进行了编码。在致力于为CL的更多表达片段进行公理化的研究范围内,本文引入了一种新的演绎系统CL12并就CL的语义证明了其健全性和完整性。 CL12保守地扩展了经典谓词演算,并提供了可观的表达和演绎能力,它为经典逻辑提供了合理,在计算上有意义的,建设性的替代方法,可作为应用理论的基础。为了获得此类理论的模型实例,本文将传统的,基于经典逻辑的Peano算法重建为基于可计算逻辑的对等算法。本贡献的目的之一是为作者希望希望成为具有潜在有趣发现潜力的新研究领域提供一个起点-探索基于CL的算术的非常不寻常的元理论和其他基于CL的应用系统。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号