This web page gives the official definition of what it means for a variable v to be free in a formula ϕ of a first-order language L .
The definition of what it means for of a first-order language L is y induction on terms and formulas. We shall specify what it means for v to be free in each of the constructions of terms and formulas, and assume that it is already understood what v is free in ϕ [or term t ] 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 L and variable v of L . Here are the clauses defining what it means for v to be free in ϕ .
That's it. You should be able to check that this defines v 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 v is free in ϕ . In other words, this notion is (rather easily) computable.
Show that v is not free in ϕ is equivalent to the statement that Each occurence of v in ϕ is in the scope of a quantifier ∀ v or v .
It is common to write a formula ϕ or term t with arguments displayed as ϕ ( v 1 , … , v k ) or t ( v 1 , … , v k ) . When so-doing it is important to list all of the variables that occur free in ϕ or t . 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 ϕ ( v 1 , v 2 ) and ϕ ( v 1 , v 2 ) ∧ ( v 3 = v 3 ) so it is OK to write the former as ϕ ( v 1 , v 2 , v 3 ) . But it would be a mistake to write ϕ ( v 1 , v 2 ) ∧ ( v 3 = v 3 ) as ϕ ( v 1 , v 2 ) as the v 3 does play a role and must not be forgotten.
A is a term which has no free variables (and hence has no variables at all). A is a formula which has no free variables. Sentences are sometimes called .