LLPO is the statement $\forall x \in \mathbb R. x \leq 0 \vee x \geq 0.$ The statement should be understood as a fragment of the Law of Excluded Middle, rather than a statement about the ordering of the real line. The fragment is usually considered large enough to not be constructive in any reasonable sense.
I have a conjecture on the relation of LLPO to universal statements about dense subspaces, and am looking for a proof or refutation of that conjecture.
As background, consider the following non-constructive statements, which are all provable using LLPO:
-
For every pair of unit vectors $u, v$ in $\mathbb R^3$, there is a unit vector $w \in \mathbb R^3$ such that $u \perp w \perp v$.
-
The Intermediate Value Theorem: For every continuous function $f \in C([0,1])$ with $f(0) \leq 0 \leq f(1)$, there is an $x \in [0,1]$ such that $f(x) = 0$.
-
Every square matrix with entries in $\mathbb C$ has an eigenvector.
Each of these has a universal quantifier over some topological space $T$, which can be replaced with a dense subspace $\hat T$ for which a constructive proof is possible:
-
$T$ = pairs of unit vectors, $\hat T$ = pairs of non-parallel unit vectors. Given non-parallel vectors $u$ and $v$, we use the cross product to set $w := \frac{u \times v}{|u \times v|}$. However, perturbing nearly-parallel vectors slightly can radically alter the set of vectors perpendicular to them.
-
$T$ = continuous functions, $\hat T$ = piecewise-linear functions with rational slopes. However, perturbing a function slightly can radically alter its set of roots.
-
$T$ = matrices, $\hat T$ = matrices whose characteristic polynomials have only simple roots. However, perturbing such matrices slightly can radically alter their eigenspaces.
Has this phenomenon been studied in any generality?
Full statement of conjecture
Given some theory of constructive topology,
- Let $T$ be overt.
- Let $K$ be compact.
- Let $H$ be Hausdorff.
- Let $f, g : T \times K \to H$ be continuous functions.
Then the following two claims entail each other:
$$\text{LLPO} \implies \forall x \in T. \exists y \in K. f(x,y) = g(x,y)$$
$$\exists \hat T \text{ dense in }T. \forall x \in \hat T. \exists y \in K. f(x,y) = g(x,y)
$$
Does anyone have a proof or refutation for this conjecture?
Best Answer
A counterexample to "Stuff provable by $\mathrm{LLPO}$ is constructively true on some dense set" can be built as follows:
We start with two recursively inseparable disjoint c.e. set $A, B \subseteq \mathbb{N}$. Using $\mathrm{LLPO}$ countably many times, we can actually built a "decidable" set $C \subseteq \mathbb{N}$ with $A \subseteq C$ and $B \cap C = \emptyset$. We just use $\mathrm{LLPO}$ to pick a true case between $n \notin A$ and $n \notin B$. Our domain is $\mathbb{N}$, which is as nice as it could be, and has no non-trivial dense subsets.
To put this example into the specified format, we use $T = \mathbb{N}$, $K = \{0,1\}$ and $H = \mathbb{R}$. The function $g$ is constant $0$. To define $f$, we use effective enumerations $(a_n)_{n \in \mathbb{N}}$ of $A$ and $(b_n)_{n \in \mathbb{N}}$ (which exist since $A$ and $B$ are c.e.). We now let $f(n,0) = 2^{-\min \{i \mid a_i = n\}}$, $f(n,0) = 0$ if $n \notin A$, $f(n,1) = 2^{-\min \{i \mid b_i = n\}}$, $f(n,1) = 0$ if $n \notin B$.
The difference between how I've used $\mathrm{LLPO}$ here versus how it is used in your examples is that in your examples the union of the two open sets defined by "Only first answer is correct" and "Only second answer is correct" was dense. But this is not necessary, as the set of instances leading to "Both answers are correct" can have non-empty interior. And getting this interior as an open set is not constructive, but actually needs countably many $\mathrm{LPO}$'s / $\mathrm{ACA}_0$ / $\operatorname{lim}$.
If we use $\mathrm{LLPO}$ just once and use a sufficiently classical metatheory, we can get a dense open set on which the construction is continuous though. Working in a Baire space, we can then even use $\mathrm{LLPO}$ countably many times and get a dense set on which stuff is still continuous.