Stipulative definitions

The logic of expanding a formal language by introducing defined terms and relations

Mathematicians recognize that a key initial step for mounting a successful mathematical investigation is often simply to give names to the objects and properties at hand—by expanding our language we become able to express more clearly the ideas, constructions, and results that will constitute the framework of our understanding. We advise calculus students to “let x be the thing you want to know,” and more generally, in every field of mathematics we fruitfully make definitions that in effect give names to the concepts in which we are interested. When studying an order relation ⩽ we define the concepts of being least, greatest, and incomparable; in the bare-bones language of set theory with just the element-of relation ∈ we define the notions of subset, power set, ordinal, cardinal, ultrafilter, and so on, building an enormous conceptual edifice of defined notions in which the mathematics ultimately takes place.

Let us look into how this works more precisely. The basic fact is that in every first-order theory, we may introduce new notions by stipulative definition, defining a new concept in terms of concepts already understood.