Computing an integer using a Grothendieck topos

Setting philosophy aside, one of the major applications of constructive logic is that it's the internal language of toposes (and related kinds of categories). This usually simplifies proofs considerably and can produce new results.

Some examples, Joyal and Tierney's An extension of the Galois theory of Grothendieck, CJ Mulvey's papers from the 70s (Intuitionistic algebra and representations of rings for example) and Blechschmidt's A General Nullstellensatz for Generalized Spaces.

Johnstone's Sketches of an Elephant often has both internal and external proofs for comparison and it's easily seen that the internal version is both easier to write and to understand.

For an article explicitly focused on using internal languages in algebraic geometry, see Blechschmidt's notes [0]. In particular, section 20 is dedicated to proving things that are difficult without the internal language.

[0] https://github.com/iblech/internal-methods

You don't have do it because it might be useful somewhere else. There's definitely richness to the topic, and it attracts curiosity and answers questions at least some people thought were worth answering. It would be an anomaly if it never found some profound link with stone mainstream more applied field. All the same, when it does prove "useful" that will just be incidental. It won't be a pay-off or vindication or anything. (At least this is my half-baked mathematical philosophy, reasonably people may certainly differ.)

I'll assume that Bauer's not yet convinced you, even though you fully grok their examples.

One application for computer scientists is to focus on computability of the real numbers. Turing's proof that there are uncomputable real numbers is nonconstructive, and it turns out that we can choose "all reals are computable" as an axiom of a topos. (This is the "Russian school" of constructive maths, ala Markov, IIUC.) This is "interesting and important" for both theory and engineering.

For Poincaré-level mindblowing moments, we'll have to search across the landscape of topos theory, a landscape which was only dried out because of constructive maths damming up the floods of LEM and Choice. From homotopy type theory, we have the idea that types are like spaces; objects of the same type are related precisely by the possibility that one object might be deformable into the other. From higher category theory, we have the idea that sets are like 0-categories, and that set theory is just the bottommost slice of a 3D pyramid of category theories.

Proving results neutrally to LEM and Choice is "not just stunts and gimmickry", because the proofs may be reused in any topos, and thus a neutral result is more true or less contextual than one which relies upon LEM. Bauer gives Johnstone, Diff, and RT as example topoi where LEM simply isn't true, but where neutral proofs would be reusable. Since RT is realizeable (by definition, it's the "realizability topos!") this means that neutral proofs each give runnable computer programs.

This is sort of like beating Halo with only the pistol, and developing a sort of "pistol speedrun theory" where we study speedruns with games that have pistols. We aren't saying that there's not non-pistol speedruns, but emphasizing that pistols are a common feature. (Of course, the analogy breaks down here, since not all speedruns are pistol speedruns. Not all topoi are Grothendieck topoi, I suppose.)

https://en.wikipedia.org/wiki/Synthetic_differential_geometr... is worth mentioning. It builds on topos theory which as OP says is closely linked to non-classical mathematics.

In the context of programming languages, constructive mathematics maps well to type systems.

There are type systems that correspond to non constructive logics, but those are the weirder ones.

Elliptic geometry is not a subset of absolute geometry (as absolute geometry is typically formalized). The problem isn't with Euclid's other postulates, it's with things that Euclid didn't formalize, specifically, betweenness. In absolute geometry, given any line containing three distinct points, exactly one of the points will be between the other two. There's no sensible way to define this in elliptic geometry. Intuitively, this makes sense; when you have three points on a line in elliptic geometry, you can travel from any of the three points to any other without passing by the third point.

It's been a while since I've actively studied this, but my recollection is that all you have to do is replace the axioms for betweenness with axioms for separation, and you get a theory which is suitable for elliptic geometry.

(Separation is an arity-4 relationship on points. Intuitively, given any four distinct and collinear points, A and C separate B and D if the order of the points on the line (traveling in either direction) is ABCD.)

https://en.wikipedia.org/wiki/Foundations_of_geometry#Ellipt... appears to agree

I tried to find a proof online one way or the other, but there seems to be no concrete consensus. It's possible that whether or not elliptic geometry is a subset of absolute geometry is a consequence of the formulation of the axioms - since you can modify any axiom involving the existence of parallel lines using something like "If parallel lines exist, then...".

Certainly the way I learned it was that the parallel postulate is the only axiom which distinguishes the elliptic, Euclidean, and hyperbolic geometries.

