The calculus of relations was introduced by De Morgan and Peirce during the second half of the 19th century, as an extension of Boole's algebra of classes. Later developments on quantification theory by Frege and Peirce himself, paved the way to what is known today as first-order logic, causing the calculus of relations to be long forgotten. This was until 1941, when Tarski raised the question on the existence of a complete axiomatisation for it. This question found only negative answers: there is no finite axiomatisation for the calculus of relations and many of its fragments, as shown later by several no-go theorems. In this paper we show that -- by moving from traditional syntax (cartesian) to a diagrammatic one (monoidal) -- it is possible to have complete axiomatisations for the full calculus. The no-go theorems are circumvented by the fact that our calculus, named the calculus of neo-Peircean relations, is more expressive than the calculus of relations and, actually, as expressive as first-order logic. The axioms are obtained by combining two well known categorical structures: cartesian and linear bicategories.
翻译:关系演算由德摩根和皮尔士于19世纪下半叶引入,作为布尔类代数的扩展。随后,弗雷格和皮尔士本人在量化理论方面的进展,为现今所谓的一阶逻辑铺平了道路,导致关系演算长期被遗忘。这一状况直至1941年才改变,当时塔尔斯基提出了关于其完备公理化体系存在性的问题。该问题仅得到否定性答案:如后续多个不可行定理所示,关系演算及其多数片段均不存在有限公理化。本文证明——通过从传统(笛卡尔)语法转向图示化(幺半)语法——可以为完整的关系演算建立完备公理化体系。不可行定理之所以被规避,是因为我们提出的新皮尔士关系演算比传统关系演算更具表达力,且实际上与一阶逻辑具有同等表达力。公理体系通过结合两种著名的范畴结构——笛卡尔双范畴和线性双范畴——而构建。