|
|
lugita15@xxxxxxxxx wrote:
> The simple theory of types, or TST, is a set theory equivalent to
> Zermelo set theory
That's actually not quite true. In simple type theory, the types are
indexed by the natural numbers. In Zermelo set theory, there are a
hierarchy of levels which are indexed by the ordinal numbers up to
omega times two, and it may go beyond, it's just that you can't prove
that it does. Zermelo set theory can prove the consistency or the
arithmetical soundness of the deductive closure of the Peano axioms in
simple type theory. So it is a stronger 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.
>
I haven't studied NF in detail, but I think you'll find it's quite
different both to Zermelo set theory and the simple theory of types.
Its consistency is an open problem, for example.
> 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.
I'm not sure I understand the relation between NF and simple type
theory which you're asserting.
|
|