1.1.7 Subformulae, Free Variables
Defining the concepts of subformula and free variable.
Subformulae.
In what follows, we occasionally use the term subformula . As an explanation, the subformulae of any formula 
are itself as well as all of the formulae that are used to build . For example, the subformulae of
are 
, 
, and 
.
Exercise 1.2
Give an inductive definition of subformulahood.
Free and Bound Variables.
Let's now turn to a rather important topic: the distinction between free variable s and bound variable s.
Have a lok at the following formula:
The first occurrence of x is free, whereas the second and third occurrences of x are bound, namely by the first occurrence of the quantifier 
. The first and second occurrences of the variable y are also bound, namely by the second occurrence of the quantifier . Here's the full definition:
Any occurrence of any variable is free in any atomic formula.
No occurrence of any variable is bound in any atomic formula.
If an occurrence of any variable is free in
or in 
, then that same occurrence is free in 
, 
, 
, and 
.If an occurrence of any variable is bound in
or in , then that same occurrence is bound in , , , . Moreover, that same occurrence is bound in 
and 
as well, for any choice of variable y.In any formula of the form
or (where y can be any variable at all in this case) the occurrence of y that immediately follows the initial quantifier symbol is bound.If an occurrence of a variable x is free in
, then that same occurrence is free in and , for any variable y distinct from x. On the other hand, all occurrences of x that are free in , are bound in 
and in 
.
If a formula contains no occurrences of free variables we call it a sentence .