Sequent type system in which all formulae are closed In most presentations of the sequent calculus, the formulae that appear in a sequent $\Delta \vdash \Gamma$ may be open; i.e., may have free variables.
I am looking for elegant presentations of something like the sequent calculus for predicate logic

*

*that are complete, and


*in which all the formulae in $\Delta$, $\Gamma$ must be closed (i.e., have no free variables.)
 A: You are looking for a proof system that either contains infinitely many schemas of inference rules (which is not good at all for a proof system), or is not much more expressive than propositional logic (which is useless if the goal if to be complete for predicate logic). Indeed, in any sequent calculus that is complete for predicate logic, formulas in a sequent need in general to be open. Why?
Consider for example the sequent
$$\tag{1}\vdash \forall x \, P(x) \to \exists x \, P(x)$$
This sequent should be provable in a complete sequent calculus for predicate logic, because the formula $\forall x \, P(x) \to \exists x \, P(x)$ is valid, that is, it is satisfied in every structure for predicate logic (under the usual assumption that the domain of a structure is not empty).
The usual way to prove $(1)$ in the sequent calculus is the following derivation, which contains open formulas.
$$
\dfrac{\dfrac{\dfrac{}{P(x)\vdash P(x)}ax}{P(x) \vdash \exists x P(x)}\exists_R}{\dfrac{\forall x P(x) \vdash \exists x P(x)}{\vdash \forall x P(x) \to \exists x P(x)}\to_R}\forall_L
$$
In a standard sequent calculus, there is no way to prove $(1)$ without dealing with open formulas.
Apparently, a possible workaround would be to add an inference rule (or an axiom) of the form
\begin{align}\tag{1'}
\dfrac{}{\vdash \forall x P(x) \to \exists x P(x)} 
&& or && 
\dfrac{}{\forall x P(x) \vdash \exists x P(x)} 
&& or &&
\dfrac{\forall x P(x)}{\exists x P(x)}
\end{align}
to the sequent calculus, so that $(1)$ can be proved without dealing with open formulas.
But then, consider the sequent
$$\tag{2}
\vdash \exists x \forall y \, Q(x,y) \to  \forall y \exists x \, Q(x,y)
$$
This sequent should be provable in a complete sequent calculus for predicate logic, because the formula $\exists x \forall y \, Q(x,y) \to \forall y\exists x \, Q(x,y)$ is valid.
The usual way to prove $(2)$ in the sequent calculus is a derivation that contains open formulas, similarly to the derivation to prove $(2)$.
And in a standard sequent calculus, even if the rules $(1')$ are added to it, there is no way to prove $(2)$ without dealing with open formulas.
Again, a possible workaround would be to add an inference rule (or an axiom) of the form
\begin{align}\tag{2'}
\dfrac{}{\vdash \exists x \forall y Q(x,y) \to \forall y \exists x Q(x,y)} 
&& or && 
\dfrac{}{\exists x \forall y Q(x,y) \vdash \forall y \exists x Q(x,y)} 
&& or &&
\dfrac{\exists x \forall y Q(x,y)}{\forall y \exists x Q(x,y)}
\end{align}
to the sequent calculus, so that $(2)$ can be proved without dealing with open formulas.
But then, it is easy to find another sequent that expresses a valid formula with quantifiers but that cannot be proved in a seuqnt calculus where the rules $(1')$ and $(2')$ are added.
You can endlessly repeat this argument: find a sequent that can be proved only by dealing with open formulas, add that sequent as an axiom or inference rule to the sequent calculus (so that it can be proved without dealing with open formulas), find another sequent that can be proved only by dealing with open formulas (even in the extended sequent calculus).
Finally, if the sequent calculus is required to deal only with closed formulas, then

*

*either the sequent calculus is complete but it contains infinitely many of schemas of inference rules (or axioms), and this is not a good structural property for a proof system (it would be like having an axiom for every valid formula);


*or the sequent calculus contains finitely many schemas  of inference rules or axioms (which is a good structural property for a proof system) but it is not complete for predicate logic because it cannot prove infinitelymany closed formulas with quantifiers (such a sequent calculus is complete for propositional logic only).
