The principle of unique choice (PUC), also called the principle of function comprehension, says that if $R$ is a relation between two sets $A,B$, and for every $x\in A$ there exists a unique $y\in B$ such that $R(x,y)$, then there exists a function $f:A\to B$ such that $R(x,f(x))$ for every $x\in A$.

In ZF set theory (without the axiom of choice) this principle is provable; indeed it is basically the definition of what it means to be a "function". The same is true in weaker, e.g. intuitionistic set theories, and also for h-sets and h-relations in homotopy type theory / univalent foundations. However, PUC is not provable in (classical or intuitionistic) higher-order logic (HOL) — unless we assert it, or something that implies it, as an additional axiom.

Moreover, there are naturally-arising models of HOL in which PUC fails. For instance, we can take the types to be topological spaces, and the predicates on a space $A$ to be the subspaces of $A$ (subsets with the subspace topology); then a relation $R$ as in PUC corresponds to a span $A \leftarrow R \to B$ in which $R\to A$ is a continuous bijection, but need not have a continuous inverse enabling us to define a continuous map $A\to B$. (To be more precise, it would be better to replace topological spaces by something slightly better-behaved, such as a quasitopos.) We can also take the types to be partial equivalence relations on a partial combinatory algebra, or partial equivalence relations in a tripos.

Constructive mathematicians following Brouwer and Bishop have explored in depth what mathematics looks like in the absence of the full axiom of choice and the law of excluded middle. Usually it's not much different; one just has to take extra care in various places and state various theorems in idiosyncratic ways. Moreover, classical mathematics can be embedded in constructive mathematics, e.g. by judicious insertion of double-negations; thus constructive mathematics is simply "more informative", i.e. it "draws distinctions that classical mathematics ignores".

However, all constructive mathematicians that I know of accept the principle of unique choice. Has anyone seriously explored what mathematics would look like in the absence of PUC? I don't mean simply using the internal language of a quasitopos to prove a few things; I mean a serious development of large swaths of mathematics akin to Bishop's Constructive analysis.

