4 ms·

I just want to mention that there is a much deeper discussion to be had about the axiom of choice than the apparent impossibility of Banach Tarski, and it has t

I just want to mention that there is a much deeper discussion to be had about the axiom of choice than the apparent impossibility of Banach Tarski, and it has to do with equality. In mathematics is is common to change the equality between sets (form quotient sets). For example, the set of real numbers are infinite sequences of rational numbers (fractions) which approximate the value. But the equality which we place on this set is not the equality of sequences, which is too strict. We put a new equality on these real numbers which identify two of them iff they come arbitrarily close to each other. The axiom of choice (AC) says that if for a ∈ A there is b ∈ B satisfying some requirement, then there is a function A → B selecting these elements. The axiom of choice is only problematic if we require that choice function it produces respects some quotient equality we placed on A and B. The confusion arise because ZF Set Theory cannot express the weaker notion of a function which does not express the quotient equality. Other foundations, such as Martin-Löf Type Theory, can express this difference and you get AC without the paradoxes.

JoshTriplett 11y ago
What's the disadvantage of those other foundations that makes them unsuitable for universal use?
- black_knight 11y ago
  Of course the proponents of these other foundations claim that they are suitable for universal use. But sets came first, and is good enough for most purposes, and mathematicians in general are more concerned with mathematics than foundations. Actually the recent movement of "Homotopy Type Theory" is gaining some traction among non-logicians, giving easier formulations and proofs in category theory and topology. Also in computer science type theory is becoming more usual, since all results are constructive (provides algorithms) and is in fact a programming language in it self.
- tel 11y ago
  They're certainly not unsuitable, but they have a tendency to take observation/realization/grasping/proving as an instantaneous process. In most people's regular understanding of logic, however, this is false. There is a process by which new data and new conclusions from that data are drawn and made available to you. So ultimately, if those things matter for either UX of mathematics or for actual mathematical content is a large question, but it's fairly clear that if you need to capture something closer to the actual dynamics of knowledge/learning/understanding then you are sunk when you base your foundations in set theory.
auggierose 11y ago
I don't think there is any confusion here. Of course ZF set theory can express this weaker notion. But in ZF these different functions have different domains and ranges A, A mod r, B, B mod r, where r is the equivalence relation. In my experience it is type theory which introduces A LOT of confusion. Like the above confused comment.
- black_knight 11y ago
  I am not saying ZF cannot distinguish functions which respect an equivalence relation and those which do not — the axiom of choice concerns equality, not any old equivalence relation. I am saying that ZF cannot distinguish those sets for which the logical "for all x there exists a y" defines a function. This is because logical equality in ZF can be forced to be be any equivalence relation, without any additional restriction on the logical constructions. This forces us to add extra axioms saying which sets are ok: countable choice, dependent choice etc. At the extreme end there is the axiom saying all sets have this property, with consequences such as Banach-Tarski and Diaconescu's theorem. Type theory introduces nuances, which may not be appreciated by the non-logician (constructiveness, intensionality…). Homotopy type theory goes some way in mitigating this by allowing quotients (but the logical constructions are suitably restricted to preserve choice), and adding function extensionality (not to mention univalence).
  - auggierose 11y ago
    And ZF should'nt distinguish those sets for which the logical "for all x there exists a y" defines a function or not. If you want the notion of a unique function, you should have the logical statement "for all x there exists a unique x". I have no problem with Banach-Tarski. Sets of points just do not describe properly our intuition of 3-dimensional space. Measurable sets of points more so. Type theory just shuts out certain things its inventors don't want to think about. How does that help anyone?
    - black_knight 11y ago
      The intuition behind the type theoretical axiom of choice is that the choice is given by a (hypothetical) proof of the "∀x ∈ A ∃ y …"-statement. The constructive interpretation of the statement is precisely that there is such a choice function — so it becomes a tautology (provable without any extra axioms). And I believe that agrees with the naive intuition one has why the axiom of choice is true. The problem is when the logic allows proofs (or semantics) which does not preserve the equality. In type theory the equality is intensional and thus preserved by structure. Unique choice is besides the point here. There may be a unique function, or there may be many. The intuition of choosing is the same. I also have no issue with B-T, as I expect weird consequences of ZFC; the axioms and logic being so profoundly non-constructive and removed from my intuitions in the first place. That said, I would not deny the set-theorists enjoying their theory, I merely observe that there are subtle things their theories fail to describe. Type theory does not shout anything, but is carefully constructed from the needs of its creators. Some people want to extract algorithms from their proofs, or want to prove that their algorithms are correct. And if you want this, the nuances of type theory are actually nuances of things you care about — algorithms and proofs. If these are not among your interests, then type theory is not for you. Thats fine, I am sure you have other interests.

