Variabile libera
variabile di una formula logica non presente nello scope di un quantificatore
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 non ci sono quantificatori su tale variabile.
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.
Definizione induttiva
La nozione di variabile libera in si può definire induttivamente 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 è libera in se lo è in e .
- se ha la forma oppure allora x è libera in se è libera in e