On Mon, 7 Jan 2008, Josef Urban wrote:
On Mon, 7 Jan 2008, Freek Wiedijk wrote:Personally I always worry about the choice operator, which is implicitly present in Mizar. I like foundations that don't have that, but then how do you translate your formal mathematics that implicitly is built on it?The Axioms of Choice is a theorem in TG.I wasn't talking about AC. (Who would want to do mathematics without AC?)I was talking about a choice _operator._ So a functor that given a non empty set gives you an element of that set.I vaguely remember hearing from various sources (I think last time from Bob Solovay) that the difference between choice and strong choice is not a big deal
There are two relevant results here:1) There is a model of GB in which the set form of AC holds but there is no class which gives a functor taking a non-empty set to an element of that set.
2) Suppose we consider the following extension of ZFC: a) There is a new function symbol F;b) We add the new instances of Replacement and selection schema in which F appears;
c) We add an axiom saying that if x is not empty, then F(x) is a member of x.
This theory is a conservative extension of ZFC. That is, if a sentence of the new theory in which F does not appear is a theorem of the new theory, then it is already a theorem of ZFC.
--Bob Solovay