Fully adequate Gentzen systems and the deduction theorem

• Autorzy: Font J. , Jansana R. , Pigozzi D.
• Języki publikacji: EN

Abstrakty

EN

A deductive system over an arbitrary language type A is a finitary and substitution-invariant consequence relation over the formulas of A. A Gentzen system is a finitary and substitution-invariant consequence relation over the sequents of A. A matrix model of a deductive system S is a pair (A,F) where A is A-algebra and F is an S-filter on A, i.e., a subset of A closed under all interpretations of the consequence relation of S in A. A generalized matrix is a pair (A,C) where C is an algebraic closed-set system over A; it is a model of a Gentzen system G if C is closed under all interpretations of the consequence relation of G in A. 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, FisA), where FisA is the set of all S-filters on A. The existence of a fully adequate Gentzen system for a given protoalgebraic deductive system S is completely characterized in terms of the following variant of the standard deduction theorem of classical and intuitionistic logic. The main result of the paper is the following: Theorem. A protoalgebraic deductive system has a fully adequate Gentzen system if and only if it has a Leibniz-generating PGDD (a parameterized graded deduction-detachment) system over all Leibniz theories. Two corollaries: (I) A weekly algebraizable deductive system has a fully adequate Gentzen system iff it has the multiterm deduction-detachment theorem. (II) A finitely equivalential deductive system has a fully adequate Gentzen system iff it has a finite Leibniz-generating system for over all Leibniz S-filters. Several different variants of the deduction theorem arise in the course of the paper showing that this familiar notion is only one manifestation of a surprisingly complex phenomenon.

Słowa kluczowe

EN

abstract algebraic logic; protoalgebraic logic; Leibniz congruence; deduction theorem; adequate Gentzen system

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Reports on Mathematical Logic
• Rocznik: 2001
• Tom: No. 35
• Strony: 115--165
• Opis fizyczny: Bibliogr. 22 poz.

Twórcy

autor

Font J.

• Faculty of Mathematics University of Barcelona Gran Via 585 E-08007 Barcelona Spain

autor

Jansana R.

• Faculty of Philosophy University of Barcelona Baldiri Reixach, s.n. E-08028 Barcelona Spain

autor

Pigozzi D.

• Department of Mathematics Iowa State University Ames, IA 50011 USA

Bibliografia

• [1] W. J. Blok and D. Pigozzi, Abstract algebraic logic and the deduction theorem, Bull. of Symbolic Logic, to appear.
• [2] W. J. Blok and D. Pigozzi, Protoalgebraic logics, Studia Logica, 45 (1986), 337–369.
• [3] W. J. Blok and D. Pigozzi, Algebraizable logics, volume 396 of Mem. Amer. Math. Soc. American Mathematical Society, Providence, January 1989.
• [4] W. J. Blok and D. Pigozzi, Local deduction theorems in algebraic logic, in J. D. Andréka, H. Monk and I. Németi, editors, Algebraic Logic (Proc. Conf. Budapest 1988), volume 54 of Colloq. Math. Soc. János Bolyai, pages 75–109. North-Holland, Amsterdam, 1991.
• [5] W. J. Blok and D. Pigozzi, Algebraic semantics for universal Horn logic without equality, in A. Romanowska and J. D. H. Smith, editors, Universal Algebra and Quasigroup Theory, pages 1–56. Heldermann, Berlin, 1992.
• [6] J. Czelakowski, Equivalential logics I and II, Studia Logica, 40 (1981), 227–236 and 355–372.
• [7] J. Czelakowski, Algebraic aspects of deduction theorems, Studia Logica, 44 (1985), 369–387.
• [8] J. Czelakowski, Consequence operations. Foundational studies, Technical report, Institute of Philosophy and Sociology. Polish Academy of Science, Warszawa, 1992.
• [9] J. Czelakowski and W. Dziobiak, A deduction theorem schema for deductive systems of propositional logics, Studia Logica, Special Issue on Algebraic Logic, 50 (1991), 385–390.
• [10] J. Czelakowski and R. Jansana, Weakly algebraizable logics, J. Symbolic Logic, 65 (2000), 641–668.
• [11] J. Czelakowski and D. Pigozzi, Fregean logics, Technical Report 440, Centre de Recerca Matem`atica, Apartat 50, D-08193 Bellaterra, Spain, September 2000.
• [12] J. Czelakowski and D. Pigozzi, Fregean logics with the multiterm deduction theorem and their algebraization, Technical Report 433, Centre de Recerca Matemática, Apartat 50, D-08193 Bellaterra, Spain, February 2000.
• [13] J. M. Font, On the Leibniz congruences, in C. Rauszer, editor, Algebraic Methods in Logic and in Computer Science, number 28 in Banach Center Publications, pages 17–36. Polish Academy of Sciences, Warszawa, 1993.
• [14] J. M. Font and R. Jansana, Leibniz filters and the strong version of a protoalgebraic logic, Archive for Mathematical Logic, to appear.
• [15] J. M. Font and R. Jansana, A general algebraic semantics for sentential logics. Number 7 in Lecture Notes in Logic. Springer-Verlag, 1996.
• [16] J. M. Font, R. Jansana, and D. Pigozzi, Fully adequate Gentzen systems and closure properties of the class of full models, Preprint.
• [17] J. M. Font and V. Verd´u, Algebraic logic for classical conjunction and disjunction, Studia Logica, 50 (1991), 391–419.
• [18] B. Herrmann, Equivalential and algebraizable logics, Studia Logica, 57 (1996), 419–436.
• [19] B. Herrmann, Characterizing equivalential and algebraizable logics by the Leibniz operator, Studia Logica, 58 (1997), 305–323.
• [20] T. Prucnal and A. Wroński, An algebraic characterization of the notion of structural completeness, Bull. Section of Logic, 3 (1974), 30–33.
• [21] J. Rebagliato and V. Verd´u, On the algebraization of some Gentzen systems, Fund. Inform., Special Issue on Algebraic Logic and its Applications, 18 (1993), 319–338.
• [22] V. V. Rybakov, Admissibility of logical inference rules, volume 136 of Studies in Logic and the Foundations of Mathematics, Elsevier Science Ltd., 1997.