On the Algebraization of Some Gentzen Systems¹

Article type: Research Article

Authors: Rebagliato, Jordi | Verdú, Ventura

Affiliations: Faculty of Mathematics, University of Barcelona, Gran Via 585, 08007 Barcelona, Spain

Note: [1] Work partially supported by grants PB90-0465-C02-01 of the Spanish DGICYT and 91BV of the Ministry of Education and Science of Spain.

Abstract: In this paper we study the algebraization of two Gentzen systems, both of them generating the implication-less fragment of the intuitionistic propositional calculus. We prove that they are algebraizable, the variety of pseudocomplemented distributive lattices being an equivalent algebraic semantics for them, in the sense that their Gentzen deduction and the equational deduction over this variety are interpretable in one another, these interpretations being essentially inverse to one another. As a consequence, the consistent deductive systems that satisfy the properties of Conjunction, Disjunction and Pseudo-Reductio ad Absurdum are described by giving apropriate Gentzen systems for them. All these Gentzen systems are algebraizable, the subvarieties of the variety of pseudocomplemented distributive lattices being their equivalent algebraic semantics respectively. Finally we give a Gentzen system for the conjunction and disjunction fragment of the classical propositional calculus, prove that the variety of distributive lattices is an equivalent algebraic semantics for it and give a Gentzen system, weaker than the latter, the variety of lattices being an equivalent algebraic semantics for it.

DOI: 10.3233/FI-1993-182-417

Journal: Fundamenta Informaticae, vol. 18, no. 2-4, pp. 319-338, 1993