Gentzen-Type Sequent Calculi for Extended Belnap–Dunn Logics with Classical Negation: A General Framework | Logica Universalis Skip to main content
Springer Nature Link
Log in

Gentzen-Type Sequent Calculi for Extended Belnap–Dunn Logics with Classical Negation: A General Framework

  • Published:
Logica Universalis Aims and scope Submit manuscript

Abstract

Gentzen-type sequent calculi GBD+, GBDe, GBD1, and GBD2 are respectively introduced for De and Omori’s axiomatic extensions BD+, BDe, BD1, and BD2 of Belnap–Dunn logic by adding classical negation. These calculi are constructed based on a small modification of the original characteristic axiom scheme for negated implication. Theorems for syntactically and semantically embedding these calculi into a Gentzen-type sequent calculus LK for classical logic are proved. The cut-elimination, decidability, and completeness theorems for these calculi are obtained using these embedding theorems. Similar results excluding cut-elimination results are also obtained for alternative Gentzen-type sequent calculi gBD+, gBDe, gBD1, and gBD2 for BD+, BDe, BD1, and BD2, respectively. These alternative calculi are constructed based on the original characteristic axiom scheme for negated implication.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Almukdad, A., Nelson, D.: Constructible falsity and inexact predicates. J. Symb. Log. 49(1), 231–233 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  2. Angell, R.: A propositional logics with subjunctive conditionals. J. Symb. Log. 27, 327–343 (1962)

    Article  MathSciNet  MATH  Google Scholar 

  3. Arieli, O., Avron, A., Zamansky, A.: Ideal paraconsistent logics. Stud. Log. 99(1–3), 31–60 (2011)

    MathSciNet  MATH  Google Scholar 

  4. Belnap, N.D.: A useful four-valued logic. In: Epstein, G., Dunn, J.M. (eds.) Modern Uses of Multiple-Valued Logic, pp. 5–37. Reidel, Dordrecht (1977)

    Chapter  Google Scholar 

  5. Belnap, N.D.: How a computer should think. In: Ryle, G. (ed.) Contemporary Aspects of Philosophy, pp. 30–56. Oriel Press, Stocksfield (1977)

    Google Scholar 

  6. Béziau, J.-Y.: A new four-valued approach to modal logic. Log. et Anal. 54(213), 109–121 (2011)

    MathSciNet  MATH  Google Scholar 

  7. De, M., Omori, H.: Classical negation and expansions of Belnap–Dunn logic. Stud. Log. 103(4), 825–851 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  8. Dunn, J.M.: Intuitive semantics for first-degree entailment and ‘coupled trees’. Philos. Stud. 29(3), 149–168 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  9. Gurevich, Y.: Intuitionistic logic with strong negation. Stud. Log. 36, 49–59 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  10. Kamide, N.: Paraconsistent double negations as classical and intuitionistic negations. Stud. Log. 105(6), 1167–1191 (2017)

    Article  MathSciNet  MATH  Google Scholar 

  11. Kamide, N.: Proof theory of paraconsistent quantum logic. J. Philos. Log. 47(2), 301–324 (2018)

    Article  MathSciNet  MATH  Google Scholar 

  12. Kamide, N., Omori, H.: An extended first-order Belnap–Dunn logic with classical negation. In: Proceedings of the 6th International Workshop on Logic, Rationality, and Interaction (LORI 2017), Lecture Notes in Computer Science, vol. 10455, pp. 79–93 (2017)

  13. Kamide, N., Shramko, Y.: Embedding from multilattice logic into classical logic and vice versa. J. Log. Comput. 27(5), 1549–1575 (2017)

    MathSciNet  MATH  Google Scholar 

  14. Kamide, N., Wansing, H.: Proof theory of Nelson’s paraconsistent logic: a uniform perspective. Theor. Comput. Sci. 415, 1–38 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  15. Kamide, N., Zohar, Y.: Yet another paradefinite logic: the role of conflation. Log. J. IGPL (Publisher online first) (2018)

  16. McCall, S.: Connexive implication. J. Symb. Log. 31, 415–433 (1966)

    Article  MathSciNet  MATH  Google Scholar 

  17. Meyer, R.K., Routley, R.: Classical relevant logics I. Stud. Log. 32(1), 51–68 (1973)

    Article  MathSciNet  MATH  Google Scholar 

  18. Nelson, D.: Constructible falsity. J. Symb. Log. 14, 16–26 (1949)

    Article  MathSciNet  MATH  Google Scholar 

  19. Odintsov, S.P.: The class of extensions of Nelson paraconsistent logic. Stud. Log. 80, 291–320 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  20. Omori, H., Waragai, T.: Some observations on the systems LFI1 and LFI1\(^*\). In: Proceedings of 22nd International Workshop on Database and Expert Systems Applications (DEXA 2011), pp. 320–324 (2011)

  21. Rautenberg, W.: Klassische und Nicht-klassische Aussagenlogik. Vieweg, Braunschweig (1979)

    Book  MATH  Google Scholar 

  22. Sano, K., Omori, H.: An expansion of first-order Belnap–Dunn logic. Log. J. IGPL 22(3), 458–481 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  23. Vorob’ev, N.N.: A constructive propositional calculus with strong negation. Dokl. Akad. Nauk SSSR 85, 465–468 (1952). (in Russian)

    Google Scholar 

  24. Wansing, H.: Connexive Logic, Stanford Encyclopedia of Philosophy. http://plato.stanford.edu/entries/logic-connexive/ (2014)

  25. Zaitsev, D.: Generalized Relevant Logic and Models of Reasoning. Moscow State Lomonosov University doctoral dissertation (2012)

Download references

Author information

Authors and Affiliations

  1. Department of Information and Electronic Engineering, Teikyo University, Toyosatodai 1-1, Utsunomiya, Tochigi, 320-8551, Japan

    Norihiro Kamide

Authors
  1. Norihiro Kamide
    View author publications

    You can also search for this author inPubMed Google Scholar

Corresponding author

Correspondence to Norihiro Kamide.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

We would like to thank the anonymous referees for their valuable comments. This research was supported by JSPS KAKENHI Grant Numbers JP18K11171, JP16KK0007 and JSPS Core-to-Core Program (A. Advanced Research Networks).

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Kamide, N. Gentzen-Type Sequent Calculi for Extended Belnap–Dunn Logics with Classical Negation: A General Framework. Log. Univers. 13, 37–63 (2019). https://doi.org/10.1007/s11787-018-0218-3

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11787-018-0218-3

Mathematics Subject Classification

Keywords