# Inhabited versus nonempty sets - disasters without excluded middle?

The attached screenshot, from Goldblatt's Topoi, shows at a glance the distinction between the constructive concept of inhabited set versus that of the classical nonempty set.

These definitions seem only equivalent if the axiom of excluded middle is assumed. However, in the absence of this axiom, the distinction seems fundamental (Why isn't this taught in the math curriculum?)

By analogy to Herrlich's Axiom of Choice which lists "disasters without choice", "disasters with choice" and "disasters either way", is there a published list of consequences of this difference?

In other words, which major results that rest on provably nonempty sets in classical logic cannot be proven to be inhabited sets without excluded middle?

By the way, at the end of Khamsi and Kirk's Introduction to metric spaces and fixed point theory the authors point out three variations on constructive mathematics developed by different mathematicians such as Brouwer and A Markov (Jr). It would be interesting then to also compare what effect these variations have on the emergent set theory.

-
It isn’t taught in the usual math curriculum because the law of the excluded middle is (properly, in my view) taken for granted in most mathematical practice, and the odd exceptional areas aren’t part of the common curriculum. – Brian M. Scott Nov 11 '12 at 20:39
I was fairly certain that the axiom of choice and geometry were fine with one another. I don't see why the axiom of choice means that you can't have geometry in three dimensions. – Asaf Karagila Nov 11 '12 at 20:59
As far as I’m concerned, the real point of Herrlich’s book is that AC is necessary for doing a great deal of lovely mathematics. It’s interesting for its own sake to know just what depends on it and to what extent, but otherwise I don’t care: I don’t consider AC any more problematic than the axiom of infinity. The question of what depends on EM also has some intrinsic interest, but as far as I’m concerned not much more than the question of what depends on modus ponens. – Brian M. Scott Nov 11 '12 at 21:02
Of course it’s a bias. Unlike teaching only Euclidean geometry, however, it’s a desirable bias. – Brian M. Scott Nov 11 '12 at 21:03
@alancalvitti: You tried that argument with me before. I think that you have a very strong bias against set theory, and it has come up before in your comments. I don't wish to repeat my argument with you because frankly I find such arguments childish. I also think that prizes are not everything in mathematics, but apparently you seem to disagree. – Asaf Karagila Nov 11 '12 at 21:13

I would not say there are "disasters" either way.

Various cases of the distinction are familiar in other terms. Programmers well know a problem may have no solutions, or may have solutions which are not computable, or may have computable solutions. In the effective topos this is precisely expressed by saying the solution set is empty, or non-empty, or inhabited.

Sorry, I got this slightly wrong when I first posted : "Geometers and analysts know the difference between a sheaf having sections locally all over a space versus having a global section. In the topos of sheaves on the space this is the difference between a non-empty set and an inhabited one." In fact that is the difference between being non-empty and having a nameable instance. Non-empty in this case is having local sections 'almost everywhere' in the sense of over some dense open subset -- for example as a Riemann surface has local sections except at branch points.

So you might say we don't need the topos terminology since special cases are already known. Or you might think the terminology helps bring out what is common to the special cases.

-

Rather than speculate about the importance of the difference between inhabited and non-empty, I will simply explain what the difference is in the context of topos theory.

Definition. An inhabited object is an object $X$ for which the sentence $(\exists x \in X . \, \top)$ is true. A non-empty object is an object $X$ for which the sentence $\lnot (\forall x \in X . \, \bot)$ is true.

Here, of course, I am interpreting formulae using the Kripke–Joyal semantics internal to a topos. (Set theorists may wish to substitute "intuitionistic Kripke model of IZF" for "topos".) The formulae I have used are not exactly the same as Goldblatt's, because Kripke–Joyal semantics can only interpret bounded quantifiers; if you think about it a little you will see that the usual translation of bounded quantifiers to unbounded quantifiers recovers Goldblatt's version.

What does this mean in the external logic? Well, an object $X$ is inhabited if and only if the unique morphism $X \to 1$ is an epimorphism, and $X$ is non-empty if and only if, for all subobjects $U \subseteq 1$, if $X \times U$ is empty, then $U$ itself is empty.

For concreteness, let $\mathcal{E} = \textbf{Sh}(B)$ be the topos of sheaves on a non-trivial topological space $B$, say, the circle $S^1$. An object of $\mathcal{E}$ is a sheaf on $B$, i.e. a topological space $E$ equipped with a local homeomorphism $E \to B$, and a morphism in $\mathcal{E}$ is a continuous map making the obvious triangle commute. It is not hard to find examples of inhabited objects: the terminal sheaf $1$, corresponding to the identity map $\textrm{id} : B \to B$, is inhabited for trivial reasons. A more interesting example would be the 2-to-1 connected covering space $E \to B$ of the circle: this is inhabited, but it is also impossible to find a "global" element of $E$.

In general, any inhabited object is non-empty, but here the converse is false: if we take $V$ to be a dense open subset of $B$, say, $B$ minus a point, then the sheaf $V \hookrightarrow B$ will be non-empty but not inhabited. Why is this? Well, clearly, $V \hookrightarrow B$ is not an epimorphism of sheaves, and the only open subset $U \subseteq B$ such that $U \cap V = \emptyset$ is $U = \emptyset$ itself. More generally, a sheaf $E$ on $B$ will be non-empty if and only if the image of the projection map $E \to B$ is dense in $B$. (Set theorists familiar with forcing should find this vaguely familiar: this is precisely the interpretation of existence needed to make a model satisfy classical logic.)

-
+1 for the exposition, but similarly to Herrlich's program, is it possible to work out the consequence of these various assumptions to existing results from mainstream mathematics? (note Herrlich's examples I quoted in the comments above, eg nonexistence of nontrivial ultrafilters; nonexistence of vector space basis) – alancalvitti Nov 12 '12 at 4:18
It's possible, but first of all one would have to work out the consequences of the law of excluded middle. And I doubt anyone has the patience to do that. – Zhen Lin Nov 12 '12 at 8:04
Kolmogorov called double-negated propositions "pseudo-true." Why are these regarded as more important than true propositions, apparently even by Kolmogorov since he only wrote one paper on this. – alancalvitti Nov 12 '12 at 15:06
On the other hand, Kolmogorov also said that only finitary math is useful for applications. So maybe a related question is which pseudo-true results are finitary. – alancalvitti Nov 12 '12 at 15:43