First order logic proof with identity rules

Question

There is this entailment I'm trying to prove: ∀x∀y(R(x,y) ∨ x=y), ∀x∃y¬x=y ⊢ ∀y∃x(¬x=y ∧ R(x,y)). I have tried the following, where PR is premise, AS assumption, R is by repetition, X is by principle of explosion, and --- is a line break.

1.∀x∀y(R(x,y) ∨ x=y):PR
2.∀x∃y¬x=y:PR
3.∃y¬a=y:∀E 2
4.   ¬a=b:AS
5.   ∀y(R(a,y) ∨ a=y):∀E 1
6.   R(a,b) ∨ a=b:∀E 5
7.      R(a,b):AS
8.      R(a,b):R 7
9.   ---
10.     a=b:AS
11.     ⊥:¬E 4,10
12.     R(a,b):X 11
13.  R(a,b):∨E 6, 7-8, 10-12
14.  R(a,c) ∨ a=c:∀E 5
15.     ¬a=c:AS
16.        R(a,c):AS
17.        R(a,c):R16
18.     ---
19.        a=c:AS
20.        ⊥:¬E 15, 19
21.        R(a,c):X 20
22.     R(a,c):∨E 14, 16-17, 19-21
23.     ¬a=c ∧ R(a,c):∧I 15, 22
24.     ∃x(¬x=c ∧ R(x,c)):∃I 23
25.  ∃x(¬x=c ∧ R(x,c)):∃E 3, 15-24
26.  ∀y∃x(¬x=y ∧ R(x,y)):∀I 25
27.∀y∃x(¬x=y ∧ R(x,y)):∃E 3, 4-26

I know my problem in this proof is in line 25 since when doing existential elimination, c occurs as part of the closed assumption on line 15. So I would probably have to insert a new variable that is not c, or a, or b, since those are all part of assumptions. But then I believe that would just require that I open a different assumption with a new variable d and it would be a never ending loop of keep opening up a new assumption inside with a new variable.

Is there another way that I could fix that or something else I could do? Thanks for the help.

Answer 1

Note that you didn't do anything with the $b$ after line 13!

Indeed, rather than introducing a new object, think of how you can get to your goal $\forall y \exists x (x \neq y \land R(x,y))$ in terms of $a$ and $b$.

Well, since $a$ was a completely arbitrary object, while $b$ came from the more restricted existential on line 3, you want $a$ to take the role of the $y$, and $b$ to take the role of the $x$ in your goal. As such, you are looking to prove $b \neq a \land R(b,a)$

Now, $b \neq a$ can be inferred from $a \neq b$, and once you have that, you instantiate premise 1 to get $R(b,a) \lor b = a$, and thus $R(b,a)$, and now it's just a matter of tidying it all up.

Here's the completed proof in Fitch:

Answer 2

Starting from 2nd premise with $\forall$-elim and assuming $\lnot (y=a)$ for $\exists$-elim, with $a$ the parameter for the $\exists$-intro assumption.

From 1st premise we get $y=a \lor R(y,a)$, and thus, by propositional rules, we get : $R(y,a)$.

Now we use again 1st premise swapping the variables to be used in the instantiation, and we get, with the same process above : $R(a,y)$.

The key point is the fact that $=$ is symmetric, and thus $\lnot (y=a)$ and $\lnot (a=y)$ are the same.

Thus we get :

$\lnot (a=y) \land R(a,y)$,

and we can perform $\exists$-intro on it, to get :

$\exists x (\lnot (x=y) \land R(x,y))$.

Now the parameter $a$ is no longer present, and we can close the $\exists$-elim.