Formal Logic/Predicate Logic/Free and Bound Variables

From Wikibooks, open books for an open world
Jump to: navigation, search
← Formal Syntax ↑ Predicate Logic Informal Conventions →



Free and Bound Variables[edit]

Informal notions[edit]

The two English sentences,

If Socrates is a person, then Socrates is mortal,
if Aristotle is a person, then Aristotle is mortal,

are both true. However, outside any context supplying a reference for 'it',

(1)    If it is a person, then it is mortal,

is neither true nor false. 'It' is not a name, but rather an empty placeholder. 'It' can refer to an object by picking up its reference from the surrounding context. But without such context, there is no reference and no truth or falsity. The same applies to the variable 'x' in

(2)    If x is a person, then x is mortal.

This situation changes with the two sentences:

(3)    For any object, if it is a person, then it is mortal,
(4)    For any object x, if x is a person, then x is mortal.

Neither the occurrences of 'it' nor the occurrences of 'x' in these sentences refer to specific objects as with 'Socrates' or 'Aristotle'. But (3) and (4) are nonetheless true. (3) is true if and only if:

(5)    Replacing both occurrences of 'it' in (3) with a reference to any object whatsoever (the same object both times) yields a true result.

But (5) is true and so is (3). Similarly, (4) is true if and only if:

(6)    Replacing both occurrences of 'x' in (4) with a reference to any object whatsoever (the same object both times) yields a true result.

But (3) is true and so is (4). We can call the occurrences of 'it' in (1) free and the occurrences of 'it' in (3) bound. Indeed, the occurrences of 'it' in (3) are bound by the phrase 'for any'. Similarly, the occurrences 'x' in (2) are free while those in (4) are bound. Indeed, the occurrences of 'x' in (4) are bound by the phrase 'for any'.

Formal definitions[edit]

An occurrence of a variable \alpha\,\! is bound in \varphi\,\! if that occurrence of \alpha\,\! stands within a subformula of \varphi\,\! having one of the two forms:

\forall \alpha\, \psi\ ,\,\!
\exists \alpha\, \psi\ .\,\!

Consider the formula

(7) \quad (\exists x_0\, \mathrm{F^1_0}(x_0) \rightarrow \forall y_0\, \mathrm{F^1_0}(y_0))\ .\,\!

Both instances of x_0\,\! are bound in (7) because they stand within the subformula

\exists x_0\, \mathrm{F^1_0}(x_0)\ .\,\!

Similarly, both instances of y_0\,\! are bound in (7) because they stand within the subformula

\forall y_0\, \mathrm{F^1_0}(y_0)\ .\,\!


An occurrence of a variable \alpha\,\! is free in \varphi\,\! if and only if \alpha\,\! is not bound in \varphi\,\!. The occurrences of both x_0\,\! and y_0\,\! in

(8) \quad (\mathrm{F^1_0}(x_0) \rightarrow \mathrm{G^1_0}(y_0))\,\!

are free in (8) because neither is bound in (8).


We say that an occurrence of a variable \alpha\,\! is bound in by a particular occurrence of \forall\,\! if that occurrence is also the first (and perhaps only) symbol in the shortest subformula of \varphi\,\! having the form

\forall \alpha\, \psi\ .\,\!

Consider the formula

(9) \quad \forall x_0\, (\mathrm{F^1_0}(x_0) \rightarrow \forall x_0\, \mathrm{G^1_0}(x_0))\ .\,\!

The third and fourth occurrences of x_0\,\! in (9) are bound by the second occurrence of \forall\,\! in (9). However, they are not bound by the first occurrence of \forall\,\! in (9). The occurrence of

(10) \quad \forall x_0\, \mathrm{G^1_0}(x_0)\,\!

in (9)—as well as the occurrence of (9) itself in (9)—are subformulae of (9) beginning with a quantifier. That is, both are subformula of (9) having the form

\forall \alpha\, \psi\ .\,\!

