I'm translating logic formulas into English and I've come across the following logic L-formula:
$ \forall i \forall j \forall k: (\mathrm{in}(i,xs) \land \mathrm{in}(j,xs) \land \mathrm{in}(k,xs) \Rightarrow i = j \lor j = k \lor i = k)$
With the $\mathrm{in}(x,xs)$ predicate meaning $x$ is in $xs$.
To which I have translated as "At least two elements are the same" but I can't be sure whether this is correct or not. My thinking is that if one of them satisfies then right hand side then the whole statement is true but as this is an implication the left hand side can be false for the whole formula to be true.
I think an example of a list with four elements that satisfies this would be something like
$[1,1,2,3]$
And a list of elements that violates this would be
$[1,2,3,4]$
The discourse is the set of natural numbers.
I am pretty sure I have translated this incorrectly. Does the right hand side of the implication mean that at least two elements are the same? I am quite unsure about this.
The actual translation of the formula is
In other words, there cannot be three different elements all present in $xs$.
So, if $xs = [1,2,3]$, then the statement is false, since I can set $i=1,j=2,k=3$ and the implication falls: