I have a hunch I need to figure out versions of unique choice or definite description for partial and multi-valued functions. But I'm entirely confused about how you'd axiomize partial or multi-valued versions of choice.

I am most familiar with Coq but I would totally be interested in how other assistants and foundations deal with these issues.

Constructive principle of unique choice ought to be the statement an entire functional relation is a function

Axiom puc: forall {A B} (P: A -> B -> Prop), (forall x, exists! y. P x y) -> { f: A -> B | forall x, P x (f x) }.

A partial version ought to be "a functional relation is a partial function"

Axiom partial_puc: forall {A B} (P: A -> B -> Prop), (forall x, ! y. P x y) -> { f: A -> option B | (forall x y, P x y <=> f x = Some y) /\ forall x, (forall y, not (P x y)) <=> f x = None }.

A multi-valued version ought to be "a functional relation is a multi valued function". I think you want to map relations to uncountable streams of results here.

Axiom multi_puc: forall {A B} (P: A -> B -> Prop), (forall x, exists y. P x y) -> { f: A -> (nat -> Prop) -> B | forall x y, P x (f x y) }.

Combined you would want something like "a relation is a partial multi-valued function".

Axiom partial_multi_puc: forall {A B} (P: A -> B -> Prop), { f: A -> option (nat -> Prop) | (forall x y, P x y <=> exists z w, f x = Some z /\ z w = y) /\ forall x, f x = None <=> forall y, not (P x y)}.

I am not at all sure these are the "right" ways to axiomize partial and multi-valued versions of unique choice. These axioms all seem very suspicious to me. Even if these axioms happen to work out there have to be more standard versions of these.

  • $\begingroup$ Where did nat come from? $\endgroup$ Oct 25, 2022 at 6:00
  • $\begingroup$ @AndrejBauer I was going to use the reals but I remembered classically 2^N is the same size? Pretty sure $\Omega^{\mathbb{N}}$ is usually uncountable anyhow. $\endgroup$ Oct 25, 2022 at 21:40
  • $\begingroup$ What has size got to do with the question? $\endgroup$ Oct 26, 2022 at 6:24

1 Answer 1


The principles you seek are there, but they are simply true, unless you work with a hampered foundation or you mix things up and phrase them badly. Allow me to give a short overview. I trust you will be able to pick and choose from it what you need.

I shall work in set theory, and comment on type theory at the end. Write $\Omega$ for the set of all propositions (in type theory usually written as $\mathsf{Prop}$), so the predicates on a set $A$ are the same thing as maps $A \to \Omega$. We also identify the powerset $P(A)$ with $A \to \Omega$. Thus for $S \in P(A)$ the notation $x \in S$ is just shorthand for $S x$.

The singleton $\{x\}$ corresponding to a given $x \in A$ is the map $\{x\} : A \to \Omega$ defined by $\{x\} y = (x = y)$, which is just the transposition of identity ${=} : A \times A \to \Omega$.

To deal with partial maps we define for each set $A$ its set of partial elements $\tilde{A}$ by $$\tilde{A} = \{p : A \to \Omega \mid \forall x, y \in A .\, p x \land p y \Rightarrow x = y \}.$$ We think of $\emptyset$ as “undefined” and a singleton $\{x\}$ as “defined” (and there are no other elements in $\tilde{A}$). Do not confuse $\tilde{A}$ with $1 + A$, or $\mathsf{option}(A)$, for $\tilde{A} \cong 1 + A$ implies excluded middle! A partial map from $X$ to $Y$ can be thought of as a map $X \to \tilde{Y}$.

To deal with multivalued maps, define for each set $A$ the set of multivalues $P_*(A)$ by $$P_*(A) = \{ p : A \to \Omega \mid \exists x \in A .\, p x\}.$$ A multivalued map from $X$ to $Y$ can be thought of as a map $X \to P_*(Y)$.

