Mathematics without the principle of unique choice

Question

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).

Answer 1

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).

Answer 2

Posting on behalf of Milli Maietti.

A foundation for constructive mathematics without unique choice is the Minimalist Foundation (MF) ideated in

Maietti, Sambin, Towards a minimalist foundation for constructive mathematics

and completed in

Maietti, A minimalist two-level foundation for constructive mathematics

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

Maietti, Sambin, Why topology in the minimalist foundation must be pointfree

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

Maietti, Rosolini, Quotient completion for the foundation of constructive mathematics

as a generalization of the ex/lex completion.

Answer 3

I am not sure whether Yannick Forster is hanging out around here, so allow me to refer you to his PhD thesis and his recent research.

Yannick uses the following setup to carry out synthetic computability theory (see his home page to get a feel for how much computability theory he handles):

• calculus of inductive constructions
• a Prop with excluded middle
• a form of Church's thesis "all functions are computable"

At first sight this looks contradictory because Church's thesis and excluded middle together produce a contradiction, as we can diagonalize to produce a non-computable function $f : \mathbb{N} \to \mathbb{N}$:

$$ f(n) = \begin{cases} k + 1 & \text{if $n$-th computable function outputs $k$ on input $n$}\\ 42 \text{otherwise} \end{cases} $$ Now, $f$ is total by excluded middle, hence there is some $m \in \mathbb{N}$ such that $f$ is the $m$-th computable function, but then we get $f(m) = f(m) + 1$.

Actually, the above proof secretly used unique choice. When we write down the definition of $f$ carefully, we notice that we actually gave the graph of $f$: $$F(n,k) \iff (\text{$n$-th machine on input $n$ outputs $k$}) \lor ((\text{$n$-th machine on input $n$ diverges}) \land k = 42) $$

Luckily, unique choice is not validated by the calculus of inductive constructions.

Answer 4

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.

Answer 5

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.

Answer 6

Your question does not distinguish between classical or constructive math, so I will provide an answer for the former.

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

In [1, 2] below, Dag Normann and I show that the following are equivalent in Kohlenbach's higher-order RM ([0)), where item (o) is a weak fragment of PUC. Here, strongly countable means that there is a bijection from the set to $\mathbb{N}$.

o) For $Y^2$, $(\forall n \in \mathbb{N})(\exists! f \in \mathbb{N}^{\mathbb{N}})(Y(f, n)=0 )$ implies $(\exists g:\mathbb{N}\rightarrow\mathbb{N}^\mathbb{N})(\forall n \in \mathbb{N})(Y(g(n), n)=0) $.

a) every strongly countable set $A\subset [0, 1]$ can be enumerated.

b) every strongly countable set in $2^{\mathbb{N}}$ has a supremum.

c) and many more

As you can see, mathematics without PUC would look mighty strange, even classically.

References

[0] U. Kohlenbach Higher order reverse mathematics, Reverse mathematics 2001, Lect. Notes Log., vol. 21, ASL, 2005, pp. 281–295.

[1] D. Normann and S. Sanders, On robust thms due to Cantor, Weierstrass, and Heine-Borel, Submitted, arxiv: https://arxiv.org/abs/2102.04787

[2] S. Sanders. Countable sets versus sets that are countable, Submitted, https://arxiv.org/abs/2011.01772