In the $k$-pebble game on two structures $M$ and $N$, a position is a pair of $k$-tuples, one in each structure. Two tuples agree on their atomic type, relative to a family $S$ of relation symbols, when they satisfy the same equalities between coordinates and the same relations of $S$ at every selection of coordinates. A relation between $k$-tuples of $M$ and of $N$ has the back-and-forth property at a position when, whichever pebble the spoiler moves and wherever, on either side, the duplicator can move the same pebble on the other side so that the new position is again in the relation. The $k$-pebble equivalence generated by an initial relation is the limit of the chain of refinements that keep the positions of the initial relation satisfying the back-and-forth property with respect to the previous stage: the positions from which the duplicator can play forever. Unlike the rounds of an Ehrenfeucht–Fraïssé game, the pebbles are reused, so the game bounds the number of variables and not the quantifier depth.

For a simultaneous induction, $k$ is a variable budget when it covers, for each relation variable, its arity plus the quantifier depth of its step formula; and the induction uses relations of $S$ when the symbols of the base vocabulary in its step formulas and output sentence all lie in $S$.