Is this predicate logic derivation valid?

Question

Could someone please be so kind as to check the validity of my predicate derivation? I am trying to prove that the set $\{(\forall x)\lnot(\exists y)Gxy,(\forall z)[Hz\implies(\exists z) Gzy],(\exists w)Hw\}$ is inconsistent, and have so conjured the following derivation:

1. $(\forall x)\lnot(\exists y)Gxy$____Assumption
2. $(\forall z)[Hz\implies(\exists z) Gzy]$____Assumption
3. $(\exists w)Hw$____Assumption
4. Hb____A/$\exists$E
5. Hb $\implies$ ($\exists y$)Gby____2$\forall$E
6. $(\exists y)$Gby____4,5$\implies$E
7. Gba____A/$\exists$E
8. $\lnot$Gab____A/$\lnot$E
9. ($\exists$ y)Gby____7$\exists$I
10. $\lnot(\exists y)$Gby____1$\forall$E
11. Gab____8-10$\lnot$E
12. Gab____7-11$\exists$E
13. ($\exists y$)Gay____12$\exists$I
14. ($\exists y$)Gay____4$\exists$E
15. $\lnot(\exists y)Gay$____1$\forall$E

I ask for this because I am still getting used to predicate proofs, and hence seek affirmation from the more proffesional. Thank you in advance.

Answer 1

Not knowing the exact rules of the particular proof system you are working with this is a little hard to answer, but my guess is that your system would not allow step 12: in lines 7-11 you use $a$ as a temporary placeholder for the 'something $y$ for which $Gby$ holds' ... but when you then apply the $\exists E$ rule on those lines 7-11, I bet that you are not allowed to infer any statement that refers to that very $a$, because outside of that context of lines 7-11, $a$ suddenly becomes to mean a specific object.

Fortunately, you don't need any of lines 7-11 in the first place! Note that once you have $(\exists y)Gby$ on line 6, you can apply a $\forall E$ on line 1 to obtain $\neg (\exists y)Gby$ on line 7, so there is your contradiction.

Of course, you still need to 'pull out' this contradiction so it is not within the context of the assumption made on line 4, and unfortunately you don't seem to have an explicit contradiction symbol $\bot$ that you can work with in your system. As such, you will need to do something awkward like first assuming $(\exists w)Hw$ on line 4, then do everything you did on lines 4-6 (so those become lines 5-7), then do my suggested $\neg (\exists y)Gby$ on line 8, then get $\neg (\exists y)Gby$ on line 9 by applying $\exists E$ on lines 5-8, and finally get $\neg (\exists w) Hw$ on line 10 by applying $\neg I$ on lines 4-9 (I assume you have a $\neg I$ rule that works like that)

Answer 2

Lines 9 and 10 are already a contradiction so I don't see why you need any of the subsequent lines.