Let us also define the somewhat silly looking $$ S(A) = \tilde{A} \cap P_*(A) = \{p : A \to \Omega \mid \exists x \in A . p x \land \forall y \in A . p y \Rightarrow x = y \}. $$ It is the set of all singletons of $A$. The inverse $\iota : S(A) \to A$ of the singleton map $\{{-}\} : A \to S(A)$ is known as the definite description operator. Its existence is equivalent to unique choice.

A relation $\phi : A \times B \to \Omega$ is:

  • single-valued when $\forall x \in A . \forall y, z \in B . \phi(x,y) \land \phi(x,z) \Rightarrow y = z$,
  • total when $\forall x \in A . \exists y \in B . \phi (x, y)$,
  • functional when it is total and single-valued.

We may now write down three principles which are simply true:

  1. Single-valued relations $A \times B \to \Omega$ are in bijective correspondence with maps $A \to \tilde{B}$.
  2. Total relations $A \times B \to \Omega$ are in bijective correspondence with maps $A \to P_*(B)$.
  3. Functional relations $A \times B \to \Omega$ are in bijective correspondence with maps $A \to S(B)$.

In all three cases the proof goes as follows: a relation $\phi : A \times B \to \Omega$ may be transposed to a map $\overline{\phi} : A \to (B \to \Omega)$ defined by $\overline{\phi} x = \lambda y . \phi(x,y)$, which is precisely the one we're looking for in each of the three cases.

The above three principles are equivalent to the logical statements, for $\phi : A \times B \to \Omega$:

  1. A single-valued relation is the graph of a partial map: \begin{multline*} (\forall x \in A . \forall y, z \in B . \phi (x, y) \land \phi x z \Rightarrow y = z) \Rightarrow \\ \exists f : A \to \tilde{B} . \forall x \in A . \forall y \in B . (p x y \Leftrightarrow y \in f(x)). \end{multline*}

  2. A total relation is the graph of a multivalued map: \begin{multline*} (\forall x \in A . \exists y \in B . \phi (x, y)) \Rightarrow \exists f : A \to P_*(B) . \forall x \in A . \forall y \in B . (p x y \Leftrightarrow y \in f(x)). \end{multline*}

  3. A functional relation is the graph of a singleton-valued map: \begin{multline*} (\forall x \in A . \exists! y \in B . \phi (x, y)) \Rightarrow \exists f : A \to S(B) . \forall x \in A . \forall y \in B . (p x y \Leftrightarrow y \in f(x)). \end{multline*}

I will leave these as exercises – they are all true.

If unique choice holds then the definite description operator $\iota$ can be used to replace $S(B)$ with $B$: \begin{multline*} (\forall x \in A . \exists! y \in B . \phi (x, y)) \Rightarrow \exists f : A \to B . \forall x \in A . \forall y \in B . (p x y \Leftrightarrow y = f(x)). \end{multline*} This form is the usual statement of unique choice. It implies the existence of $\iota$.

Observe that $A \mapsto \tilde{A}$, $A \mapsto P_*(A)$ and $A \mapsto S(A)$ are all monads (and the last one is trivial when unique choice holds). The monad structure is induced by the covariant powerset monad.

By altering the monads we obtain variations.

For example, if we replace $\Omega$ with decidable truth values $\mathsf{Bool} = \{p \in \Omega \mid p \lor \neg p\}$, then $P(A)$ is the set of decidable subsets of $A$ and $\tilde{A} \cong 1 + A$ (also known as $\mathsf{option}(A)$ in type theory).

Another example is $\Omega$ is replaced with semidecidable truth values $$\Sigma = \{p \in \Omega \mid \exists f : \mathbb{N} \to \mathsf{Bool} . (p \Leftrightarrow \exists n . f n)\}.$$ In type theory this one is known as the delay monad.

When we switch from set theory to type theory we may replace $\Omega$ with $\mathsf{Prop}$ (or even $\mathsf{Type}$). The principles will still hold, and the existence of $\iota$ will hinge on the usual nuances about $\Sigma$ vs. $\exists$ and elimination from propositions into types.

  • $\begingroup$ Huh thanks. I definitely need to go over this more but this gives me a lot to play with. $\endgroup$ Oct 25, 2022 at 21:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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