Just as with propositional logic, one can define a proof system for first order logic. We first need two definitions.
Definition 1 If 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 2 Let 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