Reports on Mathematical Logic

No.35


Josep Maria Font, Ramon Jansana, and Don Pigozzi

Fully adequate Gentzen Systems and the Deduction Theorem

A b s t r a c t. An infinite sequence $\bgD=\<\gD_n(\seq x0{n-1},y,\vu):n<\bgo\>$ of possibly infinite sets of formulas in $n+1$ variables $\seq x0{n-1},y$ and a possibly infinite system of parameters $\vu$ is a \emph{parameterized graded deduction-detachment} (PGDD) \emph{system} for a deductive system $\bcS$ over a $\bcS$-theory $T$ if, for every $n<\bgo$ and for all $\seq\gph0{n-1},\gps\in\Fm_\gL$, $T,\seq\gph0{n-1}\ent_\bcS\gps$ iff $T\ent_\bcS\gD_n(\seq\gph0{n-1},\gps,\vgth)$ for every possible system of formulas $\vgth$. A $\bcS$-theory is \emph{Leibniz} if it is included in every $\bcS$-theory with the same Leibniz congruence. A PGDD system $\bgD$ is \emph{Leibniz generating} if the union of the $\gD_n(\seq\gph0{n-1},\gps,\vgth)$ as $\vgth$ ranges over all systems of formulas generates a Leibniz theory.
A Gentzen system $\bcG$ is \emph{fully adequate} for a deductive system $\bcS$ if (roughly speaking) every reduced generalized matrix model of $\bcG$ is of the form $\<\sbA,\Fi_\bcS\sbA\>$, where $\Fi_\bcS\sbA$ is the set of all $\bcS$-filters on $\sbA$.

Theorem.
Let $\bcS$ be a protoalgebraic deductive system over a countable language type. If $\bcS$ has a Leibniz-generating PGDD system over all Leibniz theories, then $\bcS$ has a fully adequate Gentzen system.

Theorem.
Let $\bcS$ be a protoalgebraic deductive system. If $\bcS$ has a fully adequate Gentzen system, then $\bcS$ has a Leibniz-generating PGDD system over every Leibniz theory.

Corollary.
If $\bcS$ is a weakly algebraizable deductive system over a countable language type, then $\bcS$ has a fully adequate Gentzen system iff it has the multiterm deduction-detachment theorem.

Corollary.
If $\bcS$ is a finitely equivalential deductive system over a countable language type, then $\bcS$ has a fully adequate Gentzen system iff there is a finite Leibniz-generating \textup{GDD} system for $\bcS$ over all Leibniz $\bcS$-filters.


Back to Main Menu