Understanding Troelstra's Uniformity Principle in Constructive Mathematics I have seen Troelstra's Uniformity Principle stated as:
$\forall x \exists n R(x,n) \rightarrow \exists n \forall x R(x,n)$
where $x$ ranges over $\mathbb{P(N)}$ and $n$ ranges over $\mathbb{N}$.
Unless I'm misunderstanding something, this is obviously false in classical mathematics. For example, take $R$ to be the relation $R(x,n)$ iff $n$ is the smallest element of $x$, or $x$ is the empty set and $n=0$.
What is it about constructive mathematics that makes this counterexample invalid there?
Would the principle be classically valid if $x$ was restricted to recursive sets?
Or am I misunderstanding something?
 A: You have stated Troelstra's Uniformithy Principle correctly (contrary to François's claim). There are two reasons why your counterexample does not work. First, we cannot show that every $X \subseteq \mathbb{N}$ is empty or not. Second, we cannot show that every inhabited subset of $\mathbb{N}$ has a minimal element. And we do not need any story about constructivism here. As soon as we assume the Uniformity Principle, it follows that:


*

*Not every $X \subseteq \mathbb{N}$ is empty or not, because that would allows us to form the non-uniform total relation $(X = \emptyset \implies n = 1) \land (X \neq \emptyset \implies n = 42)$.

*Not every inhabited subset $X \subseteq \mathbb{N}$ has a minimal element, because that would allow us to form the non-uniform total relation $\min (X \cup \lbrace 42 \rbrace) = n$.
[I added this paragraph later.] Even without the uniformity principle we cannot expect the two statements to be constructively valid because they imply (a restricted form of) excludded middle:


*

*If every set is empty or not, given any truth value $p \in \Omega$, consider the set $\lbrace \star \mid p \rbrace$: it is either empty or not, therefore either $\lnot p$ or $\lnot\lnot p$, which is a restricted form of excluded middle. [EDIT: thanks to Andreas Blass for pointing out an error here.] 

*If every inhabited set of natural numbers has a minimum, given any truth value $p \in \Omega$, the minimum of the set $\lbrace n \in \mathbb{N} \mid n > 1 \lor p\rbrace$ is either $0$ or not, therfore either $p$ or $\lnot p$, which is excluded middle.
There is no hope to make the Uniformity Principle classically valid, even if we try to restrict to a subfamily of sets:
Theorem: Suppose excluded middle holds and $S \subseteq \mathcal{P}(\mathbb{N})$ is an inhabited family which satisfies the uniformity principle $(\forall X \in S \exists n \in \mathbb{N} . R(X,n)) \implies \exists n \in \mathbb{N} \forall X \in S . R(X, n)$. Then $S$ contains exactly one set.
Proof. Easy exercise. But let's do it anyway. There is an inhabitant $X_0 \in S$. Define the map $f : S \to \mathbb{N}$ by (use of excluded middle coming up...)
$$f(X) = \begin{cases}
42 & \text{if $X = X_0$} \\\\
23 & \text{if $X \neq X_0$}
\end{cases}$$
Let $R(X,n)$ be the relation $f(X) = n$. Since $n = 42$ is the only $n$ related to $X_0$, by Uniformity Principle for $S$ we have $\forall X \in S . f(X) = 42$, therefore $\forall X \in S . X = X_0$. QED.
That is, Troelstra's Uniformity Principle is a very non-classical axiom. I disagree that it is a continuity principle. It does not allow one to prove any of the usual continuity statements "all maps are continuous".
A: The reason why your proposed example is invalid is that equality of sets is not constructively decidable and, in particular, one cannot constructively check whether a set is empty or not. Indeed, checking that $X = \varnothing$ amounts to checking that $n \notin X$ for every $n$, which is not a finite process. Restricting to computable sets does not help. For example, define $X_e$ to be the set of all $s \in \mathbb{N}$ such that the $e$-th Turing machine halts (with blank input) in at most $s$ steps. Deciding whether $X_e = \varnothing$ is equivalent to the halting problem.
That said, your formulation for Troelstra's Uniformity Principle is not correct since it is invalid when $R(X,n)$ is the statement $(0 \in X \rightarrow n = 0) \land (0 \notin X \rightarrow n = 1)$. (I understand that $X$ is a complemented subset of $\mathbb{N}$, which is the usual convention in this context.) The mantra for uniformity principles is that every total function is continuous. Thus your statement is correct if $X$ ranges over $[0,1]$ or $\mathbb{R}$ (which are connected) but not over $\mathcal{P}(\mathbb{N})$ or $\mathbb{N}^\mathbb{N}$ (which are totally disconnected). Thus all continuous functions $[0,1]\to\mathbb{N}$ are constant but there are a larger variety of continuous functions on $\mathcal{P}(\mathbb{N})$. Namely, if $f:\mathcal{P}(k)\to\mathbb{N}$ is any function where $k = \lbrace 0,\dots,k-1\rbrace$, then $F(X) = f(X \cap k)$ defines a continuous function on $\mathcal{P}(\mathbb{N})$ and every continuous function $\mathcal{P}(\mathbb{N})\to\mathbb{N}$ is of this form for some $k$. Thus a correct version of the uniformity principle for $\mathcal{P}(\mathbb{N})$ has the weaker conclusion where the $n$ satisfying $R(X,n)$ is given by such a function.
As Andrej pointed out, the above was confusing the Uniformity Principle with the Continuity Principle. Though they are similar in some ways they occur in different constructive systems and, in particular, the Uniformity Principle does not not occur in contexts where subsets of $\mathbb{N}$ are complemented.
