Variabile libera

Template:F 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

Ognuno dei seguenti operatori vincola la variabile x.

$\sum _{x\in S}\prod _{x\in S}\underset{0}{\overset{\mathrm{\infty }}{\int }}dx\underset{x\to 0}{\lim }\mathrm{\forall }x\mathrm{\exists }x$

Esempi

• Nella formula

$\mathrm{\forall }xA(x)$

(dove $A$ è un simbolo per predicato unario) la sola variabile presente è $x$ che non occorre libera poiché è quantificata da $\mathrm{\forall }x$.

• Nella formula

$\mathrm{\forall }xA(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)\vee \mathrm{\forall }x\mathrm{\neg }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 $\mathrm{\forall }$) che come variabile quantificata.

Definizione ricorsiva

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 $\mathrm{\forall }{x}_iℬ$ oppure $\mathrm{\exists }{x}_iℬ$ allora x occorre libera in $𝒜$ se occorre libera in $ℬ$ e $x\ne x_i$

Il fatto che questa definizione ricorsiva sia ben posta è garantito dal teorema di ricorsione assieme con il teorema di leggibilità unica.

Collegamenti esterni

• Template:Collegamenti esterni