命题可计算性逻辑 I

正如经典逻辑是关于真理的形式理论一样，最近提出的被称为可计算性逻辑的方法是关于可计算性的形式理论。它将（交互式）计算问题理解为机器与环境对弈的游戏，将其可计算性理解为存在一台总能赢得该游戏的机器，将逻辑算子理解为对计算问题的操作，并将逻辑公式的有效性理解为“总是可计算的”问题的方案。本文详细阐述了对可计算性逻辑中最基本片段之一的公理化的可靠性与完备性证明。该片段的逻辑词汇包含用于所谓并行和选择操作的算子，其原子代表基本问题，即标准意义上的谓词。本文是自洽的，解释了所有相关概念。然而，尽管在技术上并非必需，但熟悉基础性论文《Introduction to computability logic》[Annals of Pure and Applied Logic 123 (2003), pp.1-99] 将极大地帮助读者理解可计算性逻辑的哲学、底层动机、潜力与效用——这一背景决定了本文结果的价值。该主题的在线介绍可在 http://www.cis.upenn.edu/~giorgi/cl.html 和 http://www.csc.villanova.edu/~japaridz/CL/gsoll.html 获取。