Will all the models of the following formula be bipartite graphs, with edges being represented by $R$ and $A$ and $\neg A$ being two disjoint groups of vertices ?
$$\forall x \forall y R(x,y) \rightarrow (\neg A(x) \leftrightarrow A(y))$$
Is this encoding right ?
On
All models will be bipartite graphs. However, "are all bipartite graphs models?" is complicated to answer.
You've demonstrated that bipartitions are expressible in first-order logic. That is, given a graph (specified by a relation $R$) and a predicate $A$, we get a partition of the vertex set into two parts: those for which $A$ holds, and those for which $A$ does not hold. Then we can express the statement "This partition is a bipartition of the graph" in first-order logic, which is essentially what you've done.
This is different from the statement "The graph is bipartite" or "The graph has some bipartition." To build from the axioms in the question to such a statement, we'd need to begin with "There exists a predicate $A$ such that ..." which is not allowed in first-order logic.
We can get closer. A graph is bipartite if and only if it does not have any odd cycles. For any fixed $n$, we can express the statement "The graph does not have any cycles of length $2n+1$" in first-order logic. So with infinitely many axioms, we can express "A graph is bipartite" just by combining these statements for $n=1,2,3,\dots$.
With finitely many axioms we can't get there. I don't have the technical know-how to explain why, but the intuitive idea is that any finite set of axioms only works on some "local" scale. For large enough $n$, $C_{2n+1}$ will be indistinguishable from a bipartite graph on that scale, because you have to go all the way around the very long odd cycle to notice that the graph is not bipartite.
Literally speaking, I think YES: all models (i.e. value assignments of $R$ and $A$) of your FOL formula are bipartite graphs (together with their bipartitions). In other words, each $R$ and $A$ satisfying your formula is indeed a bipartite graph $G(V,R)$ and $A$ is a bipartition of this graph (there may exist more than one bipartitions if there are isolated vertices in the graph). Of course, to be more precise we should assume a vertex set $V$ and your formula should be written as $\forall x \in V, y \in V. R(x,y) \rightarrow (\neg A(x) \leftrightarrow A(y))$.
But this does not mean that bipartition (or in general k-colorability) is expressible in FOL. In fact, it's only expressible in MSO (or more expressible logics), where your $A$ is a set variable as existential quantifiers: $G(V,R)$ is bipartite iff $\exists A \subset V. \forall x \in V, y \in V. R(x,y) \rightarrow (\neg A(x) \leftrightarrow A(y))$.
Or maybe we can see it in this way: given any $R$ and $A$, your FOL formula can be used to test if $R$ is a bipartite graph with $A$ as its bipartition. If the test succeeds (e.g. by loop over all edges in $R$), for sure $R$ is a bipartite graph. But if the test failed, it does not mean that $R$ is not a bipartite graph, because it could be that the $A$ part is wrong - it's not a bipartition. For instance, if we use a bipartition graph $R$ and the set of all vertices $V$ to test your formula, the formula will obviously fail, and thus this pair ($R$ and $V$) is not a model of the formula. But (by assumption) still $R$ is a bipartite graph.
In summary, just because your FOL formula doesn't give a one-one correspondence of any single input $R$ and the bipartite property of it, this FOL formula cannot be used to express (or define) bipartite graphs. Yet your original question indeed has a YES answer, just it cannot conclude that your graph property (bipartition here) is FOL-expressible.