\begin{definition}[Definition:Minimization/Relation]
Let $\map \RR {n_1, n_2, \ldots, n_k, y} $ be a $k + 1$-ary relation on $\N^{k + 1}$.
Let $n = \tuple {n_1, n_2, \ldots, n_k} \in \N^k$ be fixed.
Then the '''minimization operation on $\RR$''' is written as:
:$\mu y \map \RR {n, y}$
and is specified as follows:
:$\mu y \map \RR {n, y} = \begin{cases}
\text{the smallest } y \in \N \text{ for which } \map \RR {n, y} \text{ holds} & : \text{if there exists such a } y \\
\text{undefined} & : \text{otherwise}
\end{cases}$
We can consider the definition for a function to be a special case of this.
Compare the bounded minimization operation which is always a total function.
Category:Definitions/Mathematical Logic
\end{definition}