# Prove the formula $(\forall x Px \wedge \forall x Qx) \leftrightarrow \forall x [Px \wedge Qx]$

I'm sure this implication is correct. However, are there rules on how one can manipulate with quantifiers? It might somehow be related to whether no free variables are becoming bounded after the operation.

• Are you asking how to prove $(\forall x P(x))\land(\forall x Q(x))$ is equivalent to $\forall x (P(x)\land Q(x))$?
– Karl
Commented Nov 19, 2023 at 17:38
• If so, the details will depend on the deductive system you're using. See e.g. natural deduction.
– Karl
Commented Nov 19, 2023 at 17:43
• The proof might be more straightforward if you made the domain of discourse explicit: $\forall x:[U(x) \to P(x)] \land \forall x:[ U(x) \to Q(x)] \iff \forall x:[U(x) \to P(x) \land Q(x)]$ Commented Nov 19, 2023 at 21:09

Below I offer a syntactic proof using a first-order logic natural deduction system and the following inference rules:

$$\begin{array}{l} \text{- conditional proof (CP)} \\ \text{- universal elimination (\forall Elim)} \\ \text{- universal introduction (\forall Intro)} \\ \text{- conjunction elimination (\wedge Elim)} \\ \text{- conjunction introduction (\wedge Intro)} \\ \text{- biconditional introduction (\leftrightarrow Intro)} \\ \end{array}$$

Let the propositional functions $$Px$$ and $$Qx$$ be defined as follows:

$$\begin{array}{ll} Px: & x \notin A \vee x \in C \\ Qx: & x \notin B \vee x \in C \\ \end{array}$$

Then, we show

$$\vdash (\forall x Px \wedge \forall x Qx) \leftrightarrow \forall x [Px \wedge Qx]$$

as follows:

$$\begin{array}{llll} \{1\} & 1. & \forall x Px \wedge \forall x Qx & \text{Assumption for CP} \\ \{1\} & 2. & \forall x Px & \text{1 \wedge Elim} \\ \{1\} & 3. & Pa & \text{2 \forall Elim} \\ \{1\} & 4. & \forall x Qx & \text{1 \wedge Elim} \\ \{1\} & 5. & Qa & \text{4 \forall Elim} \\ \{1\} & 6. & Pa \wedge Qa & \text{3,5 \wedge Intro} \\ \{1\} & 7. & \forall x [Px \wedge Qx] & \text{6 \forall Intro} \\ \{\emptyset\} & 8. & (\forall x Px \wedge \forall x Qx) \to \forall x [Px \wedge Qx] & \text{1,7 CP} \\ \{9\} & 9. & \forall x [Px \wedge Qx] & \text{Assumption for CP} \\ \{9\} & 10. & Pa \wedge Qa & \text{9 \forall Elim} \\ \{9\} & 11. & Pa & \text{10 \wedge Elim} \\ \{9\} & 12. & \forall x Px & \text{11 \forall Intro} \\ \{9\} & 13. & Qa & \text{10 \wedge Elim} \\ \{9\} & 14. & \forall x Qx & \text{13 \forall Intro} \\ \{9\} & 15. & \forall x Px \wedge \forall x Qx & \text{12,14 \wedge Intro} \\ \{\emptyset\} & 16. & \forall x [Px \wedge Qx] \to (\forall x Px \wedge \forall x Qx) & \text{9,15 CP} \\ \{\emptyset\} & 17. & (\forall x Px \wedge \forall x Qx) \leftrightarrow \forall x [Px \wedge Qx] & \text{8,16 \leftrightarrow Intro} & \square \\ \end{array}$$

In short, we begin by assuming $$\forall x Px \wedge \forall x Qx$$ on line $$1$$, and we derive $$\forall x [Px \wedge Qx]$$ on line $$7$$ under that assumption. Thus, we are justified in saying "if $$\forall x Px \wedge \forall x Qx$$ is the case, then $$\forall x [Px \wedge Qx]$$ is the case." This is meaning of the conditional formula $$(\forall x Px \wedge \forall x Qx) \to \forall x [Px \wedge Qx]$$ on line $$8$$. We use analogous reasoning to infer the conditional formula $$\forall x [Px \wedge Qx] \to (\forall x Px \wedge \forall x Qx)$$ on line $$16$$. As a result of deriving both conditionals, we may say "$$\forall x Px \wedge \forall x Qx$$ is the case if and only if $$\forall x [Px \wedge Qx]$$ is the case." This is the meaning of the biconditional formula $$(\forall x Px \wedge \forall x Qx) \leftrightarrow \forall x [Px \wedge Qx]$$ derived on line $$17$$.

In the future, it would be helpful if you specified the type of proof you prefer (formal, informal, etc), the proof format (Suppes, Fitch, etc), the formal system (natural deduction, axiomatic, etc), and any axioms or inference rules of the system. I understand this may sound like a foreign language to a novice, so I went ahead and made a few assumptions and answered your question.

$$\forall x \ Px \land \forall x \ Qx \implies \begin{cases} \forall x \ Px \implies Px \\ \forall x \ Qx \implies Qx \end{cases} \implies Px \land Qx \implies \forall x \ (Px \land Qx)$$ (via conjunction elimination, universal quantifier elimination, conjunction introduction, and universal quantifier introduction respectively).

$$\forall x \ (Px \land Qx) \implies Px \land Qx \implies \begin{cases} Px \implies \forall x \ Px \\ Qx \implies \forall x \ Qx \end{cases} \implies \forall x \ Px \land \forall x \ Qx$$ (via universal quantifier elimination, conjunction elimination, universal quantifier introduction, and conjunction introduction respectively).