Here's an argument that's quite clearly valid, but which I'm having trouble proving in Natural Deduction:

$\exists x~\exists y~\lnot x=y \vdash\forall x~\exists y~\lnot x=y$

The informal reasoning: the premise is that there are at least two distinct elements; this implies that for every element, there is at least one element which is distinct from it.

I presume the proof will end (and I'm using what I believe is called a proof tree):

$$\exists y~\lnot a=y\over\forall x~\exists y~\lnot x=y$$

with the top sentence following from an application of negation elimination or from $\lnot a=b$ (or some constant). But after hours of trying I haven't been able to complete a proof. Can someone advise me?

  • 2
    $\begingroup$ Are you using intuitionistic logic? If so then this is not provable. Try proving it assuming also the law of excluded middle $\forall P. P \vee \neg P$ $\endgroup$ – Max New Jan 3 '18 at 17:48
  • 3
    $\begingroup$ Or more specifically, decidable equality should do $\forall x. \forall y. (x = y) \vee \neg (x = y)$ $\endgroup$ – Max New Jan 3 '18 at 17:56

Here's a proof in Fitch ... you can probably convert it to a proof in your system:

enter image description here


Proof sketch

1) $∃x ∃y \ ¬(x=y)$ --- premise

2) $¬∀x ∃y \ ¬(x=y)$ --- assumed [a]

3) $¬(a=b)$ --- from 1) by two $∃$-elim

4) $∃x ∀y \ (x=y)$ --- from 2) by equivalences: to be derived

5) $∀y \ (c=y)$ --- from 4) by $∃$-elim

6) $c=a$ --- from 5)

7) $c=b$ --- from 5)

8) $a=b$ --- from 6) and 7) by transitivity of equality

9) $\bot$ --- from 2) and 8)

Now we can close all the $∃$-elim's, because there are no free variables in 9). Thus:

$∀x ∃y \ ¬ (x=y)$ --- from 2) by Double Negation [that is not intuitionistically valid; see also @Max New's comment], discharging [a].


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.