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 :
discharging [a].