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:
-
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.
-
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).
Best Answer
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):
And a later addendum (1985) by Bridges (page 13, chptr 1. Notes):
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).