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}$$

  • 1
    $\begingroup$ 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$. $\endgroup$ – მამუკა ჯიბლაძე Dec 7 '19 at 20:59

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.

  • $\begingroup$ $\neg \neg (p \vee \neg p)$ is an intuitionistic tautology, I think $\endgroup$ – jkabrg Dec 8 '19 at 19:59
  • $\begingroup$ Assume $\neg (p \vee \neg p)$. We conclude both $p$ and $\neg p$, which is a contradiction. So it's a tautology $\endgroup$ – jkabrg Dec 8 '19 at 20:06
  • 3
    $\begingroup$ ¬¬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$. $\endgroup$ – Jem Dec 8 '19 at 20:11
  • $\begingroup$ You're right. Good stuff $\endgroup$ – jkabrg Dec 8 '19 at 20:19
  • $\begingroup$ I wonder how strong ¬¬LEM really is $\endgroup$ – jkabrg Dec 8 '19 at 20:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.