I am wondering if I have completed this proof properly. I don't think I have it right. It's tricky!
Conclusion: ¬∃x∀y[E(x,y) ↔ ¬E(y,y)]
Here is a proof using a Fitch-style, natural deduction proof checker.
To make well-formed sentences I had to rewrite some of the names used in the OP's example. In place of "E", I used "P", since "E" is a symbol for the existential quantifier in this proof checker. Also the notation in this proof checker is more compact. For example, "E(x,y)" became "Pxy".
Rather than starting with a negation of the conclusion, I removed the negation sign from the conclusion with the intent of introducing the negation at the end which I did on line 12.
From line 2 to line 10 I used a subproof to start the attempt to eliminate the existential quantifier (∃E on line 11) taking the name "a" for the variable "x". I used the same name to eliminate the universal quantifier (∀E) on line 3. This allowed me to use the law of the excluded middle (LEM) to reach a contradiction on line 10 discharging the assumptions made on lines 4 and 7 by closing the subproofs.
Line 10 allowed me to eliminate the existential quantifier on line 11 discharging the assumption on line 2. The contradiction on line 10 allowed me to introduce a negation on line 12 and complete the proof.
References
Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org
I haven't used/taught LPL myself, so I don't know the format or standards for finishing a RAA proof. The indented lines 1-4 are correct; for the un-indented line 2, either it's malformed (Eaa if and only if E?) or I don't understand how to parse it.
In my logic courses, I would probably accept 4 as sufficient to show that 1 leads to a contradiction, QED.
To prove ~P begin by assuming P with the aim to demonstrating a contradiction. Thus use "negation introduction". (Note: Do not assume a double negation if you can avoid it - especially if your first move is to eliminate it.)
To obtain a contradiction from ƎxⱯy Qxy use the quantifier instantiation rules and show that Qba is a contradiction for witness b and arbitrary a (which may possibly be b too).
To obtain a contradiction from Eba <-> ~Eaa, for witness b and arbitrary a, well, note that when a is b you have a contradiction. So your universal elimination is to the existential's witness.
To summarise: We should assume ƎxⱯy (Exy <-> ~Eyy), then assume a witness [b] for the existential, that is Ɐy (Eby <-> ~Eyy), so we may eliminate that universal to the witness, so Ebb <-> ~Ebb, and demonstrate this is contradiction, allowing us to thus discharge the assumptions and finish with negation introduction.
Demonstrating that Ebb <-> ~Ebb is a contradiction is simply a matter of using negation elimination and biconditional eliminations. Assuming Ebb derives a contradiction from the biconditional, thus introducing a negation. ~Ebb likewise derives the needed contradicion from the biconditional.
|_
| |_ Ǝx Ɐy (Exy <-> ~Eyy)
| | |_ [b] Ɐy (Eby <-> ~Eyy)
| | | Ebb <-> ~Ebb
| | | |_ Ebb
| | | | ~Ebb
| | | | ┴
| | | ~Ebb
| | | Ebb
| | | ┴
| | ┴
| ~Ǝx Ɐy (Exy <-> ~Eyy)
The statement ¬∃x∀y[E(x,y)⟷¬E(y,y)] is equivalent, using the properties of negation to
∀x∃y{[E(x,y)∧¬¬E(y,y)]∨[¬E(y,y)∧¬E(x,y)]} .
The sentence in curly brackets is always true for y=x using ¬¬E→E, and this proves the statement. This proof has the advantage of avoiding the use of reductio ad absurdum, and thus the law of excluded middle; however it uses the fact that ¬¬E→E. Hence, this proof would not be acceptable in intuitionistic logic. OP's statement is a theorem in classical logic but not in the weaker intuitionistic logic.
