# Language Logic Proof Question: ¬∃x∀y[E(x,y) ↔ ¬E(y,y)]

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)]

1. ¬¬∃x∀y[E(x,y) ↔ ¬E(y,y)]
1. ∃x∀y[E(x,y) ↔ ¬E(y,y)] ¬E,1
1. |a| ∀y[E(a,y) ↔ ¬E(y,y)] ∃E,2
1. |a| [E(a,a) ↔ ¬E(a,a)] ∀E, 3
2. Eaa ↔E, 4

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.