Definitions and Designations

The following is from J. R. Abrial and L. Mussat  ["On Using Conditional Definitions in Formal Theories",  in D. Bert et al (Eds.), ZB2002, Lecture Notes in Computer Science. pages 242-269, Springer, 2002]:

Suppes first introduces two criteria characterizing the definition of new symbols in a formal theory: (1) the Criterion of Eliminability, and (2) the Criterion of Non-creativity. The former requires that "any definition introducing a new symbol may be used to eliminate all subsequent meaningful occurrences (of that new symbol)". The latter requires that any definition of a new symbol "(does not) make possible the derivation of some previously unprovable theorem stated wholly in terms of primitive and previously defined symbols". In other words, a proper definition must not add any extra "power" to a theory, it is just a useful, but not indispensable, extension to it.

This means that definitions are just abbreviations and therefore cannot be used to build a theory; they can only be used to express an existing theory in a different way.

Michael Jackson ["Software Requirements and Specifications", Addison Wesley, 1995, pages 51-54] has some interesting things to say on the subject of the symbols used in specifications:

One way to define a term is to give a designation. That means giving a recognition rule for recognizing some class of phenomenon that you could observe in a domain. In the domain of human relationships you might have these designations:

x is a human being (homo sapiens) = Human(x)

x is male = Male(x)

x is female = Female(x)

x is the biological (genetic) mother of y = Mother(x,y)

x is the biological (genetic) father of y = Father(x,y)

[...] You can use the designated terms in refutable descriptions that make assertions about the domain. [...]

Thus designated terms (symbols) here connect the theory with the domain that the theory describes. Jackson goes on:

Now suppose that you want to make some assertions about grandparents, and aunts and uncles, and cousins and brothers and sisters.  You don't have any designations for these terms, but it will be very inconvenient and difficult to do without them.  there are two ways of making them available for use in your descriptions.  One way is to write some more designations.  For example

x is the genetic full brother of y = Brother(x,y)

[...]

Sometimes this is the right thing  to do.  But probably it is not the right thing here.  The right thing here is to do it the other way: to give a formal definition of each of the new terms, using the terms you have already designated.  [...]

Brother(x,y)  ≙ 
  Male(x) ∧
     ∃ f . (Father(f,x) ∧ Father(f,y) ) ∧
     ∃ m . (Mother(m,x) ∧ Mother(m,y) )

This is a definition in the style of Suppes.   However, I think it is unsatisfactory to regard 'Brother' as purely a convenience to make the theory shorter.  If it was, then it wouldn't matter if you replaced 'Brother' by say 'Aunt' throughout the theory.  The choice of names is important even in strictly unnecessary definitions.  They also designate things in the domain.

In my way of specifying there is no need to introduce new symbols, as all possible symbols already exist.  Writing a specification is just a matter of defining the constraints on these already existing symbols.

(By the way, did you spot that the definition of Brother requires the extra constraint x ≠ y?  Without this I would be my own brother.)