What is the definition of a definition? In mathematical logic or other formal systems, what is the definition of a definition, formally?
If  "A" is defined as "B",  what is the definition of "A" like?
Does it involve both "A" and "B" (e.g. "A := B"), or just "B"?
For example, on p126 in §3.  Extensions by Definitions in VIII  Syntactic Interpretations and  Normal Forms in Ebbinghaus' Mathematical Logic, suppose that $S$ is a (non-logical) symbol set,

3.1  Definition.  Let $\Phi$  be a set of $S$-sentences.
(a)  Suppose  $P \notin S$ is  an $n$-ary relation symbol and $\phi_P(v_0, ... , v_{n-1})$  an
$S$-formula. Then we say that
$$ \forall v_0, .... \forall v_{n-1}   (P v_0 ... n_{n-1} \leftrightarrow \phi_P(v_0, ... , v_{n-1})) $$
is  an $S$-definition of $P$  in $\Phi$.

Which shall I call as an $S$-definition of $P$ in $\Phi$:

*

*$ \forall v_0, .... \forall v_{n-1}   (P v_0 ... n_{n-1} \leftrightarrow \phi_P(v_0, ... , v_{n-1})) $?

*

*Is it circular to define $P$ in terms of itself?


*Is an $$-definition of $$ in $Φ$ an interpretation of symbol $P$ as an $S'$-sentence? (as part of a syntactic interpretation of $S'$ in $S'$ itself?)


*Is the appearance of $P$ in its own definition $∀ _0,....∀ _{−1}(_0...v_{−1}↔_(_0,...,_{−1}))$, in the same sense as the appearance of $A$ in $:=$?




*$\phi_P(v_0, ... , v_{n-1})) $ ? (I guess that $P$ is defined as $\phi_P(v_0, ... , v_{n-1})) $ in $\Phi$.)


*$\phi_P$? (Compare that to the second: $P$ itself doesn't involve variables)
See How does this definition define a symbol $P$ outside the symbol set $S$ as a $S$-sentence?
Thanks.
 A: Below I'll first try to describe the process in a more intuitive way, then address your worries about circularity. I suspect the latter point may actually be more helpful, so feel free to read the second section first - and in particular, the highlighted motto there will I think be quite helpful.
(Re: your final comment, the definition is $(1)$ - the thing which tells you how the new symbol behaves, in terms of the old symbols you already have and understand.)

The key phrase here is "expansion by definitions."
Intuitively, we have in mind the following process:

*

*Starting with a signature $S$ and some set $\Phi$ of $S$-sentences, we become a little annoyed by inefficiencies: there are some things which we can talk about using $S$-formulas but only in a roundabout way. Think for example about the language of set theory, $\{\in\}$: we can express things like "$x$ is the Cartesian product of $y$ and $z$" in this language, but only via annoyingly long formulas. (It's a good exercise to handle the previous example - using, say, Kuratowski pairs.)


*So given our really complicated formula $\varphi(x_0,...,x_{n-1})$, we want to whip up a new theory which is basically the same as $\Phi$ except that it additionally has an "abbreviation" for $\varphi$.


*First, this means we want to enlarge our language: rather than work with $S$ we want to work with $S\cup\{R\}$ for some $n$-ary relation symbol $R\not\in S$ which we intend to serve as an abbreviation for $\varphi$.


*Now we have to define a theory in this larger language. This theory should subsume what we already have (that is, $\Phi$), should correctly dictate the behavior of $R$ (that is, say that it's an abbreviation for $\varphi$), and shouldn't do anything else. This leads us to consider the new theory $$\Phi':=\Phi\cup\{\forall x_0,...,x_{n-1}(R(x_0,...,x_{n-1})\leftrightarrow \varphi(x_0,...,x_{n-1})\}.$$
The passage from $S,\Phi$, and $\varphi$ to $S\cup\{R\}$ and $\Phi'$ is an expansion by definitions. We have some serious redundancy here: in a precise sense, $\Phi'$ is really no better than $\Phi$. (Formally, $\Phi'$ is a conservative extension of $\Phi$ in the strongest possible sense: every model of $\Phi$ has exactly one expansion to a model of $\Phi'$.) This isn't surprising. We already knew we could express the thing we cared about via $\varphi$, we just wanted to be able to do so more quickly.
Incidentally, note that this suggests a natural "maximally efficient" version of any theory: just add new symbols for every formula! This is called Morleyization, and is occasionally useful (although usually kind of silly).

OK, now what about the circularity you are worried about?
First, note that "$R$" itself is just a symbol. The new sentence we're adding isn't really a definition of $R$, but rather a definition of the meaning of $R$, or if you prefer a rule governing the behavior of $R$.
More seriously, circularity is never an issue in FOL! The key idea is the following, which I think is an important departure from the intuitions one might bring in from programming:
A set of first-order sentences doesn't create things, it describes things.
Specifically, a set of first-order sentences $\Phi$ carves out a particular class of structures, those about which it is an accurate description. For instance, the possibly-dangerous-looking sets $$\{\forall x(P(x)\leftrightarrow P(x))\}$$ and $$\{\forall x(Q(x)\leftrightarrow \neg Q(x))\}$$ are perfectly circle-free; they're just vacuous (= hold of every structure) and contradictory (= hold of no structure) respectively.
A: We have a signature $S$ and we extend it to $S':=S\cup\{P\}$.
The $S$-definition of $P$ is the $S'$-formula
$$\forall v_0\dots v_{n-1}: Pv_0\dots v_{n-1}\leftrightarrow \phi_P(v_0,\dots,v_{n-1})$$
which can be formally handled as an extra axiom to the given $S$-theory we're working with, thus producing an equivalent $S'$-theory, in which the symbol $P$ can be used as abbreviation for the formula $\phi_P$.
For example, the below formula is the definition of the usual ordering relation $\le$ of nonnegative integers in the language $(0,+)$:
$$\forall x,y:\ x\le y\,\leftrightarrow\,\exists z: x+z=y$$
