Is the theory of the adjunction operation, used for algebraization of hereditarily finite set theory, algebraizable?

Question

The operation used for algebraization of hereditarily finite set theory is named adjunction in 〈A. Tarski, S. Givant, A Formalization of Set Theory without Variables, Providence, RI: American Mathematical Society. 1987〉 and its infix sign is this: “$\rhd$”. Even though the adjunction is represented in a different manner (by using punctuation signs) in the paper 〈L. Kirby, Finitary Set Theory, Notre Dame Journal of Formal Logic Volume 50, Number 3, 2009.〉, this paper is a nice presentation of the theory of inheritably finite sets.

The adjunction operation can be expressed through union and singleton like this

$$x \rhd y = x \cup \{y\}.$$

However, the axiom stating the existence of this operation (i.e. stating that for any two sets $x$, $y$, the set $x \rhd y$ exists.) was formulated way earlier in 〈Bernays, Paul (1937), A System of Axiomatic Set Theory—Part I, The Journal of Symbolic Logic, Association for Symbolic Logic, 2 (1): 65–77〉 as an axiom of a formulation of set theory in Bernays's terms, like this:

$$\forall x \forall y \exists u \forall z\ (z\in u\leftrightarrow(z\in x\lor z=y)).$$

My question is whether the theory in the language with two symbols “$\in$” and “$=$”, with this axiom as well as the axioms for “=” is algebraizable. I will name this theory “pure adjunctive theory” (PAT) for the reasons below.

Usually, they name “adjunctive set theory” this theory plus the axiom of existence of empty set, and when they also add the extensionality axiom they denote the resulting theory “ST”. But I am interested in “algebraizability” more than in other aspects, like those which served as reason to add axioms to Bernays' axiom and study the resulting theory.

The empty set axiom is usually added to PAT, since without it, the natural numbers could not be represented in the theory. But I am more interested to learn how the PAT theory with atoms, including with Quine atoms, will look like. Thus, my question is about PAT without other axioms added to it.

An important remark is that I am not sure what is “algebraization of set theory” and I am expecting to learn this from your answers (see also my other question What is "algebraic theory" in the wide sense?).

Answer 1

To get things started, consider an algebraic theory with a binary symbol $\triangleright$, and axioms (where $x \triangleright y \triangleright z = (x \triangleright y) \triangleright z$):

\begin{align*} z \triangleright x \triangleright y &= z \triangleright y \triangleright x\\ y \triangleright x \triangleright x &= y \triangleright x \end{align*}

We may introduce some abbreviations:

• $x \in y$ stands for $y = y \triangleright x$
• $\{x_1, \ldots, x_n\}$ stands for $\emptyset \triangleright x_1 \triangleright \cdots \triangleright x_n$

We are not done, however, because it introduce $\emptyset$ and state $\forall x \,.\, x \not\in \emptyset$ in an algebraic way. We could do it if we had binary $\cup$, but that is not exprssible using only $\triangleright$. Indeed, there are models which are closed under $\triangleright$ (interpreted as adjoining an element to a set) but not under binary unions.