Formulas are mathlib's, $L.Formula (Fin k)$ for formulas with free variables x₁, …, x_k, and $L.BoundedFormula (Fin k) n$ for their subformulas with n further bound variables. A finite relational signature is a relational language with finitely many relation symbols in total. The arity bound α plays no role in the definitions.

Equivalence quantifies over all structures whose domain lies in one universe, which is an explicit parameter of the definition. The domains may be empty or infinite.

adj_σ is the conjunction of x₁ ≠ x₂ with the disjunction, over the relation symbols R of arity β ≥ 2, of ∃x₃ … ∃x_β ⋁π R(x{π(1)}, …, x_{π(β)}), where π ranges over the permutations of the β positions. The quantified variables may coincide with x₁, x₂ or each other, so this is exactly adjacency in the Gaifman graph. Symbols of arity at most one contribute nothing. Its quantifier rank is at most α − 2.

dist(x₁, x₂) ≤ r quantifies the r vertices v₁, …, v_r of a walk x₁ = v₀, v₁, …, v_r, requires v_r = x₂, and requires every step to be an equality or an adjacency. So it holds exactly if a walk of length at most r joins x₁ and x₂, as in $GaifmanGraph.WithinDist$. Its quantifier rank is at most r plus that of adj_σ, so at most r + α. For r = 0 it is equivalent to the equality x₁ = x₂.

Finite disjunctions and conjunctions are mathlib's $iSup$ and $iInf$. They fix some order of the members, which affects neither the meaning nor the quantifier rank. A formula over the variables x₁, x₂ is placed at given terms by substitution.

The guard of a quantifier over Ball_s(x̄) is the disjunction over i of dist(xᵢ, y) ≤ s, where y is the newly bound variable. For a formula without free variables, the ball is empty and the guard is falsum. A local formula is built from atoms by falsum and implication, which give all Boolean connectives, and by the guarded quantifiers ∀y (guard → φ) and ∃y (guard ∧ φ). The inner formulas of a local formula may have more free variables than x̄, namely the bound variables, but the balls are always taken around x̄. The dist formulas inside the guards are exempt, exactly as in the paper.

In a basic local sentence the m witnesses are the m bound variables of an existential block, and "dist(xᵢ, xⱼ) > 2r'" is the negation of the dist formula of radius 2r'. The case m = 0 is allowed and gives a true sentence.