Any occurrence of a variable in a formula can be either free or bound.
- Any occurrence of any variable in an atomic formula is free
- Given formulae
, any occurrence of a variable in or remains an occurrence of the same type in - If
is a formulae and has at least one free occurrence in then every free occurence of in becomes bound in (everything else is unchanged)
We let be the set of free variables in a formula i.e. variables that have at least one free occurrence in