\documentclass[11pt]{amsart}
\usepackage[margin=1.15in]{geometry}
\usepackage{amssymb,mathtools,booktabs,array}
\usepackage[hidelinks]{hyperref}
\usepackage[capitalise,noabbrev]{cleveref}

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\raggedbottom
\newcommand{\sameas}{\mathrel{=_{\mathsf{s}}}}
\newcommand{\der}{\sim}
\newcommand{\sem}{\equiv}
\newcommand{\law}[1]{\textup{\textsc{#1}}}
\newcommand{\fv}{\operatorname{fv}}
\newcommand{\Lf}{\mathsf{Lf}}
\newcommand{\RCA}{\mathsf{RCA}}
\newcommand{\Cs}{\mathsf{Cs}}
\newcommand{\CA}{\mathsf{CA}}
\newcommand{\SP}{\mathbf{SP}}

\title[Five equations for first-order logic]{Five equations for first-order logic, modulo the structure of existential graphs}
\author{Anthony Hart}
\address{Independent researcher}
\email{soobtoob@gmail.com}
\date{\today}

\begin{document}
\begin{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 \wedge \neg(X \wedge Y) \Leftrightarrow X \wedge \neg Y$, annihilation $\bot \wedge X \Leftrightarrow \bot$, substitution of equals, and existential introduction $X(a) \wedge \exists u.X(u) \Leftrightarrow 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.
\end{abstract}
\maketitle

\section{Introduction}\label{sec:intro}

Peirce's existential graphs draw a first-order formula on a sheet. Conjunction is drawing side by side, negation is drawing an enclosure around a subgraph, and a quantified variable is drawn as a line (Peirce's \emph{line of identity}), with lines joined to express equality. Much of the syntax of a formula is therefore not visible in the drawing: the order and grouping of conjuncts, the names and order of bound variables, which conjunct a quantifier is attached to when the others do not mention its variable, and which of several equivalent sets of equalities joins the same variables. We take for granted the laws that identify formulas differing only in these respects, the \emph{structural laws} (\cref{def:struct}), and ask which two-way laws must be added to obtain all of first-order logic.

Five suffice: double negation, deiteration $X \wedge \neg(X \wedge Y) \Leftrightarrow X \wedge \neg Y$, annihilation $\bot \wedge X \Leftrightarrow \bot$, substitution of equals, and existential introduction (\cref{def:laws}). Together with the structural laws, they connect any two formulas that are equivalent in ordinary first-order logic with equality over nonempty domains, by rewriting subformulas in either direction. None of the five follows from the other four.

Our motivation is a constraint-handling language whose store is a formula held as an existential graph, and whose programs may invoke logical equivalences. Such a system gets the structural laws from its representation for free, and the laws a programmer uses on top should be few and recognisable.

For the propositional part such a set is known. Spencer-Brown reads juxtaposition as disjunction; under the dual reading, his reflexion, generation and integration \cite{spencer-brown} are double negation, deiteration and annihilation, and Kauffman and Collings adopt them, following Bricken, as a complete basis \cite{kauffman-collings,bricken86}.

For first-order logic, two complete presentations are available, and neither suits rewriting. The cylindric-algebra axioms of Henkin, Monk and Tarski (\cref{sec:ca}) are two-way equations, but they need a separate Boolean basis such as Huntington's equation, and their only substitution axiom, (C7), says that $x(v_i)$ and $\neg x(v_j)$ cannot both hold when $v_i = v_j$: it rewrites to false, never $x(v_i)$ to $x(v_j)$. The calculus of neo-Peircean relations of Bonchi, Di~Giorgio, Haydon and Sobociński \cite{bdhs-lics24,bdhs-lmcs} is complete, but its proofs are chains of inequalities, it allows the empty domain, and it has 64 axioms.

Our contributions are:
\begin{enumerate}
\item \emph{Five laws that, with the structural laws, are complete for first-order logic with equality over nonempty domains} (\cref{thm:complete}), and independent when the signature has a relation symbol of positive arity (\cref{thm:independent}).
\item \emph{A direct proof for the propositional part} (\cref{thm:boolean}): a four-step derivation of Huntington's equation from double negation, deiteration and annihilation, and the independence of the three; neither appears in the works cited in \cref{sec:related}. Meguire's published basis \cite{meguire} for boundary algebra (Spencer-Brown's calculus of nested enclosures, equivalent to Boolean algebra), which uses $\neg\neg\top \Leftrightarrow \top$ in place of double negation, is incomplete (\cref{prop:meguire}).
\item \emph{A search for recognisable laws} (\cref{sec:search}). Enumerating valid equations by size and keeping those not derived from smaller ones yields, among others, double negation, idempotence, annihilation, non-contradiction, absorption, substitution of equals and existential introduction. Neither search keeps deiteration.
\end{enumerate}

\Cref{sec:syntax} fixes the formulas, the structural laws and the five laws. \Cref{sec:boolean} treats the propositional part, whose derivations \cref{sec:fo} reuses; \cref{sec:fo} proves completeness and independence. \Cref{sec:search} describes the search, \cref{sec:related} compares with prior work, and \cref{app:derivations} gives the derivations behind the search.

\section{Formulas, structural laws and the five laws}\label{sec:syntax}

\begin{definition}[Formulas]
Fix a relational signature $\Sigma$ and an infinite set of variables. Formulas are given by
\[
\varphi, \psi \;::=\; \top \;\mid\; R(w_1,\dots,w_n) \;\mid\; w = w' \;\mid\; \varphi \wedge \psi \;\mid\; \neg\varphi \;\mid\; \exists w.\,\varphi
\]
where $R \in \Sigma$ has arity $n$. A formula $w = w'$ is an \emph{equality}. We write $\bot$ for $\neg\top$ and $\fv(\varphi)$ for the free variables of $\varphi$. Disjunction, implication and $\forall$ are the usual abbreviations.
\end{definition}

\begin{definition}[Structural identity]\label{def:struct}
\emph{Structural identity} $\sameas$ is the least congruence on formulas generated by the following \emph{structural laws}:
\begin{enumerate}
\item[(S1)] $\wedge$ is associative and commutative with unit $\top$;
\item[(S2)] bound variables may be renamed;
\item[(S3)] $\exists w.(\varphi \wedge \psi) \sameas (\exists w.\varphi) \wedge \psi$ when $w \notin \fv(\psi)$, and $\exists w.\exists v.\varphi \sameas \exists v.\exists w.\varphi$;
\item[(S4)] $w = w \sameas \top$, \ $w = v \sameas v = w$, \ $w{=}v \wedge v{=}z \sameas w{=}v \wedge w{=}z$, \ and $w{=}v \wedge w{=}v \sameas w{=}v$.
\end{enumerate}
\end{definition}

Up to $\sameas$, a formula is a tree. Each node is the top level or a negation, and holds a multiset of atoms and negated subformulas, the variables quantified at that node, and the partition of variables that its equalities generate. Existential-graph syntax gives the structural laws for free: formulas related by $\sameas$ are drawn as the same graph, so a system that works on graphs never has to apply (S1)--(S4).

Each structural law is invisible in a graph for a concrete reason. (S1): conjuncts drawn side by side on a sheet have no order or grouping. (S2): a line is merely drawn, with no name to distinguish it from another line, so renaming a bound variable changes nothing in the graph. (S3): a quantified variable is a line, and a line has no position relative to a subgraph it does not touch, so the two can be moved past each other freely; nor do two lines have an order. (S4): equalities are drawn by joining lines, so $w{=}v \wedge v{=}z$ and $w{=}v \wedge w{=}z$ draw the same three joined lines.

The structural laws are valid equivalences of first-order logic, so they act as further axioms: ``five laws'' means five in addition to (S1)--(S4). Idempotence of conjunction and vacuous quantification are not structural; they follow from the five laws (\cref{sec:derived}).

\begin{definition}[Meaning]
A structure $M$ has a \emph{nonempty} universe $U$ and a relation $R^M \subseteq U^n$ for each $R \in \Sigma$. Satisfaction $M, s \models \varphi$ under an assignment $s$ of elements to variables is the usual one. Formulas $\varphi$ and $\psi$ are \emph{equivalent}, $\varphi \sem \psi$, when $M, s \models \varphi \iff M, s \models \psi$ for every $M$ and $s$.
\end{definition}

\begin{definition}[Laws and instances]\label{def:instances}
A \emph{law} is an equation $L \Leftrightarrow R$ between \emph{schemas}: formulas that may also contain \emph{schema variables} $X, Y$ and \emph{schema parameters} $a, b$, which stand for object variables. A schema variable may take arguments, as in $X(a)$; each schema variable in the five laws takes at most one. An \emph{instance} replaces each parameter by a variable and each schema variable by a formula: a unary $X$ becomes an abstraction $\lambda x.\varphi$, and $X(w)$ becomes the capture-avoiding substitution $\varphi[w/x]$, renaming bound variables of $\varphi$ as (S2) allows. The formula $\varphi$ may have free variables besides $x$, and the law's own bound variables, such as $u$ in \law{ei} below, are renamed to differ from all of them.
\end{definition}

So a schema variable stands for any formula, including one that mentions variables the law does not name. This is the usual reading of a schema variable: a law valid for every predicate is valid for every predicate with extra fixed parameters.

\begin{definition}[The five laws]\label{def:laws}
\begin{align*}
&\text{(\law{dn}) double negation} && \neg\neg X \Leftrightarrow X\\
&\text{(\law{dt}) deiteration} && X \wedge \neg(X \wedge Y) \Leftrightarrow X \wedge \neg Y\\
&\text{(\law{an}) annihilation} && \bot \wedge X \Leftrightarrow \bot\\
&\text{(\law{sub}) substitution of equals} && a{=}b \wedge X(a) \Leftrightarrow a{=}b \wedge X(b)\\
&\text{(\law{ei}) existential introduction} && X(a) \wedge \exists u.\,X(u) \Leftrightarrow X(a)
\end{align*}
\emph{Derivability} $\der$ is the least congruence on formulas (for $\wedge$, $\neg$ and $\exists w$) that contains $\sameas$ and every instance of the five laws.
\end{definition}

Three relations on formulas are now in play: $\varphi \sameas \psi$, the same up to the structural laws; $\varphi \der \psi$, connected by the five laws; and $\varphi \sem \psi$, logically equivalent. \Cref{thm:complete} says $\der$ and $\sem$ coincide.

Because $\der$ is a congruence, a law applies to any subformula, to any part of a conjunction, and in both directions. In particular it may rewrite a subformula in which $w$ is free although $w$ is bound further out.

\law{dt} is the simplest case of Peirce's deiteration: when $X$ is a conjunct beside $\neg(X \wedge Y)$, the copy of $X$ inside may be erased; Peirce also erases copies nested deeper. \law{an} is Spencer-Brown's integration, and is also called domination. \law{ei} is the equational form of the rule $\varphi(a) \to \exists u.\varphi(u)$: a formula absorbs a copy of itself in which some occurrences of a variable are replaced by a fresh bound one.

\begin{remark}[Where nonempty domains enter]\label{rem:scope}
Instantiating \law{ei} with $X := \lambda x.\top$ gives the law of vacuous quantification,
\[\text{(\law{u})}\qquad \exists u.\top \der \top.\]
The instance must supply a variable for the parameter $a$, which neither side mentions; \cref{def:instances} allows that, and nonemptiness is used exactly there.

An implementation may instead work in context: every free variable of a law instance, including those of the formulas substituted for schema variables, must be bound above the point of application or free in the formula being rewritten as a whole. Then \law{u} is not derivable between sentences, and must be added as a sixth law. To see this, note that a derivation between sentences then passes only through sentences. Evaluate them over the empty domain, where every $\exists w.\chi$ is false. A rewrite below a quantifier cannot change the truth value. At the top level no variable is in scope, so \law{sub} and \law{ei} cannot apply there, and \law{dn}, \law{dt}, \law{an} and (S1)--(S4) are valid. So every equivalence between sentences derivable in context holds over the empty domain, but $\exists u.\top \Leftrightarrow \top$ does not.
\end{remark}

\section{The propositional part}\label{sec:boolean}

We treat the propositional part first because \cref{sec:fo} reuses its derivations. In this section formulas are Boolean terms: $x, y$ range over propositions, $x \cdot y$ is $x \wedge y$, and $-x$ is $\neg x$. Let $\bot := -\top$.

\begin{theorem}\label{thm:boolean}
The equations
\[
x \cdot y = y \cdot x,\quad (x\cdot y)\cdot z = x \cdot (y \cdot z),\quad x \cdot \top = x,
\]
\[
\text{(\law{dn})}\ {-}{-}x = x,\qquad \text{(\law{dt})}\ x \cdot -(x\cdot y) = x \cdot -y,\qquad \text{(\law{an})}\ \bot \cdot x = \bot
\]
axiomatise Boolean algebras, with $\cdot$ as meet, $-$ as complement and $\top$ as top. Each of \law{dn}, \law{dt}, \law{an} is independent of the other five equations in this list.
\end{theorem}

The three laws are Spencer-Brown's Consequences 1--3, dualised, which Kauffman and Collings take as a complete basis (\cref{sec:related}). We give a direct proof.

\begin{proof}
All six equations hold in every Boolean algebra. For the converse we derive Huntington's equation, written with $\cdot$ in place of his $+$:
\[
\text{(H)}\qquad -(-x \cdot y) \cdot -(-x \cdot -y) = x .
\]
Huntington proved that commutativity, associativity and (H), written with $+$, axiomatise Boolean algebras with $+$ as the join \cite{huntington33,mccune-robbins}. So our equations make $\cdot$ the join of some Boolean order. Under the reverse order $\cdot$ is the meet, and $-$ is still the complement, because complement is an order-reversing involution. The unit law then says $\top$ is the top. The derivation has four steps.
\begin{enumerate}
\item $-\bot = \top$: \ $-\bot = --\top = \top$ by \law{dn}.
\item \emph{Contradiction}, $x \cdot -x = \bot$: \ $x \cdot -x = x \cdot -(x \cdot \top) = x \cdot -\top = \bot \cdot x = \bot$, by the unit, \law{dt} with $y := \top$, commutativity and \law{an}.
\item \emph{Absorption}, $x \cdot -(-x \cdot y) = x$: \ $x \cdot -(-x\cdot y) = x \cdot -(x \cdot -x \cdot y) = x \cdot -(\bot \cdot y) = x \cdot -\bot = x \cdot \top = x$, by \law{dt} read right to left, contradiction (2), \law{an}, step 1 and the unit.
\item (H): put $B := -(-x \cdot y)$. \law{dt} with $-x$ in place of its $x$ gives $-x\cdot-(-x\cdot y) = -x \cdot -y$, so $-x \cdot -y = -x \cdot B$, and the second factor of (H) is $-(-x \cdot B)$. The left side of (H) is therefore $B \cdot -(B \cdot -x) = B \cdot --x = B \cdot x = x \cdot -(-x\cdot y) = x$, by commutativity, \law{dt}, \law{dn}, commutativity and absorption (3).
\end{enumerate}
For independence, each of the following algebras, with $\cdot$ as $\min$ and $\top$ as the largest element, satisfies commutativity, associativity, the unit and two of the three laws, and falsifies the third:
\begin{center}
\begin{tabular}{llll}
\toprule
falsified & universe & complement & failing instance\\
\midrule
\law{dn} & $\{0,1\}$ & $-x = 0$ & $--1 = 0$\\
\law{dt} & $\{0,1,2\}$ & $-0 = 2,\ -1 = 1,\ -2 = 0$ & $1 \cdot -(1\cdot 2) = 1 \ne 0 = 1 \cdot -2$\\
\law{an} & $\{0,1\}$ & $-x = x$ & $\bot \cdot 0 = 0 \ne 1 = \bot$\\
\bottomrule
\end{tabular}
\end{center}
The second is Kleene's strong three-valued logic. A computer check over all argument values confirms each row.
\end{proof}

\begin{proposition}\label{prop:meguire}
Meguire's basis for boundary algebra \cite[\S3]{meguire} does not axiomatise Boolean algebras. In our notation it consists of commutativity and associativity (his B1), ${-}{-}\top = \top$ (B2), $-x \cdot x = \bot$ (B3) and \law{dt} (B4).
\end{proposition}

\begin{proof}
Take the universe $\{e, p, q\}$ with $\top = e$, the product given by $e \cdot x = x$, $p \cdot p = e$ and $q \cdot x = q$, and complement $-e = q$, $-p = q$, $-q = e$. All of B1--B4 and the unit hold, but $--p = e \ne p$ and $p \cdot p = e \ne p$. The model was found by the finite-model finder Mace4 \cite{prover9} and re-checked by a separate computer evaluation. Meguire derives $x \cdot x = x$ and $--x = x$ with a ``calculation'' rule, which infers $\alpha = \beta$ from $(\alpha \leftrightarrow \beta) = \top$. That rule is not an equational consequence of B1--B4, and it fails in this model.
\end{proof}

\section{First-order logic: completeness and independence}\label{sec:fo}

We now prove that the five laws, with the structural laws, connect exactly the logically equivalent formulas, and that none of the five can be dropped.

\begin{theorem}\label{thm:complete}
For all formulas $\varphi$ and $\psi$, \ $\varphi \sem \psi$ if and only if $\varphi \der \psi$.
\end{theorem}

Soundness is routine: each law is valid for every choice of formulas, including formulas with extra free variables, and $\sameas$ preserves meaning. \Cref{sec:derived,sec:ca,sec:translations} prove completeness: we translate formulas into cylindric-algebra terms, use Tarski's theorem there, and translate the resulting equational proof back. \Cref{sec:independence} proves independence.

\subsection{Derived laws}\label{sec:derived}
The proof uses these consequences of the five laws; $u$ is always a bound variable not free elsewhere.
\begin{align*}
&\text{(\law{u}) vacuous quantification} && \exists u.\top \der \top && \text{\law{ei} with } X := \lambda x.\top\\
&\text{(\law{i}) a variable has a witness} && \exists u.\,(u = a) \der \top && \text{\law{ei} with } X := \lambda x.\,(x = a)\\
&\text{(\law{op}) one-point rule} && \exists u.\,(u = a \wedge X(u)) \der X(a) && \text{\law{sub}, (S3), \law{i}}\\
&\text{(\law{ctr}) contradiction} && X \wedge \neg X \der \bot && \text{step 2 of \cref{thm:boolean}}\\
&\text{(\law{abs}) absorption} && X \wedge \neg(\neg X \wedge Y) \der X && \text{step 3 of \cref{thm:boolean}}
\end{align*}
For \law{i}, the instance of \law{ei} reads $(a{=}a) \wedge \exists u.(u{=}a) \Leftrightarrow a{=}a$, and $a{=}a \sameas \top$ by (S4). For \law{op}: $\exists u.(u{=}a \wedge X(u)) \der \exists u.(u{=}a \wedge X(a)) \sameas (\exists u.\,u{=}a) \wedge X(a) \der X(a)$. The derivations in \cref{thm:boolean} use only \law{dn}, \law{dt}, \law{an} and (S1), so they hold with $\wedge$ for $\cdot$, $\neg$ for $-$, and arbitrary formulas for $x$ and $y$. Idempotence also follows: $\exists u.X \sameas X \wedge \exists u.\top \der X$ by (S3) and \law{u}, so $X \wedge X \der X \wedge \exists u.X$, which is $\der X$ by \law{ei} with its schema variable set to $\lambda x.X$, which ignores $x$.

\subsection{Cylindric algebras}\label{sec:ca}
We use the axioms of Henkin, Monk and Tarski as stated by Monk \cite{monk-henkin}. Because we will generate a congruence from the axioms, we need the Boolean part as equations. We take commutativity, associativity and unit of $\cdot$, Huntington's equation (H), and $0 = -1$, and define $x + y := -(-x \cdot -y)$; by the proof of \cref{thm:boolean} these axiomatise Boolean algebras with $\cdot$ as meet. A \emph{cylindric algebra of dimension $\omega$} is such a Boolean algebra $(A, \cdot, -, 1)$ with operations $c_i$ (read as $\exists v_i$) and constants $d_{i,j}$ (read as $v_i = v_j$) for $i,j<\omega$, such that
\begin{align*}
&\text{(C1)}\ c_i 0 = 0 &&\text{(C2)}\ x + c_i x = c_i x\\
&\text{(C3)}\ c_i(x \cdot c_i y) = c_i x \cdot c_i y &&\text{(C4)}\ c_i c_j x = c_j c_i x\\
&\text{(C5)}\ d_{i,i} = 1 &&\text{(C6)}\ d_{j,k} = c_i(d_{j,i}\cdot d_{i,k}) \text{ for } i \notin\{j,k\}\\
&\text{(C7)}\ c_i(d_{i,j}\cdot x)\cdot c_i(d_{i,j}\cdot -x) = 0 \text{ for } i \neq j.
\end{align*}
$\CA_\alpha$ is the class of cylindric algebras of dimension $\alpha$.

The \emph{dimension set} of $x$ is $\{i : c_i x \neq x\}$, and an algebra is \emph{locally finite} if every dimension set is finite. $\Lf_\omega$ is the class of locally finite algebras in $\CA_\omega$.

The \emph{full cylindric set algebra} with base $U$ is $(\mathcal{P}({}^\omega U), \cap, S \mapsto {}^\omega U\setminus S, {}^\omega U, C_i, D_{i,j})$, where ${}^\omega U$ is the set of sequences $s\colon\omega\to U$, $C_i S = \{s : s[i \mapsto e] \in S \text{ for some } e \in U\}$ and $D_{i,j} = \{s : s_i = s_j\}$. $\Cs_\omega$ is the class of its subalgebras, for all $U$. For a class $K$, $\SP K$ is the class of algebras isomorphic to subalgebras of products of members of $K$. An algebra is \emph{representable} if it lies in $\RCA_\omega := \SP\,\Cs_\omega$.

\begin{theorem}[Tarski]\label{thm:tarski}
Every locally finite cylindric algebra of dimension $\omega$ is representable: $\Lf_\omega \subseteq \RCA_\omega$.
\end{theorem}

Monk writes: ``That every infinite dimensional locally finite $\CA_\alpha$ is representable is due to Tarski'' \cite{monk-henkin}. Andréka, Németi and Sain use $\Lf_\omega \subseteq \RCA_\omega$ in the proof of their Theorem~7.9 and give $\RCA_\omega = \SP\,\Cs_\omega$ as their Theorem~2.4(iii) \cite{ans-handbook}, citing the proofs in \cite{hmt2}.

\subsection{Translations}\label{sec:translations}
Only finitely many relation symbols occur in $\varphi$ and $\psi$, and equivalence over $\Sigma$-structures coincides with equivalence over structures for those symbols, so assume $\Sigma$ is finite. Let $N$ bound its arities. Let $\mathbf{F}$ be the algebra of terms built from one constant $R$ for each $R \in \Sigma$ with the cylindric operations. Let $\approx$ be the congruence on $\mathbf{F}$ generated by every instance of the cylindric axioms (any terms for the axioms' variables) together with the \emph{dimension equations} $c_i R = R$ for $i \geq \operatorname{ar}(R)$. So $\approx$ is to terms what $\der$ is to formulas.

A term $t$ has a meaning $[\![t]\!]_M \subseteq {}^\omega U$ in each structure $M$: the operations act as in the full set algebra, and $[\![R]\!]_M = \{s : (s_0,\dots,s_{n-1}) \in R^M\}$. In other words a term is a first-order formula over the variables $0, 1, 2, \dots$ in which an atom $R$ always has the variables $0,\dots,n-1$ as arguments; $c_i$ is $\exists$ over variable $i$, and $d_{i,j}$ says that variables $i$ and $j$ are equal. This is the ranked first-order logic of \cite[\S7]{ans-handbook}.

By (S2), rename the bound variables of $\varphi$ and $\psi$ so that no variable is bound twice and none is both bound and free. Choose an injection $\kappa$ from their variables into $\{N, N+1, \dots\}$; coordinates $0,\dots,N-1$ are then left for the arguments of atoms. The translation $\operatorname{tr}$ sends
\begin{gather*}
\top \mapsto 1,\quad \chi \wedge \theta \mapsto \operatorname{tr}\chi \cdot \operatorname{tr}\theta,\quad \neg\chi \mapsto -\operatorname{tr}\chi,\quad \exists w.\chi \mapsto c_{\kappa w}\operatorname{tr}\chi,\quad (w = v) \mapsto d_{\kappa w,\kappa v},\\
R(w_1,\dots,w_n) \mapsto c_0 \cdots c_{n-1}\,(d_{0,\kappa w_1}\cdots d_{n-1,\kappa w_n}\cdot R).
\end{gather*}
The atom case sets coordinate $m-1$ equal to coordinate $\kappa w_m$ for each $m$, applies $R$ to coordinates $0,\dots,n-1$, and quantifies those coordinates away. Since every $\kappa w \geq N \geq n$, induction on $\chi$ gives
\begin{equation}\label{eq:tr}
s \in [\![\operatorname{tr}\chi]\!]_M \iff M, s\circ\kappa \models \chi ,
\end{equation}
where $s \circ \kappa$ is the assignment $w \mapsto s_{\kappa w}$.

Conversely, fix distinct variables $v_0, v_1, \dots$ with $v_{\kappa w} = w$ for each variable $w$ of $\varphi$ and $\psi$, and with every other $v_i$ occurring in neither. Define $\iota\colon \mathbf{F} \to$ formulas by $\iota(R) = R(v_0,\dots,v_{n-1})$, $\iota(1) = \top$, $\iota(0) = \bot$, $\iota(t\cdot t') = \iota t \wedge \iota t'$, $\iota(-t) = \neg\,\iota t$, $\iota(c_i t) = \exists v_i.\,\iota t$ and $\iota(d_{i,j}) = (v_i = v_j)$.

\begin{lemma}\label{lem:iota}
If $t \approx t'$ then $\iota t \der \iota t'$.
\end{lemma}

\begin{proof}
The relation $\{(t,t') : \iota t \der \iota t'\}$ is a congruence on $\mathbf{F}$, because $\iota$ is defined compositionally and $\der$ is a congruence. So it suffices that $\iota$ sends each generating equation to a derivable one. Write $P = \iota x$ and $Q = \iota y$.
\begin{itemize}
\item Commutativity, associativity and the unit hold by (S1). $0 = -1$ holds by definition of $\iota$. Huntington's (H) was derived from \law{dn}, \law{dt}, \law{an} in \cref{thm:boolean}.
\item (C1): $\exists v_i.\bot \sameas \bot \wedge \exists v_i.\top \der \bot$ by (S3) and \law{an}.
\item (C2): write $E := \exists v_i.P$. By \law{ei} with $X := \lambda v_i.P$ and $a := v_i$, $P \der P \wedge E$. So $\iota(x + c_i x) = \neg(\neg P\wedge\neg E) \der \neg(\neg(P \wedge E)\wedge\neg E)$. By absorption (\law{abs}, with $\neg E$ for $X$ and $P$ for $Y$) and \law{dn}, $\neg E\wedge\neg(E \wedge P) \der \neg E$, so $\iota(x + c_i x) \der \neg\neg E \der E = \iota(c_i x)$.
\item (C3): $\exists v_i.(P \wedge \exists v_i.Q) \sameas (\exists v_i.P) \wedge (\exists v_i.Q)$ by (S3), since $v_i \notin \fv(\exists v_i.Q)$. (C4) is the second clause of (S3).
\item (C5): $v_i = v_i \sameas \top$ by (S4).
\item (C6): $\exists v_i.(v_j{=}v_i \wedge v_i{=}v_k) \sameas (\exists v_i.\,v_i{=}v_j) \wedge v_j{=}v_k \der v_j{=}v_k$ by (S4), (S3) and \law{i} ($\exists u.\,u{=}a \der \top$). This covers $j = k$, where $v_j{=}v_k \sameas \top$.
\item (C7): apply the one-point rule \law{op} with $u := v_i$ and $a := v_j$, once with $X := \lambda v_i.P$ and once with $X := \lambda v_i.\neg P$. This gives $\exists v_i.(v_i{=}v_j \wedge P) \wedge \exists v_i.(v_i{=}v_j\wedge\neg P) \der P[v_j/v_i] \wedge \neg P[v_j/v_i]$, which is $\der \bot$ by contradiction (\law{ctr}).
\item Dimension equations: $\exists v_i.R(v_0,\dots,v_{n-1}) \sameas R(v_0,\dots,v_{n-1}) \wedge \exists v_i.\top \der R(v_0,\dots,v_{n-1})$ by (S3) and vacuous quantification (\law{u}), since $i \geq n$.\qedhere
\end{itemize}
\end{proof}

\begin{lemma}\label{lem:roundtrip}
$\chi \der \iota(\operatorname{tr}\chi)$ for every formula $\chi$ whose variables are in the domain of $\kappa$.
\end{lemma}

\begin{proof}
By induction on $\chi$; every case but atoms is immediate from the definitions and congruence. For an atom,
\[\iota(\operatorname{tr}R(w_1,\dots,w_n)) = \exists v_0 \cdots \exists v_{n-1}.\,(v_0{=}w_1 \wedge \cdots \wedge v_{n-1}{=}w_n \wedge R(v_0,\dots,v_{n-1})),\]
where the $v_m$ differ from the $w$'s because $\kappa w \geq N$. Using (S3) to move each quantifier next to its equality, $n$ applications of the one-point rule \law{op} give $R(w_1,\dots,w_n)$.
\end{proof}

\begin{lemma}\label{lem:separate}
If $[\![t]\!]_M = [\![t']\!]_M$ for every structure $M$, then $t \approx t'$.
\end{lemma}

\begin{proof}
The quotient $\mathbf{F}/{\approx}$ satisfies the cylindric axioms, since every element is the class of a term and all instances were identified. It is locally finite: $c_k[t] = [t]$ whenever $k \geq N$ and $k$ does not occur in $t$, so the dimension set of $[t]$ lies in $\{0,\dots,N-1\}$ together with the indices occurring in $t$, a finite set. This follows by induction on $t$ from the dimension equations and these standard consequences of the axioms, the last three under the hypothesis $c_k x = x$ and $c_k y = y$:
\begin{itemize}
\item $c_k 0 = 0$ (C1), $c_k 1 = 1$ (C2 with $x := 1$) and $c_k c_k y = c_k y$ (C3 with $x := 1$);
\item $c_k d_{i,j} = d_{i,j}$ for $k \notin \{i,j\}$, from (C6) and $c_k c_k = c_k$;
\item $c_k(x\cdot y) = c_k(x \cdot c_k y) = c_k x \cdot c_k y = x \cdot y$ (C3);
\item $c_k(-x) = -x$: by (C3) and (C1), $c_k(-c_k x)\cdot c_k x = c_k(-c_k x \cdot c_k x) = c_k 0 = 0$, so $c_k(-c_k x) \le -c_k x$; with (C2) this is equality;
\item $c_k c_i x = c_i c_k x = c_i x$ by (C4).
\end{itemize}

Suppose $t \not\approx t'$. By \cref{thm:tarski} there is a homomorphism $h$ from $\mathbf{F}$ into a full cylindric set algebra over some base $U$ with $h(t) \neq h(t')$: compose the quotient map, the embedding into a product of set algebras, and a projection that separates the two images. Then $U \neq \emptyset$, since over the empty base the algebra has one element. Pick $z \in h(t) \mathbin{\triangle} h(t')$, and let $W$ be the set of sequences that differ from $z$ in finitely many places. Any two sequences in $W$ differ in finitely many coordinates, and the dimension equations let us change one coordinate at a time, so finitely many such steps connect them. Changing one coordinate of a sequence in $W$ keeps it in $W$, so $S \mapsto S \cap W$ preserves the Boolean operations (relative to $W$) and $C_i$, and sends $D_{i,j}$ to $D_{i,j} \cap W$.

Let $M$ have universe $U$, and for $R$ of arity $n$ let $R^M = \{(s_0,\dots,s_{n-1}) : s \in h(R)\cap W\}$. Then $h(R) \cap W = [\![R]\!]_M \cap W$. Indeed, if $s \in W$ agrees below $n$ with some $s' \in h(R) \cap W$, then $s$ and $s'$ differ in finitely many coordinates, all at least $n$. Since $h$ preserves the dimension equations, $C_i h(R) = h(R)$ for $i \geq n$, so changing those coordinates one at a time keeps us in $h(R)$. By induction on terms, $h(r) \cap W = [\![r]\!]_M \cap W$ for every term $r$. As $z \in W$, $z$ lies in exactly one of $[\![t]\!]_M$ and $[\![t']\!]_M$, contradicting the hypothesis.
\end{proof}

\begin{proof}[Proof of \cref{thm:complete}]
Let $\varphi \sem \psi$, renamed and translated as above. By \eqref{eq:tr}, $[\![\operatorname{tr}\varphi]\!]_M = [\![\operatorname{tr}\psi]\!]_M$ for every $M$. So $\operatorname{tr}\varphi \approx \operatorname{tr}\psi$ by \cref{lem:separate}, and $\iota\operatorname{tr}\varphi \der \iota\operatorname{tr}\psi$ by \cref{lem:iota}. By \cref{lem:roundtrip}, $\varphi \der \psi$.
\end{proof}

\begin{remark}[Concrete formulas, not schemas]
\Cref{thm:complete} is about concrete formulas: every instance of a valid law is derivable. It does not say that a valid law is derivable \emph{uniformly}, by one derivation in which its schema variables stay opaque symbols. We do not claim that. Monk's theorem suggests it fails: no finite set of equations in the cylindric signature axiomatises the representable cylindric algebras \cite{monk69}. We have not proved the translation from uniform derivability to cylindric equations that would make this a consequence.
\end{remark}

\subsection{Independence}\label{sec:independence}

\begin{theorem}\label{thm:independent}
Suppose $\Sigma$ contains a relation symbol $R$ of positive arity. Then none of the five laws is derivable from the other four together with $\sameas$.
\end{theorem}

The hypothesis is used for \law{dt}, \law{an} and \law{sub}, whose counterexamples below need an atom; for $\Sigma = \emptyset$ we have not settled their independence.

\begin{proof}
For each law we give an interpretation, compositional in the formula constructors and invariant under $\sameas$, that validates the other four laws for all instances and falsifies one instance of the law in question.
\begin{itemize}
\item \law{dn}, \law{dt}, \law{an}: forget variables. Use the three algebras with $\cdot = \min$ tabulated in the proof of \cref{thm:boolean}. Send $\wedge$ to $\cdot$, $\neg$ to $-$, $\top$ and every equality to $\top$, and $\exists w.\chi$ to the value of $\chi$; assign each relation symbol a value, which every atom with that symbol takes, whatever its arguments. \law{sub} becomes $\top \cdot x = \top \cdot x$, and \law{ei} becomes $x \cdot x = x$, which holds because $\min$ is idempotent. (S1)--(S4) hold trivially. \law{dn} fails at $\neg\neg\top$ in the first algebra. With $R$ given the value $1$, the instance $R \wedge \neg(R \wedge \top) \Leftrightarrow R \wedge \neg\top$ of \law{dt} takes values $1$ and $0$ in the second; with $R$ given the value $0$, the instance $\bot \wedge R \Leftrightarrow \bot$ of \law{an} takes values $0$ and $1$ in the third (writing $R$ for an atom $R(w,\dots,w)$).
\item \law{sub}: interpret $=$ as an arbitrary equivalence relation on $U$ rather than equality. (S4) holds because the relation is an equivalence, and \law{dn}, \law{dt}, \law{an}, \law{ei} do not depend on what $=$ means. With $U = \{0,1\}$, $=$ total and $R^M = \{0\}$, the instance $a{=}b \wedge R(a) \Leftrightarrow a{=}b \wedge R(b)$ fails at $a \mapsto 0$, $b \mapsto 1$.
\item \law{ei}: interpret every $\exists w.\chi$ as false. (S3) holds because both sides of each of its equations are then false; \law{sub} still holds because quantified subformulas are constant; \law{dn}, \law{dt}, \law{an} are Boolean identities. The instance $\exists u.\top \Leftrightarrow \top$ fails.\qedhere
\end{itemize}
\end{proof}

\section{Searching for the laws}\label{sec:search}

The five laws were chosen to be few and recognisable (\cref{sec:intro}). To find recognisable candidates we searched valid equations in order of size. The first-order search, run up to size 5, kept four of the five laws; deiteration has size 7 and was added by hand. The method follows Wolfram's listing of Boolean theorems by size. He observes that ``with the exception of the second distributive law'' the textbook's named theorems ``are exactly the ones that cannot be derived from preceding theorems in the list'' \cite[p.~817]{nks}. QuickSpec applies the same filter to discover laws of programs \cite{quickspec}. The method is:
\begin{enumerate}
\item enumerate valid equations in order of total size, up to the structural laws;
\item try to derive each from the equations kept so far;
\item keep it if that fails.
\end{enumerate}
Minimality is not the goal, so step 2 may be a bounded search: its only possible error is keeping a redundant law.

\subsection{Propositional search}
The propositional search tests the method against a known complete basis. Equations over at most four variables in $(\cdot, -, \top)$ were listed up to associativity, commutativity and unit, and ordered by size, the number of symbol occurrences. Each was given to Prover9 \cite{prover9} for 3 seconds with the equations kept so far as hypotheses. If Prover9 failed, the equation was kept, and Mace4 searched for a model of the earlier kept equations in which the new one fails. Every kept equation received such a countermodel, so none is derivable from the ones before it. After each addition, Prover9 had 30 seconds to derive Huntington's equation (H).

Up to size 10 there are 571 valid equations. Seven were kept:
\begin{center}
\begin{tabular}{rlll}
\toprule
& equation & elements in countermodel & name\\
\midrule
1 & $--\top = \top$ & 2 & double negation of $\top$\\
2 & $--x = x$ & 2 & double negation\\
3 & $x\cdot x = x$ & 2 & idempotence\\
4 & $\bot \cdot x = \bot$ & 2 & annihilation\\
5 & $-(-x\cdot x) = \top$ & 3 & non-contradiction\\
6 & $-(-x \cdot y)\cdot x = x$ & 6 & absorption\\
7 & $-(-(x\cdot y)\cdot x)\cdot y = y$ & 6 & (no standard name)\\
\bottomrule
\end{tabular}
\end{center}
After entry 7, Prover9 derived (H) in 0.04 seconds. Deiteration also has size 10, but the order within a size placed it after entry 7, and Prover9 derived it from the seven kept entries, so it was not kept. Prover9 derives (H) from $--x = x$ and entry 7 alone, so these two form a complete basis. We prefer double negation, deiteration and annihilation, because entry 7 is not a move a person would recognise.

A second sweep took eight candidate laws and determined, for each set of at most three of them, whether it derives (H): double negation; its instance $--\top = \top$; idempotence; deiteration under one negation (\law{dt}) and under two, $x \cdot -(y \cdot -(x \cdot z)) = x \cdot -(y \cdot -z)$; annihilation; contradiction $x \cdot -x = \bot$; and $x \cdot -(\bot \cdot y) = x$. Of the 92 sets, exactly four are complete, each of size three:
\begin{itemize}
\item double negation, deiteration and annihilation;
\item the same with annihilation replaced by contradiction, or by $x \cdot -(\bot \cdot y) = x$;
\item double negation, deiteration under two negations, and contradiction.
\end{itemize}
The other 88 have countermodels, with 2 elements (57 of them), 3 (30) or 6 (1). Replacing double negation by its instance $--\top = \top$ always loses completeness.

Published bases were also checked, each by asking Prover9 to derive (H) from it: Huntington's; Robbins' (with the unit law $x\cdot\top = x$ added); the single axiom DN1 and Meredith's pair, both as given by McCune et al.\ \cite{mccune-single}; Kauffman's pair \cite{kauffman}; Spencer-Brown's single equation, his Consequence 6 \cite{spencer-brown}, as formalised in \cite{lofmm}; Bricken's rules \cite{bricken}; and Meguire's B1--B4 \cite{meguire}. All are complete except Meguire's (\cref{prop:meguire}).

Bricken's rules without his involution law ($--x = x$) do not derive involution: in the two-element model with $\cdot = \min$, $\top = 1$ and $-x = 1$, his other rules hold, including deiteration into every context, while double negation fails.

All 121 countermodels were re-checked by a separate script that evaluates the equations in each model directly: 88 from the subset sweep, 26 from runs on single candidate laws and on the published bases, and 7 from the size-ordered search.

\subsection{First-order search}
First-order laws were enumerated as equations between schemas. A schema has at most two schema variables, with at most two arguments each, and two schema parameters $a, b$; it is built from these with negations, quantifiers and equalities. Size counts schema-variable occurrences, negations, quantifiers and equalities. The equalities at one node count as the number of joins needed to connect their variables: $a{=}b$ counts 1, and $a{=}b \wedge b{=}c$ counts 2. Schemas were enumerated up to structural identity. They were grouped by their truth values in all interpretations over domains of size 1 and 2, and in sampled interpretations over sizes 3 and 4. Prover9 then split each group into equivalence classes, reading a schema variable as an uninterpreted predicate on its arguments; each pair within a class is a valid equation. All 180{,}301 Prover9 runs succeeded, so no pair was left undecided.

Derivability was tested by a rewriting engine written for the purpose. It represents a formula up to structural identity, as the tree described after \cref{def:struct}. A law's negations match whole negated subformulas, its quantified variables match quantified variables used nowhere outside the match, and its schema variables match parts of a conjunction. The engine runs a bidirectional breadth-first search over formulas in two stages. The first goes to depth 6, visits at most 4{,}000 formulas, and allows intermediate formulas at most 2 larger than the larger side of the equation. The second goes to depth 7, visits at most 30{,}000, and allows 4. An equation is kept only if both searches fail, so for first-order laws ``kept'' means only ``not derived within these bounds''. The engine's soundness was tested on 1{,}067{,}173 rewrite steps, each checked to preserve truth values in sampled finite structures.

The outcome depended on how schema variables match. At first a schema variable could only match formulas whose free variables were among its arguments. Under that convention the search kept one variant of non-contradiction for each number of extra free variables, up to the size bound, because a two-argument schema variable cannot match a formula with three free variables. Allowing the matched formula to mention further variables in scope, as in \cref{def:instances}, removed these variants.

All 2{,}417 valid equations between schemas of total size (both sides) at most 5 were each either derived or kept: 1{,}526 derived directly by the engine, 880 by composing derivations already found, and 11 kept.
\begin{center}
\begin{tabular}{rll}
\toprule
size & kept equation & name\\
\midrule
1 & $\exists u.\top \Leftrightarrow \top$ & vacuous quantification (\law{u})\\
2 & $\exists u.\,a{=}u \Leftrightarrow \top$ & a variable has a witness (\law{i})\\
2 & $\neg\bot \Leftrightarrow \top$ & double negation of $\top$\\
3 & $\neg(\bot \wedge X) \Leftrightarrow \top$ & (no standard name)\\
3 & $\bot \wedge X \Leftrightarrow \bot$ & annihilation\\
3 & $X \wedge X \Leftrightarrow X$ & idempotence\\
4 & $a{=}b \wedge X(a,b) \Leftrightarrow a{=}b \wedge X(a,a)$ & substitution of equals\\
4 & $\neg(\neg X\wedge X) \Leftrightarrow \top$ & non-contradiction\\
4 & $\neg\neg X \Leftrightarrow X$ & double negation\\
4 & $X(a,b)\wedge \exists u.\,X(a,u) \Leftrightarrow X(a,b)$ & existential introduction\\
5 & $\exists u.\,\neg(\neg X(a,u) \wedge X(u,b)) \Leftrightarrow \top$ & drinker-style law\\
\bottomrule
\end{tabular}
\end{center}
The kept substitution and existential-introduction equations are \law{sub} and \law{ei} of \cref{def:laws} with $X$ also mentioning $b$, which \cref{def:instances} allows. The drinker-style law says $\exists u\,(X(u,b) \to X(a,u))$; it holds by cases, taking $u = a$ or $u = b$, like the drinker principle.

These eleven equations do not derive (H). To see this, forget variables as in the proof of \cref{thm:independent}: send equalities to $\top$ and drop quantifiers. The six-element countermodel for entry 7 of the propositional table then satisfies all eleven and falsifies (H). Adding deiteration, which has size 7, suffices. From the five laws alone the engine derived 13 targets, checking every step: \law{u} and \law{i}; the five kept equations not among the five laws or these two; Huntington's (H); absorption \law{abs}; the one-point rule \law{op}; and the schema forms of (C2), (C6) and (C7) that the completeness proof uses, (C6) being $\exists u.(a{=}b \wedge a{=}u) \Leftrightarrow a{=}b$.

The drinker-style law took 12 steps chosen by hand, with the gaps between them filled by the engine. \Cref{app:derivations} gives every one of these derivations. By \cref{thm:complete}, any set of valid laws that derives the five, such as the kept equations together with deiteration, is complete.

\section{Related work}\label{sec:related}

\emph{Equational presentations of the propositional part.} The three propositional laws come from Spencer-Brown's primary algebra \cite{spencer-brown}, an equational calculus of enclosures with juxtaposition read as disjunction; dualised, his reflexion, generation and integration are \law{dn}, \law{dt} and \law{an}. Kauffman and Collings adopt these three, credited to a 1986 report of Bricken, ``as an axiomatically complete basis for the Primary Algebra'' \cite{kauffman-collings,bricken86}. Bricken presents occlusion, involution and pervasion (deiteration at every depth) as the axioms of boundary logic and relates them to Peirce's alpha graphs \cite{bricken,bricken-difference}. Meguire's boundary algebra \cite{meguire} is incomplete (\cref{prop:meguire}).

\emph{Peirce's graphs as proof systems.} Proof systems for Peirce's graphs use one-way weakening; our laws are all two-way. Brady and Trimble prove that alpha, as an equational theory, is the theory of Boolean algebras \cite{brady-trimble-alpha}. Their equivalence is mutual derivability under Peirce's rules, including weakening, and their completeness proof uses weakening. Their beta calculus is sound and complete for first-order logic, again with weakening, and with rules that cut and splice lines, together generating a preorder \cite{brady-trimble-beta}. Ma and Pietarinen give a deep-inference reformulation of alpha whose rules include deletion and insertion \cite{ma-pietarinen}; Donato's flower calculus is complete for intuitionistic provability \cite{donato-flower}. These systems derive theorems; our laws connect any two equivalent formulas without passing through a non-equivalent one.

\emph{Diagrammatic first-order logic.} Our laws are equations on formulas with negation primitive, not a diagrammatic calculus. The closest diagrammatic calculi either reason by inequalities or derive negation. Haydon and Sobociński give a compositional calculus of beta graphs and conjecture it complete \cite{haydon-sobocinski}; it uses inequalities and a contraposition rule. Bonchi, Di~Giorgio, Haydon and Sobociński prove a complete axiomatisation of the calculus of neo-Peircean relations \cite{bdhs-lics24,bdhs-lmcs}. Its proofs are chains of inequalities, negation is derived rather than primitive, empty domains are allowed, and the authors call the axioms ``far from minimal''. Bonchi, Di~Giorgio and Trotta give an equational presentation of Boolean hyperdoctrines in the same style, again with negation derived \cite{bdt-mfcs24}. Our result does not settle the Haydon--Sobociński conjecture, whose calculus is different.

\emph{Cylindric algebras.} The route of \cref{sec:fo}, through Tarski's representation theorem, is the classical proof of completeness for ranked first-order logic \cite[Thm.~7.9]{ans-handbook}. Our contribution there is the translation showing that the five laws derive every cylindric axiom, given the structural laws.

\appendix
\section{Derivations of the search targets}\label{app:derivations}

Each of the 13 targets of \cref{sec:search} follows from the five laws. All but the drinker-style law follow directly from results in \cref{sec:boolean,sec:fo}:
\begin{center}
\begin{tabular}{ll}
\toprule
target & derivation\\
\midrule
\law{u}: $\exists u.\top \Leftrightarrow \top$ & \law{ei} with $X := \lambda x.\top$ (\cref{sec:derived})\\
\law{i}: $\exists u.\,a{=}u \Leftrightarrow \top$ & \law{ei} with $X := \lambda x.(x = a)$ (\cref{sec:derived})\\
$\neg\bot \Leftrightarrow \top$ & \law{dn}, since $\neg\bot = \neg\neg\top$\\
$\neg(\bot \wedge X) \Leftrightarrow \top$ & \law{an}, then $\neg\bot \Leftrightarrow \top$\\
$X \wedge X \Leftrightarrow X$ & \law{u}, (S3), \law{ei} (\cref{sec:derived})\\
$\neg(\neg X \wedge X) \Leftrightarrow \top$ & \law{ctr} inside the negation, then $\neg\bot \Leftrightarrow \top$\\
(H) & steps 1--4 of the proof of \cref{thm:boolean}\\
\law{abs}: $X \wedge \neg(\neg X \wedge Y) \Leftrightarrow X$ & step 3 of the proof of \cref{thm:boolean}\\
\law{op}: $\exists u.(u{=}a \wedge X(u)) \Leftrightarrow X(a)$ & \law{sub}, (S3), \law{i} (\cref{sec:derived})\\
(C2): $X(a,b) \wedge \exists u.X(u,b) \Leftrightarrow X(a,b)$ & \law{ei} at $\lambda x.X(x,b)$\\
(C6): $\exists u.(a{=}b \wedge a{=}u) \Leftrightarrow a{=}b$ & (S4), (S3), \law{i}\\
(C7): $\exists u.(u{=}a \wedge X(u)) \wedge \exists v.(v{=}a \wedge \neg X(v)) \Leftrightarrow \bot$ & \law{op} twice, then \law{ctr}\\
\bottomrule
\end{tabular}
\end{center}

The remaining target needs one more lemma: from $\neg\exists u.\varphi(u)$ one may add $\neg\varphi(a)$ for any $a$.

\begin{lemma}[Universal instantiation]\label{lem:ui}
$\neg\exists u.Z(u) \der \neg\exists u.Z(u) \wedge \neg Z(a)$.
\end{lemma}

\begin{proof}
Write $S := \exists u.Z(u)$. Absorption \law{abs}, read right to left with $\neg S$ for its $X$ and $Z(a)$ for its $Y$, gives $\neg S \der \neg S \wedge \neg(\neg\neg S \wedge Z(a))$. Double negation inside turns this into $\neg S \wedge \neg(S \wedge Z(a))$, and $Z(a) \wedge \exists u.Z(u) \der Z(a)$ by \law{ei}, which leaves $\neg S \wedge \neg Z(a)$.
\end{proof}

\begin{proposition}[The drinker-style law, $\exists u\,(X(u,b) \to X(a,u))$]
$\exists u.\,\neg(\neg X(a,u) \wedge X(u,b)) \der \top$.
\end{proposition}

\begin{proof}
Write $D(w) := \neg(\neg X(a,w) \wedge X(w,b))$, which says $X(w,b) \to X(a,w)$, and $S := \exists u.D(u)$. The idea: if $S$ failed, both $D(b)$ and $D(a)$ would fail, and their failures contradict each other on $X(a,b)$.
\begin{align*}
S &\der \neg\neg S && \law{dn}\\
&\der \neg(\neg S \wedge \neg D(b) \wedge \neg D(a)) && \text{\cref{lem:ui}, twice}\\
&\der \neg(\neg S \wedge \neg X(a,b) \wedge X(b,b) \wedge \neg X(a,a) \wedge X(a,b)) && \text{\law{dn} on $\neg D(b)$ and on $\neg D(a)$}\\
&\der \neg(\neg S \wedge X(b,b) \wedge \neg X(a,a) \wedge \bot) && \text{\law{ctr} on $X(a,b) \wedge \neg X(a,b)$}\\
&\der \neg\bot && \law{an}\\
&\der \top && \law{dn}.
\end{align*}
Both uses of \cref{lem:ui} are inside the outer negation. The engine's chain for this derivation has the same shape, with each use of \cref{lem:ui} spelled out as its three steps.
\end{proof}

\begin{thebibliography}{10}

\bibitem{ans-handbook}
Hajnal Andr{\'e}ka, Istv{\'a}n N{\'e}meti, and Ildik{\'o} Sain.
\newblock Algebraic logic.
\newblock In {\em Handbook of Philosophical Logic}, volume~2, pages 133--247.
  Springer, 2nd edition, 2001.
\newblock Preprint:
  \url{https://old.renyi.hu/pub/algebraic-logic/handbook.pdf}.

\bibitem{bdhs-lics24}
Filippo Bonchi, Alessandro Di~Giorgio, Nathan Haydon, and Pawe{\l}
  Soboci{\'n}ski.
\newblock Diagrammatic algebra of first order logic.
\newblock In {\em Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in
  Computer Science (LICS 2024)}, pages 1--15. ACM, 2024.

\bibitem{bdhs-lmcs}
Filippo Bonchi, Alessandro Di~Giorgio, Nathan Haydon, and Pawe{\l}
  Soboci{\'n}ski.
\newblock The calculus of neo-{P}eircean relations.
\newblock {\em Logical Methods in Computer Science}, 22(2):29:1--29:75, 2026.

\bibitem{bdt-mfcs24}
Filippo Bonchi, Alessandro Di~Giorgio, and Davide Trotta.
\newblock When {L}awvere meets {P}eirce: An equational presentation of
  {B}oolean hyperdoctrines.
\newblock In {\em 49th International Symposium on Mathematical Foundations of
  Computer Science (MFCS 2024)}, volume 306 of {\em LIPIcs}, pages 30:1--30:19.
  Schloss Dagstuhl, 2024.

\bibitem{brady-trimble-alpha}
Geraldine Brady and Todd~H. Trimble.
\newblock A categorical interpretation of {C.S.} {P}eirce's propositional logic
  {A}lpha.
\newblock {\em Journal of Pure and Applied Algebra}, 149(3):213--239, 2000.

\bibitem{brady-trimble-beta}
Geraldine Brady and Todd~H. Trimble.
\newblock A string diagram calculus for predicate logic and {C. S.} {P}eirce's
  system {B}eta.
\newblock Preprint, 1998, revised 2000.
  \url{https://ncatlab.org/nlab/files/BradyTrimbleString.pdf}, 2000.

\bibitem{bricken86}
William Bricken.
\newblock A deductive mathematics for efficient reasoning.
\newblock Technical Report HITL-R-86-2, Human Interface Technology Laboratory,
  1986.

\bibitem{bricken-difference}
William Bricken.
\newblock What's the difference? {C}ontrasting boundary and {B}oolean algebras.
\newblock Manuscript, October 2005.
  \url{http://iconicmath.com/mypdfs/bl-the-difference.080830.pdf}, 2005.

\bibitem{bricken}
William Bricken.
\newblock Boundary logic and alpha existential graphs.
\newblock Manuscript dated 2006-01-23.
  \url{http://iconicmath.com/mypdfs/bl-aeg.060123.pdf}, 2006.

\bibitem{donato-flower}
Pablo Donato.
\newblock The flower calculus.
\newblock In {\em 9th International Conference on Formal Structures for
  Computation and Deduction (FSCD 2024)}, volume 299 of {\em LIPIcs}, pages
  5:1--5:24. Schloss Dagstuhl, 2024.

\bibitem{haydon-sobocinski}
Nathan Haydon and Pawe{\l} Soboci{\'n}ski.
\newblock Compositional diagrammatic first-order logic.
\newblock In {\em Diagrammatic Representation and Inference (Diagrams 2020)},
  volume 12169 of {\em LNCS}, pages 402--418. Springer, 2020.

\bibitem{hmt2}
Leon Henkin, J.~Donald Monk, and Alfred Tarski.
\newblock {\em Cylindric Algebras, Part {II}}, volume 115 of {\em Studies in
  Logic and the Foundations of Mathematics}.
\newblock North-Holland, Amsterdam, 1985.

\bibitem{huntington33}
Edward~V. Huntington.
\newblock New sets of independent postulates for the algebra of logic, with
  special reference to {W}hitehead and {R}ussell's {P}rincipia mathematica.
\newblock {\em Transactions of the American Mathematical Society},
  35(1):274--304, 1933.

\bibitem{kauffman}
Louis~H. Kauffman.
\newblock Robbins algebra.
\newblock \url{http://homepages.math.uic.edu/~kauffman/Robbins.htm}.

\bibitem{kauffman-collings}
Louis~H. Kauffman and Arthur~M. Collings.
\newblock The {BF} calculus and the square root of negation.
\newblock In {\em Laws of Form: A Fiftieth Anniversary}, Series on Knots and
  Everything, pages 253--283. World Scientific, 2023.
\newblock Preprint arXiv:1905.12891.

\bibitem{ma-pietarinen}
Minghui Ma and Ahti-Veikko Pietarinen.
\newblock Proof analysis of {P}eirce's alpha system of graphs.
\newblock {\em Studia Logica}, 105(3):625--647, 2017.

\bibitem{mccune-robbins}
William McCune.
\newblock Solution of the {R}obbins problem.
\newblock {\em Journal of Automated Reasoning}, 19(3):263--276, 1997.

\bibitem{prover9}
William McCune.
\newblock Prover9 and {M}ace4, 2005--2010.
\newblock Version 2009-11A. \url{https://www.cs.unm.edu/~mccune/prover9/}.

\bibitem{mccune-single}
William McCune, Robert Veroff, Branden Fitelson, Kenneth Harris, Andrew Feist,
  and Larry Wos.
\newblock Short single axioms for {B}oolean algebra.
\newblock {\em Journal of Automated Reasoning}, 29(1):1--16, 2002.

\bibitem{meguire}
Philip Meguire.
\newblock Boundary algebra: A simpler approach to {B}oolean algebra and the
  sentential connectives.
\newblock Working Papers in Economics 10/50, Department of Economics and
  Finance, University of Canterbury, 2010.
\newblock \url{https://repec.canterbury.ac.nz/cbt/econwp/1050.pdf}.

\bibitem{monk69}
J.~Donald Monk.
\newblock Nonfinitizability of classes of representable cylindric algebras.
\newblock {\em Journal of Symbolic Logic}, 34(3):331--343, 1969.

\bibitem{monk-henkin}
J.~Donald Monk.
\newblock Leon {H}enkin and cylindric algebras.
\newblock In {\em The Life and Work of Leon Henkin}, Studies in Universal
  Logic, pages 59--66. Birkh{\"a}user, 2014.
\newblock Author's copy: \url{https://euclid.colorado.edu/~monkd/monk85.pdf}.

\bibitem{lofmm}
Naipmoro.
\newblock lofmm: {L}aws of {F}orm in {M}etamath.
\newblock \url{https://naipmoro.github.io/lofmm/}.

\bibitem{quickspec}
Nicholas Smallbone, Moa Johansson, Koen Claessen, and Maximilian Algehed.
\newblock Quick specifications for the busy programmer.
\newblock {\em Journal of Functional Programming}, 27:e18, 2017.

\bibitem{spencer-brown}
G.~Spencer-Brown.
\newblock {\em Laws of Form}.
\newblock Allen and Unwin, London, 1969.

\bibitem{nks}
Stephen Wolfram.
\newblock {\em A New Kind of Science}.
\newblock Wolfram Media, Champaign, IL, 2002.
\newblock pp.~816--818.

\end{thebibliography}
\end{document}