<p>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. </p>

<p>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.</p>

<p>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.)</p>

CC BY-SA 4.0
2019-07-24T04:43:53.677Z
Thank! To this I'll add a few entries I've found in the meanwhile. (1) "Introduction to Logic" (1957) by Patrick Suppes, chapter 8 "Theory of Definition". (2) Benson Mates "Elementary Logic" (2nd ed., 1972), section 11.5 "Definitions" (and possibly other places in the book, I'm not sure), (3) Some half-baked, non-rigorous remarks on the topic can be found in the beginning of chapter 4 "Definitions and Rules of Inference in the Sentential Calculus" by Jan Łukasiewicz's "Elements of Mathematical Logic" (English translation 1963 of the Polish 2nd ed. of 1958).
Evan Aad
CC BY-SA 4.0
2019-07-24T04:48:11.643Z
Considering all of these references are quite old: the two most current are Hinman from 2005 and Morse from 1986, and from a cursory perusal of Hinman, I'm not at all sure he takes the proof-theoretic approach I'm looking for, one wonders why this topic is so absent from contemporary treatises of logic.
Evan Aad
CC BY-SA 4.0
2019-07-24T05:02:51.170Z
Also, someone of authority suggested Boolos, Burgess, and Jeffrey's "Computability and Logic", (5th ed., 2007), but I'm not sure where in the book (possibly chapter 20 "The Craig Interpolation Theorem"), and, at any rate, I suspect it doesn't take the proof-theoretic approach to the topic I am looking for. Finally, there's also Moschovakis' "Elementary induction on abstract structures" (1974), which focuses on certain self-referential definitions.
Evan Aad
CC BY-SA 4.0
2019-07-23T22:21:17.347Z
2019-07-23T22:21:17.347Z
Andreas Blass
<p>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 <a href="https://plato.stanford.edu/entries/definitions/" rel="nofollow noreferrer">Anil Gupta's Stanford Encyclopedia of Philosophy article titled Definitions</a>, namely conservativeness and eliminability, definitions in normal form, and implicit definitions. It doesn't have to be all in a single resource.</p>

CC BY-SA 4.0
2019-07-23T19:43:55.363Z
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?
Andrej Bauer
CC BY-SA 4.0
2019-07-23T19:48:52.607Z
@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.
Evan Aad
CC BY-SA 4.0
2019-07-24T07:29:58.357Z
My condolances for having an obviously math question closed on Math SE. We are happy to adopt you here.
Andrej Bauer
CC BY-SA 4.0
2019-07-24T07:33:05.430Z
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).
Andrej Bauer
CC BY-SA 4.0
2019-08-29T00:30:17.030Z
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.
Michael Wehar
CC BY-SA 4.0
2019-08-29T00:45:49.063Z
I think this is an interesting topic.  I'm always happy to discuss this more.  :)
Michael Wehar
<reference-request><proof-theory><definitions><first-order-logic>
The theory of definitions in first order logic
Evan Aad
# The theory of definitions in first order logic

(Asked by: username_0 on 2019-07-21)

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](https://plato.stanford.edu/entries/definitions/), namely conservativeness and eliminability, definitions in normal form, and implicit definitions. It doesn't have to be all in a single resource.

**Tags:** reference-request, proof-theory, definitions, first-order-logic

> **Comments:**
> **username_1**: 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?  
> **username_0**: @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.  
> **username_1**: My condolances for having an obviously math question closed on Math SE. We are happy to adopt you here.  
> **username_1**: 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).  
> **username_2**: 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.  
> **username_2**: I think this is an interesting topic.  I'm always happy to discuss this more.  :)  

---

## 1 answers

### Answer by username_3 on 2019-07-23. Score: 6

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.)

> **Comments:**
> **username_0**: Thank! To this I'll add a few entries I've found in the meanwhile. (1) "Introduction to Logic" (1957) by Patrick Suppes, chapter 8 "Theory of Definition". (2) Benson Mates "Elementary Logic" (2nd ed., 1972), section 11.5 "Definitions" (and possibly other places in the book, I'm not sure), (3) Some half-baked, non-rigorous remarks on the topic can be found in the beginning of chapter 4 "Definitions and Rules of Inference in the Sentential Calculus" by Jan Łukasiewicz's "Elements of Mathematical Logic" (English translation 1963 of the Polish 2nd ed. of 1958).  
> **username_0**: Considering all of these references are quite old: the two most current are Hinman from 2005 and Morse from 1986, and from a cursory perusal of Hinman, I'm not at all sure he takes the proof-theoretic approach I'm looking for, one wonders why this topic is so absent from contemporary treatises of logic.  
> **username_0**: Also, someone of authority suggested Boolos, Burgess, and Jeffrey's "Computability and Logic", (5th ed., 2007), but I'm not sure where in the book (possibly chapter 20 "The Craig Interpolation Theorem"), and, at any rate, I suspect it doesn't take the proof-theoretic approach to the topic I am looking for. Finally, there's also Moschovakis' "Elementary induction on abstract structures" (1974), which focuses on certain self-referential definitions.  

---

