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

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

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.

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

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.

Collegamenti esterni

• (EN) free variable, su Enciclopedia Britannica, Encyclopædia Britannica, Inc.
• (EN) Eric W. Weisstein, Variabile libera, su MathWorld, Wolfram Research.
• (EN) Variabile libera, su Encyclopaedia of Mathematics, Springer e European Mathematical Society.