enter image description here

The only way I could think of to do this problem is reductio, but since the two biconditional terms are not contradictory, I am pretty stuck.

  • Are you allowed to use the law of excluded middle? – user2953 Jun 2 '18 at 7:31
  • I think you perform existential and universal elimination on your reductio premise and reach a contradiction – Schiphol Jun 2 '18 at 10:00

Smells like Russell's Paradox ...

Anyway, yes, you totally had the right idea: proof by contradiction! And the two conditionals will contradict as long as you instantiate them with the same constant a:

enter image description here


E(x,y) <-> ¬ E(y,y) is clearly false if x and y are the same, because then the statement becomes E(x,x) <-> ¬ E(x,x).

Whatever we choose for x, E(x,y) <-> ¬ E(y,y) is not true for all y, because it is not true for y = x.

  • This is only correct in classical logics; see the discussion under my answer. – user2953 Jun 2 '18 at 23:19

Here is a proof using the law of excluded middle. After eliminating the existential quantifier to get x, apply the universal quantification on x itself to get E(x,x) ↔ ¬E(x,x). This is false if E(x,x) is true or false.

enter image description here

In Coq:

Variable P : Prop -> Prop -> Prop.
Axiom LEM : forall p, p \/ ~p.

Goal ~exists x, forall y, (P x y -> ~P y y) /\ (~P y y -> P x y).
elim H.
assert (P x x \/ ~P x x) by apply LEM.
elim H1; intro.
apply H0 with x; assumption.
apply H0 with x; apply H0; assumption.
  • It is unclear whether "no premises" means no law of excluded middle. If yes, I'll remove this. – user2953 Jun 2 '18 at 13:59
  • Since you can prove LEM from no premises, you could always begin with that proof and satisfy the terms of the question. – Dennis Jun 2 '18 at 18:59
  • @Dennis LEM does not hold in intuitionistic logic. – user2953 Jun 2 '18 at 19:01
  • 1
    I was assuming OP was working in a classical system. Since most intro logic books assume such a system it seems likely, but you’re right that it wouldn’t be an intuitionistically valid proof. – Dennis Jun 2 '18 at 19:03

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.