 The concepts of a free and bound occurrence of a variable in a formula are defined in the usual way. A formula is called a sentence if it has no free variables. The concept of a term being free for a variable in a formula is defined as in first order logic.