A class of formulas in a Language is
closed under bounded quantification
if for any :

Lemma

Let be a Transitive Model of .
Suppose is Absolute for .
Then and are Absolute for .

Proof

Let have Free Variables, one of which is
(otherwise we can’t quantify over )
By definition, we have for any

where is a Model of
Let .

Suppose

Then for some we have

and by assumption

is a Substructure of so (in ) and thus

Suppose

Then pick an such that and .
As by assumption, and is Transitive,
it has to be that and thus .
Hence we are done as

which works for any in

Similar to .

Similar to .