A first order language for graphs Let $L$ be a first order language with a relation $E(x,y)$. We can think of variables $x,y,z...$ as representing vertices and $E(x,y)$ representing "There is an edge incident to $x,y$". I need to express in $L$, the following statements:

  
*
  
*The Graph has no loops 
  
*The Graph has no multiple edges 
  
*Edges are undirected 
  
*There are no cycles of length 3 
  
*The degree of each vertex is at most 2
  

So far I have come up with:

  
*
  
*$\forall x (\neg E(x,x))  $
  
*Unsure
  
*Unsure
  
*$\forall x \forall y \forall z((E(x,y)\wedge E(y,z))\rightarrow\neg E(x,z)) $
  
*$\forall a \forall b \forall c \forall d((E(a,b)\wedge E(a,c)\wedge E(a,d)\rightarrow((b=c)\vee(c=d))))  $
  

I appreciate help with the others
 A: First of all, logical formulations of multigraph properties require having separate variables for vertices and edges (see https://en.wikipedia.org/wiki/Logic_of_graphs). Therefore, the language $L = \{ E \}$ consisting of a single binary relation as given above is not the appropriate language for multigraphs, but is the appropriate language for simple graphs.
Since model-theoreetic properties of multigraphs require having separate variables for vertices and edges, the singleton language $L = \{ E \}$ cannot be used to construct statements such as 'the graph has no multiple edges.' 
In the language $L = L_{\text{simple}} = \{ E \}$ of simple graphs, the $L$-sentence $$\forall u \ \forall v \left( E(u, v) \Longrightarrow E(v, u) \right)$$ is the axiom for undirected graphs 
Also observe that the $L$-sentence given for the fourth statement given above is not quite correct if graphs considered in the context of this problem are allowed to have multiple edges.  The original sentence $$\sigma_4 = \forall x \  \forall y \  \forall z \ E(x, y) \wedge E(y, z) \Longrightarrow \neg E(x, z)$$ does not exactly express that 'there are no cycles of length 3' if graphs considered in the context of this problem are allowed to have multiple edges.  For example, consider the $L$-structure given by the (undirected) multigraph $C_{2} = \{ \{ v_1, v_2 \}, \{ e_1, e_2 \}  \}$, where $e_1$ and $e_2$ both join the two vertices in $V(C_{2})$. In this case it is obviously true that $C_{2} \models \sigma_{4}$, because $$E(v_{1}, v_{2}) \wedge E(v_{2}, v_{1}) \Longrightarrow \neg E(v_{1}, v_{1})$$ and $$E(v_{2}, v_{1}) \wedge E(v_{1}, v_{2}) \Longrightarrow \neg E(v_{2}, v_{2}).$$
A: (3). To say that edges are undirected, you just say $\forall x \forall y (E(x,y) \leftrightarrow E(y,x))$. 
(2). If you just have the predicate $E(x,y)$ if there is an edge, then you just can't express anything related to edge multiplicity (besides presence or absence). However, you could use the incidence graph as underlying logical structure, and have an object $e$ representing each edge, and instead of $E$ you have a predicate $\in$ that tells you the vertex $x$ belongs to $e$. Then if you have a multiple edge you will have $e_1$ and $e_2$ that are both connected to $x_1$ and $x_2$ (with $e_1 \neq e_2$, etc). In this language the absence of loop is expressed by the absence of edges of degree $1$. Furthermore this alternative way to see the first-order logic of graph has exactly the expressive power of the classical framework when restricted to graphs. You can read more about it in Courcelle's work.
