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

Question

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.

Answer 1

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.

Answer 2

$\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).