[FOM] Predicative Set Theory

[Zuhair Abdul Ghafoor Al-Johar]

Dear N. Weaver:

Separation scheme here defines new subsets as we go up, this leads to the production 
of different power sets say of N for example, however non of those powers contain all 
subsets of N, each power contains all definable subsets of N up to the respective level, 
we cannot prove the uncountability of any of them and externally the theory have one 
model that is well founded, countable and transitive. It is indeed not strictly predicative,
for that we may need typing or the use of bounded formulas. I'm not sure now how this 
theory compares to the spectrum of finitary theories, I thought it would be equiconsistent
to a subset of second order arithmetic because we never retain the full power of N here 
despite the existence of a spectrum of powers for N. I think if we further restrict it using only
bounded formulas then we'd be working below the full strength of second order arithmetic.
I'm not sure if this is enough to render it predicative though, however a typed approach 
would secure that.

Thanks

Zuhair Al-Johar



 Nik Weaver wrote:

The separation scheme is impredicative.  It affirms the existence of
sets which are defined by formulas which quantify over all sets.