Is it allowed to only substitute one of several fresh variables in a natural deduction proof step?

Question

I am working on the following proof: ∀x∀y (x = g(y) → f (x) = y) $\vdash$ ∀x f (g(x)) = x and I have tried solving it as:

∀x∀y (x = g(y) → f(x)=y) premise | x0 x0 = g(x0) assumption | ∀y (x0 = g(y) → f(x0)=y) ∀xe 1 | (x0 = g(x0) → f(x0)=x0) ∀ye 3 | f(x0) = x0 →e 4, 2 | f(g(x0)) = x0 =e 2, 5 ∀x f(g(x)) = x ∀xi 2--6

It is the =e 2, 5 I am asking about. Is it allowed to only substitute on of the x0s like this?

Answer 1

Long comment

I think that the above derivation does not work...

You correctly instantiate the premise with $x_0$ getting :

$∀y \ (x_0 = g(y) \to f(x_0)=y)$

and then we instantiate again :

$(x_0 = g(x_0) → f(x_0)=x_0)$.

Assuming :

$x_0=g(x_0)$ --- [a]

after $\to$-elim we may use $=$-elim to substitute only one occurrence of $x_0$, getting :

$f(g(x_0))=x_0$.

But now we have problems...

First, we have the open assumption [a] with $x_0$ free: thus, we cannot apply $\forall$-intro.

Second, also if we apply $\exists$-intro (no restriction) getting :

$\exists x \ (f(g(x))=x)$

we still have the assumption [a]. Thus out derivation amounts to:

$∀x \ ∀y \ (x = g(y) \to f(x)=y), \ x_0=g(x_0) \vdash \exists x \ (f(g(x))=x).$

---

To fix the problem, we have to use the equality axiom:

$\forall x (x=x)$

as an additional "premise"; being an axiom, it is not an assumption, and thus we have no need to discharge it.