Questa voce o sezione sull'argomento matematica non cita le fonti necessarie o quelle presenti sono insufficienti.

---

Puoi migliorare questa voce aggiungendo citazioni da fonti attendibili secondo le linee guida sull'uso delle fonti. Segui i suggerimenti del progetto di riferimento.

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 tale variabile appare al di fuori del dominio di un quantificatore sulla variabile stessa.

Ognuno dei seguenti operatori vincola la variabile x.

${\displaystyle \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}$

• 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.

• Nella formula

${\displaystyle A(x)\lor \forall x\lnot A(x)}$

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

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.

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