Formal proof of the statement

Question

Given two formulae $\varphi $ and $\varphi '$, how does one formally prove the following statement?

$$\forall x (\varphi (x)\wedge \varphi'(x))\equiv \forall y \varphi (y)\wedge \forall z \varphi'(z)$$

Answer 1

I don't know if this up to your standards of rigor, but here's how I'd do it.

Remark. If you truly want a "formal proof," you'll need to specify what deductive system you're working in. Anyway, what follows is what I'd call a "rigorous, informal proof."

$(\Longrightarrow)$ Suppose $\forall x[\phi(x) \wedge \phi'(x)].$

Let $x$ be arbitrary.

---

Then $\phi(x) \wedge \phi'(x)$.

Thus $\phi(x)$, and also $\phi'(x)$.

Since we have shown $\phi(x)$ under the assumption that $x$ is arbitrary, we may conclude $\forall x \phi(x)$. Similarly, we may conclude $\forall x \phi'(x)$. Thus

$$\forall x \phi(x) \wedge \forall x \phi'(x)$$

as required.

$(\Longleftarrow)$ Suppose $\forall x \phi(x) \wedge \forall x \phi'(x)$. Thus

$$[1] \quad \forall x \phi(x)$$

$$[2] \quad \forall x \phi'(x)$$

Let $x$ be arbitrary.

---

Then by [1], we have $\phi(x)$.

And by [2], we have $\phi'(x)$.

Thus $\phi(x) \wedge \phi'(x)$.

Since we have shown $\phi(x) \wedge \phi'(x)$ under the assumption that $x$ is arbitrary, we may conclude that $$\forall x[\phi(x) \wedge \phi'(x)]$$ as required.