I work relative to a fixed first-order language $L$. As usual I call those formulas which do not contain free variables sentences. There are several derivation systems for first-order logic. For example, in Goldrei's Propositional and Predicate Calculus a derivation of $\psi$ relative to a set $Ax$ of sentences is a list of formulas $\phi_1,....,\phi_n$ such that $\phi_n = \psi$ and each $\phi_j$ is either an axiom or can be obtained from the previous formulas via some rules. One such rule is for example that $\phi_j$ can be $\forall x\phi_k$ when $k<j$ and $x$ is free in $\phi_k$. There are also other derivation systems which manipulate sequents $$\phi_1,...,\phi_n\vdash_{\underline x} \psi_1,...,\psi_m$$according to rules, but here again the $\phi_i$ and $\psi_j$ are formulas.
Is this use of formulas instead of sentences essential, or just convenient? Are there derivation systems which only manipulate sentences and have (a reasonable amount) of rules which tell how to produce new proven sentences from already proven ones?
Motivation: I am working with a complicated semantic, and I can only define truth-conditions for closed formulas. I want to check that my semantic is sound, but I can not just check the rules blindly, because they are of the form "when those formulas are derivable, then so is that formula".