# Undirected graph in first order logic

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).

• The middle one seems fine. – André Nicolas Nov 9 '15 at 23:05
• @AndréNicolas Thanks for the answer, the problem I stumble upon is that it makes my model unsatisfiable when I try using the middle Has_Symm_Connection predicate. (Any of them actually). In my current model I simply use Has_Connection(a, b) to indicate I want a connection, if change this to (Has_Connection(a, b) || Has_Connection(b, a)) the unsat arises. Which is quite odd, as it I don't see why an OR would have that kind of influence.. – drx Nov 9 '15 at 23:11
• What language are you using? Doesn't || denote 'or' rather than 'and' (&&). You want 'and' there . If it were 'or' the right hand side would be true when just a one-way connection existed. – Graham Kemp Nov 9 '15 at 23:18
• Can you give an example of when it becomes unsatisfiable? The middle one looks fine to me. – Alt Nov 9 '15 at 23:20

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.