I am one of the (rare on the Internet now) people that is a fan of "everything is a set".
Of course I don't believe that set theory is the One True Foundation and everything else is a lie, the fact that one can give a foundation with just one type of object, just one binary relation and relatively few simple axioms (or axiom schemas) is quite relaxing and I would say a bit unappreciated.
And also unlike other fellow students I never encountered any problem with more seemingly complicated constructions like tensor products or free groups since one can easily see how they are coded in set theory if one is familiar with it as a foundation.
As one of those that do not like the “sets at the bottom” approach I just want to highlight why. For me, mathematics built on sets have leaky abstractions. Say I want natural numbers, I need to choose a concrete implementation in set theory e.g. Von Neumann, but there are multiple choices. For all good definitions, so get Peano arithmetic and can work with, but the question “Is 1 and member of 3” depends on your chosen implementation. Even though it is a weird question, it is valid and not isomorphic under implementations. That is problematic, since it is hidden in how we do mathematics mostly. Secondly, it is hard to formalize, and I think mathematics desperately needs to be formalized. Finally, I do not mind sets, they are great, and a very useful tool, I just do not like they as the foundation. I firmly believe we should teach type theoretic or categorical foundations in mathematics and be less dependent on sets.
> Say I want natural numbers, I need to choose a concrete implementation in set theory e.g. Von Neumann, but there are multiple choices.
You don't need to choose a concrete implementation. If you don't want to choose a construction, you can just say something like "let (N, 0, +, *) be a structure satisfying the peano axioms" and work from there.
> For all good definitions, so get Peano arithmetic and can work with, but the question “Is 1 and member of 3” depends on your chosen implementation. Even though it is a weird question, it is valid and not isomorphic under implementations. That is problematic, since it is hidden in how we do mathematics mostly.
Why is that problematic? The constructions are isomorphic under the sentences that actually matter. This kind of statement is usually called a "junk theorem", and they are a thing in type theory too, see for example this quote from a faq by Kevin Buzzard about why Lean defines division by zero to be zero:
> The idiomatic way to do it is to allow garbage inputs like negative numbers into your square root function, and return garbage outputs. It is in the theorems where one puts the non-negativity hypotheses.
> Secondly, it is hard to formalize, and I think mathematics desperately needs to be formalized.
Is that actually true? At the very least writing out the axioms and derivation rules is easier for set theory, since it's simpler than type theory. And there has been plenty of computer-verified mathematics done in Metamath/set.mm and Isabelle/ZF, even though less has been done than in type theory. Currently the automated tools are better for type theory, but it seems likely to me that that has more to do with how much effort has been put into type theory than any major inherent advantages of it.
---
More generally, types in type theory are also constructed! The real numbers in Lean don't come from the platonic realm of forms, they are constructed as equivalence classes of cauchy sequences. And the construction involves a lot of type-theoretic machinery which I'd usually rather ignore when working with reals, much like I'd usually rather ignore the set-theoretic construction of the real numbers. And the great thing is that I can ignore them, in either foundation!
So I just don't really buy these common criticisms of set theory, which to me seem like double standards.
Sure you can work around it most of the time, but some times you cant. The whole point is that isomorphic is not equality in set theory, and sometimes proofs does not transfer along isomorphism because they refer to implementations. I agree that it is much preferable to work with abstract structure, but that not always what happens in practice. The natural number example is contrived but easy to see.
My point of view is also that I do not like the Lean approach. It would actually like no junk theorems to exist in my theory. I am much more partial to the univalent approach and in particular univalent implementation that compute e.g. cubical. Regarding how easy it is to formalize, you are right. Lots of good work happens with set theory based type theory. My point was also that set theoretic foundations themselves are very hard to formalize, e.g ZFC + logic is very difficult to work from. A pure type theoretical foundations is much easier to get of the ground from. To prove that plus commutes directly from ZFC is a nightmare.
Yes, I am very familiar with category theory. Not sure I would consider it the "next step from sets". Sure, there are alternative foundations based on category theory, but that is not its only or its main use.
I don't understand arguments like "nobody can agree on what set theory is". This is not how mathematics work.
In mathematics labels are _not_ important, definitions are.
One simple example that everybody can relate to: do natural numbers include 0 or not? Who cares? Some definitions include it, some do not. There's even a convention of using N for N with 0, and N+ for excluding it, but even the convention is just a convention, not a definition. You could call them "funky numbers, the set of whole positive numbers including 0", and you're fine. Funky, natural, those are just names, labels, as long as you define them, it doesn't matter.
Same applies to set theory, there's many, many set theories, and they differ between properties, and this has never caused problems, because in mathematical discussion or literature...you provide or point to a definition. So you'll never discuss about "set theory" without providing one or pointing to one.
This is very, very different from how normal people waste their time.
E.g. arguing whether AI "thinks" or not, but never defining what thinking means, thus you can't even conclude whether you think or not, because it's never been defined.
The distinction between material set theories (like ZF and other set-theoretical foundations you might have heard about) and structural set theories (like ETCS, SEAR and most likely the "typed set theories" mentioned in OP) is rather fundamental. To the point that calling both of them "set theory" feels quite misleading.
Maybe because there are many different set theories. The one taught in school is not a correct one but grokable for most students. Then you got the Zermeno Frenkel set theory, and you got the Homotopy Type Theory one which can yield or emulate the same results. So in a sense the opening statement is correct. There is no consensus on a single "this is THE one and true correct set theory"
I am one of the (rare on the Internet now) people that is a fan of "everything is a set".
Of course I don't believe that set theory is the One True Foundation and everything else is a lie, the fact that one can give a foundation with just one type of object, just one binary relation and relatively few simple axioms (or axiom schemas) is quite relaxing and I would say a bit unappreciated.
And also unlike other fellow students I never encountered any problem with more seemingly complicated constructions like tensor products or free groups since one can easily see how they are coded in set theory if one is familiar with it as a foundation.
As one of those that do not like the “sets at the bottom” approach I just want to highlight why. For me, mathematics built on sets have leaky abstractions. Say I want natural numbers, I need to choose a concrete implementation in set theory e.g. Von Neumann, but there are multiple choices. For all good definitions, so get Peano arithmetic and can work with, but the question “Is 1 and member of 3” depends on your chosen implementation. Even though it is a weird question, it is valid and not isomorphic under implementations. That is problematic, since it is hidden in how we do mathematics mostly. Secondly, it is hard to formalize, and I think mathematics desperately needs to be formalized. Finally, I do not mind sets, they are great, and a very useful tool, I just do not like they as the foundation. I firmly believe we should teach type theoretic or categorical foundations in mathematics and be less dependent on sets.
> Say I want natural numbers, I need to choose a concrete implementation in set theory e.g. Von Neumann, but there are multiple choices.
You don't need to choose a concrete implementation. If you don't want to choose a construction, you can just say something like "let (N, 0, +, *) be a structure satisfying the peano axioms" and work from there.
> For all good definitions, so get Peano arithmetic and can work with, but the question “Is 1 and member of 3” depends on your chosen implementation. Even though it is a weird question, it is valid and not isomorphic under implementations. That is problematic, since it is hidden in how we do mathematics mostly.
Why is that problematic? The constructions are isomorphic under the sentences that actually matter. This kind of statement is usually called a "junk theorem", and they are a thing in type theory too, see for example this quote from a faq by Kevin Buzzard about why Lean defines division by zero to be zero:
> The idiomatic way to do it is to allow garbage inputs like negative numbers into your square root function, and return garbage outputs. It is in the theorems where one puts the non-negativity hypotheses.
https://xenaproject.wordpress.com/2020/07/05/division-by-zer...
> Secondly, it is hard to formalize, and I think mathematics desperately needs to be formalized.
Is that actually true? At the very least writing out the axioms and derivation rules is easier for set theory, since it's simpler than type theory. And there has been plenty of computer-verified mathematics done in Metamath/set.mm and Isabelle/ZF, even though less has been done than in type theory. Currently the automated tools are better for type theory, but it seems likely to me that that has more to do with how much effort has been put into type theory than any major inherent advantages of it.
---
More generally, types in type theory are also constructed! The real numbers in Lean don't come from the platonic realm of forms, they are constructed as equivalence classes of cauchy sequences. And the construction involves a lot of type-theoretic machinery which I'd usually rather ignore when working with reals, much like I'd usually rather ignore the set-theoretic construction of the real numbers. And the great thing is that I can ignore them, in either foundation!
So I just don't really buy these common criticisms of set theory, which to me seem like double standards.
Sure you can work around it most of the time, but some times you cant. The whole point is that isomorphic is not equality in set theory, and sometimes proofs does not transfer along isomorphism because they refer to implementations. I agree that it is much preferable to work with abstract structure, but that not always what happens in practice. The natural number example is contrived but easy to see. My point of view is also that I do not like the Lean approach. It would actually like no junk theorems to exist in my theory. I am much more partial to the univalent approach and in particular univalent implementation that compute e.g. cubical. Regarding how easy it is to formalize, you are right. Lots of good work happens with set theory based type theory. My point was also that set theoretic foundations themselves are very hard to formalize, e.g ZFC + logic is very difficult to work from. A pure type theoretical foundations is much easier to get of the ground from. To prove that plus commutes directly from ZFC is a nightmare.
Have you considered the next step from sets into Category Theory?
Yes, I am very familiar with category theory. Not sure I would consider it the "next step from sets". Sure, there are alternative foundations based on category theory, but that is not its only or its main use.
[dead]
I don't understand arguments like "nobody can agree on what set theory is". This is not how mathematics work.
In mathematics labels are _not_ important, definitions are.
One simple example that everybody can relate to: do natural numbers include 0 or not? Who cares? Some definitions include it, some do not. There's even a convention of using N for N with 0, and N+ for excluding it, but even the convention is just a convention, not a definition. You could call them "funky numbers, the set of whole positive numbers including 0", and you're fine. Funky, natural, those are just names, labels, as long as you define them, it doesn't matter.
Same applies to set theory, there's many, many set theories, and they differ between properties, and this has never caused problems, because in mathematical discussion or literature...you provide or point to a definition. So you'll never discuss about "set theory" without providing one or pointing to one.
This is very, very different from how normal people waste their time.
E.g. arguing whether AI "thinks" or not, but never defining what thinking means, thus you can't even conclude whether you think or not, because it's never been defined.
The distinction between material set theories (like ZF and other set-theoretical foundations you might have heard about) and structural set theories (like ETCS, SEAR and most likely the "typed set theories" mentioned in OP) is rather fundamental. To the point that calling both of them "set theory" feels quite misleading.
Maybe because there are many different set theories. The one taught in school is not a correct one but grokable for most students. Then you got the Zermeno Frenkel set theory, and you got the Homotopy Type Theory one which can yield or emulate the same results. So in a sense the opening statement is correct. There is no consensus on a single "this is THE one and true correct set theory"
what… argument? anyway, pretty sure larry is quite fluent with how mathematics is done.
Doesn't show in the premise.
That first sentence has very little to do with the content of the essay; you’re being pedantic. You understand very well what was meant.
You're probably right, that was a bit pointless of a comment.