| Definition | - an explicit eliminable definition of a mathematical operator or concept ; |
In the sense of a definition of a mathematical operator or concept, we mean an eliminable definition that does not have any further epistemic content. The "meaning" of an expression should remain unchanged when an a definiendum is replaced by it definiens. In a program source this is meant to be like a macro; in a mathematical discourse, the intention is that the truth value or provability of any assertion is preserved by definition elimination or introduction, although the proof itself may require modification with regard, for example, to whether the definiendum is mentioned in inference specifications.
While the creation of a definition provides a new, though semantically shallow, resource for possible use in expression or argument, no substantial epistemic content is implied by the definition; this is in contrast to the addition of axioms or primitive rules of inference. The same goes for theorems and derived rules of inference.
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html