# Tricky proof in Natural Deduction [¬∀x∃y¬Rxy ⊢ ∃x∀yRxy]-help appreciated

As it says in the title, I'm trying to prove the statement ¬∀x∃y¬Rxy ⊢ ∃x∀yRxy in the system of Natural Deduction, with basic rules for negation intro and elimination, and existential or universal quantifier intro and elim.

I can use the premiss to create a contradiction, so the penultimate line might be:

¬∀x∃y¬Rxy ∀x∃y¬Rxy

     ∃x∀yRxy


But how do I derive the assumption ∀x∃y¬Rxy? It might be:

               ¬Rab
∃y¬Ray
∀x∃y¬Rxy


So ¬Rab must be derived from some assumption Rab that leads to contradiction-that's where I'm stuck! Any help appreciated-this is not my homework or anything, it just bugs me!

We need :

1) $¬∀x∃y¬Rxy$ --- premise

2) $¬∃x∀yRxy$ --- assumption [a] : the assumption to be contradicted, deriving (by Double Negation) the sought conclusion : $∃x∀yRxy$

3) $∀yRxy$ --- assumption [b] : in order to derive a contradiction with 2) to conclude, by $¬$-intro, with : $¬∀yRxy$, discharging [b].

Now we need a "detour", in order to derive from $¬∀yRxy$ the classically equivalent : $∃y¬Rxy$.

Having derived $∃y¬Rxy$, we can "generalize" it to $∀x∃y¬Rxy$. We can do it, because neither in the premise nor into assumption [a] $x$ is free.

Thus, $∀x∃y¬Rxy$ contradicts the premise 1) and we can conclude by Double Negation again with :

$∃x∀yRxy$,

discharging [a].

• Thanks Mauro, I've got it now! I didn't use the right assumption, that got me into trouble. – user211309 Nov 19 '15 at 10:43

$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline #2\end{array}}$$

The thing about natural deduction is that if something is provable, you can often reverse engineer the proof by deciding what needs to be, and may be, introduced or eliminated, step by step.

Okay, so our goal is to prove that a conditional statement is a theorem (that it holds with no premises). $$\fitch{}{~~\vdots\\\neg\forall x\exists y~\neg Rxy\to\exists x\forall y~Rxy}$$

Well, clearly, to derive a conditional statement we need a conditional proof.

$$\fitch{}{\fitch{\neg\forall x\exists y~\lnot Rxy}{~~\vdots\\\exists x\forall y~Rxy}\\\neg\forall x\exists y~\neg Rxy\to\exists x\forall y~Rxy}$$

We have nothing available to construct a witnesses, so to derive this existential statement, we need to show that it cannot not hold (ie: a proof by contradiction). And obviously the thing we will be contradicting is that assumption. So we need a universal introduction proof.

$$\fitch{}{\fitch{\neg\forall x\exists y~\lnot Rxy}{\fitch{\neg\exists x\forall y~Rxy }{\fitch{[a]}{~~\vdots\\\exists y~\neg Ray}\\\forall x\exists y~\neg Rxy\\\bot}\\\neg\neg\exists x\forall y~Rxy\\\exists x\forall y~Rxy}\\\neg\forall x\exists y~\neg Rxy\to\exists x\forall y~Rxy}$$

Again, to prove this existential statement we need a proof by contradiction, this time aiming to contradict the second assumption.

$$\fitch{}{\fitch{\neg\forall x\exists y~\lnot Rxy}{\fitch{\neg\exists x\forall y~Rxy }{\fitch{[a]}{\fitch{\neg\exists y~\neg Ray}{~\vdots\\\exists x\forall y~Rxy\\\bot}\\\neg\neg\exists y~\neg Ray\\\exists y~\neg Ray}\\\forall x\exists y~\neg Rxy\\\bot}\\\neg\neg\exists x\forall y~Rxy\\\exists x\forall y~Rxy}\\\neg\forall x\exists y~\neg Rxy\to\exists x\forall y~Rxy}$$

Okay, we finally have something that might act as a witness for this existential statement, that is if we can derive $$\forall y~Ray$$, so attempting a universal proof is indicated.

$$\fitch{}{\fitch{\neg\forall x\exists y~\lnot Rxy}{\fitch{\neg\exists x\forall y~Rxy }{\fitch{[a]}{\fitch{\neg\exists y~\neg Ray}{\fitch{[b]}{~~\vdots\\Rab}\\\forall y~Ray\\\exists x\forall y~Rxy\\\bot}\\\neg\neg\exists y~\neg Ray\\\exists y~\neg Ray}\\\forall x\exists y~\neg Rxy\\\bot}\\\neg\neg\exists x\forall y~Rxy\\\exists x\forall y~Rxy}\\\neg\forall x\exists y~\neg Rxy\to\exists x\forall y~Rxy}$$

Now to derive this statement ($$Rab$$) from the assumptions, it is time to do a proof by contradiction for the assumption of $$\neg\exists y~\neg Ray$$.   Well, since the required existential may immediately be introduced from the assumption, we are done.

$$\fitch{}{\fitch{\neg\forall x\exists y~\lnot Rxy}{\fitch{\neg\exists x\forall y~Rxy }{\fitch{[a]}{\fitch{\neg\exists y~\neg Ray}{\fitch{[b]}{\fitch{\neg Rab}{\exists y~\neg Ray\\\bot}\\\neg\neg Rab\\Rab}\\\forall y~Ray\\\exists x\forall y~Rxy\\\bot}\\\neg\neg\exists y~\neg Ray\\\exists y~\neg Ray}\\\forall x\exists y~\neg Rxy\\\bot}\\\neg\neg\exists x\forall y~Rxy\\\exists x\forall y~Rxy}\\\neg\forall x\exists y~\neg Rxy\to\exists x\forall y~Rxy}$$

Okay, aside from numbering the lines and adding justifications, we are done.

$$\blacksquare$$