termine libero
termine libero o termine aperto, in logica, termine di un linguaggio formale che contiene almeno una variabile libera. In particolare, nel linguaggio dei predicati, termine che contiene almeno una variabile non vincolata da alcun quantificatore. Per esempio, nella formula ben formata ∀x(A(x, y) ≥ s(x)) (si legge «per ogni x, A di x e y è maggiore o uguale a s di x»), i simboli che compaiono nella formula sono:
• il quantificatore universale ∀ (si legge «per ogni»);
• il simbolo di funzione A che, applicato alle variabili x e y, forma il termine A(x, y) che può essere interpretato come l’addizione di due numeri naturali x + y;
• il simbolo di funzione s che, applicato alla variabile x, forma il termine s(x) che può essere interpretato come il successore di x;
• il simbolo di relazione ≥ applicato ai due termini A(x, y) e s(x).
La formula precedente assume quindi la seguente interpretazione: «dato un qualsiasi numero naturale x, la somma di x con un altro numero y è maggiore o uguale al successore di x». In questa formula il termine s(x) non è libero perché l’unica variabile in esso contenuta (la x) risulta vincolata dal quantificatore universale, cioè compare nel campo di azione di un quantificatore; il termine A(x, y), invece, risulta libero in quanto, oltre a x, contiene la variabile libera y che non è vincolata dal quantificatore universale.
☐ Nel → lambda-calcolo un termine è libero se fra le sue variabili ne contiene almeno una che non è vincolata dal simbolo λ. Per esempio, nell’espressione λz(y)z il termine (y)z è libero perché contiene la variabile y che non è vincolata dal simbolo λ, al contrario della variabile z.