5

In classical mathematics, following two statements are equivalent:

  1. If $f(x) = f(y)$ then $x = y$ for each $x$ and $y$.

  2. If $x\neq y$ then $f(x)\neq f(y)$ for each $x$ and $y$.

However, in a constructive sense, they could not be equivalent. Clearly, 1 implies 2, but the other direction is not trivial.

My question is:

a) Is there a counterexample $f$ (in constructive sense) satisfying 2. but not 1.? I think some function over reals (I even don't know about real numbers in the constructive sense!) might be a counterexample, but I can't find it.

b) Consider the function $f:\Bbb{N}\to\Bbb{N}$. If $f$ satisfies 2 then it should satisfy 1? For computable $f$ it seems trivial but I don't certain in case of more complex $f$.

Thanks for any help!

Hanul Jeon
  • 27,376
  • I would argue that even $(1)\implies(2)$ is not so trivial. – Nicolas M. Gutierrez May 08 '21 at 20:24
  • 1
    In page 63 of Constructive Analysis by Bishop and Bridges, your definition 1 is called weakly injective, while your definition 2 is called injective. Considering mappings $f$ from an interval $I$ into $\mathbb{R}$, they ask one to prove that the following statements are equivalent:
    1. Every weakly injective map $f:[0,1]\to\mathbb{R}$ is injective.
    2. If $x$ is a real number such that the equality $x = 0$ is impossible, then $x\neq 0$.
    3. For each sequence $(x_n„)$ in ${0,1}$, if it is impossible that $x_n=0$ for all $n$, then there exists $n$ with $x_n = 1$ (Markov's principle).
     – Nicolas M. Gutierrez May 08 '21 at 20:33
  • 1
    @NicolasM.Gutierrez It depends on the meaning of $\neq$, which I hadn't clarified due to my ignorance at that time. If $\neq$ simply denotes a negation of $=$, then the implication is actually trivial. If $\neq$ means apartness relation, however, I would agree with your opinion. – Hanul Jeon May 08 '21 at 20:33

1 Answers1

3

This is a partial answer:

b) Yes. This is because the $=$ relation on $\mathbb{N}$ is decidable (use induction to prove that). Suppose $f$ satisifes 2 and $f(x) = f(y)$. If $x \neq y$, then $f(x)\neq f(y)$ (Contradiction). So $\neg x\neq y$. Beacause $=$ ist decidable, we have $x = y$.

My understanding of constructive mathematics is to basic to answer a). I want to point out something else though: In many cases (where equality is not decidable), constructive mathematicians are not primarily interested in the relation given by negating the equality of a set, called denial inequality, but instead in an apartness relation $\neq$. That is a relation on a set, such that: $$\neg x\neq x$$ $$x\neq y \Rightarrow y \neq x$$ $$x \neq z \Rightarrow x \neq y \text{ or } y\neq z$$ If $x\neq y$ and $x = y$, then $x\neq x$ (Contradiction). So $x\neq y \Rightarrow \neg(x = y)$. The negation of an apartness relation is always an equivalence relation, the converse is only provable classically. In particular, denial inequality need not be an apartness relation. Therefore, in general the existence of an apartness relation is an extra property a set may have. Of course, with this the definition of an injection between sets equipped with apartness relations according to 2. changes (and may become more interesting and useful).

Stefan Perko
  • 12,467