Is the class of image mappings axiomatizable by equations and subset relations?

Question

This is a follow-up to my question on axiomatizability of image mappings, here: Is the class of image mappings first-order axiomatizable?. I should have really asked this question first, for this is the question I really want answered. Is the class of image mappings axiomatizable by a set of equations and subset relations? And if so, is it axiomatizable by a finite such set? By a subset relation, I mean a sentence of the form $t \subseteq t'$, for some terms $t$ and $t'$.

Answer 1

Yes and no.

First of all, let me observe that given a powerset algebra $\mathcal{P}(S)$, a function $f\colon \mathcal{P}(S)\to \mathcal{P}(S)$ is the image mapping for a binary relation $R$ on $S$ if and only if $f$ preserves all unions.

Proof: It is easy to check that image mappings preserve all unions. Conversely, suppose $f$ preserves all unions. Define a binary relation $R$ on $S$ by $xRy$ if and only if $\{y\}\subseteq f(\{x\})$, and let $f'$ be the image mapping for $R$. It remains to show that $f = f'$. So take any $X\in \mathcal{P}(S)$. Since $f$ preserves unions, $$f(X) = f\left(\bigcup_{x\in X}\{x\}\right) = \bigcup_{x\in X} f(\{x\}).$$ So for any $y\in S$, ($y\in f(X)$) iff ($y\in f(\{x\})$ for some $x\in X$) iff ($xRy$ for some $x\in X$) iff ($y\in f'(X)$), and hence $f(X) = f'(X)$.

---

This characterization gives a partial positive answer to your question. $f$ preserving all unions is axiomatizable by a set of equations (the equations $f(\bigcup_{i\in I} x_i) = \bigcup_{i\in I} f(x_i)$ for all index sets $I$), but only if we have function symbols for arbitrary infinitary unions in our language. In your previous question, you said you wanted to consider powerset algebras in the language of Boolean algebras, namely $\{0,1,\cup,\cap,\setminus, \subseteq\}$, and here I assume the union symbol is binary. In fact, allowing infinitary unions takes us outside of first-order logic, where all function symbols have finite arity.

If you want to stay within a finitary framework and work with the language of Boolean algebras, your question has a negative answer. Note that any class axiomatized by a set of universally quantified atomic formulas (in this case equations and subset relations) is closed under homomorphic images. So it suffices to find a surjective homomorphism $(\mathcal{P}(S),f,0,1,\cup,\cap,\setminus,\subseteq) \to (\mathcal{P}(S'),f',0,1,\cup,\cap,\setminus,\subseteq)$ such that $f$ is an image mapping on $\mathcal{P}(S)$ but $f'$ is not an image mapping on $\mathcal{P}(S')$.

Let $S = \omega\sqcup \omega$, so $\mathcal{P}(S) \cong \mathcal{P}(\omega)\times \mathcal{P}(\omega')$, writing the second copy of $\omega$ as $\omega' = \{0',1',2',\dots\}$. Consider the relation $R = \{(n,n')\mid n\in \omega\}$ on $S$, and let $f$ be the image mapping for $R$. Thinking of $f$ as a unary function on $\mathcal{P}(\omega)\times \mathcal{P}(\omega')$, we have $f(A,B) = (\varnothing,A')$, where $A' = \{n'\mid n\in A\}$.

Let $S' = \omega\sqcup \{*\}$, so $\mathcal{P}(S') \cong \mathcal{P}(\omega)\times 2$. Pick a non-principal ultrafilter $\mathcal{U}$ on $\omega'$. This gives us a Boolean homomorphism $h_{\mathcal{U}}\colon \mathcal{P}(\omega')\to 2$, by $$h_{\mathcal{U}}(C) = \begin{cases} \{*\}&\text{if }C\in \mathcal{U}\\ \varnothing&\text{if }C\notin \mathcal{U}.\end{cases}$$ Define $f'$ on $\mathcal{P}(\omega)\times 2$ by $f'(A,B) = (\varnothing,h_{\mathcal{U}}(A'))$.

Now define a homomorphism $g\colon \mathcal{P}(\omega)\times \mathcal{P}(\omega')\to \mathcal{P}(\omega)\times 2$ by $g(A,B) = (A,h_\mathcal{U}(B))$. This is a product of two Boolean homomorphisms, so it is a Boolean homomorphism, and it is also a homomorphism in the language with the unary function symbol. Indeed, $$g(f(A,B)) = g(\varnothing,A') = (\varnothing,h_{\mathcal{U}}(A')) = f'(A,h_{\mathcal{U}}(B)) = f'(g(A,B)).$$

But $f'$ is not an image mapping on $\mathcal{P}(S')$, because it does not preserve arbitrary unions. For every $n\in \omega$, $\{n'\}\notin \mathcal{U}$ since $\mathcal{U}$ is non-principal, so $f'(\{n\},\varnothing) = (\varnothing, h_{\mathcal{U}}(\{n'\}) = (\varnothing,\varnothing)$. So $$\bigcup_{n\in \omega} f'(\{n\},\varnothing) = \bigcup_{n\in \omega}(\varnothing,\varnothing) = (\varnothing,\varnothing),$$ while $$f'\left(\bigcup_{n\in \omega} (\{n\},\varnothing)\right) = f'(\omega,\varnothing) = (\varnothing,h_{\mathcal{U}}(\omega)) = (\varnothing,\{*\}).$$

---

In my answer to the linked question, I showed that the class of image mappings is first-order definable within the class of powerset algebras, essentially by translating the "preserves arbitrary unions" condition to one that can be described by quantifying over the atoms of the algebra. But quantifying over the atoms requires a higher quantifier complexity - you can't play the same trick if you restrict yourself to universally quantified equations and subset relations.

An interesting follow-up question is whether this class can be defined by a universal first-order theory (i.e. by a theory made up of finite Boolean combinations of equations and subset relations). We would get a negative answer if we could find $h\colon (\mathcal{P}(S),f)\to (\mathcal{P}(S'),f')$ which an embedding of Boolean algebras expanded with a new unary function, and such that $f'$ preserves arbitrary unions but $f$ does not.