Defining suitable predicate and function symbols.

Question

I am really struggling to build intuition with regards to how to do this sort of question.

The abstract: A graph is a set (whose elements are called nodes) together with a symmetric relation on that set (related nodes are said to have an edge between them). A binary tree is a graph which has a distinguished node, called the root, which is connected to two other (distinct) nodes, and every other node is connected to three distinct nodes or one (distinct) node.

The question: How would I define a suitable set of predicate symbols and function symbols together with their arities that give rise to a first order language suitable for specifying binary trees?

Answer 1

A graph is a pair $\mathcal G = (V,E)$ where $V$ is a set of elements called vertices (or nodes) and $E$ is an anti-reflexive and symmetric binary relation on $V$ called the edge relation.

This means that the relation $E$ must satisfy the following axioms :

$\forall x \lnot E(x,x)$

meaning that there is no edge "looping" on a single vertice (this is anti-reflexivity), and :

$\forall x \forall y (E(x,y) \rightarrow E(y,x))$

meaning that if there is and edge connecting the vertices $x$ and $y$, the same edge connects $y$ and $x$ (this is symmetry).

---

For a binary tree we can try adding to the above language an individual constant $r$ for the root and a unary function symbol : $f$ for the "father" of a node.

They have to satisfy the following axioms :

$\forall x (x \ne r \rightarrow \exists y (x = f(r)))$

$\forall x \forall y \forall z(E(x,y) \land E(x,z) \rightarrow (x=f(y) \land x=f(z)))$.