In mathematical logic (in fact, in predicate logic):

A variable in a formula (more specifically in a well-formed formula) of a logical language is called free if there is some occurrence of it in the formula that is not within the scope of a quantifier that mentions it.

A variable that is not free is a bound variable.

The two logical quantifiers are the existential and the universal . The scope of them is how far the (explicit or implicit) bracketing following them extends. And by "that mentions it" I mean that the quantifier quantifies one particular variable, and can only bind that one variable.

Examples:

x (x is a hyena)
-- the quantifier covers everything in the brackets
-- it mentions x first (it governs x), then x occurs again within its scope
-- so x is not free

x (y is a hyena)
-- y is not mentioned with the quantifier
-- so y is free

x (x and y are hyenas)
-- x is bound but y is free

(∀ x (x and y are hyenas)) & (x laughs a lot)
-- tricky
-- x is bound within a substring of the formula, but its final occurrence is not covered by the scope of the ∀, so overall x is free in this formula.

The last one illustrates the difference between a variable and an instance of a variable. One instance of the variable is bound and the other is free. The variable itself (x) is free, because at least one instance of it is.

Likewise, in a set of formulae, a variable is said to be free if it is free in any one (or more) of the formulae.

The existence of free variables in a formula means that truth values can not yet be assigned. The truth of the formula is a function of the truth values of its free variables.

In propositional logic, the freedom of variables is determined as follows. If x is free in a proposition A then it is free in ¬A. If it is free in either A or B then it is free in AB. And if it is free in A it is free in ∀y (A) iff x and y are different variables. All other propositional connectives can be constructed from these three, so this is exhaustive.