Is the class of image mappings first-order axiomatizable?

Question

Let $S$ be a set, and let $R$ be a binary relation on $S$. $R$ induces a mapping $f:\mathcal{P}(S) \rightarrow \mathcal{P}(S)$ such that for any subset $T$ of $S$, $f(T)$ is the image of $T$ under the relation $R$. Now, consider the class of structures of the form $(\mathcal{P}(S);f,0,1,\cup,\cap,\setminus,\subseteq)$, where $0$ is the empty set, $1$ is the set $S$, $\setminus$ is set difference, and the other symbols are well-known. We can write down some statements that image mappings satisfy, like $f(0)=0$ and $f(x \cup y) = f(x) \cup f(y)$. My question is this. In the first-order language $\{f,0,1,\cup,\cap,\setminus,\subseteq\}$, is there a set of axioms that characterize whenever $f$ is an image mapping induced by a relation $R$. More precisely, if we restrict our attention on the class of structures of the form $(\mathcal{P}(S);f,0,1,\cup,\cap,\setminus,\subseteq)$, and we interpret $0$ as the empty set, $1$ as the set $S$, $\cup$ as union, $\cap$ as intersection, $\setminus$ as set difference, and $\subseteq$ as the subset relation, is there a set of first-order axioms that hold true precisely when $f$ is an induced image mapping? And if there is, is there a finite such set of axioms?

Answer 1

First note that the set of atoms in the power set algebra is definable. Now consider the following sentence $\varphi$: for all $X$ and all atoms $y$, $y$ is below $f(X)$ if and only if there is some atom $x$ below $X$ such that $y$ is below $f(x)$.

Suppose $R$ is a binary relation on $S$, and $f\colon \mathcal{P}(S)\to \mathcal{P}(S)$ is the image mapping. Note that $xRy$ if and only if $\{y\}\subseteq f(\{x\})$. And for any $X\subseteq S$, $y\in f(X)$ if and only if there is $x\in X$ such that $xRy$. Putting these observations together, for an atom $\{y\}$, we have $\{y\}\subseteq f(X)$ if and only if there exists an atom $\{x\}\subseteq X$ such that $\{y\}\subseteq f(\{x\})$. This shows that every image mapping satisfies $\varphi$.

Conversely, I claim that for every structure $(\mathcal{P}(S);f,0,1,\cup,\cap,\setminus,\subseteq)$ which satisfies $\varphi$, $f$ is the image mapping for some binary relation $R$ on $S$. Define the relation $R$ by $xRy$ if and only if $\{y\}\subseteq f(\{x\})$, and let $f'$ be the image mapping for this $R$. It remains to show that $f' = f$. So pick $X\subseteq S$ and show that $f(X) = f'(X)$. For any $y\in S$, we have $y\in f(X)$ iff $\{y\}\subseteq f(X)$ iff (by $\varphi$) there is some $\{x\}\subseteq X$ such that $\{y\}\subseteq f(\{x\})$ iff (by definition of $R$) there is some $x\in X$ such that $xRy$ iff $y\in f'(X)$.