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.

Esempi

• Nella formula

$\forall x A(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 x A(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.

Portale Matematica: accedi alle voci di Wikipedia che trattano di matematica