Predicato funzionale

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

$\mathrm{\forall }x\left(\mathrm{\exists }y\right(\mathrm{\Phi }(x,y))\Rightarrow \mathrm{\forall }z(\mathrm{\Phi }(x,z)\Rightarrow (z=y)\left)\right).$

In altri termini, fissata una variabile $x$ della teoria o non esiste alcuna variabile $y$ della teoria che verifica il predicato $\mathrm{\Phi }$ oppure, se esiste una variabile $y$ che, insieme ad $x$ verifica $\mathrm{\Phi }$, allora ogni altra variabile $z$ che verifica $\mathrm{\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 $\mathrm{\Phi }$.

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