title: Variabile libera
text: # 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.
  
  