Are ordered and unordered pairing functions "definably equivalent?" This question is basically a lift to MO of a part of an old MSE question. That question asked, roughly, for the model-theoretic relationship between ordered and unordered pairing functions. To keep things precise, given a structure $\mathcal{A}$ say that

*

*$\mathcal{A}$ has a pairing function iff there is a formula $\varphi(x,y,z)$ with parameters from $\mathcal{A}$ such that $$\mathcal{A}\models\forall x,y\exists!z\varphi(x,y,z)\wedge \forall x,y,x',y',z(\varphi(x,y,z)\wedge\varphi(x',y',z)\leftrightarrow x=x'\wedge y=y'),$$ and


*$\mathcal{A}$ has an unordered pairing function iff there is a formula $\varphi(x,y,z)$ with parameters from $\mathcal{A}$ satisfying the same condition but with the clause $x=x'\wedge y=y'$ replaced by $(x=x'\wedge y=y')\vee (x=y'\wedge y=x')$.
Any of the usual definitions of set-theoretic ordered pairs show that every structure that has an unordered pairing function also has a pairing function. The converse, however, is open:

Is there a structure $\mathcal{A}$ which has a pairing function but does not have an unordered pairing function?

There is a natural guess at such a structure: namely, $$\mathcal{G}=(\mathbb{N};g)$$ where $g$ is a "sufficiently generic" bijection $\mathbb{N}^2\rightarrow\mathbb{N}$ with respect to the poset of finite partial injections $\mathbb{N}^2\rightarrow\mathbb{N}$ ordered by reverse inclusion as usual. I suspect there's actually an easy argument here, but I'm not seeing it:

Is $\mathcal{G}$ as defined above indeed an example of the type of structure desired?

 A: The answer is no. Consider absolutely free algebra $\mathfrak{A}=(A;0,\langle \cdot,\cdot\rangle)$ with one binary function $\langle \cdot,\cdot\rangle$ and one generator $0$. Clearly, $\langle \cdot,\cdot\rangle$ is a pairing function on $\mathfrak{A}$. As I will show below there are no definable unordered pairing functions on this structure.
The elementary theory of $\mathfrak{A}$. admits quatifier elimination in the language extended by functions $\pi_1(x),\pi_2(x)$, where $\pi_1(0)=\pi_2(0)=0$, $\pi_1(\langle x,y\rangle)=x$, and $\pi_2(\langle x,y\rangle)=y$ (this follows from a more general result of Mal'tsev[1]).
Suppose for a contradiction that we have an unordered pairing  function $\varphi(x,y,z)$. We put in quantifier-free form. Since over $\mathfrak{A}$ we could transform equality $\langle t,u\rangle=v$ to the conjunction $t=\pi_1(v)\land u=\pi_2(v)$, we equivalently transform $\varphi(x,y,z)$ to a quantifier-free formula without function $\langle \cdot,\cdot\rangle$. Hence each term in $\varphi(x,y,z)$ is of the form $\pi_{i_1}\ldots\pi_{i_m}(w)$, where $w\in \{x,y,z\}$, or of the form $\pi_{i_1}\ldots\pi_{i_m}(0)$; further we transform all the terms of the latter form to just $0$.
Let terms $t_n(x)$ be $$t_0(x)=x\text{ and }t_{n+1}(x)=\langle t_n(x),0\rangle.$$ By choosing $n$ to be equal to the maximal length of $\pi$-function chains in $\varphi$-terms we observe that $\varphi(t_n(x),t_n(y),z)$ is equivalent to a quantifier-free formula $\psi(x,y,z)$, where all terms are either $0,x,y$, or of the form $\pi_{i_1}\ldots\pi_{i_m}(z)$. Of course, $$\mathfrak{A}\models \forall x,y\exists!z \;\psi(x,y,z).$$ Now it is easy to see that there should be a term $u(x,y)$ using just $0$ and $\langle\cdot,\cdot\rangle$ such that $$\mathfrak{A}\models \forall x,y,z( \psi(x,y,z)\land x\ne y\land x\ne 0\land y\ne 0 \to z=u(x,y)).$$
However, for any $a\ne b$, $a\ne 0$, $b\ne 0$ from $\mathfrak{A}$, clearly $\mathfrak{A}\models u(a,b)\ne u(b,a)$. We should have had
$$\mathfrak{A}\models \forall z\; (\psi(a,b,z)\mathrel{\leftrightarrow} \psi(b,a,z)).$$
However, $\mathfrak{A}\models \psi(a,b,u(a,b))$ and  $\mathfrak{A}\not\models \psi(b,a,u(a,b))$, contradiction.
[1]Anatolii I. Mal’tsev, On the elementary theories of locally free universal algebras, Doklady Akademii Nauk SSSR 138 (1961), no. 5, pp. 1009–1012 (in Russian), English translation in: Soviet Mathematics – Doklady 2 (1961), no. 3, pp. 768–771.
