一句话:用图表式幺半语法替代笛卡尔语法,提出与一阶逻辑等表达力的新皮尔士关系演算,并给出完全公理化。
关系演算由 De Morgan 和 Peirce 在 19 世纪提出,是 Boole 类代数的扩展,后来被一阶逻辑取代。Tarski 于 1941 年提出其完全公理化问题,但结论是否定的:关系演算及其许多片段都不存在有限公理化。本文提出新皮尔士关系演算,将传统笛卡尔语法改为图表式幺半语法,从而绕开这些 no-go 定理。该演算比传统关系演算更具表达力,实际上与一阶逻辑等表达力;其公理通过组合两种已知范畴结构——笛卡尔双范畴与线性双范畴——得到。作者由此为完整演算给出完全公理化,表明语法呈现方式的转变可恢复可公理化性。
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. arXiv admin note: substantial text overlap with arXiv:2401.07055
DOI 原文 · arXiv · PDF(开放获取) · DBLP
@article{BonchiGHS26,
title = {The calculus of neo-Peircean relations},
author = {Filippo Bonchi and Alessandro Di Giorgio and Nathan Haydon and Pawel Sobocinski},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 2},
year = {2026},
doi = {10.46298/lmcs-22(2:29)2026}
}