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 ${\displaystyle {\mathcal {A}}}$ se nella formula non ci sono quantificatori su tale variabile.

Esempi

• Nella formula

${\displaystyle \forall xA(x)}$ 

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

• Nella formula

${\displaystyle \forall xA(x,y)}$ 

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

Definizione ricorsiva

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

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