Let
We define the following
is the smallest class of formulae which
- contains all atomic formulae
- Closed Under Bounded Quantification
- Closed under
, , ,
A formula is
for
A formula is
for
A formula is
Definition
If
define
to a formula in
Theorem
Proof
By induction on the formula complexity in
Note that the Transitiveness comes into play
when dealing with bounded quantifiers.
It is then straightforward to extend the statement for
Corollary
while