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?)
who would want to do constructive mathematics? :-)
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
Josef