Prove if a = b, then f(a) = f(b) for any function f (with natural deduction)

I want to be able to prove that for all functions f, that $a = b \to f(a) = f(b)$. That this is true is obvious, but I'm not sure how to formally prove it using only the rules of inference in first-order logic (using natural deduction). I'm guessing I need to reference a formal definition for a function, where $f \subset A \times B$ and satisfies:

$$ (\forall x \in A)(\exists y \in B)((x,y) \in f \wedge (\forall z \in B)((x,z) \in f\to y=z))$$

However, I don't have any clue where to begin with this. Can anyone help? Please only give hints/answers using natural deduction as the deductive system.

Solution 1:

To prove it in set theory, we need some definitions and some basic results :

Definition of function : $(∀x)(∀y)(∀z)(\langle x,y \rangle \in f \land \langle x,z \rangle \in f \to y = z)$;

equality between (Kuratowski) pairs :

$\langle x,y \rangle = \langle u,v \rangle \to x = u \land y = v$;

definition of domain of a relation:

$\mathcal D R$ is the set of all $x$ such that, for some $y : \ \langle x,y \rangle \in R$.

We cannot prove the formula in your question as is, due to the fact that not all functions are total.

We have to rewrite it as :

if $a \in \mathcal D f$ and $a=b$, then $f(a)=f(b)$.

We need also to formalize the abbreviation $f(x)$; form the definition of function we have:

for every $a \in \mathcal D f : \ \exists ! y \ (\langle a,y \rangle \in f)$.

Thus, we are licensed to write :

for every $a \in \mathcal D f : f(a)=\iota y \ (\langle a,y \rangle \in f)$.

Now for the proof :

1) $a \in \mathcal D f$ --- assumed [a]

2) $a=b$ --- assumed [b]

3) $\langle a, f(a) \rangle \in f$ --- from 1) and abbreviation

4) $\langle b, f(b) \rangle \in f$ --- from 2) and 3)

5) $\langle a, f(b) \rangle \in f$ --- from 2) and 4).

Note : the above steps are substitutions of terms into formulae. The formula is : $\{ a, \{a, f(a) \} \} \in f$ and we use the equality axiom :

$a = b \to (\varphi \to \varphi')$, where where $\varphi'$ is obtained from $\varphi$ by replacing $a$ in zero or more (but not necessarily all) places by $b$.

Form the definition of function, by instantiation (or : $\forall$-elim) :

6) $\langle a,f(a) \rangle \in f \land \langle a,f(b) \rangle \in f \to f(a) = f(b)$.

7) $f(a) = f(b)$ --- from 6), 3) and 5) by modus ponens twice.

Thus, discharging assumptions [a] and [b] by Deduction Th (or : $\to$-intro) :

$a \in \mathcal D f \land a=b \to f(a) = f(b)$.

The conclusion (for every $a$ ...) follows by generalization (or : $\forall$-intro).