Is it possible to express that functions are inverses, quantifying over one variable? So, I have two functions, $f:X \to Y$ and $g: Y \to X$, and I want to express the proposition that they are inverses of each other.
The classical way to do this is showing that $\forall x\in X \ldotp g(f(x))=x$, and that $\forall y \in Y \ldotp f(g(y)) = y$.
However, I'm using these in an SMT setting, and for technical reasons, I can only quantify over the set $X$, not $Y$.
I'm wondering, is there some proposition $P(x,f,g)$ I can use, where $f$ and $g$ are inverses of each other, if and only if $\forall x \in X \ldotp P(x,f,g)$?
EDIT: I had an extra function application in each condition, thanks @yanko
 A: No, this is not possible.  To be more precise, working over a two-sorted language with $X$ and $Y$ as the sorts and two function symbols $f:X\to Y$ and $g:Y\to X$, there is no first-order sentence $\varphi$ with quantifiers only on variables from $X$ which expresses that $f$ and $g$ are inverses.  To prove this, note that such a sentence can only involve variables from $X$, and so the only way a $Y$-valued term can appear in it is via the function $f$.  This means that the only elements of $Y$ you can ever refer to are elements which are in the image of $f$.  Thus such a sentence is true for $f:X\to Y$ and $g:Y\to X$ iff it is true for $f:X\to f(X)$ and $g|_{f(X)}:f(X)\to X$, where you replace $Y$ with the image $f(X)$.  If $g$ is a left inverse to $f$ but not a right inverse, then $g$ becomes a two-sided inverse after replacing $Y$ with $f(X)$, so any $\varphi$ that is true for inverses will also be true whenever $g$ is just a left inverse to $f$.
(To be more precise, you can prove by induction on formulas that if $\varphi(x_1,\dots,x_n)$ is any formula with only variables from $X$, then $\varphi(a_1,\dots,a_n)$ is true for any $a_1,\dots,a_n$ in some structure iff it is true in the modified structure where you replace $Y$ with $f(X)$.  We are then using this fact in the special case that $\varphi$ is a sentence.)