Both contain the second third and fourth occurrences of x_0\,\! in (9). However, the occurrence of (10) in (9) is the shortest subformula of (9) that meets these conditions. That is, the occurrence of (10) in (9) is the shortest subformula of (9) that both (i) has this form and (ii) contains the third and fourth occurrences of x_0\,\! in (9). Thus it is the second, not the first, occurrence of \forall\,\! in (9) that binds the third and forth occurrences of x_0\,\! in (9). The first occurrence of \forall\,\! in (9) does, however, bind the first two occurrences of x_0\,\! in (9).


We also say that an occurrence of a variable \alpha\,\! is bound in by a particular occurrence of \exists\,\! if that occurrence is also the first (and perhaps only) symbol in the shortest subformula of \varphi\,\! having the form

\exists \alpha\, \psi\ .\,\!


Finally, we say that a variable \alpha\,\! (not a particular occurrence of it) is bound (or free) in a formula if the formula contains a bound (or free) occurrence of \alpha\,\!. Thus x_0\,\! is both bound and free in

(\forall x_0\, \mathrm{F^1_0}(x_0) \rightarrow \mathrm{F^1_0}(x_0))\,\!

since this formula contains both bound and free occurrences of x_0\,\!. In particular, the first two occurrences of x_0\,\! are bound and the last is free.

Sentences and formulae[edit]

A sentence is a formula with no free variables. Sentential logic had no variables at all, so all formulae of \mathcal{L_S}\,\! are also sentences of \mathcal{L_S}\,\!. In predicate logic and its language \mathcal{L_P}\,\!, however, we have formulae that are not sentences. All of (7), (8), (9), and (10) above are formulae. Of these, only (7), (9), and (10) are sentences. (8) is not a sentence because it contains free variables. exception Err

datatype ty
  = IntTy
  | BoolTy
datatype exp
  = True
  | False
  | Int of int
  | Not of exp
  | Add of exp * exp
  | If of exp * exp * exp
fun typeOf (True) = BoolTy
  | typeOf (False) = BoolTy
   | typeOf (Int _) = IntTy
   | typeOf (Not e) = if typeOf e = BoolTy then BoolTy else raise Err
  | typeOf (Add (e1, e2)) = 
      if (typeOf e1 = IntTy) andalso (typeOf e2 = IntTy) then IntTy else raise Err
  | typeOf (If (e1, e2, e3)) = 
      if typeOf e1 <> BoolTy then raise Err
      else if typeOf e2 <> typeOf e3 then raise Err
      else typeOf e2

Examples[edit]

All occurrences of x_0\,\! in

(11) \quad \forall x_0 (\mathrm{F^1_0}(x_0) \rightarrow  \mathrm{G^2_0}(x_0, y_0))\,\!

are bound in the formula. The lone occurrence of y_0\,\! is free in the formula. (11) is a formula but not a sentence.

Only the first two occurrences of x_0\,\! in

(12) \quad (\forall x_0 \mathrm{F^1_0}(x_0) \rightarrow  \mathrm{G^2_0}(x_0, y_0))\,\!

are bound in the formula. The last occurrence of x_0\,\! and the lone occurrence of y_0\,\! in the formula are free in the formula. (12) is a formula but not a sentence.

All four occurrences of x_0\,\! in

(13) \quad (\forall x_0 \mathrm{F^1_0}(x_0) \rightarrow  \exists x_0 \mathrm{G^2_0}(x_0, y_0))\,\!

are bound. The first two are bound by the universal quantifier, the last two are bound by the existential quantifier. The lone occurrence of y_0\,\! in the formula is free. (13) is a formula but not a sentence.

All three occurrences of x_0\,\! in

(14) \quad \forall x_0 (\mathrm{F^1_0}(x_0) \rightarrow  \exists y_0 \mathrm{G^2_0}(x_0, y_0))\,\!

are bound by the universal quantifier. Both occurrences of y_0\,\! in the formula are bound by the existential quantifier. (14) has no free variables and so is a sentence and as well as a formula.