|
|
Rupert wrote:
> 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.
>
Yes, Zermelo set theory is a stronger theory than TST, and I never said
anything contrary to that. I said that TST is equivalent to Zermelo
set theory with the seperation scheme restricted to formulas that use
only bounded quantifiers. I believe you cut off my sentence by
accident.
> > 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.
>
I know that NF is different from both Zermelo set theory and TST.
Rather, NF is equivalent to TST plus an axiom scheme which asserts that
every formula phi is equivalent to phi+, which raises 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.
>
> I'm not sure I understand the relation between NF and simple type
> theory which you're asserting.
Yes, I do. I apologize if I did not express myself very clearly.
|
|