How to express a function $f:A\rightarrow B$ as a first order structure? Suppose $A$ and $B$ are non-empty sets and $f:A\rightarrow B$ is an onto function
What is the standard way to express this as a first order structure?
For example, one may consider a language $L$ containing a $2$-ary predicate symbol $F$ (intuitively Fxy means $(x,y)\in f$, i.e. $f(x)=y$), two $1$-ary predicate symbols $P_{A}$ and $P_{B}$ ($P_{A}x$ intuitively means $x\in A$, and similarly for $P_{B}x$), then constant symbols $c_{a}$ and $c_{b}$ for each $a\in A$ and $b\in B$ and an equality symbol $=$.
Then and onto function $f$ between the sets $A$ and $B$ is an $L$-structure $\mathcal{M}$ satisfying the obvious $L$-sentences: (onto axiom) $\forall x\;P_{B}x\Rightarrow \exists y\;P_{A}y\wedge Fyx$, the axioms $Fc_{a}c_{b}$ for all $(a,b)\in f$, and the well-defined axiom.
The domain of $\mathcal{M}$ is $A\cup B$, then $F^{\mathcal{M}}:= f$, $P_{A}^{\mathcal{M}}:=A$, $P_{B}^{\mathcal{M}}:=B$, the constant symbols are interpreted as $c_{a}^{\mathcal{M}}:=a$ and $c_{b}^{\mathcal{M}}:=b$ ($=$ is interpreted in the obvious manner).
Is my approach correct? $\mathcal{M}$ should "be" the function $f$, no? I feel I am missing something.
 A: What you write is correct, there are only a couple redundancies.
You only need the predicate $F$ in the language, then domain and range are definable by $\exists y Fxy$ and $∃ x Fxy$.
There is no need to introduce parameters (for your purpose these are irrelevant).
A: Somewhat contra Primo Petri's answer, in my opinion there isn't a single way to construe a function as a structure - it all depends on what you want that structural construction to do.
For example, here's one case where having constant symbols is absolutely crucial: if we want a construction $$f\leadsto\mathcal{M}_f$$ such that whenever $g$ is a function with domain and codomain containing those of $f$ and $\mathcal{M}_f$ is elementarily equivalent to (the appropriate reduct of) $\mathcal{M}_g$ we get that $f$ is a "subfunction" of $g$. This is often desired when applying compactness (similarly to here) but crucially relies on the presence of constant symbols.
I would say that your approach is the optimal one for as-yet-undetermined applications - if all I know is that I'm about to use model theory to think about a function in some way but I don't know the details, I'd probably adopt the construction you describe - but I'd rather emphasize flexibility and pragmatism than pick a specific construction without further details.
