2
$\begingroup$

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.

$\endgroup$

1 Answer 1

5
$\begingroup$

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.

Since the set of universal closures of boolean combinations of atomic formulas is in fact closed under subformulas, we immediately get that the cut-free sequent calculus restricted to only your allowed formulae constitutes a sound and complete proof system for your logic. Note that there is no "cheating": this restricted system is indeed a set of axioms and inference rules dealing only with ∀-formulas.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .