Let be a Language.
We define the following

is the smallest class of formulae which

A formula is if it is of the form

for

A formula is if it is of the form

for

A formula is if it is both and .

Definition

If is any Theory, and a class of formulae,
define to be the class of formulas that are equivalent in
to a formula in .

Theorem

formulas are Absolute for Transitive Models of .

Proof

By induction on the formula complexity in we prove the statement for .
Note that the Transitiveness comes into play
when dealing with bounded quantifiers.
It is then straightforward to extend the statement for .

Corollary

formulas are Upwards Absolute for Transitive Models of ,
while are Downwards Absolute.

Corollary

formulas are Absolute for Transitive Models of .