# A sound and complete proof system for $\forall$-first-order logic

There is, as is well-known, a sound and complete proof system for first-order logic. It is also known that equational logic, which is the fragment of first-order logic that concerns only universally quantified equations, has a sound and complete proof system. I am interested in a logic that is between equational logic and full first-order logic. I call it $$\forall$$-first-order logic, which, as its name implies, is the fragment of first-order logic which deals with $$\forall$$-formulas, which are universal closures of boolean combinations of atomic formulas. I want to know if there is a sound and complete proof system for this logic. Note, I consider it "cheating" to just use the proof system for full first-order logic. It has to be a set of axioms and inference rules that deal only with $$\forall$$-formulas, just like equational logic has a set of axioms and inference rules that deal only with equations. Also, I want to know, has this question been studied before, and if so, I would like some references that talk about this.

The subformula property of Gentzen's sequent calculus LK states that in a cut-free proof of $$\frac{\vdots}{\Gamma\vdash \Delta}$$ any formula appearing above the line is a subformula of a formula in $$\Gamma\cup \Delta$$.
LK is sound and complete with respect to the usual classical semantics. Moreover, by Gentzen's Hauptsatz, if $$\Gamma \vdash \Delta$$ has a sequent calculus proof, then it has a cut-free proof.