Definition:Stipulative Definition

Definition

A stipulative definition is a definition which defines how to interpret the meaning of a symbol.

It stipulates, or lays down, the meaning of a symbol in terms of previously defined symbols or concepts.

The symbol used for a stipulative definition is:

$\text {(the symbol being defined)} := \text {(the meaning of that symbol)}$

This can be written the other way round:

$\text {(a concept being assigned a symbol)} =: \text {(the symbol for it)}$

when it is necessary to emphasise that the symbol has been crafted to abbreviate the notation for the concept.

The symbol used to introducing a stipulative definition varies throughout the literature.

Here are some instances:

$\text {(the symbol being defined)} \mathrel{\stackrel {\mathbf {def}} {=\!=}} \text {(the meaning of that symbol)}$

$\text {(the symbol being defined)} \mathrel{=_{df}} \text {(the meaning of that symbol)}$

$\text {(the symbol being defined)} = \text {(the meaning of that symbol)} \quad \text{Df.}$

These constructs are not used on $\mathsf{Pr} \infty \mathsf{fWiki}$ through being cumbersome and awkward to reproduce.