Fully adequate Gentzen systems and the deduction theorem
by Josep Maria Font, Ramon Jansana and Don Pigozzi
Reports on Mathematical Logic 35 (2001) 115--165
Abstract
An infinite sequence D = (D_n(x_{0}, . . . ,x_{n-1},y,u) : n\in\omega) of possibly infinite sets of formulas in n+1 variables x_{0}, . . . ,x_{n-1},y and a possibly infinite system of parameters u is a parameterized graded deduction-detachment (PGDD) system for a deductive system S over an S-theory T if, for every n\in\omega and for all formulas p_{0}, . . . ,p_{n-1},q, the following holds:
T, p_{0}, . . . ,p_{n-1},q |-_{S} if and only if for all u, T |-_{S} D_{n}(p_{0}, . . . ,p_{n-1},q,u)
An S-theory is Leibniz if it is included in every S-theory with the same Leibniz congruence.
A PGDD system D is Leibniz-generating if the union of the sets D_{n}(p_{0}, . . . ,p_{n-1},q,u) as u 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 (A,Fi_{S}A), where Fi_{S}A is the set of all S-filters on A.
The main results in this paper are:
- Theorem
- Let S be a protoalgebraic deductive system over a countable language type. If S has a Leibniz-generating PGDD system over all Leibniz theories, then S has a fully adequate Gentzen system.
- Theorem
- Let S be a protoalgebraic deductive system. If S has a fully adequate Gentzen system, then S has a Leibniz-generating PGDD system over all Leibniz theories.
- Corollary
- If S is a weakly algebraizable deductive system over a countable language type, then S has a fully adequate Gentzen system if and only if it has the multiterm deduction-detachment theorem.
- Corollary
- If S is a finitely equivalential deductive system over a countable language type, then S has a fully adequate Gentzen system if and only if there is a finite Leibniz-generating GDD system (i.e., a PGDD system without parameters) over all Leibniz theories.