Note that, as is the case with classical and constructive mathematics, ordinary mathematics with PUC should embed into mathematics without PUC by simply interpreting the word "function" to mean a total functional relation as appears in the hypothesis of PUC (which I call an anafunction after Makkai's "anafunctors"). So it seems that mathematics without PUC should again be simply "drawing previously-ignored distinctions", keeping track of which anafunctions are actually functions.

Edit: Frank Waaldijk's answer below points out that I should be more specific about what I mean by "mathematics without PUC", as there is actually more than one way that PUC could fail. In this question I'm thinking about mathematics formalizable (though not necessarily actually formalized) in higher-order logic in one of two ways:

  1. Define "sets" to be types equipped with equivalence relations (or partial equivalence relations), and "functions" to be maps between types ("operations") that preserve these equality relations.

  2. Include "subtypes" and "quotient types" in the logic, and define "sets" to be simply types, and "functions" to be maps between them.

In either case there is also a natural notion of "anafunction", namely a binary relation that is total and functional, and PUC need not hold: not every anafunction is representable by a function. By contrast, we can also formalize mathematics with PUC in HOL in either of these ways by defining a "function" to be such an "anafunction", i.e. a total functional binary relation. For instance, this is what is done semantically in constructing a topos from a tripos.

Frank describes a different approach that is something akin to the following (also in HOL):

  • Define a "set" to be a type equipped with both an equivalence relation of "equality" and a compatible binary relation of inequality or apartness, and define a "function" to be a binary relation between types that is total, functional, and reflects inequality (i.e. is "strongly extensional").

Here we appear to take the "anafunction" route by defining a "function" to be a total functional relation, but we also include "strong extensionality" in the definition of "function". Now PUC fails because a total functional relation need not be strongly extensional. This is also interesting, but it is not what I had in mind.

Of course, the two could be combined: we could define a function to be a map of types that is strongly extensional, so that a total functional relation could fail to be represented by a map of types and also fail to be strongly extensional.

Edit 2: Monroe Eskew points out in the comments yet another situation (again, not the one I'm asking about right now) where a version of PUC can fail, namely in ZF-type set theories without the replacement axiom. In that case one can have a class-relation that is functional and whose domain is a set, but whose codomain is not a set, and hence which does not define a function (a function being required to be itself a set).

  • 1
    $\begingroup$ See perhaps Arnaud Spiwack’s PhD thesis: Verified Computing in Homological Algebra. $\endgroup$ – Vej Kse Jun 5 '18 at 12:11
  • 1
    $\begingroup$ Unique choice is absent from classical reverse maths. It possible that someone has also tried to remove it from constructive reverse maths, but I cannot currently find a precise reference. $\endgroup$ – Bas Spitters Jun 5 '18 at 22:05
  • 3
    $\begingroup$ @MonroeEskew In 1927 Hilbert wrote "taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists." But now we know that he was quite wrong; surprisingly little is lost from mathematics when you take away excluded middle, and there are good reasons to ask the question. It pays to keep an open mind. $\endgroup$ – Mike Shulman Jun 11 '18 at 13:27
  • 3
    $\begingroup$ @MonroeEskew I don't know what you mean by a "foundational perspective", but from a practical perspective, internal languages of all sorts are, I think, undeniably useful. Whether or not one believes the law of excluded middle to be "true", it is a fact that it fails in the internal language of general toposes, and that internal language is a useful tool when studying such toposes. Even more basic logical laws like contraction and weakening fail in the internal languages of monoidal categories, yet the resulting "linear logics" are again a useful tool in their study. $\endgroup$ – Mike Shulman Jun 11 '18 at 18:41
  • 2
    $\begingroup$ (Which is not to disparage the importance of solving specific problems! The two activities are synergistic; trying to solve a specific problem can also often lead to general insights that can then be abstracted and applied to new domains.) $\endgroup$ – Mike Shulman Jun 11 '18 at 23:23

You ask: Has anyone seriously explored what mathematics would look like in the absence of PUC?

Actually, I believe I have done so in my PhD thesis modern intuitionistic topology. Don't let the title mislead you: more than half of the thesis is actually directly acceptable in BISH, and these results are all marked with an asterisk.

In my thesis, I define 'function' precisely according to what you describe, which is the ZF-definition. I have always considered this set-theoretic approach very convenient for a fundamental reunion of Bishop's and Brouwer's perspective. The usual dictum that BISH is a common core of INT and CLASS is actually untrue, since much of Bishop's definitions are too vague and therefore unacceptable in INT. But they can be naturally interpreted when using the ZF-definition, which I adopted in my thesis.

In my thesis, pretty large samples of constructive math are developed using this definition. (I would not call it large swaths, but I do not see any obstruction to expand these samples to large swaths). I can't recall even one instance where PUC would help one to prove more than what can be proven using the ZF-definition.

Just an example: the Dugundji Extension Theorem is proved in this way in chapter three.

Of course, I do use restricted forms of countable choice and dependent choice in my thesis. But that seems a separate issue from what you are asking.

To then specialize to INT or RUSS (recursive mathematics), I found (and find) it very convenient to define special functions, such as spread-functions and computable functions. One shows that these special functions indeed also specify functions (ZF-style), and then one can prove additional INT or RUSS results using either INT or RUSS choice axioms.

So I'm fairly confident in my answer that yes, large parts of constructive mathematics can be developed without PUC.

Update to reflect the comments below:

In my thesis the definition of function (0.1.3) essentially runs like this:

Let $(X,\#_1), (Y,\#_2)$ be apartness spaces, then $f\subset X\times Y$ is called a function iff:

(i) $\forall x\in X\ \exists y\in Y\ [\,(x,y)\in f\,]$

(ii) $\forall x,w\in X\ \forall y,z\in Y\ [\,((x,y)\in f\wedge(w,z)\in f\wedge y\#_2 z) \rightarrow x\#_1 w\,]\,$

With this definition of function, large samples of constructive math are developed, like I said. This does not require any form of PUC, and it is debatable whether PUC even holds in general with this definition.

That depends on how literal one wants to interpret PUC, and whether one wishes to include equivalence/apartness relations which are not the 'simple' Baire space equivalence/apartness.

But even to say that with this definition PUC holds for Baire space, is to interpret the quantifier $\exists!$ in a very specific way. Because one cannot derive (ii) from the usual interpretation of $\forall x \exists! y$.

Second update to reflect further comments below:

First I would like to recommend the OP's paper Linear logic for constructive mathematics. I find it well written and it gives a promising (meta-)insight how to resolve annoying deficiencies of constructive logic, especially when constructivizing classical definitions.

Second, let me repeat that the above definition of function is far from the usual one in BISH (which is very vague!, see chptr. 2 def. 1.1 of Constructive Analysis [Bishop&Bridges1985]). It therefore stands alone in BISH, and it is not a trivial result that with this definition large parts of BISH can be developed.

Moreover, in BISH there is a real necessity for PUC as an axiom, since it does not follow at all from the definition of function and the other axioms. I give the following quotes (page 12, chptr. 1 'A constructivist manifesto' written in 1967):

A choice function exists in constructive mathematics, because a choice is implied by the very meaning of existence.

And a later addendum (1985) by Bridges (page 13, chptr 1. Notes):

At first sight, Bishop' remark, "A choice function exists in constructive mathematics, because a choice is implied by the very meaning of existence", appears to be contradicted by counterexamples of the sort discussed in connection with the least-upper-bound principle. In fact, there is no contradiction here. To see this, consider a paraphrase of Bishop's remark: if to each $x$ in a set $A$ there corresponds an element $y$ of a set $B$ such that a given property $P(x, y)$ holds, then it is implied by the very meaning of existence in constructive mathematics that there is a finite routine for computing an appropriate $y \in B$ from a given $x \in A$; although this routine may not be a function relative to the given equality relation on $A$, it is a function relative to the equality relation of identity (intensional equality) on A, in which two elements are equal if and only if they are given as identically the same object.

With the relational definition given in my thesis, there is no need for PUC as an axiom, like I said. And this remains so even if one interprets the quantifier $\exists!$ in such a way that PUC is validated for the natural apartness on Baire space. This natural apartness is not an extra structure, but the intuitionistic (and constructive!) way of handling equality. It corresponds rather precisely I believe to the linear-logic way of defining inequality (in the OP's paper mentioned above).

  • 2
    $\begingroup$ I don't understand what you are saying; the ZF-definition of function makes PUC true by definition. $\endgroup$ – Mike Shulman Jun 6 '18 at 3:50
  • $\begingroup$ I was probably too brief, I will expand a bit more in an update. $\endgroup$ – Frank Waaldijk Jun 6 '18 at 21:57
  • $\begingroup$ Ah, I see. I don't really think the question of whether all functions should be assumed strongly extensional is much related to PUC, though. In particular, in intuitionistic logic the presence of an apartness relation is extra structure on a set, and so a notion like "strongly extensional" which depends on such structure can't sensibly appear in a foundational principle like PUC. $\endgroup$ – Mike Shulman Jun 8 '18 at 20:34
  • 1
    $\begingroup$ By contrast, in the linear logic of arxiv.org/abs/1805.07518, inequality relations on every set are "built into the logic", but in this case they are also built into the notion of "unique existence", so that PUC can hold (but doesn't have to). $\endgroup$ – Mike Shulman Jun 8 '18 at 20:35
  • 2
    $\begingroup$ Hmm... maybe I understand better now what you are getting at: PUC could fail in other ways than the one I had in mind. I'll update the question to clarify what I'm asking about. $\endgroup$ – Mike Shulman Jun 9 '18 at 18:15

Posting on behalf of Milli Maietti.

A foundation for constructive mathematics without unique choice is the

Minimalist Foundation (MF) ideated in


and completed in


This is meant as a base system to formalize constructive point-free topology and perform constructive reverse mathematics, where

  • Dedekind reals and Cauchy reals defined in terms of functional relations do not form a set

(only Cauchy type-theoretic reals do form a set), even in the classical extension of MF with excluded middle as explained in


A quotient completion of a tripos which does not impose unique choice has been introduced in


as a generalization of the ex/lex completion.


In a Bishop setting without any form of choice, while PUC does not hold generally, there are codomains for which it is provable, in a way that perhaps feels trivial. For the simplest example I can think of, given some set $B$ (equipped with an equality relation), consider the set of singleton subsets of $B$, $$S(B) := \{ X \in \mathscr{P}(B) \mid X \text{ inhabited and } x = y \text{ for all } x,y \in X\},$$ with equality just the usual equality of subsets ($X = Y$ when $x \in X$ iff $x \in Y$). Now, given a total functional relation $R$ over $A \times S(B)$, we can define $f:A \to S(B)$ by $$ f(a) := \{ b \in B \mid \text{for all } Y \in S(B), R(a, Y) \text{ implies } b \in Y \}.$$ It is not difficult to show (1) $f(a) \in S(B)$ for $a \in A$, (2) $R(a,Y)$ implies $Y = f(a)$ for $a \in A$, $Y \in S(B)$, (3) $R(a,f(a))$ for $a \in A$, and (4) $f$ respects equality on $A$. That proves PUC for codomain $S(B)$.

This is of course not magic, since we still need a choice function to recover anything from an element of $S(B)$. In a sense, we've just "flattened" two applications of choice into one.

You may well ask why you'd ever want to use this particular codomain, since it's basically just the classical definition of equivalence classes, avoiding which was the whole point of Bishop's idea of sets equipped with equality relations. Well, for basically the same reason as for $S(B)$, PUC is provable for the codomain of the Dedekind reals.

Another example of a codomain for which PUC is provable is Richman's construction of the completion of a metric space $X$ as a subset of $\mathbb{Q}^{+} \to \mathscr{P}(X)$ satisfying Cauchy-like criteria [1]. It's notable that Richman's motivation for the construction was to avoid (countable/dependent) choice. (I've also seen this construction referred to as Cauchy approximations.) I would argue that the "best" definition of metric completion is the terminal object of an appropriate category (specifically, the objects under a metric space $X$ in the category of dense isometries). If you accept that, then it follows that PUC is provable when the codomain is a metric completion, at least in this foundational setting (since Richman's construction has the corresponding universal property).

So, at least in this foundational setting, large swaths of mathematics (particularly analysis) remain unchanged without PUC, since it is simply provable (in perhaps an unsatisfying way) for many codomains of interest, particularly the reals and any other complete metric space.

[1] Richman, Fred, Real numbers and other completions, Math. Log. Q. 54, No. 1, 98-108 (2008). ZBL1134.03041.

  • 1
    $\begingroup$ This is a good point. In tripos-theoretic language, these are the "weakly complete" sets. The absence of PUC seems only to matter for "predicative" sets whose construction doesn't involve powersets, such as $\mathbb{N},\mathbb{Z},\mathbb{Q}$, and the ordinary Cauchy reals. And I wouldn't be surprised if PUC also held automatically, at least in some contexts, for sets like $\mathbb{N},\mathbb{Z},\mathbb{Q}$ that can be defined without any quotients, i.e. such that their setoid equality is Leibniz equality. $\endgroup$ – Mike Shulman Jun 13 '18 at 15:51

Rather than giving an answer, I decided to include a description of how exactly is $\exists!$ reflected in topos-theoretic context and how does it give meaning to the slogan "unique existence implies global existence". The oldest text I've seen where this occurs is Freyd's "Aspects of topoi" (Bull. Austral. Math. Soc. 7 (1972) 1--76, Proposition 2.21 on page 22)

For $f:X\to Y$, let $i_f:Q_f\rightarrowtail X$ be the equalizer of the singleton map $\{\_\}:X\to\mathscr PX$ with the composite $$ X\xrightarrow fY\xrightarrow{f^{-1}}\mathscr PX $$ where $\mathscr PX$ is the powerset, $\{\_\}$ is the transpose of the equality $X\times X\to\mathscr P1$ (classifying the diagonal $(1_X,1_X):X\rightarrowtail X\times X$) while $f^{-1}:Y\to\mathscr PX$ is the transpose of the map $X\times Y\to\mathscr P1$ classifying the graph $(1_X,f):X\rightarrowtail X\times Y$ of $f$.

Then it can be proved that this $i_f:Q_f\rightarrowtail X$ enjoys the following universal property: the square $\require{AMScd}$ \begin{CD} Q_f @>i_f>> X\\ @| @VV f V\\ Q_f @>f\circ i_f>> Y \end{CD} is pullback, and for any other pullback square \begin{CD} Q@>g>> X\\ @| @VVfV\\ Q @>f\circ g>> Y \end{CD} the map $f\circ g:Q\to Y$ factors through $f\circ i_f:Q_f\to Y$.

It thus solves the problem of finding the "largest" $g:Q\to Y$ such that $g^*(f):X\times_YQ\to Q$ is an isomorphism.

The main reason I decided to mention this is that it raises natural questions - (a) whether having such "UE pullbacks" (that is, the ones with the above universal property) is the correct reexpression of the PUE in categorical semantics, and (b) whether the full topos structure is implied by having them. I doubt this last one, actually.


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.