Re: Uncountable sets in CZF?

From: David McAnally (D.McAnally_at_i'm_a_gnu.uq.net.au)
Date: 09/04/04 

Date: 4 Sep 2004 16:34:37 GMT

D.McAnally@i'm_a_gnu.uq.net.au (David McAnally) writes:

>raf@tiki-lounge.com (Ross A. Finlayson) writes:

><snip>

>>By "plain set theory" I meant theory where the only primary objects
>>were sets as opposed to a theory where numbers are primary objects.

>ZF and ZFC are therefore what you call "plain set theories". In ZF and
>ZFC, numbers are defined AS SETS. I wonder where you got the erroneous
>idea that numbers were primary objects in ZF and ZFC???

>A natural number is defined to be either the empty set or a successor
>ordinal whose elements are all either empty or successor ordinals, a
>set n is a natural number if

>n is empty or [n is a successor ordinal and for all m in n (m is empty
>or m is a successor ordinal)].

>Equivalently, a natural number is an element of the smallest limit
>ordinal.

Equivalently, a natural number is an element of the unique smallest
inductive set, where a set x is called inductive if the empty set is an
element of x and for all y in x exists z in x for all t (t in z iff
(t in y or t = y)).

Sufficient axioms for ZF are:

(1) exists x (x in x) - this asserts the existence of at least one set,
    so it can be called the Axiom of Existence;

(2) for all x for all y (for all z (z in x <=> z in y) => x = y);

(3) for all x exists y for all z (exists t (z in t and t in x) => z in y);

(4) for all x exists y for all z (for all t (t in z => t in x) => z in y);

(5) for any formula , P(u,v), in ZF, and for arbitrary values for all
free variables in P(u,v), except for u and v,

    for all u for all v for all w ((P(u,v) and P(u,w)) => v = w) =>
    for all x exists y for all v (v in y <=> exists u (u in x and P(u,v)));

(6) exists x (empty set in x and for all y in x exists z in x for all t
    (t in z <=> (t in y or t = y))) - Axioms 1 and 5 guarantee the
    existence of an empty set, and Axiom 2 guarantees its uniqueness;

(7) for all x (exists y (y in x) => exists y in x for all z not (z in x
    and z in y)).

For ZFC, this is augmented by another Axiom:

(8) for all x ([exists y (y in x) and for all y in x [exists t (t in y)
    and for all z in x (y = z or for all t not (t in y and t in z))]]
    => exists u for all y in x exists v for all t ((t in y and t in u)
    <=> t = v)).

David

-----

Relevant Pages
Loading