Variabile libera

In logica matematica e in particolare in un linguaggio del primo ordine si dice che una variabile occorre libera in una formula ben formata ${\mathcal {A}}$ se nella formula tale variabile appare al di fuori del dominio di un quantificatore sulla variabile stessa.

Operatori che vincolano la variabili

Ognuno dei seguenti operatori vincola la variabile x.

$\sum _{x\in S}\quad \quad \prod _{x\in S}\quad \quad \int _{0}^{\infty }\,dx\quad \quad \lim _{x\to 0}\quad \quad \forall x\quad \quad \exists x$

Esempi

• Nella formula

$\forall xA(x)$

(dove $A$ è un simbolo per predicato unario) la sola variabile presente è $x$ che non occorre libera poiché è quantificata da $\forall x$.

• Nella formula

$\forall xA(x,y)$

(dove $A$ è un simbolo per predicato binario) sono presenti le variabili $x$ e $y$ di cui $y$ occorre libera (non ci sono quantificatori su $y$) ma $x$ no.

• Nella formula

$A(x)\lor \forall x\lnot A(x)$

(dove $A$ è un simbolo per predicato unario), la variabile $x$ compare sia come variabile libera (la prima istanza non ricade nel dominio del $\forall$) che come variabile quantificata.

Definizione ricorsiva

La nozione di occorrenza libera in ${\mathcal {A}}$ si può definire ricorsivamente nel seguente modo:

• se ${\mathcal {A}}$ è una formula atomica allora x occorre libera in ${\mathcal {A}}$ se x compare in ${\mathcal {A}}$.
• se ${\mathcal {A}}$ è ottenuta dalle formule ${\mathcal {B}}$ e ${\mathcal {C}}$ congiungendo queste con un simbolo di connettivo logico allora x occorre libera in ${\mathcal {A}}$ se x occorre libera in ${\mathcal {B}}$ o in ${\mathcal {C}}$.
• se ${\mathcal {A}}$ ha la forma $\forall x_{i}{\mathcal {B}}$ oppure $\exists x_{i}{\mathcal {B}}$ allora x occorre libera in ${\mathcal {A}}$ se occorre libera in ${\mathcal {B}}$ e $x\neq x_{i}$

Il fatto che questa definizione ricorsiva sia ben posta è garantito dal teorema di ricorsione assieme con il teorema di leggibilità unica.