What is added to the usual first-order machinery is a \(\textsf{where}\) construction. We will give a proper definition shortly but first, here is a concrete example. Let us assume we have a structure for arithmetic, \(\langle \{0,1,2,\ldots\}, \bS, \bZ\rangle\). Here \(\bS\) is the two-place successor relation on the domain, that is, we have \(\bS(0,1)\), \(\bS(1,2)\), …. We also assume \(\bZ\) is true uniquely of 0 and, in accord with what we said above about relations and individual constants, we act as if we had a constant symbol 0 in the formal language. Consider the following formula, where \(S\) is a two-place relation symbol interpreted by \(\bS\), and \(E\) and \(O\) are auxiliary one-place relation symbols.