How do I formally prove the following:

$$[\forall y Gy \wedge \exists x Hx] \iff \exists x[\forall y Gy \wedge Hx]$$

and by formally I mean using premises and whatever other first order logical axioms are needed.

I proved it like such, but this is not how I was supposed to do it.

$[\forall y Gy \wedge \exists x Hx] \iff \exists x[\forall y Gy \wedge Hx]$ : Distribute Quantifier

$\implies$ $[\forall y Gy \wedge \exists x Hx] \iff [\forall x\forall y Gy \wedge \exists x Hx]$ :Null Quantification

$\implies$ $[\forall y Gy \wedge \exists x Hx] \iff [\forall y Gy \wedge \exists x Hx]$

Can anyone help? Here are some of the Axioms accepted:

$$M.P: Modus Ponens$$

$$TA : Tautologies$$

$$\forall x(\delta \implies \psi) \implies (\forall x\delta \implies \forall x\psi)$$

$$E.I: Existential Instantiation$$ $$U.G: Universal Generalization$$ $$U.I: Universal Instantiation$$ $$E.G: Existential Generalization$$

  • $\begingroup$ This depends on the axioms and rules you have available. Can you please post them? $\endgroup$
    – Git Gud
    Commented Dec 6, 2016 at 0:22
  • $\begingroup$ @GitGud Yes, I will edit it. $\endgroup$ Commented Dec 6, 2016 at 0:42
  • $\begingroup$ It doesn't seem like your language includes the connective $\iff$. How should it be interpreted? Aren't there any propositional calculus rules? $\endgroup$
    – Git Gud
    Commented Dec 6, 2016 at 1:07
  • $\begingroup$ @GitGud $\iff$ is included yes, I only listed some of the axioms. $\endgroup$ Commented Dec 6, 2016 at 1:08
  • $\begingroup$ @GitGud You could interpret it as $(p \implies q) \wedge (q \implies p)$ $\endgroup$ Commented Dec 6, 2016 at 1:11

2 Answers 2


I see you were trying Quantifier Distribution and null Quantification so I assume it is ok to use equivalence rules.

Well, this is an immediate application of a Prenex Law:

$Q \land \exists x \phi(x) \Leftrightarrow \exists x (Q \land \phi(x))$

Where Q does not contain $x$ as a free variable.

If equivalence rules are not allowed, then we will need to know what inference rules you are allowed.

  • $\begingroup$ Yes I know about the Prenex Law but I still don't know how to write it formally. Would it be something along the lines of: $$[1]: 1. [\forall y Gy \wedge \exists x Hx] : Premise$$ $$[1]: 2.\forall y [Gy \wedge \exists xHx] :Prenex $$ $\endgroup$ Commented Dec 6, 2016 at 1:03
  • $\begingroup$ The Prenex Law is an equivalence principle ... I have never seen it as an inference rule. But, if it were an inference rule, it would go either way. $\endgroup$
    – Bram28
    Commented Dec 6, 2016 at 1:16

Here's a proof that I think complies with your rules.

Formal proof


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .