# Does there exist a function such that for all $y$ there exists a $x$ such that $f(y) \ne x$

$$\forall x \forall y ( x \ne y \implies f(x) \ne f(y)) \land \exists x \forall y (f(y) \ne x)$$

Is this first order equation satisfiable? Does there exist such a function? Because there can exist infinity of functions one can never prove that is unsatisfiable. My idea is, this is decidable but in infinity model. Is my way of thinking correct?

• The function $f(x) = \exp(x)$ satisfies your condition. Now take $x=-1$, then for all $y \in \mathbb{R}$, $\exp(y) \neq x$. – LinAlg Jan 18 '17 at 19:22

Let $f\,\colon A \rightarrow B$ be any function that is injective but not surjective.

Since $f$ is injective, $\forall x \forall y ( x \ne y \implies f(x) \ne f(y))$.

Since $f$ is not surjective, $\exists x \forall y (f(y) \ne x)$.

For example, the function $f\,\colon\mathbb{R} \rightarrow \mathbb{R}$ such that $f(x) = \text{arctan}(x)$ satisfies the requirements.

The successor function used in the Peano Axioms will do nicely!

The two relevant axioms are:

$\forall x \: s(x) \not = 0$

$\forall x \forall y (s(x) = s(y) \rightarrow x = y)$

The first axiom guarantees that $\exists x \forall y \: s(y) \not = x$

And applying contraposition on the second axiom we get $\forall x \forall y (x \not = y \rightarrow s(x) \not = s(y) )$

And yes, the Peano Axioms have a model! That is, the successor function for the Natural numbers has your desired property.