Predicato funzionale

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

${\displaystyle \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 ${\displaystyle x}$ della teoria o non esiste alcuna variabile ${\displaystyle y}$ della teoria che verifica il predicato ${\displaystyle \Phi }$ oppure, se esiste una variabile ${\displaystyle y}$ che, insieme ad ${\displaystyle x}$ verifica ${\displaystyle \Phi }$, allora ogni altra variabile ${\displaystyle z}$ che verifica ${\displaystyle \Phi }$ è necessariamente uguale ad ${\displaystyle y}$. In altra maniera, fissata una generica variabile ${\displaystyle x}$, esiste al più una variabile ${\displaystyle y}$ (ossia o non ne esiste alcuna oppure, se ne esiste una, allora ne esiste una sola) che verifica il predicato ${\displaystyle \Phi }$.

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