Fully adequate Gentzen systems and the deduction theorem
Josep Maria Font-Llagunes, Ramón Jansana, Don Pigozzi · 2001
. An infinite sequence \\Delta = h\\Delta n(x0 ; : : : ; xn\\Gamma1 ; y; u) : n ! !i of possibly infinite sets of formulas in n + 1 variables x0 ; : : : ; xn\\Gamma1 ; y and a possibly infinite system of parameters u is a parameterized graded deduction-detachment (PGDD) system for a deductive system S over a S-theory T if, for every n ! ! and for all '0 ; : : : ; 'n\\Gamma1 ; / 2 Fm , T; '0 ; : : : ; 'n\\Gamma1 `S / iff T `S \\Delta n('0 ; : : : ; 'n\\Gamma1 ; /; #) for every possible system of formulas #. A S-theory is Leibniz if it is included in every S-theory with the same Leibniz congruence. A PGDD system \\Delta is Leibniz generating if the union of the \\Delta n ('0 ; : : : ; 'n\\Gamma1 ; /; #) as # ranges over all systems of formulas generates a Leibniz theory. A Gentzen system G is fully adequate for a deductive system S if (roughly speaking) every reduced generalized matrix model of G is of the form hA; FiS Ai, where FiS A is the set of all S-filters on A. Theorem. Let...