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!
This already is stadard first-order logic (resp. it is a “metasyntactical shortcut” over the standard first-order logic). The thing you call “summation notation”, but it is more about the use of bounds and unary operators, is a standard shortcut: $⋀_{i = 1}^n φ(n)$ means $φ(1) ∧ φ(2) ∧ … ∧ φ(n)$. Such shortcut can be defined for any binary operator: $∑$ is used for $+$, $∏$ is used for $⋅$ or $×$, $\bigoplus$ is used for $\oplus$, …
By the way it seems that the innermost disjunction should be a conjunction to have the desired meaning (I've also slightly reordered the expression and add some parentheses): $$ ⋀_{i=1}^{|E_\text{rows}|} \bigl(⋁_{j=1}^{|E_\text{col}|} \bigl(e_{ij} ∧ ⋀_{k=1}^{|E_\text{col}|} (k ≠ j → ¬e_{ik})\bigr)\bigr) $$