Foundations of Mathematics (2015) [pdf]
mathetal.net
mathetal.net
I have gradually come to believe that ZF theory has received a disproportionate amount of attention on account of the fact that it serves as the "official" foundations of mathematics, but that it is not an especially beautiful, or useful, structure.
I believe that ZF theory is an interesting object, worthy of mathematical study, but _not_ the best candidate for the foundations of mathematics! I am very happy to see that this year's Chauvenet Prize [1] was won by Tom Leinster's "Rethinking set theory", in which he highlights that Lawvere set theory looks like a much better candidate. I cannot do better than recommend you look at Leinster's superb article.
[1] MAA, Chauvenet Prize, https://www.maa.org/programs-and-communities/member-communit...
[2] Leinster, T., "Rethinking set theory", https://arxiv.org/abs/1212.6543
I believe people are gradually coming round to the point of view that constructive mathematics (including intuitionism) is a useful generalization of classical mathematics, rather than a handicap.
Proof assistants, while still fairly niche, continue to get more attention and the fact that constructive mathematics tends to give "proofs that compute" helps.
For what it's worth, I waffled on about this a little a few months ago right here: https://news.ycombinator.com/item?id=18404914
In my opinion HoTT is the most interesting subject in this area but we have yet to figure out exactly what its role is, and the extent to which it should serve in foundations. However the fact that it is a deep theory with significant value independent of its foundational role must surely help the constructive point of view. I think it's fair to say "Book HoTT" is not fully constructive since univalence is an axiom but this seems to have been resolved with the introduction of cubical type theory.
I also suspect the majority of mathematicians still spend very little time thinking about foundations.
1. The type theorists/homotopy theorists that are exploring homotopy/cubical type theory as a foundational approach.
2. The objective fact that in general the internal language of a topos (in general) does not validate the law of excluded middle or the axiom of choice. This means that if you prove a result while using constructive logic you can apply it to a broader class of models than classical logic. This viewpoint of logic makes the whole "argument" between constructive and classical logic seem very silly: it's like arguing whether or not it is "true" that groups are abelian. Some are and some aren't!
Intuisionism as in Brouwerian intuitionism with choice sequences etc that disprove LEM is still a niche subject, especially foundationally but is still being explored, with the help of understanding of sheaf models that allow it to be studied from a classical perspective.
Two examples: in algebraic geometry, mathematicians use schemes (introduced by Grothendieck), which have allowed to make tremendous progress. But from the point of view of intuitionist logic, a scheme is just a ring, and a quasi-coherent sheave is just a module over this ring (in more details they are ring objects and module objects in the big Zariski topos).
In synthetic differential geometry, one use a certain intuitionist topos to formalize intuitive aspects of reasoning with infinitesimal quantities (without relying on delta and epsilons). Note that non standard analysis also allows to work with infinitemismal quantities (by using ultraproducts), but has the same power has standard analysis (and in particular is classical). Synthetic differential geometry is intuitionnist, so is less powerful, but on the other hands its theorems are automatically valid for more models (complex models, formal smooth schemes...). In SDG, your reals R are a field with an (actually several) element epsilon !=0 (the infinitesimals) and such that epsilon^2=0 (that's why this only work in intuitionist logic, in classical logic R being a field would imply that epsilon=0). In this model every function f: R->R is differentiable, and we have f(x+epsilon)=f(x)+f'(x) epsilon.
In proof theory (like coq) one work with Martin Lof type theory, which is the type theory of topoi (and so is intuitionist). A recent development is to work with homotopy type theory instead, the type theory of \infty-topos. This is more powerful (and can be used as fundations for all of maths), and solve real problems, like correctly defining equality (equality is actually a tricky concept, for instance it may not be the case in the prover's theory that "for any two functions f and g such that forall x, f(x)=g(x); then f=g", but this is obviously a feature we want.) On the other hand it is quite a bit trickier to define (we need (infty,1)-categories).
For instance, in the intuitionist reals, from "x >= 0 and x != 0" you cannot conclude that "x != 0". To prove x>0 you would need to exhibit a natural number n such that x>=1/n (so in other words you need a constructive proof that x>0). But this is not always possible, you have models of R where there is an x != 0 which is smaller than all the 1/n.
There is however one nice feature of intuitionist theory: every geometric sentence which is provable in classical theory is actually true in intuitionist theory. So if you have a geometric sentence (https://ncatlab.org/nlab/show/geometric+theory) you can use LEM in your proofs, the proof will still be valid intuitionally!
I feel this would be much more adequate for then following up with pure CS studies on topics such as [1-6].
Classical math bootcamps, like Math 55, are typically algebra plus analysis and they don't even focus too much on classical foundations.
[1] https://www.elsevier.com/books/lectures-on-the-curry-howard-...
[2] https://softwarefoundations.cis.upenn.edu/
[3] https://www.cis.upenn.edu/~bcpierce/tapl/
[4] https://www.springer.com/gb/book/9783540654100
There is a guy however with a rational foundations of Math curriculum, doing algebraic calculus and rational Trig that I find easy to work with (ie: building a library) https://www.youtube.com/user/njwildberger/playlists
As stated in Tom Leinster's paper that you link to, both ZFC and Lawvere set theory are first-order theories:
"In logical terminology, both axiomatizations [i.e., ZFC and Lawvere set theory] are simply first-order theories."
This means that with both theories, we cannot categorically define important concepts such as the natural numbers, due to the compactness theorem and its consequence, the upward Löwenheim-Skolem theorem that hold in first-order logic:
https://en.wikipedia.org/wiki/Categorical_theory
https://en.wikipedia.org/wiki/L%C3%B6wenheim%E2%80%93Skolem_...
Also, the downward Löwenheim-Skolem theorem leads to Skolem's paradox, because ZFC proves (as we expect from a set theory) Cantor's theorem, and at the same time we know that if ZFC is consistent, then it has a countable model:
https://en.wikipedia.org/wiki/Skolem%27s_paradox
So, even the rather basic notion of countability is relative.
As long as you stay within first-order predicate logic, a theory of sets will run into such issues.
From what I see, such issues are often "resolved" when working with ZFC by stating explicitly that a very specific (i.e., the "intended") model is meant, with the caveat that, from a logical perspective, we do not even know whether the theory is consistent and hence whether such a model in fact exists.
Thus, even though ostensibly working "in" ZFC, a meta-logical statement about the intended models seems often necessary that cannot be formulated in first-order logic because with first-order predicate logic, we cannot control the cardinality of infinite models.
Do other considered set theories offer any improvements over ZFC in these specific respects?
I believe the answer to your question:
> Do other considered set theories offer any improvements over ZFC in these specific respects?
is "no", and that you essentially answer this yourself with the following paraphrasing of Löwenheim–Skolem:
> As long as you stay within first-order predicate logic, a theory of sets will run into such issues.
So if we opt Lawvere set theory I think we just do the same thing as if we had opted for ZCF, i.e., just assume we have a model (perhaps provided by some higher order logical system).
However in my opinion, we do have a theory with a much more intuitive set of axioms.
In set theory one has to be careful that you can have models which are not transitive models. So Löwenheim-Skolem implies that if you have a model, you have a countable model. But you may not have a transitive countable model. However you do have a transitive version of Löwenheim-Skolem, by Mostowski collapsing lemma: "there exists a transitive model" <=> there exists a countable transitive model".
In that sense there's a compelling argument that a revised set theory might be called for, in the sense that it could be a better fit for the way most mathematicians use set theory in practice. But since Leinster's set theory is axiomatically equivalent to ZFC without regularity, there's also a compelling argument that it's not worth it unless it's significantly more expedient or easy to learn.
It might be possible to build a set theory and the rest of mathematics based on the integers, but I am sure the result wouldn't look simple.
Just not sure about your point.
As formal as it gets.
Edit: (not intending to be harsh, just that I probably lack some context to properly understand what you are asking).
Conway's left and right "cuts" look like sets but then again I'm not really sure what they are. Is this alien mathematics accidentally discovered on Earth by perhaps the most intelligent Earthling who ever lived. I don't know. All I can say is I took a detour from my usual math studies to look into Surreal numbers and it was an interesting trip. I'm quite conservative when it comes to math. I don't go around preaching Surreal numbers are the way to do math but it is a curiosity none-the-less worth at least the small price of reading Knuth's short book about it from cover to cover.