Saul Kripke famously invoked a free logic to avoid validating the Barcan Formula and its converse. In that context he adduced a *generality interpretation* of free variables. The converse of the Barcan formula is derivable in standard classical modal logic by noticing that $\Box(\forall x\alpha(x)\rightarrow\alpha(y))$ and so by distibution get $\Box\forall x\alpha(x)\rightarrow\Box\alpha(y)$ and so by generalization and a quantifier rule get $\Box\forall x\alpha(x)\rightarrow\forall y\Box\alpha(y)$. But this proof procedure is blocked by Kripke's approach as $\forall x\alpha(x)\rightarrow\alpha(y)$ is then not valid whereas $\forall y(\forall x\alpha(x)\rightarrow\alpha(y))$ is.


May one presuppose an axiomatic theory along such lines as this for theories with referring terms, such as Peano arithmetics or set theory with set terms, and avoid open sentences altogether (in such a theory for PA we would e.g. be allowed to instantiate with number terms as $SSS0$ but not with variables)? 



May open sentences be eliminated?
I don't know about modal logic, but for theories like PA and ZFC which use ordinary predicate calculus the answer is yes. You can formulate any first order predicate calculus only in terms of closed sentences. For intuitionistic logic this merely involves dropping the generalization rule from a Hilbert-style system and replacing modus ponens with: from $\overline{A}$ and $\overline{A \to B}$, infer $\overline{B}$, where $\overline{A}$ is any universal closure of $A$. To get classical logic, just include as axioms universal closures of all instances of the law of excluded middle. See Chapter 2, Section 4.4 of *Constructivism in Mathematics* vol. 1 by Troelstra and van Dalen.


