Two questions on MSO

First question :

Is the following formula a valid MSO formula?

$\theta(S, r) = \exists (e_1, t_1), ... ,(e_h, t_h) \bigwedge\limits_{(e_i, e_j) \in \rho(S,r)} \mathcal{R}((e_i, t_i), (e_j, t_j))$

So my main concern here is the fact one states there exists $e_1, t_1$ etc. but then goes on to not use these in the actual formula (only using $e_i$ and $e_j$). Is this correct?

Second question :

While browsing around, I found the following :

(found in this post : MSO (Monadic second-order logic) Logic On Words)

My question here is, in MSO, how come one can still use 2-ary relations, such as $S(x,y)$ (as well as $\mathcal{R}((e_i, t_i), (e_j, t_j))$ from the first question), since I thought MSO is supposed to use only 1-ary relations, i.e. sets?

I think I might have found the answer myself, but I would like to verify : is this allowed because one does not quantify over these 2-ary relations?

You are asking two questions. The first question is about logic more generally. You are wondering whether a statement of the form
$$ \exists x \, \mathrm{True} $$
is valid, although $\mathrm{True}$ doesn't mention $x$. There is absolutely no requirement in the syntax of logical formulas that you use all the variables you quantify over. This similar to functions which don't depend on all of their arguments. Do you object to the function $f(x) = 1$?

As for your second question, monadic refers to the fact that you are only allowed to quantify over unary predicates. The language itself can freely contain $k$-ary predicates for any $k$. Compare this to first-order logic, in which you are not allowed to quantify over any predicates. Would that mean that first-order logic only allows for 0-ary predicates?

StackExchange Computer Science Q#109414, answer score: 3