(Sphere Lemma) Hanf locality Lemma and locally threshold testability I am reading the proof of Hanf's Sphere Locality lemma for (finite or infinite structures but with bounded degree), and I'm trying to understand the details of the proof!  I'm confused with the restriction for applying linear ordering. Why the use of linear order fails to define a finite neighbourhood (in infinite structures)? 
 A: I'll take a crack at answering the question that you seem to be asking in the comments. I recommend you also edit your question to make it more clear what you're asking, so it doesn't get closed.
Hanf's theorem says that given a quantifier depth $n$ and two structures $A$ and $B$ such that all of the balls of radius $3^n$ in the Gaifman graphs of $A$ and $B$ have size bounded by some finite number $e$, we can test whether $A$ and $B$ agree on all first-order sentences of quantifier depth at most $n$ by counting instances of $L$-isomorphism types of balls of radius $3^n$ in the Gaifman graphs. That is, $A\equiv_n B$ if and only if for each isomorphism type $i$, $i$ appears more than $ne$ times in both $A$ and $B$, or $i$ appears the same number of times in both $A$ and $B$.
Here the Gaifman graph of a structure $M$ is the graph with the same domain as $M$ and an edge between two elements $a$ and $b$ if and only if they appear together in some tuple from $M$ satisfying some relation in the language.
Now that bound on the sizes of the balls in the Gaifman graphs is very important. If $M$ is an infinite structure linearly ordered by $<$, and if the order relation $<$ is in the language, then for any two elements $a$ and $b$, from $M$ either $a<b$ or $b<a$, so $a$ and $b$ are only one step away in the Gaifman graph. This means that even the balls of radius $1$ in the Gaifman graph of $M$ are infinite, and there's no hope of applying Hanf's theorem.
But I think your application is ok. Just from taking a quick look at the paper you linked to, it looks like a "picture" is a structure in the language $L = \{S_1,S_2,\{P_a\}_{a\in \Sigma}\}$, where we view the elements of the structure as the positions in a 2-dimensional array, with $S_1$ and $S_2$ as successor functions in the two directions and $P_a$ as labels (each position gets exactly one label).
In this case, there's no need to include a linear order in the language to ensure that your pictures are infinite. Any infinite picture will satisfy sentences expressing the following things:


*

*Every element has a unique successor under $S_1$ and a unique successor under $S_2$.

*Every element is the successor under $S_1$ of a unique element and is the successor under $S_2$ of a unique element.

*For every $n$, there are no cycles of length $n$ for $S_1$ or $S_2$. That is, we can't find $a_1,\dots,a_n$ such that $a_{i+1} = S_1(a_i)$ for all $i$ and $a_1 = S_1(a_n)$.


And any picture satisfying the theory above will be infinite. There's no problem applying Hanf's theorem to infinite pictures in this language, since there is a uniform bound on the sizes of neighborhoods in the Gaifman graph (each element has exactly $4$ neighbors - it's successors and predecessors in the two directions).
