[FOM] Predicative Set Theory
Zuhair Abdul Ghafoor Al-Johar
zaljohar at yahoo.com
Sun Jun 24 04:09:32 EDT 2012
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.
Nik Weaver wrote:
The separation scheme is impredicative. It affirms the existence of
sets which are defined by formulas which quantify over all sets.
More information about the FOM