A class of formulas
closed under bounded quantification
if for any
where is some bound depending on the Language
In set theory, it means exactly .
In Peano Arithmetic it could mean
Lemma
Let
Suppose
Then
Proof
Let
(otherwise we can’t quantify over
By definition, we have for any
where
Let
Suppose
Then for some
and by assumption
Suppose
Then pick an
As
it has to be that
Hence we are done as
which works for any
Similar to
Similar to