Undirected graph in first order logic

Question

I'm trying to model an undirected edge in a graph. If we have an edge $(a \to b)$ given in a database, the edge $(b \to a)$ is of course implied.

Given the predicate Has_Connection(a, b). It indicates nodes a and b having a connection.

I now want to make a new predicate (eg Has_Sym_Connection(a, b)) that defines that if we have a database with Has_Connection(a, b) in it, Has_Sym_Connection(b, a) is also true.

So far I tried the following:

Has_Symm_Connection(a, b) => Has_Connection(a, b) || Has_Connection(b, a)
Has_Symm_Connection(a, b) <=> Has_Connection(a, b) || Has_Connection(b, a)
Has_Symm_Connection(a, b) <= Has_Connection(a, b) || Has_Connection(b, a)

None of them seem to do the trick. Can someone point me towards the right direction?

An example of where it goes wrong. (Example is Linear Time Calculus)

Has_Connection = {(a, b), (b, c), (c, a)}; (A structure with initial values.)

What I'm modelling in the following is that, an entity its position changes when it moves to a connected node.

This works, but only in one direction, as specified in the structure above:

$\forall$ t, loc: C_Location(t, loc1) $\leftarrow$ Move_To(t, loc1) & $\exists$ loc2 : Location(t) = loc2 & (Has_Connection(loc2, loc).

This however, leads to an unsatisfiable problem with any of the above rules:

$\forall$ t, loc: C_Location(t, loc1) $\leftarrow$ Move_To(t, loc1) & $\exists$ loc2 : Location(t) = loc2 & Has_Symm_Connection(loc, loc2).

Answer 1

Checking: $|\,|$ is the boolean 'or' in your programming language, whereas $\&\&$ is the Boolean 'and', correct?

$\begin{array}{c:c|c|c}\tiny\textsf{Has_Connection}(a,b) & \tiny\textsf{Has_Connection}(b, a) & \tiny\textsf{Has_Connection}(a,b)\,|\,|\,\textsf{Has_Connection}(b,a) & \tiny\textsf{Has_Sym_Connection}(a,b) & \tiny\textsf{Has_Connection}(a,b)\&\&\textsf{Has_Connection}(b,a) \\ \hline \color{blue}{T} & \color{blue}{T} & \color{blue}{T} & \color{blue}{T} & \color{blue}{T} \\ \color{blue}{T} & \color{red}{F} & \color{blue}{T} & \color{red}{F} & \color{red}{F} \\ \color{red}{F} & \color{blue}{T} & \color{blue}{T} & \color{red}{F} & \color{red}{F} \\ \color{red}{F} & \color{red}{F} & \color{red}{F} & \color{red}{F} & \color{red}{F} \end{array}$

So $\textsf{Has_Sym_Connection}(a,b) \implies \textsf{Has_Connection}(a,b)\,|\,|\,\textsf{Has_Connection}(b,a)$ is always satisfiable, but the other cases can be unsatisfied.

• $\implies$ requires the consequent to be true whenever the antecedent is.
• $\impliedby$ requires the antecedent to be true whenever the consequent is.
• $\iff$ requires both the antecedent and consequent to be true whenever either is.