Constrain a relation to be a function in FOL without equality Using first order logic without equality, I'd like to constrain the relation $F(x,y)$ to represent a function from $x$ to $y$.  In FOL with equality I can say:
$ \forall x \exists y \ F(x,y)\ \ \ \ \ $ (defined across entire domain, $x$)
$ \forall xwz \ F(x,w) \wedge F(x,z) \rightarrow w=z \ \ $ (unique).
But I don't know how to state the uniqueness constraint without equality.  I could define an equivalence relation:
$ \forall x \ E(x,x) $
$ \forall xy \ E(x, y) \rightarrow E(y, x) $
$ \forall xyz \ E(x, y) \wedge E(y,z) \rightarrow E(x,z) $.
But now I need to be careful.  I think it is not sufficient to state
$ \forall xwz \ F(x,w) \wedge F(x,z) \rightarrow E(w,z)$,
because that doesn't account for the equivalence relation in the domain.  So I need:
$ \forall xywz \ F(x,w) \wedge F(y,z) \wedge E(x,y) \rightarrow E(w,z)\ \ \ \ $ ($F$ is unique with respect to the equivalance relation $E$).
Is that good enough?  It seems to admit a larger class of models than did my uniqueness constraint that used "$=$".  For example, if my model's domain is the natural numbers, and $E$ is the equivalence classes odd and even, then both $F(0,1)$ and $F(0,3)$ might be true.
 A: Consider a first-order language $L$ with equality with a family of predicate symbols and function symbols.
To eliminate equality, we introduce a new binary predicate symbol $E$ and the axioms
$\forall x E(x, x)$ (reflexivity)
$\forall x \forall y (E(x, y) \to E(y, x))$ (symmetry)
$\forall x \forall y \forall z (E(x, y) \land E(y, z) \to E(x, z))$ (transitivity)
For each $n$-ary predicate symbol $P$, we add the axiom
$\forall x_1 \forall x_2 ... \forall x_n \forall y_1 \forall y_2 ... \forall y_n (E(x_1, y_1) \land E_(x_2, y_2) \land ... \land E(x_n, y_n) \land P(x_1, x_2, ..., x_n) \to P(y_1, y_2, ..., y_n))$
And for each $n$-ary function symbol, we add the axiom
$\forall x_1 \forall x_2 ... \forall x_n \forall y_1 \forall y_2 ... \forall y_n (E(x_1, y_1) \land E(x_2, y_2) \land ... \land E(x_n, y_n) \to E(f(x_1, x_2, ..., x_n), f(y_1, y_2, ..., y_n)))$
This language, without equality, is denoted $L'$.
With these axioms, it is possible to prove that the "substitution rule of $E$" is admissible. That is, it is possible to show that for any statement $T$ in the language $L'$, for all variables $x, y$ that do not occur bound in $T$, we can prove $T[y \to x] \land E(x, y) \to T$ (where $T[y \to x]$ is $T$ with all occurences of $y$ replaced by $x$). We prove this by structural induction on the formula $T$.
Define the "translation" of a statement $T$ in $L$ to be the statement $R(T)$ obtained by replacing all subformulas of the form $A = B$ with the subformula $E(a, B)$. Then $L \vdash T$ iff $L' \vdash R(T)$.
In your case, your language consists only of the 2-ary predicate symbol $F$. Thus, you need the axioms
$\forall x_1 \forall x_2 \forall y_1 \forall y_2 (E(x_1, y_1) \land E(x_2, y_2) \land F(x_1, x_2) \to F(y_1, y_2))$
$\forall x \exists y F(x, y)$
$\forall x \forall w \forall z (F(x, w) \land F(x, z) \to E(w, z))$
(The last two statements being the $R$-transations of your axioms for being a functional relation).
