Hacker News Reader

Comment by ocfnash | Hacker News Reader

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

View on HN

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?

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.

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

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/

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

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

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.

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.

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.

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

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!

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.

What's your background in math?

I am a geometer by training.

Thanks for the links!

Reply on news.ycombinator.com