Return to Answer

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:

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

2. 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 excludded middle:

1. 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 $p$.

2. 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$.

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

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:

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

2. 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:

1. 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.]

2. 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".

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:

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

2. 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$.

There is no hope to make the 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".

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:

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

2. 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 excludded middle:

1. 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 $p$.

2. 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$.

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

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.

There is no hope to make the 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 at most 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".

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:

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

2. 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$.

There is no hope to make the 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".