How do I prove FORMALLY that $\forall xPx\land\forall xQx\iff\forall x(Px\land Qx)$?

Question

I already understand the statement intuitively, so don't try to give me an intuitive explanation as that will not be helpful.

I would certainly be willing to "give my own attempts at solving the problem", but I legitimately have no idea on how to go about it. These "rules" (they're called "rules of inference" I think?) are simply to be taken intuitively/for granted no matter where I search, and there's just too many of them for them to simply be taken as axioms/to be true by definition.

Some "rules" of first-order that I am fine with taking for granted/intuitively/as axioms/by definition are the following (the domain of discorse is set $D$ and $c$ is an element of D):

$\forall xPx\implies Pc$

$Pc\implies \exists xPx$

The following, again, makes sense intuitively, but I still find it to be a stretch to take this "with no proof"/"as an axiom", simple as said proof may be:

$\neg\forall xPx\iff\exists x\neg Px$

The following (non-exhaustive) rules are even harder to make sense of intuitively (though they still do), and it's almost nonsensical to take them as axioms:

$\forall xPx\land\forall xQx\iff\forall x(Px\land Qx)$

$\forall xPx\lor\forall xQx\implies\forall x(Px\lor Qx)$

$\forall x(Px \land Q)\iff\forall xPx\land Q$

$\forall x\forall yP(x,y)\iff\forall y\forall xP(x,y)$

Answer 1

This depends entirely on your proof system. The things you said that you're fine with, are useful, but are probably not sufficient to give the necessary proof.

The proof system that I like most, allows for the proof of a sentence $\forall x \phi$ by letting $c$ be an arbitrary constant symbol. If we can prove $\phi(c)$ then we may infer $\forall x \phi$. (There are some relevant caveats about $x$ not being captured by any quantifier, but I'll ignore these technical issues since you can read about them in most symbolic logic textbooks.) In this particular case we will take $\phi = P(x)\land Q(x)$.

So assume $\forall x P(x)\land \forall x Q(x)$ and let $c$ be arbitrary. Then $\forall x P(x)$ and also $\forall x Q(x)$. From the former we obtain $P(c)$ and from the latter we obtain $Q(c)$ using the rules you said you were fine with. Then we have $P(c)\land Q(c)$. Therefore we may infer $\forall x (P(x)\land Q(x))$.

This demonstrates $\forall x P(x) \land \forall x Q(x)\Rightarrow \forall x(P(x)\land Q(x))$.

The converse is similar.

Answer 2

The usual way to do this is to start with propositional logic.

That is, you initially start with propositional logic rules such that "$\phi \vdash \phi \lor \psi $", or, "$\phi, \psi \vdash \phi \land \psi $".

Once propositional logic is done, for FOL you only have rules for intro and elimination of $\forall, \exists, =$; for example the forall elimination rule: $\forall xPx\implies Pc$.

Then using these you can prove more complex statements like $\forall xPx\land\forall xQx\iff\forall x(Px\land Qx)$

An example: Let's try to prove
$ \{\forall x (P(x) \lor Q(x)) , \lnot\exists x P(x) \} \vdash \forall x Q(x)$

1. $\{\forall x (P(x) \lor Q(x)) , \lnot\exists x P(x) \} \vdash \forall x (P(x) \lor Q(x)) $ Assumption
2. $\{\forall x (P(x) \lor Q(x)) , \lnot\exists x P(x) \} \vdash P(z) \lor Q(z) \hspace{20pt}$ $elim $ of $\forall$
3. $\{\forall x (P(x) \lor Q(x)) , \lnot\exists x P(x) \} \vdash \lnot\exists x P(x) $ Assumption
4. $\{\forall x (P(x) \lor Q(x)) , \lnot\exists x P(x), P(z) \} \vdash P(z) $ Assumption
5. $\{\forall x (P(x) \lor Q(x)) , \lnot\exists x P(x), P(z) \} \vdash \exists x P(x) \hspace{20pt}$ $intro$ of $ \exists$
6. $\{\forall x (P(x) \lor Q(x)) , \lnot\exists x P(x) \} \vdash \lnot P(z) \hspace{20pt}$ $intro$ of $\lnot$
7. $\{\forall x (P(x) \lor Q(x)) , \lnot\exists x P(x) \} \vdash Q(z) \hspace{20pt}$ using 2,6 and some propositional logic steps that i skip here as exercise
8. $\{\forall x (P(x) \lor Q(x)) , \lnot\exists x P(x) \} \vdash \forall x Q(x) \hspace{20pt}$ $intro$ of $ \forall$