4
$\begingroup$

In Bishop and Bridges' "Constructive analysis" on page 17 there is a note with explanation that

If $f\colon A\to B$, $g\colon B\to A$, and $g(f(a))=a$ for all $a$ in $A$, then the function $g$ is called a left inverse of $f$ and the function $f$ is called a right inverse of $g$. (Note that $f$ has a left inverse if and only if it is one-one, in the sense that $a = a'$ for all elements $a, a'$ of $A$ with $f(a) = f(a'))$

The "left inverse implies one-one" direction is clear to me, but I can't find the way to make it work the other way around constructively. Besides the fact that it's straight up wrong when $A$ is empty and $B$ is inhabited, I can't even make it work with the assumption that $A$ is inhabited.

If $A$ is inhabited, let $c \in A$. My intuition for building such a $g$ is like follows: for any $b\in B$, if $b = f(a)$ for some $a\in A$ set $g(b) = a$, otherwise set $g(b) = c$. The problem here is that I'm assuming that there either is such an $a$ or there isn't, i.e. I'm using the law of excluded middle. Can you help me figure out how to avoid using it?

$\endgroup$
12
  • 1
    $\begingroup$ @MauroALLEGRANZA, he is asking about the opposite direction: assume $f$ is injective. Show that $f$ has a left inverse. $\endgroup$ Commented Nov 5 at 11:28
  • 1
    $\begingroup$ @Naïm Camille Favier: Bishop has a famous quote "choice is implied by the very meaning of existence" on page 12 of the same book. It was written with a somewhat different perspective than much of contemporary constructive mathematics. It seems to me that most or all of Bishop's book can be interpreted in higher-order Heyting arithmetic which includes the axiom of choice and does not prove excluded middle. This may be better than my poor attempts at explanation - mathoverflow.net/questions/260445/… $\endgroup$ Commented Nov 5 at 14:09
  • 1
    $\begingroup$ @CarlMummert On page 13 there is a clarifying note, that basically says that the "choice function" here is really an "operation", i.e. it doesn't have to preserve equality. Which is why Bishop accepts choice on index sets where extensional equality coincides with the intensional one, like on natural numbers, for example. $\endgroup$ Commented Nov 5 at 14:47
  • 1
    $\begingroup$ Right, but Bishop doesn't mention the range. It is true constructively that $f$ has a partial left inverse defined on its range, but this is not what the remark says. I think it is just an oversight. $\endgroup$ Commented Nov 5 at 15:33
  • 1
    $\begingroup$ @CarlMummert yeah, I think that works. I think the range can be defined to contain elements that are pairs $(b, p)$, where $b \in B$ and $p$ is a proof that $\exists a \in A, f(a) = b$ equipped with equality $(b, p) = (b', p') \iff b = b'$. And then there is an inverse, but it doesn't seem to be possible to build an inverse from $B$ to $A$. $\endgroup$ Commented Nov 5 at 15:33

1 Answer 1

Reset to default
2
$\begingroup$

This is indeed nonconstructive. Take a proposition $P$ and let $f : 1 + P \to 1 + 1$ be the obvious componentwise map. It's not hard to show that $f$ is injective. Assume $f$ has a left inverse $g : 1 + 1 \to 1 + P$. Then we either have $g(\iota_2(\ast)) = \iota_2(p)$, in which case $P$ holds, or $g(\iota_2(\ast)) = \iota_1(\ast)$, in which case $P$ cannot hold (assume $p : P$, then $g(\iota_2(\ast)) = g(f(\iota_2(p))) = \iota_2(p)$, a contradiction). So this claim (assuming $A$ is inhabited) is equivalent to the law of excluded middle.

$\endgroup$
2
  • $\begingroup$ Do I understand correctly, here $P$ is thought of as the set of proofs of $P$, where all the proofs are considered equal, and $1$ is the set $\{*\}$? $\endgroup$ Commented Nov 5 at 11:45
  • 1
    $\begingroup$ Yes. I am working in type theory where propositions are types all of whose elements are equal, but you may translate this into set theory by taking the set $\{\ast \mid P\}$. $\endgroup$ Commented Nov 5 at 11:46

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.