When we're proving a statement with a goal of the form $\forall x P(x)$, we usually begin our proof by prenexing the universal quantifier to the entire formula. Afterwards, we proceed with the common proof techniques, until we check that the implication is valid. Let me give a generic example:
$\exists y \forall x P(x, y) \rightarrow \forall x \exists y P(x, y)$
$\forall u[\exists y \forall x P(x, y) \rightarrow \exists y P(u, y)]$ (prenex of $\forall x$)
$\forall u \forall v[\forall x P(x, v) \rightarrow \exists y P(u, y)]$ (EI of $\exists y \forall x P(x, y)$)
$\forall u \forall v[\forall x P(x, v) \land P(u, v) \rightarrow \exists y P(u, y)]$ (UI of $\forall x P(x, v)$)
$\forall u \forall v[\forall x P(x, v) \land P(u, v) \land \exists y P(u, y)\rightarrow \exists y P(u, y)]$ (EG of $P(u, v)$)
At this point, we know that the implication is valid. However, we still haven't performed the last universal generalization to complete the proof of the goal $\forall x P(x)$. The definition of universal generalization is if $Z \rightarrow P(n)$, then $Z \rightarrow \forall x P(x)$, where $Z$ is a formula in which the variable $n$ does not occur. In our example, the variable $u$ is both in the premise and in the conclusion of our implication. Thus, we cannot simply generalize the goal. So, how do we perform UG in such cases? I was wondering, since $\forall x [Q(x) \rightarrow P(x)]$ implies $\forall x Q(x) \rightarrow \forall x P(x)$, then we could generalize both premise and conclusion at the same time. Is this the standard solution?
FIRST EDIT on Mr. Velleman’s response: Your second interpretation is correct. In each line, I rewrite the previous one in a different form keeping the logical equivalence of the original line throughout the entire proof. When we derive the conclusion in the premise, the proof is complete, since we prove it is a tautology. I think that’s the most technical way to express proofs, since our reasoning is presented in a totally structured and concatenated way, without the usage of general expressions or ideas. It is in fact a bit confusing and definitely more complicated than the most common notations, but nonetheless very precise. In the following example, we prove Q(a) by inference from the premises $[P(a) \rightarrow Q(a)]$ and $P(a)$:
$[P(a) \rightarrow Q(a)] \land P(a) \rightarrow Q(a)$
$[P(a) \rightarrow Q(a)] \land P(a) \land Q(a) \rightarrow Q(a)$ (modus ponens)
In Section 3.3 of How to Prove It?, Velleman explains that, in order to prove a goal of the form $\forall x P(x)$, we should declare $x$ an arbitrary variable and prove $P(x)$. I understood this lesson as prenexing the universal quantifier in the goal, making its scope the entire proof. This corresponds, in the author textual presentation, to the line “let an arbitrary x” or “declare the variable x”. Example:
$\forall x [P(x) \rightarrow Q(x)] \land \forall x P(x) \rightarrow \forall x Q(x)$
$\forall y [\forall x [P(x) \rightarrow Q(x)] \land \forall x P(x) \rightarrow Q(y)]$ (prenexing the variable y: “let an arbitrary y”)
Afterwards, we manage to prove the goal. First, we universally instantiate $\forall x [P(x) \rightarrow Q(x)]$, using the universally declared variable y:
$\forall y [\forall x [P(x) \rightarrow Q(x)] \land [P(y) \rightarrow Q(y)] \land \forall x P(x) \rightarrow Q(y)]$
Then we universally instantiate $\forall x P(x)$:
$\forall y [\forall x [P(x) \rightarrow Q(x)] \land [P(y) \rightarrow Q(y)] \land \forall x P(x) \land P(y) \rightarrow Q(y)]$
Now, we infer Q(y) by modus ponens and conclude that our implication is valid:
$\forall y [\forall x [P(x) \rightarrow Q(x)] \land [P(y) \rightarrow Q(y)] \land \forall x P(x) \land P(y) \land Q(y) \rightarrow Q(y)]$
And now we arrive at the core of my problem. In Velleman’s textbook, he states that we should conclude the proof of a goal of the form $\forall x P(x)$ by deriving the universally quantified goal with the line “since $x$ is arbitrary, then $\forall x P(x)$”. In our example, that would be “since $y$ is arbitrary, then $\forall y Q(x)$”. I understood this line as a reference to the universal generalization step. However, if my supposition that the variable declaration of $y$ technically means prenexing it to the entire formula is correct, then we can’t simply apply universal generalization here, at least not according to its formal definition, precisely because the variable $y$ already appears in the premise of our proof as a free variable. Therefore, variable declaration in the sense of variable prenexing would not be compatible with universal generalization. Another possible interpretation would be to consider that the scope of the declared variable ranges exclusively over the premise of the proof. That seems what Velleman does in the Example 8 of his article Variable declarations in natural deduction. From this perspective, the universal generalization would be reduced to a mere prenex operation of the declared variable. Example:
$\forall x [P(x) \rightarrow Q(x)] \land \forall x P(x) \rightarrow \forall x Q(x)$
$\forall y [\forall x [P(x) \rightarrow Q(x)] \land \forall x P(x)] \rightarrow \forall x Q(x)$ (non-hypothetical declaration of the variable y)
$\forall y [\forall x [P(x) \rightarrow Q(x)] \land [P(y) \rightarrow Q(y)] \land \forall x P(x)] \rightarrow \forall x Q(x)$ (UI of $\forall x [P(x) \rightarrow Q(x)]$)
$\forall y [\forall x [P(x) \rightarrow Q(x)] \land [P(y) \rightarrow Q(y)] \land \forall x P(x) \land P(y)] \rightarrow \forall x Q(x)$ (universal instantiation of $\forall P(x)$)
$\forall y [\forall x [P(x) \rightarrow Q(x)] \land [P(y) \rightarrow Q(y)] \land \forall x P(x) \land P(y) \land Q(y)] \rightarrow \forall x Q(x)$ (modus ponens)
$\forall x [P(x) \rightarrow Q(x)] \land \forall y [P(y) \rightarrow Q(y)] \land \forall x P(x) \land \forall y P(y) \land \forall y Q(y) \rightarrow \forall x Q(x)$ (UG of $Q(y)$)
But then again, I’ve stumbled upon another problem. If the variable declaration ranges only over the premise, how it is possible to solve a proof with a goal of the form $\forall x P(x)$, which requires an assumption that is not in the list of the original premises. For example, let’s try to prove this:
$\forall x [P(x) \rightarrow Q(x)] \land \forall x [Q(x) \rightarrow R(x)] \rightarrow \forall x [P(x) \rightarrow R(x)]$
In this case, we need to assume $P(y)$ for an arbitrary $y$ and then infer $R(y)$ from our two premises $\forall x [P(x) \rightarrow Q(x)]$ and $\forall x [Q(x) \rightarrow R(x)]$. But how can we assume $P(y)$ without prenexing the universal quantifier in the goal, as demonstrated below?
$\forall x [P(x) \rightarrow Q(x)] \land \forall x [Q(x) \rightarrow R(x)] \rightarrow \forall x [P(x) \rightarrow R(x)]$
$\forall y [\forall x [P(x) \rightarrow Q(x)] \land \forall x [Q(x) \rightarrow R(x)] \rightarrow [P(y) \rightarrow R(y)]]$ (prenexing the variable y: “let an arbitrary y”)
$\forall y [\forall x [P(x) \rightarrow Q(x)] \land \forall x [Q(x) \rightarrow R(x)] \land P(y) \rightarrow R(y)]$ (“let P(y)”)
$\forall y [\forall x [P(x) \rightarrow Q(x)] \land [P(y) \rightarrow Q(y)] \land \forall x [Q(x) \rightarrow R(x)] \land [Q(y) \rightarrow R(y)] \land P(y) \rightarrow R(y)]$ (UI)
$\forall y [\forall x [P(x) \rightarrow Q(x)] \land [P(y) \rightarrow Q(y)] \land \forall x [Q(x) \rightarrow R(x)] \land [Q(y) \rightarrow R(y)] \land P(y) \land Q(y) \land R(y) \rightarrow R(y)]$ (modus ponens)
Thus, my second interpretation about what declaring an arbitrary variable formally means appears to me problematic, when dealing with proofs that require assumptions that come from goals, which are per se implications. Basically, I would like to know what declaring a variable formally means and its relation with the universal generalization.
SECOND EDIT on Mr Velleman’s response: I always interpreted the variable declaration as an operation which corresponds to prenexing an universal quantified variable. However, as I said in my previous explanation, this interpretation leads to the above mentioned problems with the universal generalization. To best clarify my third question, I will present a proof both in your textual system, as well as in mine, establishing a relation between every step we take. Let’s prove that $\forall x [P(x) \rightarrow R(x)]$ derives from $\forall x [P(x) \rightarrow Q(x)] \land \forall x [Q(x) \rightarrow R(x)]$.
In your system, we would have: (1) Suppose $\forall x [P(x) \rightarrow Q(x)]$ and $\forall x [Q(x) \rightarrow R(x)]$. (2) Let an arbitrary $y$. (3) Assume $P(y)$. (4) If $P(y)$ and $\forall x [P(x) \rightarrow Q(x)]$, then, by EI, $Q(y)$. (5) If $Q(y)$ and $\forall x [Q(x) \rightarrow R(x)]$, then $R(y)$. (6) Since $y$ is arbitrary, then, by EG and deduction, $\forall x [P(x) \rightarrow R(x)]$.
In my system:
(1) $\forall x [P(x) \rightarrow Q(x)] \land \forall x [Q(x) \rightarrow R(x)] \rightarrow \forall x [P(x) \rightarrow R(x)]$
(2) $\forall y[\forall x [P(x) \rightarrow Q(x)] \land \forall x [Q(x) \rightarrow R(x)] \rightarrow P(y) \rightarrow R(y)]$ (prenex the variable y)
(3) $\forall y[\forall x [P(x) \rightarrow Q(x)] \land \forall x [Q(x) \rightarrow R(x)] \land P(y) \rightarrow R(y)]$ (assume $P(y)$)
(4) $\forall y[\forall x [P(x) \rightarrow Q(x)] \land \forall x [Q(x) \rightarrow R(x)] \land P(y) \land Q(y) \rightarrow R(y)]$ (EI and inferring $Q(y)$)
(5) $\forall y[\forall x [P(x) \rightarrow Q(x)] \land \forall x [Q(x) \rightarrow R(x)] \land P(y) \land Q(y) \land R(y) \rightarrow R(y)]$ (EI and inferring $R(y)$)
Now, I can’t fully convert step (6) to my proof system. Though I can deduce $P(y) \rightarrow R(y)$ from $P(y)$ and $R(y)$, I can’t generalize $P(y) \rightarrow R(y)$ in the premise, since $y$ appears as a free variable. What I could possibly do is, since $\forall x [P(x) \rightarrow Q(x)]$ implies $\forall x P(x) \rightarrow \forall x Q(x)]$, then:
(6.1) $\forall x [P(x) \rightarrow Q(x)] \land \forall x [Q(x) \rightarrow R(x)] \land \forall y[P(y) \land Q(y) \land R(y)] \rightarrow \forall y R(y)$
(6.2) $\forall x [P(x) \rightarrow Q(x)] \land \forall x [Q(x) \rightarrow R(x)] \land \forall y[P(y) \land Q(y) \land R(y)] \land \forall y [P(y) \rightarrow R(y)] \rightarrow \forall y [P(y) \rightarrow R(y)]$
Even if this proof strategy generalizes both premise and conclusion and, thus, leads us to the conclusion we want, it is not universal generalization, at least not according to its formal definition.
Hence, my third question is, if the operation of variable declaration does not correspond to prenexing an universally quantified variable, then what does it mean? And how it is possible to universally generalize a proof with a goal of the form $\forall x [P(x) \rightarrow Q(x)]$?
Since the comments turned into a discussion of Example 8 in my paper "Variable declarations in natural deduction," I thought perhaps I should weigh in.
I find TylerD007's way of presenting logical reasoning very confusing, but I will do my best to figure out what he is thinking. In the chat discussion, he wrote: "I can't see how to express Velleman's results in a formal way." It appears, then, that he thinks my Example 8 is not expressed in a formal way, and it needs to be rewritten to make it formal. I think this is a misunderstanding. My Example 8 is already written in a formal way. It is a formal derivation, in the version of natural deduction that I present in the paper. It formalizes reasoning in a way that, I believe, closely matches the way mathematicians reason: each line either declares a variable, or introduces an assumption, or makes an inference from previous lines.
Apparently TylerD007 prefers a different way of formalizing logic, and in his original question, after a few introductory sentences, he presents his formalization in a list of five formulas. That list of formulas is not a formalization of my proof; my proof was already formalized. It is, rather, a different formal proof, in a different formal system. Perhaps it is inspired by my formal proof in Example 8, but it is not a formalization of that proof. And so the fact that the steps don't exactly match the steps in my proof is not a problem.
Now, what does TylerD007's list of five formulas mean? I have already explained how the lines of my formal proof represent the kinds of steps that mathematicians take when they are reasoning. What are TylerD007's steps?
One interpretation is that each line is an inference from the previous line. But that can't be right. It is wrong to start with what you are trying to prove and then make inferences until you reach a statement that you know is true. That's backwards. You have to start with what you know and make inferences leading to what you're trying to prove.
A second possible interpretation is that each line is meant to be a rewriting of the previous line in a different form. That's fine; one can prove a formula by rewriting it until you get it into a form that is clearly true. If that's what TylerD007 is doing, then I agree with Allegranza's interpretation that the first two steps appear to be the beginning of putting the formula into prenex form.
A third possible interpretation is that each line is supposed to be implied by the next line. At each step, TylerD007 is saying, in effect, "if we could establish this line, then the original goal would be proven." Again, that's fine, but it's not the usual way of writing logical reasoning. Most mathematicians would say that the steps are being written in the reverse of their natural order.
One minor quibble with Allegranza: He says that in my Example 8 I can generalize on $u$ because there is no free occurrence of $u$ in the premise. I would say I can generalize on $u$ because it was declared to be arbitrary in line 3. Now, it was only correct to declare it in line 3 because it was not yet declared, and that means that it couldn't appear free in the premise, so we get to the same conclusion. But I think my way of formalizing this more accurately reflects how mathematicians actually reason.