# Formal proof with first order logic axioms.

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$$

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

• 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$$ Dec 6, 2016 at 1:03
• 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. Dec 6, 2016 at 1:16

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