First-order iteration operator example

Question

I am reading on https://en.wikipedia.org/wiki/FO_(complexity)#Iterating that FO[$t(n)$] consists in first-order logic with an iteration operator that iterates $t(n)$ number of times some quantifier block Q.

Can someone provide me an example of a formula using such operator, please?

I feel that I am not understanding the concept since, for me, iterating some number of times the very same quantifier block with the same variables does not seem to add anything valuable to the formula. For instance, if I consider the quantifier block $\exists x. P(x)$, iterating it two times, as far as I understand, seems to bring $\exists x. P(x) \land \exists x. P(x)$, which is trivially equivalent to the original. Can someone clarify me this operator (preferibly, with some example)?

Answer 1

Here is an example from Section 4.3 of Immerman's Descriptive Complexity.

Consider the block $$ (\forall z. \lnot (x = y \lor E(x,y))) (\exists z) (\forall uv. (u = x \land v = z) \lor (u = z \land v = y)) (\forall xy. x=u \land y=v) $$

Here $(\forall z.P)Q$ stands for $(\forall z) P \to Q$ and $(\exists z.P) Q$ stands for $(\exists z) P \land Q$.

Denoting the block by $TC$, let's check when $TC\,R(x,y)$ holds. The first quantifier ensures that this holds if $x = y$ or $E(x,y)$. Otherwise, we need there to exist a $z$ such that for $(u,v) = (x,z)$ and for $(u,v) = (z,y)$, $R(u,v)$ holds, that is, we need both $R(x,z)$ and $R(z,y)$ to hold. In other words, $$ TC \, R(x,y) \longleftrightarrow x=y \lor E(x,y) \lor (\exists z) (R(x,z) \land R(z,y)). $$ The operator TC "recycles" variables; in particular, the inner part mentions $x,y$ again. This means that if we apply it twice, we get the following: $$ TC \, TC \, R(x,y) \longleftrightarrow x=y \lor E(x,y) \lor \\ (\exists z)(x = z \lor E(x,z) \lor (\exists w) (R(x,w) \land R(w,z))) \land (z = y \lor E(z,y) \lor (\exists w) (R(z,w) \land R(w,y))) $$ If the domain has size $n$ and we apply TC iteratively $\lceil \log_2 n \rceil$ times to $E$, then we get the transitive closure of $E$ (which is the same as solving directed reachability, an NL-complete problem).