Do you "belive" in the axiom of choice?
I think we can get an ice cream with infinite flavors. xD
No but I believe that every vector space has a basis.
Doesn't axiom of choice only give you that every basis has the same dimension (i.e. without AoC you get that it's possible to give some vector spaces multiple basis with different dimension)?
Does it bother you that a unique dimension is obviously not the case with topological basis for topologies?
More than that, it lets you declare that every vector space actually has a basis. In cases such as R considered as a vector space over Q, this is the only way of saying that there's a basis at all.
Field extensions are vector spaces. It's easy to give an infinite independent set of Q-vectors in R (roots of primes, powers of pi...) but you can't give an actual base without the AoC of course.
I only believe in the Univalence axiom.
I'm not trolling when I say that WOP is fucking retarded and anyone that believes in the Axiom of Choice is saying "Banach-Tarski makes more sense to me than the idea that we can't just assume a choice function exists for every set just because that would be useful."
The definition isn't abused. Pretty much all the stupid paradoxical shit in mathematics is either based on the Axiom of Choice or comes from naive set theory and the idea that all collections of elements are sets.
>What bothers me more is how sets are defined, and the definition is abused.
sets are not defined in set theory. but then, set theory is formalizes what people who formalize desire to do with sets. you can invent your won set theory if you do not share their visions of manipulations of sets.
>le Banach Tarski "paradox" is too unintuitive
Holy fuck, kill yourselves if this is all you can spout.
I think Axiom of Regularity is a much more interesting thing. After all, you can prove that sets don't contain themselves with it, which is much more "natural" result than some of the implications of the axiom of choice (though well ordering is a really nice thing to have)
Basically, if they weren't you would have square roots of different primes generating the same extension of Q. You could then argue (say by the use of discriminants) that this isn't possible.
What I like about Regularity is that even if a model satisfies it, there may still be an infinite descending chain [math] x_0 \ni x_1 \ni x_2 \ni \ldots [/math] -- it is only that such a chain cannot be definable.
I mean we had this thread about 6 weeks ago with lots of answers - I'm not gonna rewrite my same answer here again (too bad the archive is down).
Do you guys have any feel for what a computation/constuctive interpretation for a term of the Univalence axiom type (I think that's what they are looking for, if I understand correction) could even look like?