An unordered pairing function in Peano arithmetic

Question

I know that Peano Arithmetic can define an ordered pair function, that is a function $f$ such that $f(x,y)=f(z,w) \iff (x=z \land y=w)$. However, I would be very interested if Peano Arithmetic can define an unordered pair function, that is a function $f$ such that $f(x,y)=f(z,w) \iff ((x=z \land y=w) \vee (x=w \land y=z))$. I would also like an explicit description of such a function.

Answer 1

What about something like:

Let $f(x,y)$ be an ordered pair function.

$$g(x,y) := \begin{cases} f(x,y) \, x>y \\ f(y,x) \, x\leq y \end{cases}$$

Then $g(x,y) = g(y,x)$

And $$g(x,y) = g(z,w) \implies \\ (f(x,y)= f(z,w) \land x>y \land z>w) \\ \lor (f(x,y)= f(w,z) \land x>y \land z\leq w) \\ \lor (f(y,x)= f(z,w) \land x\leq y \land z>w) \\ \lor (f(y,x)= f(w,z) \land x\leq y \land z\leq w) \\ \implies (x=z \land y=w)\lor (x=w \land y=z) $$

Answer 2

If you write $\langle x, y \rangle$ for the representation of the ordered pair then the unordered pair can be represented by $$\mathbf{if}\; x < y \;\mathbf{then}\;\langle x, y \rangle \;\mathbf{ else}\; \langle y, x\rangle $$ (and you can use primitive recursion to represent the conditional operator).