# Formal proof of De Morgan's laws for quantifiers

Consider the set of inference rules for first order logic (analogous to the ones listed here : http://en.wikipedia.org/wiki/Sequent_calculus#Inference_rules)

I am stuck in proving the following rule

$$\vdash_{\gamma} \neg \forall x.\phi \implies \exists x. \neg \phi$$

I think it is easy to do this using the notion of soundness and completeness and checking that the left formula is valid when the right is.

However I am not able to prove it using just the formalism of manipulating proof trees with inference rules. Somehow I do not see how to get rid of the negation in $\neg \forall x.\phi$ without applying the rule I want to prove.

Any hints?

-

Would the following work?

1 $\vdash \neg \forall x. \phi$ | Hypothesis

2 $\vdash \neg \phi \implies \exists x. \neg \phi$ by existential generalization

3 $\vdash \neg \exists x. \neg \phi \implies \phi$ by 1,Contraposition

4 $\neg \exists x. \neg \phi \vdash \phi$ by 3

5 $\neg \exists x. \neg \phi \vdash \forall x. \phi$ by 4,Universal Generalization

6 $\vdash \neg \exists x. \neg \phi \implies \forall x. \phi$ by 5,Deduction

7 $\vdash \neg \forall x. \phi \implies \exists x. \neg \phi$ by 6,Contraposition

-