This web page gives the official definition of what it means for a variable to be free in a formula of a first-order language .
The definition of what it means for
to be free in or term
first-order language is y induction on terms
and formulas. We shall specify what it means for
to be free in each of the constructions of
terms and formulas, and assume that
it is already understood what
is free in
[or term ]
is already understood for all subformulas and subterms.
Most syntactical definitions in first order logic are of this kind: such definitions implicitly require the Theorem on Unique Readability, which says that for any term or formula there is a unique way of reading it as built from subformulas and subterms, and therefore exactly one of our inductive clauses applies.
Fix a first order language and variable of . Here are the clauses defining what it means for to be free in .
That's it. You should be able to check that this defines
is free in
for all . Readers
with some programming experience will recognise the definition just given
as a recursive definition, and will easily be able to write a subroutine
or function in their favourite language that computes whether
is free in . In other words, this notion is
(rather easily) computable.
is not free in
to the statement that
Each occurence of in is in the
scope of a quantifier or .
It is common to write a formula or term with arguments displayed as or . When so-doing it is important to list all of the variables that occur free in or . It is always OK to include additional variables, however, and this sometimes saves a lot of writing. The reason for this is that there is little difference between and so it is OK to write the former as . But it would be a mistake to write as as the does play a role and must not be forgotten.
A closed term is a term which has no free variables (and hence has no variables at all). A sentence is a formula which has no free variables. Sentences are sometimes called closed formulas.