I believe elliptic geometry is a subset, it's spherical geometry that isn't (though it's closely related).

Euclidean has more axioms than absolute (one more). With more axioms you can prove more things (one of them being the axiom itself). So also, elliptic has more axioms than absolute.

> Is the forgoing the excluded middle really gaining you the guarantee of computability?

It doesn't follow; that uncomputable things cannot be expressed in a constructive system doesn't mean that everything that is computable in principle is also computable, or even definable, in that system (unless by "guaranteeing computability" you meant something else).

Well it is simple for a description of a topos. If you know the definition of topos, you are likely to also know what the canonical coverage is and what sheaves are, etc.

That's pretty egregious, yeah. To be as fair as possible, the author did say "describe", not "understand", but that's small consolation.

Perhaps more materially, HN is obviously(^) not the intended audience for this article! We get a hint of this early on, when the author talks about axioms that contradict LEM -- the phrase "of course" stands out pretty starkly.

(^) Oh no, I did it too!

It is very easy to describe, in the same way that some complicated computations can be neatly packaged into a one liner. Understanding it is a totally different thing.

They said "easy to describe" ie easy to go from understanding to description, not "easy to understand" ie easy to go in the opposite direction from description to understanding.

Let's see how much I can extract from that description... (Okay, after having written this comment, I can say it's "not much", but at least I think I can identify which parts are more glue and reshaping than contain real content. I won't be upset if you hit that [-] to minimize this comment ;) )

> the monoid of continuous endomaps

An "endomap" is a functions `T -> T` over the same base type `T`. You might call these "unary operators".

The "continuous" adjective means that `T` is some kind of topological space -- which agrees, thank goodness, with the "topological" we see earlier in the quotation -- and that our functions preserve the extra properties possessed by these spaces. For the most part, that means that points have some sense of connectivity and continuity (though not necessarily "distance").

The "monoid" bit here doesn't actually add much; it's just highlighting some behavior that unary operators already have. Namely, you can compose two unary operators in sequence, and there's an operator that returns the output unchanged. There's some extra color around making sure the composition is continuous, but we can take the author on faith for now that things work out.

> the one-point compactification of the discrete natural numbers

This is the concrete `T` above.

The "natural numbers" are hopefully clear; we can probably assume the author is including zero, but I don't think it actually matters. I think we just need a set of countably-infinite cardinality.

Since we're talking about continuous maps, we need to consider the natural numbers as some kind of space, with some kind of concept of continuity. The "discrete" qualifier tells us that every natural number is its own island. (This is why I don't think it matters whether we have zero or not.) Any set of elements can be given the discrete topology, so it's not very interesting in its own right. Usually we're interested in what other mathematical widgets do at these boundary cases: since they're effectively contentless, we can better understand what those other widgets contribute purely on their own.

The "one-point compactification" of a topological space is a lot harder to dissect. In a very small nutshell: some subspaces of a topological space can be "compact". If the whole space itself is not compact, there's often a way to turn it into a compact space by adding a single extra point. Compact spaces have some really nice properties, so if you have a space that isn't compact, sometimes it makes sense to move into a compactification of that space instead. But I don't understand this particular construction yet, so I can't explain concretely what space we end up with.

Unfortunately, that also means I have no intuition for what maps `T -> T` we end up with on this compact space. That seems like a pretty key bit of information for the rest of the construction.

> take the monoid of ... considered as a category, then take sheaves for the canonical coverage

For the "considered as a category" part, every monoid is a category in a boring way. It's even more boring when your monoid is already made of maps `T -> T`: the one object of your category is `T`, and the arrows are the maps. This is purely a "perspective-shifting" statement, and the only reason you'd do that is to say something else that's easier to say in category theoretic terms.

As for "take sheaves for the canonical coverage", I'm not even going to try to dissect that. It looks like a coverage is one way to define a topos, and Grothendieck toposes are defined by sheaves on a site, but we're rapidly falling down a rabbit hole here. Summary: they're building a topos in an apparently standard way from the monoid of endomaps we've built up to this point.

I wish people would stop being so entitled. This isn't the nytimes or something. It's somebody's research blog. Your comment is analogous to demanding that Japanese speakers write in English so that you may be able to read their writing. If you don't want to invest the time then simply move on.

This piece probably has a very specific intended audience.