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

Question

$$ \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?

Answer 1

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.

Answer 2

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.