**1. Preliminaries **

Just as with propositional logic, one can define a proof system for first order logic. We first need two definitions.

Definition 1If is a formula, a generalization of is any formula of the form

(We are not requiring in the definition above that the are different or that they are present in )

Definition 2Let be a term, let be a variable, and let be a formula. We say that is substitutable for in iff no free occurrence of in is within the scope of a quantifier or with a variable occurring in