##
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