$⊢ ∀x∀y(f(x) \neq f(y) → x \neq y)$

Question

Solve the exercice in Fitch notation using natural deduction for first order logic and not using completeness.

Should I start by removing the quantifiers or by making a subproof where I start with $f(x) \neq f(y)$ and try to get $x \neq y$?

Answer 1

I don't know how exactly your rule for universal introduction (or universal generalization) is defined, or how you do a proof by contradiction in the system that you use, but the proof below will give you the general idea:

The crucial steps are of course 5 and 6.

For 5, notice that the $= Intro$ rule says that you can introduce an equality between any two of the same terms $t$, so you can use it to get $a = a$, but we can also use it (as I did here) to get $f(a) = f(a)$. If you have never seen this before, that may look a bit weird, but it makes perfect sense: since $f(a)$ is a term, it denotes some object, and whatever that object is, it is of course the same as itself. So: $f(a) = f(a)$!

For 6, we used $= Elim$ to replace the second $a$ in $f(a) = f(a)$ with a $b$, which we can do, since $a = b$. Again, this may look weird, since we are not replacing all of the $a$'s with $b$'s, but the rule says that you can replace any of the $a$ with $b$'s; it does not say that you have to replace all of them. So again, this is a perfectly good use of the rule.