HEXAGONbeta

Five equations for first-order logic, modulo the structure of existential graphs

Primarily AI-generated textHuman understanding: all partsmath.LO — Logic

Contributed by Anthony Hart ↗

SubmitterAnthony Hart

Version 1 / Sep 29, 2026 / CC BY 4.0

Abstract

Peirce’s existential graphs draw a first-order formula so that the order and grouping of conjuncts, the names and order of bound variables, the position of a quantifier relative to conjuncts that do not mention its variable, and how a network of equalities is written cannot be seen. We take these structural laws for granted. On top of them, five two-way laws are complete for ordinary first-order logic with equality over nonempty domains. That is, any two equivalent formulas are connected by applying the laws inside them, in either direction. The laws are double negation, deiteration X ∧ ¬(X ∧Y ) ⇔ X ∧ ¬Y , annihilation ⊥ ∧ X ⇔ ⊥, substitution of equals, and existential introduction X(a) ∧ ∃u.X(u) ⇔ X(a), and none of them follows from the other four. The first three were already known to be complete for the propositional part. We prove first-order completeness by reduction to Tarski’s representation theorem for locally finite cylindric algebras. A size-ordered search over first-order laws, run up to size 5, kept four of the five; deiteration has size 7 and was added by hand. We also show that a published basis for Spencer-Brown’s boundary algebra is incomplete.

Provenance statement

This was produced as part of on-going PL research related to CHR. This was a question which I couldn't find a canonical answer for, so I decided to turn it into a note after finding an answer. The basic research program was described by me and executed by Opus 5.5 with me checking the final results. The paper itself was prepared by Opus 5.5, with some guidance by me for content, style, and readability.

Tools used

Anthropic
Claude OpusVersion 5.5
University of New Mexico
Mace4
University of New Mexico
Prover9

References

  1. Hajnal Andr \'e ka, Istv \'a n N \'e meti, and Ildik \'o Sain. Algebraic logic. In Handbook of Philosophical Logic , volume 2, pages 133--247. Springer, 2nd edition, 2001. Preprint: https://old.renyi.hu/pub/algebraic-logic/handbook.pdf .link
  2. Filippo Bonchi, Alessandro Di Giorgio, Nathan Haydon, and Pawe Soboci \'n ski. Diagrammatic algebra of first order logic. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2024) , pages 1--15. ACM, 2024.
  3. Filippo Bonchi, Alessandro Di Giorgio, Nathan Haydon, and Pawe Soboci \'n ski. The calculus of neo- P eircean relations. Logical Methods in Computer Science , 22(2):29:1--29:75, 2026.
  4. Filippo Bonchi, Alessandro Di Giorgio, and Davide Trotta. When L awvere meets P eirce: An equational presentation of B oolean hyperdoctrines. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024) , volume 306 of LIPIcs , pages 30:1--30:19. Schloss Dagstuhl, 2024.
  5. Geraldine Brady and Todd H. Trimble. A categorical interpretation of C.S. P eirce's propositional logic A lpha. Journal of Pure and Applied Algebra , 149(3):213--239, 2000.
  6. Geraldine Brady and Todd H. Trimble. A string diagram calculus for predicate logic and C. S. P eirce's system B eta. Preprint, 1998, revised 2000. https://ncatlab.org/nlab/files/BradyTrimbleString.pdf , 2000.link
  7. William Bricken. A deductive mathematics for efficient reasoning. Technical Report HITL-R-86-2, Human Interface Technology Laboratory, 1986.
  8. William Bricken. What's the difference? C ontrasting boundary and B oolean algebras. Manuscript, October 2005. http://iconicmath.com/mypdfs/bl-the-difference.080830.pdf , 2005.link
  9. William Bricken. Boundary logic and alpha existential graphs. Manuscript dated 2006-01-23. http://iconicmath.com/mypdfs/bl-aeg.060123.pdf , 2006.link
  10. Pablo Donato. The flower calculus. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024) , volume 299 of LIPIcs , pages 5:1--5:24. Schloss Dagstuhl, 2024.
  11. Nathan Haydon and Pawe Soboci \'n ski. Compositional diagrammatic first-order logic. In Diagrammatic Representation and Inference (Diagrams 2020) , volume 12169 of LNCS , pages 402--418. Springer, 2020.
  12. Leon Henkin, J. Donald Monk, and Alfred Tarski. Cylindric Algebras, Part II , volume 115 of Studies in Logic and the Foundations of Mathematics . North-Holland, Amsterdam, 1985.
  13. Edward V. Huntington. New sets of independent postulates for the algebra of logic, with special reference to W hitehead and R ussell's P rincipia mathematica. Transactions of the American Mathematical Society , 35(1):274--304, 1933.
  14. Louis H. Kauffman. Robbins algebra. http://homepages.math.uic.edu/ kauffman/Robbins.htm .link
  15. Louis H. Kauffman and Arthur M. Collings. The BF calculus and the square root of negation. In Laws of Form: A Fiftieth Anniversary , Series on Knots and Everything, pages 253--283. World Scientific, 2023. Preprint arXiv:1905.12891.arXiv
  16. Minghui Ma and Ahti-Veikko Pietarinen. Proof analysis of P eirce's alpha system of graphs. Studia Logica , 105(3):625--647, 2017.
  17. William McCune. Solution of the R obbins problem. Journal of Automated Reasoning , 19(3):263--276, 1997.
  18. William McCune. Prover9 and M ace4, 2005--2010. Version 2009-11A. https://www.cs.unm.edu/ mccune/prover9/ .link
  19. William McCune, Robert Veroff, Branden Fitelson, Kenneth Harris, Andrew Feist, and Larry Wos. Short single axioms for B oolean algebra. Journal of Automated Reasoning , 29(1):1--16, 2002.
  20. Philip Meguire. Boundary algebra: A simpler approach to B oolean algebra and the sentential connectives. Working Papers in Economics 10/50, Department of Economics and Finance, University of Canterbury, 2010. https://repec.canterbury.ac.nz/cbt/econwp/1050.pdf .link
  21. J. Donald Monk. Nonfinitizability of classes of representable cylindric algebras. Journal of Symbolic Logic , 34(3):331--343, 1969.
  22. J. Donald Monk. Leon H enkin and cylindric algebras. In The Life and Work of Leon Henkin , Studies in Universal Logic, pages 59--66. Birkh \"a user, 2014. Author's copy: https://euclid.colorado.edu/ monkd/monk85.pdf .link
  23. Naipmoro. lofmm: L aws of F orm in M etamath. https://naipmoro.github.io/lofmm/ .link
  24. Nicholas Smallbone, Moa Johansson, Koen Claessen, and Maximilian Algehed. Quick specifications for the busy programmer. Journal of Functional Programming , 27:e18, 2017.
  25. G. Spencer-Brown. Laws of Form . Allen and Unwin, London, 1969.
  26. Stephen Wolfram. A New Kind of Science . Wolfram Media, Champaign, IL, 2002. pp. 816--818.

Version history

  1. v1Initial depositCurrentSep 29, 2026