The theory of definitions in first order logic I'm looking for a clear and thorough treatment of the theory of definitions in first order predicate logic from a syntactic/proof theoretic point of view (as opposed to semantic/model theoretic point of view). Ideally, the covered material should include at least what is covered in sections 2.3-2.5 of Anil Gupta's Stanford Encyclopedia of Philosophy article titled Definitions, namely conservativeness and eliminability, definitions in normal form, and implicit definitions. It doesn't have to be all in a single resource.
I don't have the books handy at the moment, but I think Shoenfield's "Mathematical Logic" and Hinman's "Fundamentals of Mathemtical Logic" would contain much if not all of what you're looking for. 

Probably not what you want but perhaps worth mentioning anyway is A. P. Morse's book "A Theory of Sets". This is a development of (a rather idiosyncratic version of) what is usually called Morse-Kelley set theory, but Morse also pays a great deal of attention to the formulation of definitions. His goal is to make the formal language close to normal mathematical English, while avoiding ambiguities. There's a long chapter, early in the book, spelling out what is allowed in definitions.

Another logician who paid close attention to definitions was S. Lesniewski. He developed a system of foundations of mathematics in which definitions played a crucial role. In contrast to most systems, definitions are not conservative in Lesniewski; some definitions play the role of comprehension axioms. Because of their importance in his framework, Lesniewski gave very careful rules for what constitutes a legitimate (in his sense) definition. Some of his work is very hard to find (and it's mostly in Polish, though a little of it is in German), but there's a book, "The Logical Systems of Lesniewski" by Luschei, that describes it well. (There should be an acute accent on the first s in "Lesniewski" but the best my keyboard and browser can do here is Le´sniewski.)