Natural deduction proof of $a = b \rightarrow f(a) = f(b)$. Where have I gone wrong?

Question

I am trying to prove a basic property of functions using the steps of natural deduction, within set theory. Namely, that if a = b, then f(a) = f(b) for any function f. I know the proof I have come up with is faulty (I will explain below why), but I'm not sure at which line this occurs.

First, I assert the following definitions:

[Def 1] $ \forall x(x \in D(f) \to \exists y((x,y) \in f \wedge \forall z((x,z)\in f \to y = z)))$ -- Defines a function $f$ with domain $D(f)$

[Def 2] $ \forall x \forall y(f(x) = y \leftrightarrow (x,y) \in f)$ -- Defines the notation $f(x)$

and from this I want to prove:

$$ \forall x \forall y((x \in D(f) \wedge x = y) \to f(x) = f(y))$$

Here is the proof I use:

1. $a \in D(f)~~~~~~~~~\text{(Assumption)}$
2. $ a = b~~~~~~~~~~~~~\text{(Assumption)}$
3. $ a \in D(f) \to \exists y((a,y) \in f \wedge \forall z((a,z)\in f \to y = z))~~~~~~~(\forall \text{-elim, Def 1.})$
4. $ \exists y((a,y) \in f \wedge \forall z((a,z)\in f \to y = z))~~~(\to\text{elim; 1, 3})$
5. $ (a,c) \in f \wedge \forall z((a,z)\in f \to c = z)~~~~\text{(Assumption)}$
6. $ (a,c) \in f~~~~~~(\wedge\text{-elim, 5.})$
7. $ f(a) = c \leftrightarrow (a,c) \in f~~~~(\forall\text{-elim twice on Def 2.})$
8. $ (a,c) \in f \to f(a) = c ~~~~~~~(\leftrightarrow\text{elim; 7.})$
9. $ f(a) = c~~~~~(\to\text{elim; 6, 8})$
10. $ (a, f(a)) \in f~~~~~~\text{(=-elim; 6, 9. Also, assumption at 5. is discharged by }\exists\text{-elim.)}$
11. $ (b, f(a)) \in f~~~~~~\text{(=-elim; 2, 10)}$
12. $ f(b) = f(a) \leftrightarrow (b,f(a)) \in f~~~~(\forall\text{-elim twice on Def 2.})$
13. $ (b,f(a)) \in f \to f(b) = f(a) ~~~~~~~(\leftrightarrow\text{elim; 12.})$
14. $ f(b) = f(a)~~~~~(\to\text{elim; 11,13})$
15. $ f(a) = f(b)~~~~~\text{(=-symm; 14)}$
16. $ (a \in D(f) \wedge a = b) \to f(a) = f(b)~~~~~~\text{(Discharge assumptions 1 and 2)}$
17. $ \forall x \forall y((x \in D(f) \wedge x = y) \to f(x) = f(y))~~~~~~~~~(\forall\text{-intro used twice)}$

(Note: I use the natural deduction rules of inference defined in Chiswell & Hodges: Mathematical Logic)

This proof must be wrong, because it doesn't use the key part of Def. 1 at all, which ensures the uniqueness of a function's value for some input. That is, I can just $\wedge$-elim it away at step 6! Can anyone point out at which step I have made an error?

PS. Sorry about the poor formatting of the proof lines, but I don't have enough latex knowledge to format it neatly.

Answer 1

In first-order logic, function symbols are inherently treated to be things that work functionally, and so from $a=b$, it will logically follow that $f(a) = f(b)$:

1. $a=b \qquad\quad\qquad$ Assumption
2. $f(a)=f(a) \qquad$ = Intro
3. $f(a)=f(b) \qquad$ = Elim 1,2

Now, I know you tried to avoid doing this by creating an axiomatic definition for a function, and trying to derive its functionality from that. However, you ended up using functional symbols, and in fact on line 10 you exploited the inherent functionality of the function symbols in logic after all, thus effectively doing what the proof above does after all, and thus eliminating the need for Def. 1.

To avoid such unintended exploitations of the nature of functional symbols in logic, I would recommend to 1) avoid function symbols altogether, 2) use Def. 1 as your one and only axiomatic definition of a function, 3) get rid of Def. 2, and 4) rephrase your goal to not use function symbols either, and instead use something like:

$ \forall x \forall y ((x \in D(f) \wedge y \in D(f) \wedge x = y) \to \forall v \forall w (((x,v) \in f \wedge (y,w) \in f) \to v = w))$

Below is a Natural Deduction proof for the desired result when following that approach.

Answer 2

Consider the relation "$\text {Son_of}(x,y)$" and introduce the notation $\text {Son_of}(x)=y$.

We have that :

if $ \ \text {John} = \text {Bobby} \ $, then $ \ \text {Son_of}(\text {John}) = \text {Son_of}(\text {Bobby}).$

But from :

$ \ \text {Son_of}(\text {John}) = \text {Ron} \ $ and $ \ \text {Son_of}(\text {John}) = \text {Tommy}$

does not follow that :

$ \ \text {Ron} = \text {Tommy} \ $.

What has gone wrong ? The definition of the notation $\text {Son_of}(x)=y$.

We cannot use it with the relation "$\text {Son_of}(x,y)$" because it is not functional.

Thus, in your proof, to apply [Def 2] you have implicitly assumed that also the uniqueness clause of [Def 1] holds.