Is simplification from 'or' ($\lor$) valid? The question in my text is :
Identify the error or errors in this argument that supposedly shows that if $\forall x (P (x ) \lor Q(x ))$ is true then $\forall x P(x) \lor \forall x Q(x)$ is true.
\begin{array}{l l l}
(1) & \forall x(P (x) \lor Q(x)) & \text{Premise} \\
(2) & P (c) \lor Q(c) & \text{Universal instantiation from }(1) \\
(3) & P (c) & \text{Simplification from }(2) \\
(4) & \forall x P (x ) & \text{Universal generalization from }(3) \\
(5) & Q(c) & \text{Simplification from }(2) \\
(6) & \forall xQ(x) & \text{Universal generalization from }(5) \\
(7) & \forall x(P (x) \lor \forall x Q(x)) & \text{Conjunction from } (4) \text{ and } (6)
\end{array}
According to me the errors occur at step 3, 5 and step 7. Step 3 because the rule for simplification is
$$(p \land q) \rightarrow p$$
and in step 7, it isn't conjunction but addition? Because rule of addition is $$ p \rightarrow (p \lor q)$$
Also step 5 because we can't assume that the $c$ that makes $P$ true is the same $c$ that makes $Q$ true.
Am I right?
 A: Depending on how the rules in your formal proof system are defined, steps 4 and 6 could be incorrect as well: when the $c$ is used for the universal instantiation, some formal proof systems consider that to be a specific individual and, as such, you can't apply universal generalization on that. Instead, these systems demand that either $c$ be 'marked' as an arbitrary individual from the domain, or that a temporary subproof structure be used, or that variables be used.
So, how is universal generalization defined? What text are you using?
A: You're correct, but your objection to step 7 is more about nomenclature (and cosmetics) which may differ somewhat. The step is otherwise correct since if we have $p$ then we can conclude $p\lor q$ (however we actually don't need to prove $q$ too for this step).
Also the instantiation means that you pick a specific $c$ from which you can't generalize later. However there are formalizations where one can do something similar (in which case $c$ isn't considered specific, but general).
I think the last comment is the most important and somewhat captures why the conclusion is not correct. It's about that in the first statement the variable $x$ work in unison in both $P$ and $Q$ while in the last they work independly (that is the last is the same as $\forall x\forall y(P(x)\lor Q(y))$).
