# 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'm voting to close this question as off-topic because it is a question about pure logic. Why is it appearing on a theoretical computer science site? Jul 23, 2019 at 19:43
• @AndrejBauer: I've tried to post it on the math stackexchange, and it was closed there too. Surely there's got to be some place where I can post this question. I think this question belongs to the present forum because my feeling is that the math logicians don't even comprehend why a logic should provide the ability to define terms. The notion of a definition has to do with the usability of the logic as a language for thinking about and communicating mathematics, which is an aspect of logic that, from my experience, math logicians are completely oblivious too. Jul 23, 2019 at 19:48
• My condolances for having an obviously math question closed on Math SE. We are happy to adopt you here. Jul 24, 2019 at 7:29
• Since you came to computer scientists, let me mention that in type theory the definitional equalities are sometimes known as $\delta$-reductions. These are meant to be just abbreviations (as opposed to Russell-style $\iota$ description operator). Jul 24, 2019 at 7:33
• Hi there! I'm not entirely sure if this is relevant, but I've always had the intuition that a unary predicate $\phi$ is a $\textbf{definition}$ relative to an axiom system $A$ if $\vdash_A \exists ! x. \phi(x)$. Maybe the word $\textbf{specification}$ is more accurate though. Aug 29, 2019 at 0:30