Variabile libera
![Niente fonti!](http://upload.wikimedia.org/wikipedia/commons/thumb/6/64/Question_book-4.svg/45px-Question_book-4.svg.png)
In logica matematica e in particolare in un linguaggio del primo ordine si dice che una variabile occorre libera in una formula ben formata 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.
Esempi
- Nella formula
(dove è un simbolo per predicato unario) la sola variabile presente è che non occorre libera poiché è quantificata da .
- Nella formula
(dove è un simbolo per predicato binario) sono presenti le variabili e di cui occorre libera (non ci sono quantificatori su ) ma no.
- Nella formula
(dove è un simbolo per predicato unario), la variabile compare sia come variabile libera (la prima istanza non ricade nel dominio del ) che come variabile quantificata.
Definizione ricorsiva
La nozione di occorrenza libera in si può definire ricorsivamente nel seguente modo:
- se è una formula atomica allora x occorre libera in se x compare in .
- se è ottenuta dalle formule e congiungendo queste con un simbolo di connettivo logico allora x occorre libera in se x occorre libera in o in .
- se ha la forma oppure allora x occorre libera in se occorre libera in e
Il fatto che questa definizione ricorsiva sia ben posta è garantito dal teorema di ricorsione assieme con il teorema di leggibilità unica.
![](http://upload.wikimedia.org/wikipedia/commons/thumb/a/af/Crystal128-kmplot.svg/25px-Crystal128-kmplot.svg.png)