Cirquent calculus is a proof system with inherent ability to account for sharing subcomponents in logical expressions. Within its framework, this article constructs an axiomatization CL18 of the basic propositional fragment of computability logic the game-semantically conceived logic of computational resources and tasks. The nonlogical atoms of this fragment represent arbitrary so called static games, and the connectives of its logical vocabulary are negation and the parallel and choice versions of conjunction and disjunction. The main technical result of the article is a proof of the soundness and completeness of CL18 with respect to the semantics of computability logic.
翻译:电路演算是一种能够自然处理逻辑表达式中子组件共享的证明系统。本文在其框架内,构建了可计算性逻辑——一种基于博弈语义、关于计算资源与任务的逻辑——的基本命题片段的一个公理化系统CL18。该片段的非逻辑原子表示任意的所谓静态博弈,其逻辑词汇中的连接词包括否定、以及合取与析取的并行版本和选择版本。本文的主要技术结果是证明了CL18相对于可计算性逻辑语义的可靠性与完备性。