What is the definition of a definition?

Question

In mathematical logic or other formal systems, what is the definition of a definition, formally?

If "A" is defined as "B", what is the definition of "A" like? Does it involve both "A" and "B" (e.g. "A := B"), or just "B"?

For example, on p126 in §3. Extensions by Definitions in VIII Syntactic Interpretations and Normal Forms in Ebbinghaus' Mathematical Logic, suppose that $S$ is a (non-logical) symbol set,

3.1 Definition. Let $\Phi$ be a set of $S$-sentences.

(a) Suppose $P \notin S$ is an $n$-ary relation symbol and $\phi_P(v_0, ... , v_{n-1})$ an $S$-formula. Then we say that $$ \forall v_0, .... \forall v_{n-1} (P v_0 ... n_{n-1} \leftrightarrow \phi_P(v_0, ... , v_{n-1})) $$ is an $S$-definition of $P$ in $\Phi$.

Which shall I call as an $S$-definition of $P$ in $\Phi$:

1. $ \forall v_0, .... \forall v_{n-1} (P v_0 ... n_{n-1} \leftrightarrow \phi_P(v_0, ... , v_{n-1})) $?

   • Is it circular to define $P$ in terms of itself?

   • Is an $$-definition of $$ in $Φ$ an interpretation of symbol $P$ as an $S'$-sentence? (as part of a syntactic interpretation of $S'$ in $S'$ itself?)

   • Is the appearance of $P$ in its own definition $∀ _0,....∀ _{−1}(_0...v_{−1}↔_(_0,...,_{−1}))$, in the same sense as the appearance of $A$ in $:=$?

2. $\phi_P(v_0, ... , v_{n-1})) $ ? (I guess that $P$ is defined as $\phi_P(v_0, ... , v_{n-1})) $ in $\Phi$.)

3. $\phi_P$? (Compare that to the second: $P$ itself doesn't involve variables)

See How does this definition define a symbol $P$ outside the symbol set $S$ as a $S$-sentence?

Thanks.

Answer 1

We have a signature $S$ and we extend it to $S':=S\cup\{P\}$.

The $S$-definition of $P$ is the $S'$-formula $$\forall v_0\dots v_{n-1}: Pv_0\dots v_{n-1}\leftrightarrow \phi_P(v_0,\dots,v_{n-1})$$ which can be formally handled as an extra axiom to the given $S$-theory we're working with, thus producing an equivalent $S'$-theory, in which the symbol $P$ can be used as abbreviation for the formula $\phi_P$.

For example, the below formula is the definition of the usual ordering relation $\le$ of nonnegative integers in the language $(0,+)$: $$\forall x,y:\ x\le y\,\leftrightarrow\,\exists z: x+z=y$$

Answer 2

Below I'll first try to describe the process in a more intuitive way, then address your worries about circularity. I suspect the latter point may actually be more helpful, so feel free to read the second section first - and in particular, the highlighted motto there will I think be quite helpful.

(Re: your final comment, the definition is $(1)$ - the thing which tells you how the new symbol behaves, in terms of the old symbols you already have and understand.)

---

The key phrase here is "expansion by definitions."

Intuitively, we have in mind the following process:

• Starting with a signature $S$ and some set $\Phi$ of $S$-sentences, we become a little annoyed by inefficiencies: there are some things which we can talk about using $S$-formulas but only in a roundabout way. Think for example about the language of set theory, $\{\in\}$: we can express things like "$x$ is the Cartesian product of $y$ and $z$" in this language, but only via annoyingly long formulas. (It's a good exercise to handle the previous example - using, say, Kuratowski pairs.)

• So given our really complicated formula $\varphi(x_0,...,x_{n-1})$, we want to whip up a new theory which is basically the same as $\Phi$ except that it additionally has an "abbreviation" for $\varphi$.

• First, this means we want to enlarge our language: rather than work with $S$ we want to work with $S\cup\{R\}$ for some $n$-ary relation symbol $R\not\in S$ which we intend to serve as an abbreviation for $\varphi$.

• Now we have to define a theory in this larger language. This theory should subsume what we already have (that is, $\Phi$), should correctly dictate the behavior of $R$ (that is, say that it's an abbreviation for $\varphi$), and shouldn't do anything else. This leads us to consider the new theory $$\Phi':=\Phi\cup\{\forall x_0,...,x_{n-1}(R(x_0,...,x_{n-1})\leftrightarrow \varphi(x_0,...,x_{n-1})\}.$$

The passage from $S,\Phi$, and $\varphi$ to $S\cup\{R\}$ and $\Phi'$ is an expansion by definitions. We have some serious redundancy here: in a precise sense, $\Phi'$ is really no better than $\Phi$. (Formally, $\Phi'$ is a conservative extension of $\Phi$ in the strongest possible sense: every model of $\Phi$ has exactly one expansion to a model of $\Phi'$.) This isn't surprising. We already knew we could express the thing we cared about via $\varphi$, we just wanted to be able to do so more quickly.

Incidentally, note that this suggests a natural "maximally efficient" version of any theory: just add new symbols for every formula! This is called Morleyization, and is occasionally useful (although usually kind of silly).

---

OK, now what about the circularity you are worried about?

First, note that "$R$" itself is just a symbol. The new sentence we're adding isn't really a definition of $R$, but rather a definition of the meaning of $R$, or if you prefer a rule governing the behavior of $R$.

More seriously, circularity is never an issue in FOL! The key idea is the following, which I think is an important departure from the intuitions one might bring in from programming:

A set of first-order sentences doesn't create things, it describes things.

Specifically, a set of first-order sentences $\Phi$ carves out a particular class of structures, those about which it is an accurate description. For instance, the possibly-dangerous-looking sets $$\{\forall x(P(x)\leftrightarrow P(x))\}$$ and $$\{\forall x(Q(x)\leftrightarrow \neg Q(x))\}$$ are perfectly circle-free; they're just vacuous (= hold of every structure) and contradictory (= hold of no structure) respectively.