I tend to agree with the idea that AC is rather unfairly described as ‘to be rejected’, especially Banach-Tarski. We are no strangers to strange things in mathematics, especially with infinity, so I don’t really understand the argumentative structure: it’s strange, then I don’t know what to conclude from that. It’s no stranger than many other things, it seems to me : such as the fact that there are as many even integers as there are integers, or that there are as many real numbers between 0 and 1 as there are real numbers. There are many strange things. Also, with “the argument of strange things”, we come back to rejecting the axiom of infinity, rather, I would say ?
But for me, that’s not the heart of the problem: An axiom is often seen, wrongly (in my opinion), as something that we posit, or don’t posit, or posit the opposite of, and then we work within that framework. This is not entirely wrong, but it is the point of view that seems to me to be erroneous as a point of view: We do not state that ‘groups are now Abelian’; no, we are going to study Abelian groups if we want to, but we do not forget that non-Abelian groups exist nonetheless; we have not ‘stated’ Abelianity, we are simply going to look at this specific type of object. Similarly, we do not ‘assume’ that the ring is commutative; at best, we say that we will only consider commutative rings in the rest of the text (book, course, etc.). In short, an axiom is not there to be assumed or not; it is there to describe a type of object, in my opinion.
So here, it is not a question of ‘postulating’ whether or not the ZF-universe verifies AC, but rather of seeing whether in our work it is more practical to work with ZF-universes that verify AC or whether we do not need to restrict ourselves to those that verify AC in order to work, and thus produce a more general result on ZF-universes; but potentially more costly to prove because it requires more generality. Or even to specify results on ZF-universes that do not verify AC, even if they are potentially less frequent.
So really seeing ZF-universes as objects, and not as somewhat transcendent entities, etc.
I think I basically agree that this is how one should consider this.
But I think there is a reasonable defence of the “ZF-universe as somewhat transcendent entities” and that is that we do virtually all of our actual maths in ZF-universes, by saying that ultimately we will be able to appeal to ZF-axioms. This makes ZF-objects pretty different from groups. E.g. I think there’s a pretty tight analogy between forcing in ZF and galois extensions (just forcing is much more complicated), but the consequences of forcing for how we do the rest of maths can be somewhat deep (e.g. CH is doomed in ZFC, consequences about Turing computability, etc). So the mystical reputation is somewhat deserved. Woodin would defend some much more complicated and involved version of this as I discussed in my post about the constructible universe.
But I agree ultimately, with our current understanding of ZF-universes that they are just another mathematical object, they just happen to be an object that we use to do other maths with, and we can step outside those objects these days with large cardinal axioms, if we’d like, and analyze other consequences of them. It’s pretty similar to how we started viewing logic and logics after Gödel’s results (i.e. clearly first-order logic is very useful because of compactness/completeness, but that doesn’t mean “Second order logic is wrong.”)
I tend to agree with the idea that AC is rather unfairly described as ‘to be rejected’, especially Banach-Tarski.
We are no strangers to strange things in mathematics, especially with infinity, so I don’t really understand the argumentative structure: it’s strange, then I don’t know what to conclude from that.
It’s no stranger than many other things, it seems to me : such as the fact that there are as many even integers as there are integers, or that there are as many real numbers between 0 and 1 as there are real numbers.
There are many strange things.
Also, with “the argument of strange things”, we come back to rejecting the axiom of infinity, rather, I would say ?
But for me, that’s not the heart of the problem:
An axiom is often seen, wrongly (in my opinion), as something that we posit, or don’t posit, or posit the opposite of, and then we work within that framework.
This is not entirely wrong, but it is the point of view that seems to me to be erroneous as a point of view:
We do not state that ‘groups are now Abelian’; no, we are going to study Abelian groups if we want to, but we do not forget that non-Abelian groups exist nonetheless; we have not ‘stated’ Abelianity, we are simply going to look at this specific type of object.
Similarly, we do not ‘assume’ that the ring is commutative; at best, we say that we will only consider commutative rings in the rest of the text (book, course, etc.).
In short, an axiom is not there to be assumed or not; it is there to describe a type of object, in my opinion.
So here, it is not a question of ‘postulating’ whether or not the ZF-universe verifies AC, but rather of seeing whether in our work it is more practical to work with ZF-universes that verify AC or whether we do not need to restrict ourselves to those that verify AC in order to work, and thus produce a more general result on ZF-universes; but potentially more costly to prove because it requires more generality.
Or even to specify results on ZF-universes that do not verify AC, even if they are potentially less frequent.
So really seeing ZF-universes as objects, and not as somewhat transcendent entities, etc.
I think I basically agree that this is how one should consider this.
But I think there is a reasonable defence of the “ZF-universe as somewhat transcendent entities” and that is that we do virtually all of our actual maths in ZF-universes, by saying that ultimately we will be able to appeal to ZF-axioms. This makes ZF-objects pretty different from groups. E.g. I think there’s a pretty tight analogy between forcing in ZF and galois extensions (just forcing is much more complicated), but the consequences of forcing for how we do the rest of maths can be somewhat deep (e.g. CH is doomed in ZFC, consequences about Turing computability, etc). So the mystical reputation is somewhat deserved. Woodin would defend some much more complicated and involved version of this as I discussed in my post about the constructible universe.
But I agree ultimately, with our current understanding of ZF-universes that they are just another mathematical object, they just happen to be an object that we use to do other maths with, and we can step outside those objects these days with large cardinal axioms, if we’d like, and analyze other consequences of them. It’s pretty similar to how we started viewing logic and logics after Gödel’s results (i.e. clearly first-order logic is very useful because of compactness/completeness, but that doesn’t mean “Second order logic is wrong.”)