Variabile libera

Da Wikipedia, l'enciclopedia 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.

Esempi[modifica | modifica sorgente]

  • Nella formula
\forall x A(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 x A(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[modifica | modifica sorgente]

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.

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