Definitions vs "conservative and eliminable"

[Cris Perdue]

Mario wrote -

- the class extension exists in metamath for a very good reason), and if we mark them as definitions then people (like Wolf in this very thread) might get confused about by what standard we judge axioms to be "definitions", which is a question of high importance considering that it forms part of the trusted base of metamath (since verifiers don't check it).

Norm replied -

The standard is that a definition must be conservative and eliminable.

--------------------------------------

It seems to me that Norm is mistaken in this, and that the usual terminology is that "definitions" have certain prescribed forms.

The wikipedia article on extension by definitions (https://en.wikipedia.org/wiki/Extension_by_definitions) refers to

• S.C. Kleene (1952), Introduction to Metamathematics, D. Van Nostrand
• E. Mendelson (1997). Introduction to Mathematical Logic (4th ed.), Chapman & Hall.
• J.R. Shoenfield (1967). Mathematical Logic, Addison-Wesley Publishing Company (reprinted in 2001 by AK Peters)

I have copies of Kleene and Shoenfield, and they describe "definitions" as having specific defining forms, which I take to be much like those that Metamath can automatically check.

In Kleene, section 74 (page 405 to 420) is titled "Eliminability of descriptive definitions", and it has subsections on "Eliminability of explicit definitions" and "Eliminability of descriptive definitions".  He also discusses eliminability of some other constructs including "a defined sort of variables" (p. 420).

In Shoenfield, section 4.6 starting p. 57 is titled "Extensions by definitions", covering definitions of new predicate symbols and definitions of new function symbols.  He states (p. 60) that, "We say that T' is an extension by definitions of T if T' is obtained from T by a finite number of extensions of the two types which we have described."

From this I conclude that these authors distinguish the concept of definition from the more general concept of being conservative and eliminable. In my mind a definition is readily identified as such from its form, but it may take nontrivial proof to determine that an extension is conservative and eliminable.

-Cris