|
|
The simple theory of types, or TST, is a set theory equivalent to
Zermelo set theory with seperation restricted to formulas with bounded
quantification which assigns sets natural numbers called types. A set
x can only be an element of a set y if y is one type higher than x.
The first axiom is the same axiom of extensionality that the usual set
theory has. The second axiom is a comprehension schema which defines a
set y of type n+1 for every formula phi(x), where x is of type n.
Quine's New Foundations, or NF, is a set theory in which the types are
dropped from variables. In other words, in NF there is extensionality
and a comprehension schema which assigns a set to every formula phi,
where all the variables in phi can be consistently assigned types.
What this means in effect is that NF is equivalent to TST plus a
typical ambiguity scheme which states that every formula phi is
equivalent to the corresponding formula phi+ which results from raising
the the types of all the variables in phi by 1.
In the standard set theory of ZFC, something similar to the types in
TST is done. Instead of types, sets in the cumulative hierarchy are
assigned ranks, which may be transfinite ordinals. My question is, is
there a set theory which is to ZFC as NF is to TST? That is, can you
add a typical ambiguity scheme to ZFC which states that every wff phi
is equivalent to the corresponding formula phi+ which results from
increasing the ranks of all the variables in phi by 1? Is the
resultant theory consistent? Is it perhaps equiconsistent with some
large cardinal axiom?
Any help would be greatly appreciated.
Thank You in Advance.
|
|