Paper detail

Sequent calculi for a unity of logic

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.