Variabile libera

Da Teknopedia, l'enciclopedia libera.
Vai alla navigazione Vai alla ricerca
Niente fonti!
Questa voce o sezione sull'argomento matematica non cita le fonti necessarie o quelle presenti sono insufficienti.

Puoi migliorare questa voce aggiungendo citazioni da fonti attendibili secondo le linee guida sull'uso delle fonti. Segui i suggerimenti del progetto di riferimento.

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

[modifica | modifica wikitesto]

Ognuno dei seguenti operatori vincola la variabile x.

  • 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

[modifica | modifica wikitesto]

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.

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