1
$\begingroup$

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

$\endgroup$
4
  • $\begingroup$ I believe you mean $gf(x)=x$ instead $fgf(x)=x$, the same with $gfg$. $\endgroup$
    – Yanko
    Nov 15, 2017 at 21:46
  • $\begingroup$ @yanko Whoops, thanks1 $\endgroup$ Nov 15, 2017 at 21:50
  • 2
    $\begingroup$ If you can't quantify over $Y$, then it would seem that you can never even speak about whether $Y$ contains elements outside the range of $f$. $\endgroup$ Nov 15, 2017 at 21:54
  • $\begingroup$ @HenningMakholm That... makes sense. $\endgroup$ Nov 15, 2017 at 22:30

1 Answer 1

2
$\begingroup$

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.)

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .