Finitely equivalential Gentzen systems and the reduced matrices of the Gentzen systems associated with finitely valued logics

• Autorzy: Gil A. J. , Rebagliato J.
• Języki publikacji: EN

Abstrakty

EN

uent calculus satisfying the cut elimination prop- erty and from which it is possible to dene all nitely valued logics determined by a matrix on the algebra. In this paper we study some algebraic properties of these sequent calculi. Our starting point is the denition of a Gentzen system as the consequence rela- tion determined by a sequent calculus over the set of (many-sided) sequents. For the Gentzen systems associated with an arbitrary - nite algebra we characterize the algebraic reducts of their reduced matrices as the quasivariety generated by the algebra. To prove this result we dene and study the basic properties of the nitely equivalential Gentzen systems. Throughout the paper dierent re- sults illustrate how to bridge the gap between the proof-theoretical and the algebraic properties of a sequent calculus.

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Reports on Mathematical Logic
• Rocznik: 2006
• Tom: Nr 41,spec. iss.
• Strony: 9--30
• Opis fizyczny: Bibliogr. 22 poz.

Twórcy

autor

Gil A. J.

autor

Rebagliato J.

• Dept. d'Economia Universitat Pompeu Fabra C/ Ramon Trias Fargas 25, 08005 Barcelona, Spain,

Bibliografia

• [1] Home page ot MUltlog: http://www.logic.at/multlog.
• [2] Home page ot MUltseq: http://www.logic.at/multseq.
• [3] A. Avron, Gentzen-type systems, resolution and tableaux, Journal of Automated Reasoning 10 (1993), pp. 265-281.
• [4] M. Baaz, C.G. Fermueller, A. Ovtrucki, and R. Zach, MULTLOG: A system for axiomatizing many valued logics, in A. Voronkov, editor, Logic Programming and Automated Reasoning. (LPAR'93) LNCS 698 (LNAI) , Springer, 1993, pp. 345-347.
• [5] M. Baaz, C.G. Fermueller, and R. Zach, Elimination of cuts in first-order finite-valued logics, Journal of Information Processing and Cybernetics. EIK, 29, 6 (1994), pp. 333-3554.
• [6] W.J. Blok and D. Pigozzi, Algebraizable Logics, volume 396 of Memoirs of the American Mathematical Society, AMS, Providence, January 1989.
• [7] 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 Quasigroups, Heldermann Verlag, Berlin 1992, pp. 1-56.
• [8] J. Czelakowski, Logic, algebra and consequence operations, Preprint, 1992.
• [9] J. Czelakowski, Protoalgebraic Logics, Kluwer Academic Publishers, The Netherlands 2001.
• [10] J.M. Font, R. Jansana, and D. Pigozzi, A survey of abstract algebraic logic, Studia Logica, Special Issue on Abstract Algebraic Logic, part II, 74(1/2) (2004), pp. 13-97.
• [11] A. J. Gil and Gernot Salzer, MUltseq: a generic prover for sequents and equations, Infederer (2000), pp. 53-89.
• [12] A.J. Gil, Sistemes de Gentzen Multidimensionals i lógiques finitament valorades.Teoria i aplicacions, PhD thesis, Facultat de Matemátiques, Universitat de Barcelona,1996. (In Catalan).
• [13] A.J. Gil, Sistemas de gentzen multidimensionales y sistemas deductivos asociados, In A. Estany and D. Quesada, editors, Actas II Congreso de la Sociedad de Lógica, Metodologa y Filosofía de la Ciencia en Espaňa, 1997, (In Spanish).
• [14] A.J. Gil and J. Rebagliato, Protoalgebraic Gentzen systems and the cut rule Studia Logica 65 (2000), pp. 53-89.
• [15] A.J. Gil, J. Rebagliato, and V. Verdú, A strong completeness theorem for the Gentzen systems associated with finite algebras, Journal of Applied Non-Classical Logics 9, 1 (1999), pp. 1-37.
• [16] A.J. Gil, A. Torrens, and V. Verdú, On Gentzen Systems Associated with the Finite Linear MV-algebras, Journal of Logic and Computation 7,4 (1997), pp. 473-500.
• [17] B. Herrmann, Equivalential Logics and Definability of Truth, PhD thesis, Freie Univ. Berlin, 1993.
• [18] J. Rebagliato and V. Verdú, Algebraizable Gentzen systems and the Deduction Theorem for Gentzen systems, Mathematics Preprint Series 175, Universitat de Barcelona, June 1995.
• [19] J. B. Rosser and A. R. Turquette, Many-Valued Logics, Studies in Logic, North-Holland, Amsterdam 1952.
• [20] G. Rousseau, Sequents in many valued logic I, Fundamenta Mathematicae 60 (1967), pp. 23-33.
• [21] G. Salzer, MUltlog: an expert system for multiple-valued logics, Collegium Logicum: Annals of the Kurt-Gödel-Society, 2 (1996), pp. 50-55.
• [22] R. Zach, Proof theory of finite-valued logics, Diplomarbeit, Technische Universität Wien, Vienna, Austria, 1993. Available as Technical Report E185.2-Z.1-93.