🚀 go-pugleaf

In article <1992Nov09.172532.43648@Cookie.secapl.com> frank@Cookie.secapl.com (Frank Adams) writes:
>In article <25916@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>>No, I am not complaining about elementhood being a proposition, I am
>>complaining about a syntactic circularity begin treated as though it
>>had semantic significance.  Neither am I concerned about the
>>unrestricted range of the quantification.  As the set {x : x = x}
>>clearly shows, there is no inconsistency inherent in either
>>self-membership or impredicativity.  I claim that {x : x = x} is a
>>perfectly reasonable set and that the mere fact that ZF proves the
>>opposite is enough to show that ZF is not an adequate axiomatization
>>of set theory.
>
>All right; but what would you put in it's place?  I'm not willing to call
>something "set theory" unless it has *some* recognizable form of the axiom
>of comprehension.  Can you formalize your ideas?

i.  Russell's paradox does have _semantic_ consequences.  Whatever
membership is, there is no set of all sets that are not members of
themselves.  Certainly the mechanics of applying the paradox are
syntactical -- so what?

ii.  NFU:

	Axiom 1.  Objects with elements that have the same elements
	are equal.  (this allows multiple objects with no elements).

	Axiom 2.  Stratified comprehension (any instance of
comprehension which would make sense in the simple theory of types
under some assignment of types to its variables holds -- further
details available on request).

	Axiom 3.  The universe is infinite.

	Axiom 4.  The universe can be well-ordered (choice).

	This is a set theory with the same consistency strength as
Russell's theory of types; it is untyped (a set definition makes sense
if it would make sense in the theory of types, but objects in this
theory are not typed).  {x|x=x}, the universe, exists (the definition
would make sense in TT); {x|~x E x}, the Russell class does not exist
(the definition would not make sense in TT -- if the first x had type
n, the second would have type n+1).

	This theory is known to be consistent (R. B. Jensen, On the
consistency of a slight (?) variation of Quine's New Foundations,
Synthese, vol. 19), and adequate for most mathematical purposes.  It
-- 
The opinions expressed		|     --Sincerely,
above are not the "official"	|     M. Randall Holmes
opinions of any person		|     Math. Dept., Boise State Univ.
or institution.			|     holmes@opal.idbsu.edu