how to formulate the following properties formally?

Question

Let (N, E, l), be a labeled directed graph, where N is a set of vertices, E ⊆ N×N is a set of edges, and l: E → L is a function assigning labels from a set L to edges. Let source and target be functions on E such that source(s, t) = s and target(s, t) = t. Formulate the following properties formally:

1. Every label in L is a label of some edge.
2. There are no nodes that are targets of more than two edges with identical labels.
3. There is at least one path of length three where all the edges have identical labels.
4. There are no nodes that are sources of edges with more than two distinct labels.

Answer 1

The most immediate way of "formally" stating these properties is to reduce them to purely logical ones. I give possible ones here.

1. $\forall x\in L\exists e\in E: \: l(e)=x$ (or said succintly, $l$ is surjective)
2. $\forall n\in N:\: ((\exists e_1,e_2,e_3\in E: \text{target}(e_1)=\text{target}(e_2)=\text{target}(e_3)=a\land l(e_1)=l(e_2)=l(e_3)) \Rightarrow e_1=e_2\vee e_2=e_3 \vee e_3=e_1)$

This one deserves explanation. It says that for any vertex (node) $n$, if there are three edges with $n$ as the target and they all have identical labels, then two of them must be equal - i.e. there does not exist three distinct edges with target $n$. You could also formulate an equivalent statement looking like $\neg(\exists n\in N: \dots)$, but I feel like this is cleaner.

3. $\exists e_1,e_2,e_3\in E: \: \text{target}(e_1)=\text{source}(e_2)\land \text{target}(e_2)=\text{source}(e_3)\land l(e_1)=l(e_2)=l(e_3)$.

4. This is very similar to (2.), and so I encourage you to work this out yourself.