pith. sign in

arxiv: 2505.05306 · v4 · submitted 2025-05-08 · 💻 cs.LO

The calculus of neo-Peircean relations

Filippo Bonchi , Alessandro Di Giorgio , Nathan Haydon , Pawel Sobocinski This is my paper

Pith reviewed 2026-05-22 16:11 UTC · model grok-4.3

classification 💻 cs.LO
keywords neo-Peircean relationscalculus of relationsmonoidal syntaxbicategoriesfirst-order logicaxiomatizationdiagrammatic reasoning
0
0 comments X

The pith

A monoidal diagrammatic syntax allows complete axiomatizations for a relation calculus as expressive as first-order logic.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper tries to establish that a shift from traditional cartesian syntax to a monoidal diagrammatic syntax enables complete axiomatizations for the calculus of relations. The new calculus of neo-Peircean relations is more expressive than the original and reaches the level of first-order logic. This matters because it circumvents the no-go theorems that showed no finite axiomatization exists for the traditional version. Sympathetic readers would see this as a way to have sound diagrammatic reasoning for relational properties in logic.

Core claim

The central claim is that the calculus of neo-Peircean relations, using a diagrammatic monoidal syntax, is as expressive as first-order logic and admits complete axiomatizations obtained by combining cartesian and linear bicategories. This circumvents the no-go theorems for the traditional calculus of relations which lacked finite axiomatizations.

What carries the argument

The combination of cartesian and linear bicategories within a monoidal diagrammatic syntax that defines the neo-Peircean relations.

Load-bearing premise

The assumption that the combination of cartesian and linear bicategories provides a complete axiomatization for the neo-Peircean calculus at the expressiveness of first-order logic.

What would settle it

An explicit first-order logic sentence that cannot be expressed using the neo-Peircean relations or a relational property that is valid but not derivable from the given axioms.

Figures

Figures reproduced from arXiv: 2505.05306 by Alessandro Di Giorgio, Filippo Bonchi, Nathan Haydon, Pawel Sobocinski.

