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

4 Answers 4


Here is a proof using a Fitch-style, natural deduction proof checker.

enter image description here

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.


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.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.