Foundations of Mathematics (2015) [pdf]

http://www.mathetal.net/data/book1.pdf

by lainon • 7 years ago

196 31 7 years ago

ocfnash4• 7 years ago

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

ernst_klim• 7 years ago

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?

ocfnash4• 7 years ago

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.

maxiepoo• 7 years ago

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.

Gondolin4• 7 years ago

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).

pfortuny2• 7 years ago

Thanks for the links!

sidusknight2• 7 years ago

What's your background in math?

ocfnash4• 7 years ago

I am a geometer by training.

nextos2• 7 years ago

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/

hackermailman• 7 years ago

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

throwawaymath2• 7 years ago

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?

valw• 7 years ago

You might be interested in the works of Gérard Huet! http://gallium.inria.fr/~huet/PUBLIC/FSCD16.pdf

triska• 7 years ago

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?

ocfnash4• 7 years ago

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.

Gondolin4• 7 years ago

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".

throwawaymath2• 7 years ago

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.

techno_modus• 7 years ago

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).

ngcc_hk• 7 years ago

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.

pfortuny2• 7 years ago

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).

sidusknight2• 7 years ago

This is why math shouldnt be posted on HN.

unixbeard1337• 7 years ago

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.

Mugwort• 7 years ago

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.

voxl• 7 years ago

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.

visualstudio• 7 years ago

Not a mathematician. If the goal is simplicity why can't you use Peano's axioms?

Retra• 7 years ago

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.

Koshkin• 7 years ago

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.

cellular• 7 years ago

I like Godel: "this sentence is unprovably true".

Foundations of Mathematics (2015) [pdf]

Related Stories