4

I hope this question isn't too obfuscated (or easy)!

Given a set $S$, let $S_\perp$ denote $\{X \in \mathcal P(S) \mid \forall x, y \in X.\, x=y\}$, the elements of which are subsingletons. In the following $Y_\perp^X$ means $(Y_\perp)^X$.

The question is: does a partial map between $X$ and $Y$ that doesn't have $\emptyset$ in its image determine a subsingleton of maps between $X$ and $Y$ which is non-empty?

The same thing written more accurately with symbols: Assume that we have an element $F$ of $Y_\perp^X$ that doesn't have $\emptyset$ in its image. Can we conclude that there exists an element $F'$ of $(Y^X)_\perp$ such that $F' \neq \emptyset$ and $\forall f' \in F'.\,\forall x \in X.\,f'(x) \in F(x)$?

In the presence of Excluded Middle, this question is easy. In its absence, it seems much harder.

This is my main lead right now:

We assume the the Axiom of Unique Choice.

We need to prove that $$\begin{align} \forall x\in X. (\forall y, y'. \phi(x,y) \wedge \phi(x,y') \implies y=y') \wedge (\neg\neg\exists y \in Y. \phi(x,y)) \tag{1} \end{align}$$ implies $$\begin{align} \neg\neg \exists f \in Y^X. \phi(x,f(x)). \tag 2 \end{align}$$

We can use the fact that $p \implies q$ implies $\neg\neg p \implies \neg\neg q$, and the Principle of Unique Choice. The calculations seem quite difficult. We would need to get (1) into the form $$\begin{align} \neg\neg(\forall x\in X. (\forall y, y'. \phi(x,y) \wedge \phi(x,y') \implies y=y') \wedge \exists y \in Y. \phi(x,y)) \tag{1'} \end{align}$$

wlad
  • 4,823
  • 1
    Maps from $Z$ to $(Y_\bot)^X$ are in one-to-one correspondence with maps from subsets $R\subseteq Z\times X$ to $Y$, and maps to the subset of $(Y_\bot)^X$ singled out by "no $\varnothing$ in the image" corresponds to those $R$ with $\forall\ z\ {x\mid(z,x)\in R}\ne\varnothing$. Maps from $Z$ to $(Y^X)\bot$ are in one-to-one correspondence with maps from subsets $Z'\times X\subseteq Z\times X$ to $Y$, where $Z'$ is any subset of $Z$, and maps to the subset of $(Y^X)\bot$ singled out by "not $\varnothing$" corresponds to those $Z'$ with $Z'\times X\ne\varnothing$. – მამუკა ჯიბლაძე Dec 07 '19 at 20:59

1 Answers1

5

Under Unique Choice, this implies ¬¬LEM.

Let $X=\Omega$ be the set of truth values, let $Y=2\subseteq\Omega$, and let $\phi$ be equality.

Then $\phi$ is a partial function, and $\neg \neg (x = \bot \lor x = \top)$ holds for any $x$, so the statement would imply that $\neg\neg \exists f:2^\Omega.\forall x:\Omega.x=f(x)$, so $\neg\neg\forall x:\Omega.x=\bot \lor x=\top$, which is ¬¬LEM.

Jem
  • 721
  • 5
  • 8
  • $\neg \neg (p \vee \neg p)$ is an intuitionistic tautology, I think – wlad Dec 08 '19 at 19:59
  • Assume $\neg (p \vee \neg p)$. We conclude both $p$ and $\neg p$, which is a contradiction. So it's a tautology – wlad Dec 08 '19 at 20:06
  • 3
    ¬¬LEM is the statement that $\neg \neg \forall x:\Omega.x \lor \neg x$, and is considerably stronger than the tautology $ \forall x:\Omega.\neg \neg (x \lor \neg x)$. In particular, if $\phi$ is provable classically, then ¬¬LEM implies $\neg \neg \phi$. – Jem Dec 08 '19 at 20:11
  • You're right. Good stuff – wlad Dec 08 '19 at 20:19
  • I wonder how strong ¬¬LEM really is – wlad Dec 08 '19 at 20:30
  • I'm uncertain how strong it actually is, but there are a fair number of axioms compatible with constructive mathematics that are anti-classical, in that they imply ¬LEM. So ¬¬LEM would in turn refute all these anti-classical axioms. So for instance, it would imply something like, 'not all total functions on the reals are uniformly continuous,' I think. – Dan Doel Dec 10 '19 at 23:32