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.
$\begingroup$
$\endgroup$
6
-
1$\begingroup$ 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? $\endgroup$– Andrej BauerJul 23, 2019 at 19:43
-
2$\begingroup$ @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. $\endgroup$– Evan AadJul 23, 2019 at 19:48
-
1$\begingroup$ My condolances for having an obviously math question closed on Math SE. We are happy to adopt you here. $\endgroup$– Andrej BauerJul 24, 2019 at 7:29
-
1$\begingroup$ 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). $\endgroup$– Andrej BauerJul 24, 2019 at 7:33
-
$\begingroup$ 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. $\endgroup$– Michael WeharAug 29, 2019 at 0:30
|
Show 1 more comment
1 Answer
$\begingroup$
$\endgroup$
3
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.)
-
$\begingroup$ 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). $\endgroup$– Evan AadJul 24, 2019 at 4:43
-
$\begingroup$ 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. $\endgroup$– Evan AadJul 24, 2019 at 4:48
-
$\begingroup$ 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. $\endgroup$– Evan AadJul 24, 2019 at 5:02