This question is probably really naive. And, I hope the title doesn't come off as too combative. I think that topoi of $\mathbf{Set}$-valued sheaves provide an excellent motivation for higher-order intuitionistic logic, because most such topoi aren't boolean. But, I have an extremely hard time accepting that $\mathbf{Set}$ is intuitionistic.


Let me elaborate on this a bit.


Suppose our intuition for the phrase "subset of $X$" comes from the idea of having an effective total function $X \rightarrow \{0,1\}$ that returns an answer in a finite amount of time. In this case, the subsets of $X$ ought to form a Boolean algebra.


Suppose on the other hand that our intuition for the phrase "subset of $X$" comes from the idea of having an effective partial function $X \rightarrow 1$, such that the program for $f(x)$ either halts in a finite amount of time, or else runs forever. Then, with a bit of thought, we see that subsets of $X$ should be closed under union and intersection. But also, there's really no way to take the complement of a subset in general. So, under this viewpoint, the subsets of $X$ form a bounded distributive lattice.


So, I'm willing to believe that $\mathbf{Set}$ is a Boolean topos (the classical viewpoint), and I'm also willing to believe that it's much, much less than that (the "algorithmic" viewpoint), because I think these are both well-motivated and reasonable positions.


The thing about trying to apply intuitionistic logic to $\mathbf{Set}$ is that it seems to straddle a very strange middle ground between these two extremes. It says: yes, you can take the complement of any subset. But no, it may not be the case that $A^c \cup A = X$ (where $A$ is a subset of $X$, and $A^c := X \setminus A.$). And, it may not be the case that $(A^c)^c = A.$ But nonetheless, you can be assured that $((A^c)^c)^c = A^c$. Huh? Look, I realize this makes perfect sense from a BHK perspective; for instance, the complement of the complement of $(0,1) \cup (1,2)$ is $(0,2)$. So, the double negation law fails. But, that's in a topological space! I mean, why would $\mathbf{Set}$ be subject to this kind of reasoning?



Why would the category of sets be intuitionistic?
You wrote:



> 
> Suppose our intuition for the phrase "subset of $X$" comes from the idea of having an effective total function $X \rightarrow \{0,1\}$ that returns an answer in a finite amount of time. In this case, the subsets of $X$ ought to form a Boolean algebra.
> 
> 
> 


Unfortunately, this is not a workable intuition at all. If you insist that all subsets be classified by "effective total functions $X \to \{0,1\}$" then the subsets of $\mathbb{N}$ are not even closed under countable unions and countable intersections. Or to put it another way, you are not allowed to say "for all $n \in \mathbb{N}$" and "there exists $n \in \mathbb{N}$" in an unrestricted way. How then are we supposed to do any actual mathematics? For instance, number theorists would not even be allowed to *state*



> 
> "For every $n \in \mathbb{N}$ there is $k > n$ such that both $k$ and $k+2$ are prime."
> 
> 
> 


without proving that there is a decision procedure which, on input $n$, decides whether there is a pair of twin primes above it. So, intuitionistic mathematicians *never* proposed such a view.


The idea that subsets be classified by termination of a partial effective procedure is equally unworkable, you just need to go one level up. It allows you to write statements of the form $\exists n \in \mathbb{N} . \phi(n)$ for decidable $\phi$, but not $\forall n \in \mathbb{N} . \phi(n)$.


*General* subsets are *not* classified by *any* kind of decision procedures, or semidecision procedures, or even procedures with access to oracles. You can always beat those with diagonalization to create more subsets. In computational terms, subsets should be thought of as being classified by completely arbitrary computational evidence. Then, among all the subsets *some* are classified by effective decision procedures (the *decidable* subsets), and *some* are classified by entirely uninformative computational evidence (those are the *complemented* subsets which are equal to their double complements).


Now, you ask why anybody would think of sets as intuitionistic objects. First of all, since you already subscribe to the idea that intuitionistic toposes make sense, you might be interested to know that every such topos begets an intuitionistic set theory, and vice versa, see [Relating first-order set theories and elementary toposes](https://doi.org/10.2178/bsl/1186666150) by Awodey et al. In this sense, the distinction between intuitionistic set theories and intuitionistic toposes (and intuitionistic type theories) is not all that important. It is known that we may often (but not always) pass between them as desired.


There are mathematical reasons for considering intuitionistic set theories, rather than toposes. For example, in theoretical computer science people tried to figure out how to do synthetic domain theory in toposes, and there were always some obstacles. In the end Alex Simpson switched to intuitionistic set theories to [solve some of the problems](https://doi.org/10.1016/j.apal.2003.12.005). Speaking a bit vaguely, he needed replacement *and* a non-trivial object $P$, or a set, with magical properties, such as $P$ containing $P^P$ as a retract. In classical set theory this is not possible due to cardinality reasons, but in intuitionistic set theory one can have such sets (and replacement). In topos theory there is no replacement.


Apart from the fact that there are good mathematical reasons for using intuitionistic set theories, one can also ask for philosophical or foundational reasons. I can only relate a personal view here. After having worked for some time with intuitionistic type theory and the internal languages of realizability toposes, I have definitely developed the idea that "bare sets", "bare types" and "bare objects" are not really just "bare collections of elements". They behave much more like topological spaces. The "intrinsic" topological structure of mathematical objects cannot be separated from the objects themselves. This point has been made by many people, but perhaps the most illuminating is the work of Martin Escardó, who puts the topological way of thinking to do surprising and interesting things in [functional programming](http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/) and [type theory](https://www.cs.bham.ac.uk/%7Emhe/papers/universe-indiscrete.pdf). Under this view the classical sets are just the "boring" intuitionistic sets. They are like the indiscrete spaces, and who would want to study those?


Once we subscribe to the idea that even the "bare sets" or "bare objects" may carry intrinsic structure, i.e., they are not just "Cantor's dust", then the double complement not being equal to the original is *the norm* rather than the exception. To give a couple of examples:


1. Suppose we work in presheaves on a category with two objects and two parallel arrows, which is just the topos of directed graphs. The double complement of a subgraph is not the original graph, but rather the full graph induced on the vertices of the original subgraph.
2. Suppose we work in a realizability topos, where an element of a subset carries computational evidence expressing *why* it is in the subset. Then an element $g$ of the subset $S = \{f : [0,1] \to \mathbb{R} \mid \exists x \in [0,1] . f(x) = 0\}$ of $[0,1] \to \mathbb{R}$ carries the computational evidence $\langle{p,q\rangle}$ where $p$ is a program for computing $g$ and $q$ is a program for calculating a real $a \in [0,1]$ such that $g(a) = 0$. An element of the double complement carries only $p$. Since $q$ cannot be algorithmically recovered just from $p$, the double complement is therefore not equal to the original.


We see here that double complement acts as a sort of regularization operation. In fact, that is precisely what it is in the topological interpretation of intuitionistic connectives: the complement of an open set $U$ in the topology is its exterior, and the double exterior of $U$ is its regularization. By observing that complements already are "regular" (the complement of a subgraph is a full subgraph, the complement of a subset has trivial computational evidence, the exterior of an open set already is regular) we come to *expect* that triple complements are the same thing as complements.


