论文标题
逻辑统一的序列结算
Sequent calculi for a unity of logic
论文作者
论文摘要
我们提出了一种新颖的逻辑统一性，即一个单个序列的演算，体现了古典，直觉和线性逻辑。具体而言，我们定义了经典的线性逻辑负（Cll $^ - $），这是一种新的逻辑，是经典且线性的，但在经典线性逻辑（CLL）中丢弃了极性和严格的DE Morgan定律。然后，我们将无线化和经典化定义在序列上，以使无线化映射cll $^ - $（分别直觉的线性逻辑（ILL））到经典逻辑（Cl）（cl）（resp。Intuitionistic逻辑（IL）和经典图像iL（resp。Ill）iL（resp。Ill）cl（ports。cons。在这两个地图上，只有一个依次的微积分，用于保守的疾病，IL，Cll $^ - $和Cl。该结果通过丢弃极性和严格的de Morgan定律来实现简单，高度系统的逻辑统一，该法律（可以说）只有CLL才有，并且包括统一的古典化和不可线化的通勤。以前的方法不满足这些观点。我们的统一性还阐明了直觉和经典性之间的二分法，以及逻辑的线性和非线性之间的二分法，这是对称的。
We present a novel unity of logic, viz., a single sequent calculus that embodies classical, intuitionistic and linear logics. Concretely, we define classical linear logic negative (CLL$^-$), a new logic that is classical and linear yet discards the polarities and the strict De Morgan laws in classical linear logic (CLL). Then, we define unlinearisation and classicalisation on sequent calculi such that unlinearisation maps CLL$^-$ (resp. intuitionistic linear logic (ILL)) to classical logic (CL) (resp. intuitionistic logic (IL)), and classicalisation maps IL (resp. ILL) to CL (resp. CLL$^-$) modulo conservative extensions. By these two maps, only a sequent calculus for a conservative extension of ILL suffices for ILL, IL, CLL$^-$ and CL. This result achieves a simple, highly systematic unity of logic by discarding the polarities and the strict De Morgan laws, which (arguably) only CLL has, and consisting of the uniform classicalisation and unlinearisation, which commute. Previous methods do not satisfy these points. Our unity also clarifies the dichotomies between intuitionisity and classicality, and between linearity and non-linearity of logic, which are symmetric.
