On Jul 2, 4:12 pm, "Ross A. Finlayson" <ross.finlay...@gmail.com> wrote: > On Jul 2, 9:28 am, MoeBlee <jazzm...@hotmail.com> wrote: > > > On Jul 2, 12:06 am, "Ross A. Finlayson" <ross.finlay...@gmail.com> > > wrote: > > > > countable choice is a theorem of ZF. > > > No, it's not.
> The definition of countable is there existing a bijective function > between some set and the natural integers or here their ordinals.
A definition of countable is ['w' stands for the set of natural numbers]:
x is countable iff (there exists a bijection from x onto a natural number of there exists a bijection from x onto w)
> A > choice function is representable by any such function bijecting an > ordinal as a set to a set.
I have no idea what you're trying to say.
['P' stands for the power set operation:]
A choice function for x is a function f whose domain is Px\{0} and such that for all y in Px\{0}, we have f(y) in y.
I guess sometimes people also refer to a choice function for x as being a function whose domain is x\{0} and such that for all y in x \{0} we have f(y) in y.
Context should make clear which sense is intended.
> Then, where countable choice means there > are choice functions for countable sets,
The axiom of countable choice is:
For all x such that 0 is not in x, there exists a function f whose domain is x and such that for all y in x we have f(y) in y.
Since finite sets are not at issue anyway, we can narrow:
For all x such that x is denumerable, there exists a function f whose domain is x\{0} and such that for all y in x\{0} we have f(y) in y.
> otherwise there are > "countable" sets with no provable bijection to the naturals,
You don't know what you're talking about. We don't require any choice principles just to prove that there exists a bijection between a countable set and either a natural number or the set of natural numbers. The result follows simply by the DEFINITION of 'countable'.
> where if > that's undecideable then so is whether they're countable, not > disproving the definition.
Get help. Start with a book on working in the first order predicate calculus.
