Definable function (source code)

= Definable function
{title2=$\operatorname{graph}(f)\text{ is definable}$}

A <function> $f:M^n\to M$ is a <definable function> if its <graph of a function> is a <definable set>. Equivalently, a <first-order formula> $\theta(\mathbf x,y)$ defines exactly the pairs with $y=f(\mathbf x)$. Totality and uniqueness mean $M\models\forall\mathbf x\exists!y\,\theta(\mathbf x,y)$. The same definition with restricted domains gives definable partial functions. A function need not be a symbol of the language to be definable; the graph can be specified through the existing relations and operations.