In first-order logic in the language of graphs, can one express that there is a pair of nodes connected by a path of length $2^m-1$ using only $\leq m$ quantifiers?
My question comes from the point of view of modal logic and bisimulation. In the context of a particular proof of the van Benthem-Rosen result, one shows that a first-order formula of quantifier-rank $m$ is $2^m-1$-bisimulation invariant.
Now, in the literature I am reading, it is claimed that the bound is sharp and that an example of a formula of quantifier-rank $\leq m$ which is bisimulation invariant but not $l$-bisimulation invariant for $l<2^m-1$ can be found by considering reachability in graphs involving exponential length as above. I can't make it out, however.