# Use conjunction / disjunction symbol like a summation symbol (over a set) - allowed?

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

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