Boolean Queries in First Order Logic

Question

I understand first order logic and how its constructed but I have some trouble understanding how the following statement and its FO query are formed.

This is from a book.

Size n = the set of graphs of size n;

The FO Query of size 2 then is :

∃x∃y(x ̸ = y) ∧ ¬∃x∃y∃z(x ̸ = y ∧ x ̸ = z ∧ y!= z)

Another Example :

Diam n the set of graphs of diameter ≤ n;

FO :

∀x∀y(x = y ∨ Exy ∨ ∃z(Exz ∧ Ezy))

Question 1:Would someone be able to translate what's going on here? Also is there a book or article which has queries of this sort that I can work on? I have tried searching for FO queries and answers but the queries i see are trivial usually and dont invovle this level of abstraction.

Question 2: Also I dont understand what 'E' in the second FO query is. Is that another way of writing an existential quantifier?

Question 3 : Also in equations like this is the negation for the whole of the second part or does it read there does not exist an X , there exits a Y and Z?

THANK YOU :)

Answer 1

The formulas are examples from Erich Gradel & Phokion Kolaitis & Leonid Libkin et alii, Finite Model Theory and Its Applications (2007), page 2.

They are relative to the collection $G_n$ of finite undirected graphs with vertex set $[n] = \{ 1, . . . , n \}$. Thus, each graph $G$ has a vertex set $V^G = [n]$ and an irreflexive and symmetric edge relation $E \subseteq [n] \times [n]$.

The second formula :

$\forall x \forall y(x = y \lor Exy \lor \exists z(Exz \land Ezy))$

says that :

"for all vertices $x$ and $y$, or $x = y$, or $x$ and $y$ are two vertices connected by an edge, or there exists a third vertice $z$ such that $x$ and $z$ are connected by an edge and $z$ and $y$ are connected by another edge".

The first formula is :

$\exists x \exists y (x \ne y) \land \lnot \exists x \exists y \exists z (x \ne y \land x \ne z \land y \ne z)$;

we must read it as : "there exists two objects $x$ and $y$ that are distict, and no more tahn two", because the second part of the formula says that : "do not exist three objects $x$, $y$ and $z$ such that they are all distinct".

It is intuitive that the last formula is true for all and only those graphs with exactly two vertex.