Implicit functions from relations

A common way to define functions is implicitly in terms of relations. Suppose R is a relation on $A \times B$ and we know that for every $x \in A$ there is a unique y in B such that R(x, y). Then we expect to have a function $f \in A \rightarrow B$ such that R(x, f(x)). How do we specify this function?

To facilitate consideration of this matter, let us define $\exists ! y\!:\!A.\ P(y)$ to mean there is a y satisfying P, and any z that satisfies it is y. Thus

Definition 11   $\exists !y\!:\!A.\ P(y)== \exists y\!:\!A.\ P(y)\ \&\ \forall z\!:\!A.\ (P(z) \Rightarrow y=z$ in A).

We expect the following formula to be true. function comprehensioncomprehension $\forall x\!:\!A.\ \exists !y\!:\!B.\ R(x, y) \Rightarrow \exists f\!:\!A \rightarrow B.\ \forall x\!:\!A.\ R\left(x, f(x)\right)$. For many instances of types A, B and relation R we can prove this formula by exhibiting a specific function. For example, if we define Root(n, r) for n, r in N as $r^2 \leq n\ \&\ n <(r+1)^2$then not only can we prove $\forall x\!:\!N.\ \exists !r\!:\!N.\ Root(n, r)$ but we can also define a function root by primitive recursion, namely

root(0)=0

root(suc(n))= if $\left(root(n) +1\right)^2 \leq n$ then $root(n) +1\ else\ root(n)$.

We know that $\lambda\left(x.\ root(x)\right) \in N\rightarrow N$ and $Root\left(n, root(n)\right)$ is true. So perhaps if there are enough expressions for defining functions, we can prove the conjecture.

In set theory, functions are usually defined as single-valued total relations, i.e., a relation R on $A \times B$ is a function iff for all x in A there is a unique y in B such that R(x, y). The relation R is a subset of $A \times B$, and this R is taken to be the function.

If the underlying logic has a choice function (or Hilbert $\in$-operator) as in [16] or HOL ([54]), then the value of the function defined by R on input x is $choice(y.\ R(x, y))$ and a $\lambda$ form for the function is $\lambda(x.\ choice(y.\ R(x, y))$.

The choice operator would not only prove the implicit function conjecture, but it would prove the closely related axiom of choice as well. That axiom is $\forall x\!:\!A.\ \exists y\!:\!B.\ R(x, y) \Rightarrow \exists f\!:\!(A \rightarrow B).\ \forall x\!:\!A.\ R(x, f(x))$. We will see in section 3 that in constructive type theory this axiom is provable because the theory has enough expressions for functions.