Proof or counterproof for $\forall x (x = f(y)) \implies \forall y (y = f(x))$

Question

I was wondering about the following fact:

$\forall x (x = f(y)) \implies \forall y (y = f(x))$

I think this is not true, but I can't find a counterexample but not I can prove it is wrong. Any ideas?

Answer 1

As indicated by the previous answer, we cannot find a counter-example because the formula is valid.

We can prove it with Natural Deduction [Note : in order to avoid mistakes, I'll use parameters : $a,b,\ldots$ as free variables.] :

1) $∀z \ (z=f(a))$ --- premise

2) $\exists z \ \lnot (z=f(b))$ --- assumed [a]

3) $\lnot (c=f(b))$ --- assumed [b] by $\exists$-elim, from 2)

4) $a=f(a)$ --- from 1) by $\forall$-elim

5) $b=f(a)$ --- from 1) by $\forall$-elim

6) $c=f(a)$ --- from 1) by $\forall$-elim

7) $a=b$ --- from 4) and 5) by the rules : $(=\text{symmetric})$ and $(=\text{transitive})$ [see : Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007), page 123]

8) $f(a)=f(b)$ --- from 7) by the rule : $(= \text{term})$ [$s=t \vdash r[s/x] = r[t/x]$; see : Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007), page 124]

9) $c=f(b)$ --- from 6) and 8) by $(=\text{transitive})$

10) $\bot$ --- from 3) and 9)

11) $\bot$ --- from 2), 3) and 10) by $\exists$-elim, discharging [b]

12) $\lnot \exists z \ \lnot (z=f(b))$ --- from 2) and 11) by $\lnot$-intro, discharging [a].

Thus, with the equivalence between $\forall$ and $\lnot \exists \lnot$ and $\to$-intro, we can conclude with :

$\vdash ∀z \ (z=f(a)) \to ∀z \ (z=f(b))$.

Answer 2

$\forall x(x=f(y))\to \forall y(y=f(x))$ is vacuously true.

Perhaps it will be clearer if we alpha replace the bound tokens for both quantifiers

$\forall z(z=f(y))\to \forall z(z=f(x))$

$\forall z(z=f(y))$ is a fallacy, (its false for any entity $y$ and and function $f$) so the implication is vacuously true.