Definizione induttiva

• Base: le occorrenze di variabili libere in un atomica P(t1, t2, ... tn) sono tutte occorrenze di variabili in t1, t2, ... tn. Cioè le variabili che ci sono nei termini sono quelle libere. ⊥ non ha occorenze di variabili libere
• Passo:
  • Le occorrenze di variabili libere in ¬P, P∧Q e le altre robe, sono tutte le occorrenze di variabili libere in P o in Q
  • Le occorenze di variabili libere in ∀xP/∃xP sono tutte le occorrenze di variabili libere in P, ad eccezione di x. Ogni occorrenza di x in P è vincolata (bound) in ∀xP

<aside> ⚠️

</aside>

<aside> ⚠️

Una variabile può avere occorenze libere e vincolate nella stessa fbf.

</aside>