Predicato funzionale

In logica matematica, per predicato funzionale o formula funzionale o simbolo funzionale in $x$ si intende un predicato $\Phi (x,y)$, in cui le variabili $x$ ed $y$ occorrono libere, avente la seguente proprietà:

$\forall x{\Bigl (}\exists y{\bigl (}\Phi (x,y){\bigr )}\Rightarrow \forall z{\bigl (}\Phi (x,z)\Rightarrow (z=y){\bigr )}{\Bigr )}.$

In altri termini, fissata una variabile $x$ della teoria o non esiste alcuna variabile $y$ della teoria che verifica il predicato $\Phi$ oppure, se esiste una variabile $y$ che, insieme ad $x$ verifica $\Phi$, allora ogni altra variabile $z$ che verifica $\Phi$ è necessariamente uguale ad $y$. In altra maniera, fissata una generica variabile $x$, esiste al più una variabile $y$ (ossia o non ne esiste alcuna oppure, se ne esiste una, allora ne esiste una sola) che verifica il predicato $\Phi$.

In maniera equivalente, un predicato $\Phi (x,y)$ in cui le variabili $x$ ed $y$ occorrono libere è funzionale in $x$ se $\forall x\forall y\forall z{\Bigl (}{\bigl (}\Phi (x,y)\wedge \Phi (x,z){\bigr )}\Rightarrow (y=z){\Bigr )}.$