JoshTriplett 11y ago

What's the disadvantage of those other foundations that makes them unsuitable for universal use?

black_knight 11y ago
Of course the proponents of these other foundations claim that they are suitable for universal use. But sets came first, and is good enough for most purposes, and mathematicians in general are more concerned with mathematics than foundations. Actually the recent movement of "Homotopy Type Theory" is gaining some traction among non-logicians, giving easier formulations and proofs in category theory and topology. Also in computer science type theory is becoming more usual, since all results are constructive (provides algorithms) and is in fact a programming language in it self.
tel 11y ago
They're certainly not unsuitable, but they have a tendency to take observation/realization/grasping/proving as an instantaneous process. In most people's regular understanding of logic, however, this is false. There is a process by which new data and new conclusions from that data are drawn and made available to you. So ultimately, if those things matter for either UX of mathematics or for actual mathematical content is a large question, but it's fairly clear that if you need to capture something closer to the actual dynamics of knowledge/learning/understanding then you are sunk when you base your foundations in set theory.

auggierose 11y ago

I don't think there is any confusion here. Of course ZF set theory can express this weaker notion. But in ZF these different functions have different domains and ranges A, A mod r, B, B mod r, where r is the equivalence relation. In my experience it is type theory which introduces A LOT of confusion. Like the above confused comment.

black_knight 11y ago
I am not saying ZF cannot distinguish functions which respect an equivalence relation and those which do not — the axiom of choice concerns equality, not any old equivalence relation. I am saying that ZF cannot distinguish those sets for which the logical "for all x there exists a y" defines a function. This is because logical equality in ZF can be forced to be be any equivalence relation, without any additional restriction on the logical constructions. This forces us to add extra axioms saying which sets are ok: countable choice, dependent choice etc. At the extreme end there is the axiom saying all sets have this property, with consequences such as Banach-Tarski and Diaconescu's theorem. Type theory introduces nuances, which may not be appreciated by the non-logician (constructiveness, intensionality…). Homotopy type theory goes some way in mitigating this by allowing quotients (but the logical constructions are suitably restricted to preserve choice), and adding function extensionality (not to mention univalence).
- auggierose 11y ago
  And ZF should'nt distinguish those sets for which the logical "for all x there exists a y" defines a function or not. If you want the notion of a unique function, you should have the logical statement "for all x there exists a unique x". I have no problem with Banach-Tarski. Sets of points just do not describe properly our intuition of 3-dimensional space. Measurable sets of points more so. Type theory just shuts out certain things its inventors don't want to think about. How does that help anyone?
  - black_knight 11y ago
    The intuition behind the type theoretical axiom of choice is that the choice is given by a (hypothetical) proof of the "∀x ∈ A ∃ y …"-statement. The constructive interpretation of the statement is precisely that there is such a choice function — so it becomes a tautology (provable without any extra axioms). And I believe that agrees with the naive intuition one has why the axiom of choice is true. The problem is when the logic allows proofs (or semantics) which does not preserve the equality. In type theory the equality is intensional and thus preserved by structure. Unique choice is besides the point here. There may be a unique function, or there may be many. The intuition of choosing is the same. I also have no issue with B-T, as I expect weird consequences of ZFC; the axioms and logic being so profoundly non-constructive and removed from my intuitions in the first place. That said, I would not deny the set-theorists enjoying their theory, I merely observe that there are subtle things their theories fail to describe. Type theory does not shout anything, but is carefully constructed from the needs of its creators. Some people want to extract algorithms from their proofs, or want to prove that their algorithms are correct. And if you want this, the nuances of type theory are actually nuances of things you care about — algorithms and proofs. If these are not among your interests, then type theory is not for you. Thats fine, I am sure you have other interests.