I have stumbled about the following formula:
$ \bigwedge\limits_{i=1}^{|E_{row}|} (\bigvee\limits_{j=1}^{|E_{col}|} (\bigvee\limits_{k=1}^{|E_{col}|} k \neq j \rightarrow \neg e_{i,k}) \land e_{i,j}) $
It is a applied onto a 2D array and makes sure that in each row, there is exactly one column true. What I have found is that generally, it seems to be possible to express this in FOF (First Order Logic - "Only One" Construct).
However, what I would like to know is if the usage of conjunction and disjunction symbols as given is legal and possibly to which logic it corresponds. I've found the formula above in a paper and like it because of its clearity but I am vary if I should adopt it in that notion or reformulate it (e.g. to FOF).
Thanks for your help!