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

Question

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.

Answer 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).

Answer 2

I know it's been a while since you asked your question, but I suppose the answer you're looking for is this one. Basically, you want to prove that $F : X \rightarrow Y$ implies $\forall x' \in X \forall x'' \in X [x'=x'' \rightarrow F(x') = F(x'')]$. As you correctly stated, $F : X \rightarrow Y$ can be translated in predicate logic as $\forall x[x \in X \rightarrow \exists y[y \in Y \land (x,y) \in F \land \forall z[z \in Y \land (x, z) \in F \rightarrow y=z]]]$. As a sidenote, the expression $\forall x' \in X \forall x'' \in X [x'=x'' \rightarrow F(x') = F(x'')]$ is equivalent to $\forall x' \forall x'' [(x' \in X \land x'' \in X \land x'=x'') \rightarrow F(x') = F(x'')]$.

The first step in our proof is to declare $x'$ and $x''$ as arbitrary variables. As a consequence, the goal of our proof turns into $(x' \in X \land x'' \in X \land x'=x'') \rightarrow F(x') = F(x'')$. The second step is to hypothetically assume $x' \in X$, $x'' \in X$ and $x'=x''$. As a consequence, the goal turns into $F(x') = F(x'')$. Hence:

PREMISE 1: $\forall x[x \in X \rightarrow \exists y[y \in Y \land (x,y) \in F \land \forall z[z \in Y \land (x, z) \in F \rightarrow y=z]]]$

PREMISE 2: $x' \in X$

PREMISE 3: $x'' \in X$

PREMISE 4: $x'=x''$

GOAL: $F(x') = F(x'')$

We apply universal instantiation upon PREMISE 1 to derive $x' \in X \rightarrow \exists y[y \in Y \land (x',y) \in F \land \forall z[z \in Y \land (x', z) \in F \rightarrow y=z]]$ and $x'' \in X \rightarrow \exists y[y \in Y \land (x'',y) \in F \land \forall z[z \in Y \land (x'', z) \in F \rightarrow y=z]]$. Since we have $x' \in X$ (PREMISE 2) and $x'' \in X$ (PREMISE 3), we use modus ponens and conclude $\exists y[y \in Y \land (x',y) \in F \land \forall z[z \in Y \land (x', z) \in F \rightarrow y=z]]$ and $\exists y[y \in Y \land (x'',y) \in F \land \forall z[z \in Y \land (x'', z) \in F \rightarrow y=z]]$.

Now, we should use existential instantiation to get rid of the existential quantifiers in both statements. Therefore, we introduce the variables $y'$ and $y''$ and assume the premises $y' \in Y \land (x',y') \in F \land \forall z[z \in Y \land (x', z) \in F \rightarrow y'=z]$ and $y'' \in Y \land (x'',y'') \in F \land \forall z[z \in Y \land (x'', z) \in F \rightarrow y''=z]$. Notice that the first expression means the same as $y' = F(x')$ and the second expression means $y'' = F(x'').$

At this point, we use universal instantiation at the uniqueness part of both expressions, substituting $z$ in the first expression by $y''$ and $z$ in the second expression by $y'$. Hence, $y' \in Y \land (x',y') \in F \land [y'' \in Y \land (x', y'') \in F \rightarrow y'=y'']$ and $y'' \in Y \land (x'',y'') \in F \land [y' \in Y \land (x'', y') \in F \rightarrow y''=y']$.

Since we have $y' \in Y \land (x',y') \in F$ and since $x'=x''$ (PREMISE 4), then, by modus ponens, we conclude $y' \in Y \land (x'',y') \in F$. Since we have from the uniqueness part of the second statement that $[y' \in Y \land (x'', y') \in F \rightarrow y''=y']$, then we conclude by modus pones $y''=y'$. Since $y'=F(x')$, since $y''=F(x'')$ and since $y'=y''$, we conclude $F(x')=F(x'')$. The same reasoning could have been applied upon statement 2 and the uniqueness part in statement 1 to reach the same result.