Monotonic and nonmonotonic gentzen deduction systems for L₃-valued propositional logic

Abstract

A sequent is a pair (Γ, Δ), which is true under an assignment if either some formula in Γ is false, or some formula in Δ is true. In L₃-valued propositional logic, a multisequent is a triple Δ|Θ|Γ, which is true under an assignment if either some formula in Δ has truth-value t, or some formula in Θ has truth-value m, or some formula in Γ has truth-value f. Correspondingly there is a sound and complete Gentzen deduction system G for multisequents which is monotonic. Dually, a comultisequent is a triple Δ : Θ : Γ, which is valid if there is an assignment v in which each formula in Δ has truth-value≠t, each formula in Θ has truth-value≠m, and each formula in Γ has truth-value≠f. Correspondingly there is a sound and complete Gentzen deduction system G⁻ for co-multisequents which is nonmonotonic.

Keywords

three-valued logic / multisequent / co-multisequent / monotonicity / Gentzen deduction system

References

[1] Hähnle R. Advanced many-valued logics. In: Gabbay D M, Guenthner F, eds. Handbook of Philosophical Logic, Vol.2. Springer, Netherlands, 2001, 297–395

[2] Malinowski G. Many-valued logic and its philosophy. In: Gabbay D M, Woods J, eds. Handbook of The History of Logic, Vol.8, The Many Valued and Nonmonotonic Turn in Logic. Elsevier, 2009

[3] Bochvar D A, Bergmann M. On a three-valued logical calculus and its application to the analysis of the paradoxes of the classical extended functional calculus. History and Philosophy of Logic, 1981, 2(1–2): 87–112

[4] Łukasiewicz J. Selected Works. Amsterdam: North-Holland, 1970

[5] Sobocínski B. Axiomatization of a partial system of three-value calculus of propositions. The Journal of Computing Systems, 1952, 1(1): 23–55

[6] Avron A. Natural 3-valued logics-characterization and proof theory. The Journal of Symbolic Logic, 1991, 56(1): 276–294

[7] Wansing H. The power of Belnap: sequent systems for SIXTEEN3. Journal of Philosophical Logic, 2010, 39(4): 369–393

[8] Avron A. On the expressive power of three-valued and four-valued languages. Journal of Logic and Computation, 2000, 9(6): 977–994

[9] Zach R. Proof theory of finite-valued logics, Technical Report TUWE185.2- Z.1-93. Institut Für Computersprachen, Technische Universität Wien, 1993

[10] Gabbay D M. Labelled Deductive Systems. Oxford: Oxford University Press, 1996

[11] Fitting MC. Many-valued modal logics. Fundamenta Informaticae, 1991, 15(3): 235–254

[12] Li W, Sui Y F. Multisequent gentzen deduction systems for B22-valued first-order logic. Journal of Artificial Intelligence Research, 2018, 7(1): 53

[13] Gottwald S. A Treatise on Many-Valued Logics, Studies in Logic and Computation, Vol.9. Baldock: Research Studies Press Ltd., 2001

[14] Reiter R. A logic for default reasoning. Artificial Intelligence, 1980, 13(1–2): 81–132

[15] Ginsberg M L. Readings in Nonmonotonic Reasoning. San Francisco: Morgan Kaufmann Publishers, 1987

[16] Clark K. Negation as failure. In: Ginsberg M L, ed. Readings in Non monotonic Reasoning. Morgan Kaufmann Publishers, 1987, 311–325

[17] Takeuti G. Proof theory. In: Barwise J, ed. Handbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics. Amsterdam, NL: North-Holland, 1987

[18] Cao C, Chen B, Sui Y. The B₄-valued propositional Belnap-Dunn logic. Journal of Intelligent and Fuzzy Systems, 2015, 28: 2705–2713

[19] Urquhart A. Basic many-valued logic. In: Gabbay D M, Guenthner F, eds. Handbook of Philosophical Logic, Vol.2. Springer, Netherlands, 2001, 249–295

RIGHTS & PERMISSIONS

Higher Education Press