Figure 1
Figure 1. Figure 1: Diagrammatic syntax of NPRΣ diagram on the left below. f f g h f g f h A difference w.r.t. traditional syntax tree is the explicit treatment of copying and discarding. The discharger informs us that the variable x2 does not appear in the term; the copier makes clear that the variable x3 is shared by two sub-terms. The string diagram on the right represents the same term if one admits the equations c = c c … view at source ↗
Figure 2
Figure 2. Figure 2: A diagram, its tiled decomposition and its term derivation. a tensor—or through wires—yielding a sequential composition. For example, consider the diagram in [PITH_FULL_IMAGE:figures/full_fig_p012_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Completely axiomatic proof of (1.1). that places each axiom in its proper context, highlighting its provenance from one of the categorical structures involved. Proofs as diagrams rewrites. Proofs in NPRΣ are rather different from those of traditional proof systems: since the only inference rules are those in (3.5), any proof of c ≲ d consists of a sequence of applications of axioms. As an example consider … view at source ↗
Figure 4
Figure 4. Figure 4: Axioms of cartesian bicategories C is a cocartesian bicategory if Cco is a cartesian bicategory. A morphism of (co)cartesian bicategories is a poset-enriched strong symmetric monoidal functor preserving the specified monoid and comonoid structures. Remark 4.2. In the original presentation of [CW87], the structures in Definition 4.1 are named cartesian bicategories of relations. Here we have chosen to go fo… view at source ↗
Figure 5
Figure 5. Figure 5: Axioms of cocartesian bicategories We draw arrows of cocartesian bicategories in black: ◀• X,! • X, ▶• X and ¡ • X are drawn X X X , X , X X X and X . Following this convention, the axioms of cocartesian bicategories are in [PITH_FULL_IMAGE:figures/full_fig_p018_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Axioms of closed symmetric monoidal linear bicategories Lemma 5.4. Let (C, ⊗,×, I) be a linear bicategory. For all arrows a, b, c the following hold: (1) id• I ≤ id◦ I (2) a ⊗ b ≤ a × b (3) (a × b) ⊗ c ≤ a × (b ⊗ c). Proof. The proof of (1) is on the left and (2) on the right: id• I = id• I ◦, id◦ I = id• I ◦, (id• I •, id◦ I ) ≤ (id• I ◦, id• I ) •, id◦ I (δl) = (id• I ⊗ id• I ) •, id◦ I (SMC) ≤ (id• … view at source ↗
Figure 7
Figure 7. Figure 7: Additional axioms for fo-bicategories Hereafter, the diagram obtained from c , by taking its mirror image c and then its photographic negative c will denote c ⊥ . 6. First-Order Bicategories Here we focus on the most important and novel part of the axiomatisation. Indeed, having introduced the two main ingredients, cartesian and linear bicategories, it is time to fire up the Bunsen burner. The remit of thi… view at source ↗
Figure 8
Figure 8. Figure 8: The axioms of fo-bicategories reduce to those above for diagrams of type 0 → 0. by requiring the axiom (id◦ 0 , d). This leads us to the definition of another relevant class of diagrammatic first-order theories, that we call closed theories. Definition 7.11. A theory T = (Σ,I) is said to be closed if all the pairs (c, d) ∈ I are of the form (id◦ 0 , d). For instance, the theory of sets and the theory of no… view at source ↗
Figure 9
Figure 9. Figure 9: Encoding of NPRΣ diagrams as FOL formulas [PITH_FULL_IMAGE:figures/full_fig_p047_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Peirce’s (de)iteration rule in FOBΣ (left) and in [HS20] (right). Note that the diagrams on the right require open cuts, a notational trick, allowing to express the rule for arbitrary contexts, i.e. any diagram eventually appearing inside the cut. In FOBΣ this ad-hoc treatment of contexts is not needed as negation is not a primitive operation, but a derived one. Moreover, observe that in both Peirce’s EG … view at source ↗
Figure 11
Figure 11. Figure 11: Axioms for NPRΣ. Here a, b, c, d are properly typed terms [PITH_FULL_IMAGE:figures/full_fig_p058_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Diagrammatic axioms for NPRΣ. Here a, b, c, d are properly typed terms [PITH_FULL_IMAGE:figures/full_fig_p059_12.png] view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper introduces the 'calculus of neo-Peircean relations' as a diagrammatic monoidal syntax extending the traditional calculus of relations. It claims that combining the axioms of cartesian bicategories with those of linear bicategories yields a complete equational axiomatization for this system, which is asserted to be as expressive as first-order logic, thereby circumventing Tarski-style no-go theorems on finite axiomatizability that apply to the less expressive calculus of relations.

Significance. If the completeness and expressiveness claims hold, the work would offer a notable contribution to algebraic logic by providing a complete diagrammatic axiomatization for a relational calculus equivalent in power to FOL. The approach of merging cartesian and linear bicategorical structures to obtain completeness in a monoidal setting could inform further developments in categorical semantics and proof systems for logics with relational operations.

major comments (2)
  1. [Abstract and §4] The abstract and the construction of the neo-Peircean calculus: the claim that the combined cartesian+linear bicategory axioms are complete for the full calculus (and thus circumvent no-go results because the system equals FOL expressiveness) lacks an explicit embedding of arbitrary FOL formulas into the diagrammatic syntax or a stated soundness/completeness theorem with respect to the intended relational models. This is load-bearing for the central claim.
  2. [§3] §3 (interaction of structures): the description of how cartesian products interact with linear composition does not verify that all quantifier-like operations and their equational consequences are generated by the listed axioms without missing interaction rules, which is required to establish that the axiomatization is complete for the claimed FOL-equivalent expressiveness.
minor comments (1)
  1. Notation for the monoidal diagrammatic syntax would benefit from additional concrete examples or a small table mapping traditional relational operations to their diagrammatic counterparts.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for the constructive major comments. We agree that the central claims require more explicit support in the form of an embedding and verification of completeness, and we will revise the paper to address these points directly.

read point-by-point responses

  1. Referee: [Abstract and §4] The abstract and the construction of the neo-Peircean calculus: the claim that the combined cartesian+linear bicategory axioms are complete for the full calculus (and thus circumvent no-go results because the system equals FOL expressiveness) lacks an explicit embedding of arbitrary FOL formulas into the diagrammatic syntax or a stated soundness/completeness theorem with respect to the intended relational models. This is load-bearing for the central claim.

    Authors: We acknowledge that the current presentation would benefit from an explicit statement of the embedding and the associated soundness/completeness result. In the revised manuscript we will add a new subsection to §4 that defines a translation from arbitrary first-order formulas (including quantifiers and connectives) into the monoidal diagrammatic syntax and proves that this translation preserves semantics in the intended relational models. We will also state and prove the soundness and completeness theorem for the combined cartesian+linear axioms with respect to those models, thereby making the circumvention of the Tarski-style no-go theorems fully rigorous. revision: yes

  2. Referee: [§3] §3 (interaction of structures): the description of how cartesian products interact with linear composition does not verify that all quantifier-like operations and their equational consequences are generated by the listed axioms without missing interaction rules, which is required to establish that the axiomatization is complete for the claimed FOL-equivalent expressiveness.

    Authors: The referee is right to ask for explicit verification of the interaction rules. We will expand §3 with two additional lemmas: one showing that the existential quantifier (arising from the linear structure) can be expressed using the given axioms, and a second demonstrating that all equational consequences involving cartesian products and linear composition are derivable from the listed axioms alone. These lemmas will confirm that no further interaction rules are required to generate the full set of quantifier-like operations, thereby supporting the completeness claim for the FOL-equivalent fragment. revision: yes

Circularity Check

0 steps flagged

No circularity: axiomatization derived from independent bicategory structures

full rationale

The paper introduces a monoidal diagrammatic syntax for neo-Peircean relations and obtains its axioms by combining two established, externally defined categorical structures (cartesian bicategories and linear bicategories). The claimed completeness for a system as expressive as first-order logic is presented as following from this combination and the shift away from cartesian syntax, without any reduction of the target result to a fitted parameter, self-referential definition, or load-bearing self-citation chain. The derivation remains self-contained against the external benchmarks of bicategory theory and relational semantics.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The construction rests on the standard axioms of cartesian and linear bicategories plus the modeling choice that their combination yields a complete system at first-order expressiveness. No free parameters or new invented entities with independent evidence are mentioned.

axioms (1)
  • domain assumption Cartesian and linear bicategories together supply a complete axiomatization for the neo-Peircean calculus.
    Stated directly in the abstract as the source of the axioms.
invented entities (1)
  • Calculus of neo-Peircean relations no independent evidence
    purpose: A monoidal diagrammatic relational calculus that is complete and first-order expressive.
    Introduced as the central new object whose properties circumvent prior no-go theorems.

pith-pipeline@v0.9.0 · 5736 in / 1413 out tokens · 48347 ms · 2026-05-22T16:11:26.381606+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

13 extracted references · 13 canonical work pages

  1. [1]

    (id ◦ 1 ⊗▶◦ 1),◦ ▶◦ 1 (▶◦ -as) = (▶ ◦ 1 ⊗id ◦ 1),◦ ▶◦ 1 ◀◦ 1 ,◦(id◦ 1 ⊗! ◦ 1) (◀◦ -un) =id ◦ 1 (id◦ 1 ⊗ ¡◦ 1),◦ ▶◦ 1 (▶◦ -un) =id ◦ 1 ◀◦ 1 ,◦σ◦ 1,1 (◀◦ -co) =◀ ◦ 1 σ◦ 1,1 ,◦ ▶◦ 1 (▶◦ -co) =▶ ◦ 1 (◀◦ 1 ⊗id ◦ 1),◦ (id◦ 1 ⊗▶◦ 1) (F◦ ) = (id ◦ 1 ⊗◀◦ 1),◦ (▶◦ 1 ⊗id ◦ 1)◀ ◦ 1 ,◦ ▶◦ 1 (S◦ ) =id ◦ 1 ¡◦ 1 ,◦ !◦ 1 (ϵ!◦ ) ≤id ◦ 0 ▶◦ 1 ,◦ ◀◦ 1 (ϵ◀ ◦ ) ≤(id ◦ 1 ⊗id ◦ ...

    work page

  2. [2]

    Herea, b, c, dare properly typed terms

    (id • 1 ×▶• 1),• ▶• 1 (▶•-as) = (▶ • 1 ×id• 1),• ▶• 1 ◀• 1 ,•(id• 1 ×!• 1) (◀• -un) =id • 1 (id• 1 ס• 1),• ▶• 1 (▶• -un) =id • 1 ◀• 1 ,•σ• 1,1 (◀• -co) =◀ • 1 σ• 1,1 ,• ▶• 1 (▶• -co) =▶ • 1 (◀• 1 ×id• 1),• (id• 1 ×▶• 1) (F• ) = (id • 1 ×◀• 1),• (▶• 1 ×id• 1)◀ • 1 ,• ▶• 1 (S• ) =id • 1 !• 1 ,• ¡• 1 (ϵ<• ) ≤id • 1 ◀• 1 ,• ▶• 1 (ϵ▶ • ) ≤id • 1 id• 0 (η<• ) ...

    work page

  3. [3]

    67 (2)a = c⊗d

    Thusa ∼=P id• 0. 67 (2)a = c⊗d . Note that, in this case both c and d must have type 0 → 0. Thus we can use the inductive hypothesis to get c′ and d′ generated by the above grammar such that c′ ∼=P c and d′ ∼=P d. Thus a ∼=P c′ ⊗d ′ ≈c ′ ,◦ d′. Note that c′ ,◦ d′ is generated by the above grammar. (3)a=c , • d. The proof follows symmetrical arguments to t...

    work page

  4. [4]

    Thus there exists ani∈Isuch thatid ◦ 0 ≲Ti id•

    ∈S i∈I ≲Ti. Thus there exists ani∈Isuch thatid ◦ 0 ≲Ti id•

    work page

  5. [5]

    (2) Suppose that T is trivial

    Against the hypothesis. (2) Suppose that T is trivial. By definition ¡◦ 1 ≲T ¡• 1 and then, by (F.1), (¡◦ 1, ¡•

    work page

  6. [6]

    Thus there exists ani∈Isuch that ¡◦ 1 ≲Ti ¡•

    ∈S i∈I ≲Ti. Thus there exists ani∈Isuch that ¡◦ 1 ≲Ti ¡•

    work page

  7. [7]

    Proof of Proposition 8.12

    Against the hypothesis. Proof of Proposition 8.12. The proof of this proposition relies on Zorn’s Lemma [ Zor35] which states that if, in a non empty poset L every chain has a least upper bound, then L has at least one maximal element. We consider the set Γ of all non-contradictory theories on Σ that includeI, namely Γ def ={T= (Σ,J)|Tis non-contradictory...

    work page

  8. [8]

    By the deduction theorem (Theorem 7.13),c≲ T′id•

    work page

  9. [9]

    Proof of Theorem 8.13

    Thereforeid ◦ 0≲T′c. Proof of Theorem 8.13. This proof reuses the well-known arguments reported e.g. in [ LP01]. We first illustrate a procedure to add Henkin witnesses without losing the property of being non-trivial. Take an enumeration of diagrams inFOB Σ[1,0] and writec i for thei-th diagram. For all natural numbersn∈N, we define Σn def = Σ∪ {k i : 0→...

    work page

  10. [10]

    (Table 3) =I ♯(◀◦ 1),◦ (I ♯(E(E1))⊗ I ♯(E(E2))),◦ I ♯(▶◦

    work page

  11. [11]

    hyp.) =⟨E1⟩I ∩ ⟨E2⟩I (4.2) =⟨E1 ∩E 2⟩I (2.4) I ♯(E(E1 ∪E 2))=I ♯(◀• 1 ,•(E(E1) × E(E2)),• ▶•

    (3.4) =◀ ◦ X ,◦(I ♯(E(E1))⊗ I ♯(E(E2))),◦ ▶◦ X (3.4) =◀ ◦ X ,◦(⟨E1⟩I ⊗ ⟨E2⟩I),◦ ▶◦ X (Ind. hyp.) =⟨E1⟩I ∩ ⟨E2⟩I (4.2) =⟨E1 ∩E 2⟩I (2.4) I ♯(E(E1 ∪E 2))=I ♯(◀• 1 ,•(E(E1) × E(E2)),• ▶•

    work page

  12. [12]

    (Table 3) =I ♯(◀• 1),• (I ♯(E(E1)) × I♯(E(E2))),• I ♯(▶•

    work page

  13. [13]

    hyp.) =⟨E1⟩I ∪ ⟨E2⟩I (4.3) =⟨E1 ∪E 2⟩I (2.4) I ♯(E(E †))=I ♯((E(E)) †) (Table 3) =(I ♯(E(E))) † (Lemma 4.8) =⟨E⟩† I (Ind

    (3.4) =◀ • X ,•(I ♯(E(E1)) × I♯(E(E2))),• ▶• X (3.4) =◀ • X ,•(⟨E1⟩I × ⟨E2⟩I),• ▶• X (Ind. hyp.) =⟨E1⟩I ∪ ⟨E2⟩I (4.3) =⟨E1 ∪E 2⟩I (2.4) I ♯(E(E †))=I ♯((E(E)) †) (Table 3) =(I ♯(E(E))) † (Lemma 4.8) =⟨E⟩† I (Ind. hyp.) =⟨E†⟩I (2.4) I ♯(E(E))=I ♯((E(E))) (Table 3) =I ♯(((E(E)) ⊥)†) (Definition of (·)) =(I ♯(E(E)) ⊥)† (Lemmas 4.8, 5.11) =((⟨E⟩I)⊥)† (Ind. hy...

    work page