I there a rigorous, mathematical, approach to definitions (denotations)? In mathematical logic, a definition is treated as an abbreviation - a denotation which simplifies the discourse making it shorter. This is so much so that in a formal theory or a logic we can do without definitions. Thus, logicians did not seem to have studied the notion of definition. This is strange because what mathematicians produce is defintions and theorems. Could it happen that logicians focused only on theorems (deduction rules, proof, etc.) but total ignored definitions?
 A: This sounds to be a complete answer to my question:
the theory of definitions is part of the theory of conservative extensions of theories.
See the following discussion in the forum FOM (Foundation of Mathematics):
http://www.personal.psu.edu/t20/fom/postings/9810/msg00068.html:
The idea of conservative extension is a generalisation
of the notion of definition. (and is used self-consciously
in that way by some proof tools e.g. HOL)
What distinguishes a "foundation system" from other logical
systems is that in a foundation system it is possible to
derive the main body of mathematics using only conservative
extensions. (of course, people used to say "definitions")
A: I've always called Godel numbers for predicates with one free variable that can be proven to be uniquely satisfied Definitions.  I've read of various formal notions of definability in Model Theory so why not Proof Theory.
For example, if you have a proof predicate $\mathtt{Pf}$, then the set of Definitions relative to this proof predicate can be specified as:
$$
A := \{ \; \ulcorner \phi \urcorner \; | \; \mathtt{Pf}(\ulcorner \exists ! x \; \phi(x) \urcorner) \; \}.
$$
Naturally, the next thing to do is consider the set of definitions for sets that do not contain their own definitions as members.
You get:
$$
B := \{ \; \ulcorner \phi \urcorner \; | \; \mathtt{Pf}(\ulcorner \exists! x \; \phi(x) \; \wedge \; \ulcorner \phi \urcorner \notin x \urcorner) \; \}.
$$
One can actually write up a predicate and then Godel number it to get a definition for B.  Let $\theta_B(x)$ denote this predicate.
Directly from the definition, one can prove that:
$$
\ulcorner \theta_B\urcorner \in B \leftrightarrow \mathtt{Pf}(\ulcorner \ulcorner \theta_B\urcorner \notin B \urcorner).
$$
Further applying the definition, one can prove that:
$$
\mathtt{Pf}(\ulcorner \ulcorner \theta_B\urcorner \notin B \urcorner) \leftrightarrow \mathtt{Pf}(\ulcorner \neg \mathtt{Pf}(\ulcorner \ulcorner \theta_B\urcorner \notin B \urcorner) \urcorner ).
$$
If $\mathtt{Pf}$ is a proof predicate for a theory that isn't too weak, then we would have that it is consistent if and only if $\mathtt{Pf}$ does not prove everything if and only if $\mathtt{Pf}$ does not prove it is consistent.
Therefore, we get:
$$
\mathtt{Pf}(\ulcorner \neg \mathtt{Pf}(\ulcorner \ulcorner \theta_B\urcorner \notin B \urcorner) \urcorner ) \leftrightarrow \mathtt{Pf}\text{ is inconsistent}.
$$
Combining all of the equivalences, we get:
$$
\ulcorner \theta_B\urcorner \in B \leftrightarrow \mathtt{Pf}\text{ is inconsistent}.
$$
Somehow, the different levels of provability allow you to avoid getting a contradiction like you do from Russell's Paradox.
Do you know of anything related to this?  Thanks!  :)
-----Addendum-----
I guess for any sentence $\psi$ where you can prove: $\psi \leftrightarrow \mathtt{Pf}(\ulcorner \neg \psi \urcorner)$.
You can also prove: $\psi \leftrightarrow \mathtt{Pf}\text{ is inconsistent}.$
