Variabile libera: differenze tra le versioni
Contenuto cancellato Contenuto aggiunto
m →top: sistemazione fonti, smistamento lavoro sporco e fix vari |
|||
(14 versioni intermedie di 12 utenti non mostrate) | |||
Riga 1:
{{F|logica|aprile 2012}}
In [[logica matematica]] e in particolare in un [[linguaggio del primo ordine]] si dice che una '''[[variabile (matematica)|variabile]]''' occorre '''libera''' in una [[formula ben formata]] <math>\mathcal A</math> se nella formula
==Operatori che vincolano la variabili==
Ognuno dei seguenti operatori vincola la variabile ''x''.
: <math>\sum_{x\in S}
\quad\quad \prod_{x\in S}
\quad\quad \int_0^\infty\,dx
\quad\quad \lim_{x\to 0}
\quad\quad \forall x
\quad\quad \exists x</math>
==Esempi==
Riga 9 ⟶ 20:
* Nella formula
:<math>\forall x A(x,y)</math>
(dove <math>A</math> è un simbolo per predicato binario) sono presenti le variabili <math>x</math> e <math>y</math> di cui <math>y</math> occorre libera (non ci sono quantificatori su <math>y</math>) ma <math>x</math> no.
* Nella formula
:<math>A(x) \lor \forall x \lnot A(x)</math>
(dove <math>A</math> è un simbolo per predicato unario), la variabile <math>x</math> compare sia come variabile libera (la prima istanza non ricade nel dominio del <math>\forall</math>) che come variabile quantificata.
== Definizione ricorsiva==
Riga 18 ⟶ 33:
* se <math>\mathcal A</math> ha la forma <math>\forall x_i \mathcal B</math> oppure <math>\exists x_i \mathcal B</math> allora ''x'' occorre libera in <math>\mathcal A</math> se occorre libera in <math>\mathcal B</math> e <math>x\neq x_i</math>
Il fatto che questa [[definizione ricorsiva]] sia ben posta è garantito dal [[teorema di ricorsione]] assieme con il [[teorema di leggibilità unica]].
== Collegamenti esterni ==
* {{Collegamenti esterni}}
[[Categoria:Logica matematica]]
|