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?

• See some aspects regarding logical theory of definitions in this post and this post Commented Jun 27, 2014 at 14:40
• @MauroALLEGRANZA, the clarification of these aspects sounded very useful. Some of your remarks support the idea I have about a logical theory or definitions, which I will share in my own answer below. Commented Jun 29, 2014 at 15:00
• You are right in saying that form a 'logical point of view' : "a definition is treated as an abbreviation". What we have to be sure is that the abbreviation is "well-defined", i.e.that, in order to introduce a new symbol denoting "inequivocally" an object satisfying the "property" $P$ (like e.g. $\emptyset$ in set theory), we have proved previously that $\exists ! xP(x)$. Commented Jun 29, 2014 at 16:26
• Really, I think this is more like a programming problem in spirit than a math problem.
– user14972
Commented Aug 5, 2014 at 0:02

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

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! :)

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}.$