Variabile libera: differenze tra le versioni

Versione delle 12:37, 28 set 2007

Versione attuale delle 11:20, 29 giu 2025

(16 versioni intermedie di 13 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 nontale civariabile sonoappare quantificatorial sudi talefuori del dominio di un [[quantificatore]] sulla variabile stessa.

==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

== Definizione induttiva==

:<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 induttivaricorsiva==

La nozione di ''occorrenza libera'' in <math>\mathcal A</math> si può definire induttivamente nel seguente modo:

La nozione di ''occorrenza libera'' in <math>\mathcal A</math> si può definire induttivamentericorsivamente nel seguente modo:

* se <math>\mathcal A</math> è una formula atomica allora ''x'' occorre libera in <math>\mathcal A</math> se ''x'' compare in <math>\mathcal A</math>.

* se <math>\mathcal A</math> è ottenuta dalle formule <math>\mathcal B</math> e <math>\mathcal C</math> congiungendo queste con un simbolo di [[connettivo logico]] allora ''x'' occorre libera in <math>\mathcal A</math> se ''x'' occorre libera in <math>\mathcal B</math> o in <math>\mathcal C</math>.

* 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 {{Portale|matematica]]}}

[[Categoria:Logica matematica]]

[[en:Free variables and bound variables]]

[[ru:Свободная переменная]]

[[zh:自由变量和约束变量]]