Is it typical for formal natural deduction systems to restrict theory axioms and deductions rules to ensure that only closed formulas (formulas with no free variables) appear in proofs? Or is the opposite true? Or does it vary system-by-system?
In a system that requires closed formulas then if we had $((\forall x )(P_x \land Q_x))$ we would be able to prove $((\forall x) P_x)$, but we would not be able to state $P_x\land Q_x$ as an axiom (since it is not closed) and we wouldn't be able to derive something like $(P_x\land Q_x)\implies P_x$.
In a system that does not require closed formulas then it would be straightforward to prove the last formula I mentioned.
I am curious if there is a standard practice in the field for these things. I'd also be interested in specific references which use one approach or the other.