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

Operatori che vincolano la variabiliModifica

Ognuno dei seguenti operatori vincola la variabile x.

 

EsempiModifica

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

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.

Collegamenti esterniModifica

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