Foundations of Mathematics (2015) [pdf](mathetal.net)
mathetal.net
Foundations of Mathematics (2015) [pdf]
http://www.mathetal.net/data/book1.pdf
31 comments
Not a mathematician. If the goal is simplicity why can't you use Peano's axioms?
The Peano axioms don't do very much, they just help model the natural numbers. You still need something to model the logic and provide foundations more complex subjects like analysis.
> simplicity
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.
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.
It would be interesting to learn about some new (unified) theory that can formalize the notion of infinity. Apparently, this can hardly be done on the basis of the classical (Cartesian) view of space which is essentially a box with points (elements).
Then John H. Conway's Surreal Numbers might be of interest to you. Donald Knuth wrote a book about the subject and it's actually in the form of a story with dialogue, not your typical math book. I'll attempt a summary. It is possible to build all number systems at once including all integers, rationals, algebraic, irrational, infinitesimal, hyper-reals and transfinite all at once using a single procedure which resembles Dedekind cuts. From that foundation one can recreate many of the results of non-standard analysis. Conway discovered his Surreal Numbers while investigating Combinatorial Game Theory. He wasn't even trying to create a new foundation for mathematics, he was just playing at his games which many of his colleagues looked down upon as useless. Apparently playing games and having fun can occasionally result in extraordinary discoveries.
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.
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.
If you listen to Conway talk about the Surreals you'll note that he considered it a game (in the game theory sense). He was interested in games of a certain kind and what properties they had, a long the way he stumbled upon this game that we now call the surreal numbers.
Is it point or is it continuous line with infinity as an “end”? And there is infinity elements without any point. Or any section of any one of these baselines (and you can have infinite dimension hence many baselines not just x y z, or r/degree etc) can be remap to itself and hence is infinite as well. The point is not the lines, as mapping proved that the points (said the natural no point) is a smaller subset of the real number or the line.
Just not sure about your point.
Just not sure about your point.
I do not understand your question: a set is infinite if and only if there is a bijection between it and one of its strict subsets.
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).
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).
This is why math shouldnt be posted on HN.
There is worse misunderstanding/bikeshedding upwards in the thread, although it's more artfully worded. And at least one of the replies to this refers to useful resources. This is, in fact, exactly why math should be posted on HN.
I like Godel: "this sentence is unprovably true".
A substantial portion of this text appears to be concerned with traditional Zermelo–Fraenkel set theory (and its extensions).
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 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
Thank you for the links!
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?
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?
Your remarks bring me close to the border of my limited knowledge of model theory so I must be careful with my response.
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.
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.
Only speaking about arithmetic rather than full set theory: in (full) second order arithmetic theory all models of the natural number N are isomorphic (in a unique way). The big drawback is that this theory is completely undecidable, so we usually interpret it in first order logic set theory where it becomes incomplete. By Godel, you cannot have an arithmetic theory with decidable proofs and completeness.
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 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".
Tangential question. Is there a mathematics curriculum out there that focuses on constructive foundations? Or is it possible to assemble one?
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
[5] http://www.concrete-semantics.org/
[6] http://adam.chlipala.net/frap/
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
[5] http://www.concrete-semantics.org/
[6] http://adam.chlipala.net/frap/
Besides these lecture notes http://www2.masfak.ni.ac.rs/cmfp2013/Nis%20lecture%20170113.... I haven't found a curriculum. This is one of the goals of Robert Harper et. all involved in type theory research https://existentialtype.wordpress.com/2018/01/15/popl-2018-t...
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
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
You might be interested in the works of Gérard Huet! http://gallium.inria.fr/~huet/PUBLIC/FSCD16.pdf
Thanks. I know about Gérard Huet, but not about this particular publication.
I'm not familiar with any curriculum focusing on constructivist foundations. Out of curiosity, why do you feel constructivist foundations would be more complementary to theoretical computer science?
Constructive maths is generally computable maths, which means less worry about whether whatever you just did is computable or not.
More precisely the effective topos is a kind of realizability topos with a nno where every function is computable. Such a (non trivial) topos cannot be classical, otherwise the halting problem would be decidable. However the effective topos can only deal with calculability, not complexity. For complexity linear logic (without exponentials) and symmetric monoidal categories are better suited (but I don't know if there exists a model where every function is in P for instance).
Speaking of the foundations: is intuitionism still alive? How is constructive math doing nowadays? Do mathematicians embrace or reject it? Did the recent HoTT change their attitude towards constructive math?
I'm not at all qualified to answer such a broad question but I'll share my amateur opinions for what they're worth.
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.
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.
Constructive mathematics is alive and well for 2 reasons.
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.
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.
Oh yes, it is very much alive. For instance any topos (with a nno) is a model of intuitionist set theory. And since topos are a very natural type of categories (a topos= acategory which has finite limits and a power object), intuitionist logic is important in category theory.
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).
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).
On the other hand, constructive set theory is still rather a niche part of mathematics (this may change with the recent development of HOTT). It is hard not to use the LEM (and I am not good at it, I am not an expert on this subject. Expert say it gets easier over time to get used to not use LEM).
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!
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'm inclined to agree with you, with a few caveats. I do think ZFC isn't the superlative candidate for foundations. That being said, most mathematicians don't really think about the foundations of mathematics often (if ever). They use ZFC's set theory because it's a succinct, versatile and useful notation which is frankly very easy to learn.
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.
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.
Thanks for the links!