I have a question about expressions of predicate logic.
As for a binary relation $R^2$, the formula $Rxy$ and $Ryx$ only differ in the location of two variables, for any n-ary relation $X^n$, the following pair of formulas only differ in the location of two variables such as ($X^nv_1v_2...v_n$, $X^nv_2v_1...v_n$) ($v_1$ and $v_2$ are changed), ($X^nv_1...v_i...v_j...v_n$, $X^nv_1...v_j...v_i...v_n$) ($v_i$ and $v_j$ are changed).
Then, I want to use the generalized form of such formulas, but I don't know how to do.
For example, I considers some dissatisfied (not in a metalogical sense like "unsatisfiable") ways of expressions although maybe I have misunderstanding. First, I wrote $\forall X^n\forall v_1...\forall v_nX^n(...v_i...v_j...)$ and $\forall X^n\forall v_1...\forall v_nX^n(...v_j...v_i...)$ but it seems that the quantifier $\forall X^n\forall v_1...\forall v_n$ does not bound the variables ($...v_j...v_i...$). Also, I wrote $\forall X^n\forall v_1...\forall v_nX^n(v_1...v_i...v_j...v_n)$ and $\forall X^n\forall v_1...\forall v_nX^n(v_1...v_j...v_i...v_n)$ but it seems that the variable $v_1$ and $v_i$ could not change their locations even if I want to consider the case that $\forall X^n\forall v_1...\forall v_nX^n(v_1v_2...v_n)$ and $\forall X^n\forall v_1...\forall v_nX^n(v_2v_1...v_n)$.
So, when there is such sentence $\phi$, I aim to write the expressions such as $\vDash\phi$ or $\vdash\phi$.
The variable in a relational symbols expression $X^n(v_1, \ldots, v_n)$ are "place holders".
Thus, what matters is their "position" in the expression: this is the reason wahy we use subscripts to name them.
In an expression:
all variables are properly bound.
This does not happens if we have e.g. $∀X^3 \ ∀v_1 ∀v_3 ∀v_2 \ X^3(v_1, v_4, v_3)$; thus, we have to take care in using "dots".
In general, if we write: $1,2,\ldots, n$, it is implicit tha we are listing all numbers between $1$ and $n$ in their proper order.
Things are different with a different "mix" of quantifiers.
Consider the binary predicate $(v_1 \le v_2)$ (that reads "$v_1$ is less-or-equal than $v_2$").
Nothing changes in writing $∀v_1 ∀v_2 (v_1 \le v_2)$ instead of $∀v_1 ∀v_2 (v_2 \le v_1)$, because the second form is the same as $∀v_2 ∀v_1 (v_1 \le v_2)$ and we can "swap" the same quantifier.
This is not so for different quantifiers: $\exists v_1 ∀v_2 (v_1 \le v_2)$ is true in $\mathbb N$, while $\exists v_1 ∀v_2 (v_2 \le v_1)$ is false.