Universal Quantifier Distributes over Conjunction
Jump to navigation
Jump to search
Theorem
Let $\map \phi x, \map \psi x$ be WFFs of the free variable $x$.
Then:
- $\forall x: \paren {\map \phi x \land \map \psi x} \dashv \vdash \paren {\forall x: \map \phi x} \land \paren {\forall x: \map \psi x}$
Proof
Forward Implication
By the tableau method of natural deduction:
Line | Pool | Formula | Rule | Depends upon | Notes | |
---|---|---|---|---|---|---|
1 | 1 | $\forall x: \paren {\map \phi x \land \map \psi x}$ | Premise | |||
2 | 1 | $\map \phi {x \gets x_0} \land \map \psi {x \gets x_0}$ | Universal Instantiation | 1 | ||
3 | 1 | $\map \phi {x \gets x_0}$ | Rule of Simplification | 2 | ||
4 | 1 | $\forall x: \map \phi x$ | Universal Generalisation | 3 | ||
5 | 1 | $\map \psi {x \gets x_0}$ | Rule of Simplification | 2 | ||
6 | 1 | $\forall x: \map \psi x$ | Universal Generalisation | 5 | ||
7 | 1 | $\paren {\forall x: \map \phi x} \land \paren {\forall x: \map \psi x}$ | Rule of Conjunction | 4, 6 |
$\Box$
Reverse Implication
By the tableau method of natural deduction:
Line | Pool | Formula | Rule | Depends upon | Notes | |
---|---|---|---|---|---|---|
1 | 1 | $\paren {\forall x: \map \phi x} \land \paren {\forall x: \map \psi x}$ | Premise | |||
2 | 1 | $\forall x: \map \phi x$ | Rule of Simplification | 1 | ||
3 | 1 | $\map \phi {x \gets x_0}$ | Universal Instantiation | 2 | ||
4 | 1 | $\forall x: \map \psi x$ | Rule of Simplification | 1 | ||
5 | 1 | $\map \psi {x \gets x_0}$ | Universal Instantiation | 4 | ||
6 | 1 | $\map \phi {x \gets x_0} \land \map \psi {x \gets x_0}$ | Rule of Conjunction | 3, 5 | ||
7 | 1 | $\forall x: \paren {\map \phi x \land \map \psi x}$ | Universal Generalisation | 6 |
$\blacksquare$