I'm looking for a solution to this problem:
$$\left\{\forall x (Qx \leftrightarrow (\exists y (Rxy \wedge \neg x = y))),\quad \forall x Qx,\quad \exists x \exists y \forall z (z = x \vee z = y)\right\} \models \forall x \forall y (Rxy \leftrightarrow Ryx)$$
I can see that the brunt of the proof will come from making a contradiction between the identities in the conjunction and those in the first premise, but I'm not sure. Some help would be much appreciated!
This is pretty old now, but I can confirm that there exists a direct proof for this that is very long and ugly - the third premise means that everything in the domain is split into two sets, those that are equal to $a$ and those that are equal to $b$. Once you instantiate for your universals in the conclusion, and your existentials in the first premise, you can check for each disjunct for each of your variables. A whole bunch will result in contradictions, because of what you get from instantiating premise 1. Those that don't, will be cases where the things in the conclusion are the same, so ($Raa$ iff $Raa$), or you'll have gotten the case where $a\neq b$, but will have that $Rab$ and $Rba$, so $Rab$ iff $Rba$.
01. ∀x[Qx↔[∃y[[Rxy]∧¬[x=y]]]] premise
02. ∀xQx premise
03. ∃x∃y∀z[[z=x]∨[z=y]] premise
04. ∃y∀z[[z=a]∨[z=y]] assumption
05. ∀z[[z=a]∨[z=b]] assumption
06. Rcd assumption
07. ¬[c=d] assumption
08. ∀x[Qx↔[∃y[[Rxy]∧¬[x=y]]]] restate 01
09. Qd↔[∃y[[Rdy]∧¬[d=y]]] ∀elim 08
10. ∀xQx restate 02
11. Qd ∀elim 10
12. ∃y[[Rdy]∧¬[d=y]] ↔elim 09 11
13. [Rde]∧¬[d=e] assumption
14. e=c assumption
15. [Rde]∧¬[d=e] restate 13
16. [Rdc]∧¬[d=c] para 15 14
17. Rdc ∧elim 16
18. [e=c]→[Rdc] →intro 19 17
19. ¬[e=c] assumption
20. ∀z[[z=a]∨[z=b]] restate 05
21. [c=a]∨[c=b] ∀elim 20
22. [d=a]∨[d=b] ∀elim 20
23. [e=a]∨[e=b] ∀elim 20
24. [Rde]∧¬[d=e] restate 13
25. ¬[d=e] ∧elim 24
26. e=a assumption
27. ¬[d=e] restate 25
28. ¬[d=a] para 27 26
29. [d=a]∨[d=b] restate 22
30. d=b ∨elim 29 28
31. ¬[e=c] restate 19
32. ¬[a=c] para 31 26
33. ¬[c=a] flip 32
34. [c=a]∨[c=b] restate 21
35. c=b ∨elim 34 33
36. ¬[c=d] restate 07
37. c=d para 35 30
38. ⊥ 36 37
39. ¬[e=a] ¬intro 26 38
40. e=b ∨elim 23 39
41. ¬[d=e] restate 25
42. ¬[d=b] para 41 40
43. d=a ∨elim 22 42
44. ¬[c=d] restate 07
45. ¬[c=a] para 44 43
46. c=b ∨elim 21 45
47. e=c para 40 46
48. ⊥ 47 19
49. ¬¬[e=c] ¬intro 19 48
50. e=c ¬¬elim 49
51. Rdc MP 18 50
52. Rdc ∃ 12 13-51
53. ¬[c=d]→[Rdc] →intro 07 52
54. c=d assumption
55. Rcd restate 06
56. Rcc para 55 54
57. Rdc para 56 54
58. [c=d]→[Rdc] →intro 54 57
59. [c=d]∨¬[c=d] LEM
60. Rdc ∨elim 58 53 59
61. [Rcd]→[Rdc] →intro 06 60
62. ∀y[[Rcy]→[Ryc]] ∀intro 61
63. ∀x∀y[[Rxy]→[Ryx]] ∀intro 62
64. ∀x∀y[[Rxy]→[Ryx]] ∃elim 04 05-63
65. ∀x∀y[[Rxy]→[Ryx]] ∃elim 03 04-64
66. ∀y[[Ray]→[Rya]] ∀elim 65
67. [Rab]→[Rba] ∀elim 66
68. ∀y[[Rby]→[Ryb]] ∀elim 65
69. [Rba]→[Rab] ∀elim 68
70. [Rab]↔[Rba] ↔intro 67 69
71. ∀y[[Ray]↔[Rya]] ∀intro 70
72. ∀x∀y[[Rxy]↔[Ryx]] ∀intro 71
Synopsis of proof:
We let $Rcd$. Then, using the premise $\forall x \exists y [Rxy \land \neg x = y]$, we conclude $Rde$. Then, we argue that $e$ must be equal to $c$, using $\forall z[z = a \lor z = b]$. Then, we conclude that $Rcd \implies Rdc$. Using symmetry, we conclude that $Rdc \implies Rcd$, hence $Rcd \iff Rdc$. Then, we generalize to $\forall x \forall y[Rxy \iff Ryx]$.
