Fully adequate Gentzen systems and the deduction theorem (Q2772907)

A deductive system over a language \(\Lambda\) is called a Gentzen system if it has a finitary and substitution-invariant consequence relation over the sequents of \(\Lambda\). A Gentzen system \({\mathcal G}\) is said to be fully adequate for a deductive system \({\mathcal S}\) if every reduced generalized matrix model of \({\mathcal G}\) is of the form \(\langle{\mathcal A},{\mathcal F}_{\mathcal S} {\mathcal A}\rangle\), where \({\mathcal F}_{\mathcal S}\) is the set of all \({\mathcal S}\)-filters on an algebra \({\mathcal A}\). This paper gives a complete characterization of protoalgebraic deductive systems that have a fully adequate Gentzen system. Namely, the authors prove:NEWLINENEWLINENEWLINEMain Theorem: A protoalgebraic deductive system \({\mathcal S}\) has a fully adequate Gentzen system if and only if it has a Leibniz-generating PGDD (parametrized graded deduction-detachment) system \(\Delta\) over every Leibniz theory.NEWLINENEWLINENEWLINEAs corollaries to this theorem, two important results are proved:NEWLINENEWLINENEWLINE(i) A weakly algebraizable deductive system has a fully adequate Gentzen system iff it has the multiterm deduction-detachment theorem;NEWLINENEWLINENEWLINE(ii) A finitely equivalential deductive system has a fully adequate Gentzen system iff it has a finite Leibniz-generating system over all Leibniz \({\mathcal S}\)-filters.