In logica matematica e in particolare in un linguaggio del primo ordine si dice che una variabile occorre libera in una formula ben formata A {\displaystyle {\mathcal {A}}} se nella formula tale variabile appare al di fuori del dominio di un quantificatore sulla variabile stessa. Wikipedia