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
    Dec 6 '16 at 0:22
  • $\begingroup$ @GitGud Yes, I will edit it. $\endgroup$ Dec 6 '16 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
    Dec 6 '16 at 1:07
  • $\begingroup$ @GitGud $\iff$ is included yes, I only listed some of the axioms. $\endgroup$ Dec 6 '16 at 1:08
  • $\begingroup$ @GitGud You could interpret it as $(p \implies q) \wedge (q \implies p)$ $\endgroup$ Dec 6 '16 at 1:11

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$ Dec 6 '16 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
    Dec 6 '16 at 1:16

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

Formal proof


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.