Is there truly convincing reason to allow natural deductions on formulas with free variables? I see some textbooks allow making deductions not only on first-order sentences(i.e., without free variables), but also formulas with free variables. For example, it is legal to write $\vdash Px\to\exists x Px$ in their book.
Well, I'd learned basic mathematical logic on Causey's book, which confined every line in a deduction proof(including premises, conclusion and middle steps) to be sentence only, and I feel quite comfortable about it. Now I'm turing to study classical mathematical logic, then suddenly I came up with this question. Why (some?) people accept doing something like this? Is there any convincing benefit?
 A: I can totally understand where you are coming from. Being  used to a proof system where every line has to be a sentence (i.e no free variables allowed!) I too find proof systems where free variables are involved 'disturbing' and somewhat 'ugly' ... though no doubt much of that is just what you are used to!
In the comments it is suggested that 'x' is nice to work with as a linguistic reference to some 'arbitrary' object, and that certainly makes sense, but you and I simply use some 'arbitrary' constant instead ... again, much of what makes 'sense' here is simply what we are used to.
Still, I think there actually is a good reason to be able to do logical inferences on general formulas. To see this, note that we can extend notions of logical equivalence, implication, etc. to formulas in general. E.g. $P(x) \lor \neg P(x)$ is a logical tautology in the sense that given any variable assignment and interpretation of $P$, the statement comes out true. 
And something like logical equivalence between formulas is actually a really important notion, as it allows us to claim that, for example, that the sentences $\forall x (P(x) \rightarrow Q(x))$ and $\forall x (\neg Q(x) \rightarrow \neg P(x))$ are logically equivalent by pointing out that their bodies are logically equivalent formulas and using the 'Substitution of logically equivalent formulas Principle' that claims that substituting logically equivalent formulas in larger formulas results in logically equivalent formulas formulas (this Principle is itself a generalization of the Substitution of logically equivalent sentences Principle of course).
Thus, there is some real use to being  able to generalise important logical concepts to formulas, rather than just  sentences. And so it would make sense to have a proof system that is able to prove those logical  properties and relationships for formulas in general.
