Universal Quantifier Distributes over Disjunction

Theorem

Let $\map \phi x, \map \psi x$ be WFFs of the free variable $x$.

Then:

$\paren {\forall x: \map \phi x} \lor \paren {\forall x: \map \psi x} \vdash \forall x: \paren {\map \phi x \lor \map \psi x}$

Proof

By the tableau method of natural deduction:

$\paren {\forall x: \map \phi x} \lor \paren {\forall x: \map \psi x} \vdash \forall x: \paren {\map \phi x \lor \map \psi x} $

Line		Pool	Formula	Rule	Depends upon	Notes
1		1	$\paren {\forall x: \map \phi x} \lor \paren {\forall x: \map \psi x}$	Premise
2		2	$\forall x: \map \phi x$	Assumption
3		2	$\map \phi {x \gets x_0}$	Universal Instantiation	2
4		2	$\map \phi {x \gets x_0} \lor \map \psi {x \gets x_0}$	Rule of Addition	3
5		5	$\forall x: \map \psi x$	Assumption
6		5	$\map \psi {x \gets x_0}$	Universal Instantiation	5
7		5	$\map \phi {x \gets x_0} \lor \map \psi {x \gets x_0}$	Rule of Addition	6
8		1	$\map \phi {x \gets x_0} \lor \map \psi {x \gets x_0}$	Proof by Cases	1, 2-4, 5-7
9		1	$\forall x: \paren {\map \phi x \lor \map \psi x}$	Universal Generalisation	8

$\blacksquare$