Re: Small Set theory:Revised.


zuhair schrieb:

-Small Set Theory-


Primitive e


Definition:


x is P_defined <-> Ay( yex<-> (~y=x & P[y]) )


x is P_embedded<-> Ay( yex<-> (~y=x & P[y]) )&P[x].


x is P_unembedded<-> Ay( yex<-> (~y=x & P[y]) )&~P[x].


Axioms:


Ax.1: Extensionality: AxAy(y=x <-> Az(zex<->zey) )
Ax.2: Comprehension:ExAy( yex<-> (~y=x & P[y]) )
Ax.3: Exclusion:AxAy( (yex & y is P_defined)-> ~P[x] )
Ax.4: Infinity: EN Ax ({}eN /\(xeN->S(x)eN) , were S(x)=xU{x}.
Pluse\minus.
Ax.5: Axiom of choice. As in ZFC.


Theorums.

1) Universe: Ev Ay ( yev ).
How to prove this? I would suspect one should use Ax.2 with P suitably
chosen
such that ~y=v & P[y] is true for all y.
But for y=v, this is false.

2) Pairing:
AaAbExAy( (yex<->(~y=x&(y=a v y=b)))&( (a is P_defined v b is
P_defined) -> ~P[x]) ).
.... and x is uniquely determined, given a and b?
.... and shall henceforth be denoted as {a,b} ?
I see no proof of this (at least not in the useful form with
uniqueness).
But at least we have singletons - sometimes:
Let a be a set that is not empty.
Let P[z] := z=a.
Then by Ax.2 there exists (at least one) set b such that
yeb <-> (~y=b & y=a)
Well, the set b may either be equal to a or not.
If b=a, then the right hand side is false, hence b is empty and so is
a.
But a was chosen not empty - contradiction.
Hence ~b=a.
Therefore, we conclude aeb (because ~a=b & a=a holds)
For any other set, i.e. for y with ~y=a, we have ~yeb.
So, yes, we can define singletons for non-empty sets.
Let's write {a} for this singleton.

What about {0} where 0 is the empty set? (BTW, 0 exists by taking ~y=y
in Ax.2 and is uniquely determined by Ax.1.)
Using P[z] := z=0 like above, we obtain by Ax.2 that there exists (at
least one) set b such that
yeb <-> (~y=b & y=0)
But this is already true for b=0. Hence the existence of {0} is not
guaranteed.
Which is a pity, not only per se, but also because Ax.4 relies on its
existence.
I might accept that, when expanded to a suitable level of explicitness,
Ax.4 also states the existence of S(x) for all x in N, esp. S(0).

Now about pairing:
The first guess would be:
From Ax.2 with P[z] := z=a v z=b, one gets the existence of a set x
such that
yex <-> (~y=x & (y=a v y=b))
The rest of the statement is probably expected to be an application of
Ax.3 to this set.
However, if a=any non-empty set, and b={a} (as defined above), then we
have ~(b=a) (see above), then x=b has the property
yex <-> y=b
<-> ~y=a & y=b
<-> ~y=a & (y=a v y=b)
Hence, what you would like to define as {a,{a}} in usual notation looks
more like {a}.

If you have a proof that {a,{a}} exists, please provide it.

3) Union:
AzExAy((yex<->(~y=x&(Eu:yeu&uez)))&(y is P_defined ->~P[x])).
and x is called the union set of z , i.e. x=Uz.

4) Separation: AzExAy (yex <->(~y=x&(yez&P1(y)))&(y is P_defined
->~P[x]))

5) Replacement: (AuE!y:P(u,y))->AzExAy:yex<->(Euez: P(u,y)&~y=x) & ( y
is P_defined ->~P[x]).

6) Power: AzExAy (yex<->((Au:uey -> uez)&~y=x)& ( y is P_defined ->
~P[x])).

I won't talk about these remaining claims since the lack of general
pairing
makes most other stuff useless.

The essence of this theory is that for y to be a member of x it should
fulfill three requirements;

1) y!=x
2) P[y]
3) if P[x] , then y cannot be P_defined.

to explain 3)there cannot be a set z such that P[z] holds, and that
have x as a member were x is P_defined. weather x is P_embedded or x is
P_unembedded.

Example: The set of all set bijectable to 2, here for P <-> bijection
to 2.
if that set is x, then x can't be a member of a set z that has two
elements, since by then z will have P, violating 2.

This set theory has a universe, has emedded sets like the set of all
ordinals, the set of all sets not bijectable to 2, etc....

It doesn't have the restriction of proper classes.

If this theory is consistent it should be something more than ZFC,
because it has all the applications of ZFC, and extra-theorums and
models.

Now I have a question, should I add an axiom stating that for every set
there is a P that defines it.

How would you proof ~xex without it?
If one wants to use Ax.3 to show that ~xex, one needs that x is
P_embedded (shudder).
But at least You would get rid of the universe by Axiom 0...

.

Relevant Pages

  • Re: Small Set theory:Revised.
    ... Ax.5: Axiom of choice. ... Universe: Ev Ay. ... Let a be a set that is not empty. ... If this theory is consistent it should be something more than ZFC, ...
    (sci.math)
  • Re: For All x
    ... the existence of any 'object' any less than ZFC ... Meanwhile, since your theory is weaker than ZFC, ... Pure unsupported assertion. ... taking as an axiom for the META-theory. ...
    (sci.logic)
  • Re: Small Set theory:Revised.
    ... Ax.5: Axiom of choice. ... Universe: Ev Ay. ... Let a be a set that is not empty. ... If this theory is consistent it should be something more than ZFC, ...
    (sci.math)
  • Re: Small Set theory:Revised.
    ... Ax.5: Axiom of choice. ... Universe: Ev Ay. ... Let a be a set that is not empty. ... If this theory is consistent it should be something more than ZFC, ...
    (sci.math)
  • Re: Small Set theory:Revised.
    ... Ax.5: Axiom of choice. ... Universe: Ev Ay. ... Hence the existence of is not ... If this theory is consistent it should be something more than ZFC, ...
    (sci.math)