Okay so I wanted to write down my thoughts on a certain topic, and I wanted to finally publish something, even if informally, so I guess I could tackle both problems in one feel swoop and make an informative thread on mathematical logic in the process.

The topic is definitions.

It should be noted that many of the things said in this thread are a product of my own research and meditation on the topic. I welcome constructive criticism, particularly any in the direction of improvements to my answers regarding the questions I had about the topic.

So, a definition in a given language can be thought of as a sort of abbreviation of an expression of that same language, called the definiens, where the abbreviation itself, called the definiendum, is an expression of an extension of this language.

This is our starting point.

Now, one can encode a language as a mathematical object, namely as a formal language. How does one encode a definition in a formal language as another mathematical object? And in particular, as a mathematical object of the theory of formal languages?

From our intuition about definitions, they are, at the very least, a rule with which we translate the definiendum into the definiens (or vice-versa). Furthermore, a definition is also an specification of the extended language, of which symbols were added to its alphabet and [...]

which rules were added to its grammar.

So, a definition of a formal language L generated by the formal grammar (A, N, P, S) could simply be encoded as a tuple (A', P', d1, d2), where A' is a set of symbols disjoint from A and N, P' is a set of production rules having [...]

the union of A and A' as terminal symbols and N as non-terminal symbols, d1 is a sentential form of the formal grammar (A U A', N, P U P', S), and d2 is a sentential form of the formal grammar of L. Further, a translation with respect to a definition is any of the two rules [...]

d1 -> d2 and d2 -> d1.

A definition generates a formal grammar for the extended language and the translation rules from this language to the original (or vice-versa). At least in the context of formal language theory, this seems to be a fine enough definition of definition.

Now, if the notion of production rules is not available, at least in a particular instance, there is still another satisfactory definition of definition, which is due to Edward Zalta. This definition relies on a deductive system for the language and on equivalence relations [...]

for the different sorts of expressions of this language (terms, formulas etc.).

A definition is a twofold judgement. First, it is a syntactic judgement, and it incorporates the definiendum into the syntax of the language, extending it. Then, it is an inferential judgement, [...]

asserting that the closures of an equivalence relation between the definiendum and the definiens are axioms.

This definition of definition can be very effectively implemented in systems like Metamath, and serves to highlight the inferential role of definitions which would [...]

otherwise be left as a metalinguistic informality.

And this is it, the two well-defined definitions of definitions I know of, for different occasions but from the same origins. This thread is getting to long so I'm going to end it here. Again, I would appreciate any feedback.