1. Preliminaries
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
![]()