1
$\begingroup$

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.

enter image description here

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.

  • 0
    That there are multiple points of view in set theory is precisely the problem I was alluding to. On the other hand, results and computations based on the properties of the real line, complex plane, and finite-dim vector spaces are built into real world control systems in communication, avionics, medical imaging, spectroscopy, mechatronics, etc. This is where math meets nature and these properties do not vary. The structures are canonical in that sense.2012-11-14

2 Answers 2

6

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.

2

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

  • 0
    On the other hand, Kolmogorov also said that only $f$initary math is $u$seful for applications. So ma$y$be a related question is which pseudo-true results are finitar$y$.2012-11-12