Abstract
In this study, falsification-aware semantics and sequent calculi for first-order classical logic are introduced and investigated. These semantics and sequent calculi are constructed based on a falsification-aware setting for first-order Nelson constructive three-valued logic (N3). In fact, these semantics and sequent calculi are regarded as those for a classical variant of N3 (i.e., a classical variant of N3 is identical to first-order classical logic). The completeness and cut-elimination theorems for the proposed semantics and sequent calculi are proved using Schütte’s method. Similar results for the propositional case are also obtained.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Almukdad, A., & Nelson, D. (1984). Constructible falsity and inexact predicates. Journal of Symbolic Logic, 49(1), 231–233.
Arieli, O., & Avron, A. (1996). Reasoning with logical bilattices. Journal of Logic, Language and Information, 5, 25–63.
Arieli, O., & Avron, A. (1998). The value of the four values. Artificial Intelligence, 102(1), 97–141.
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., & Veith, H. (2003). Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM, 50(5), 752–794.
Czermak, J. (1977). A remark on Gentzen’s calculus of sequents. Notre Dame Journal of Formal Logic, 18, 471–474.
Gentzen, G. (1969). Collected papers of Gerhard Gentzen. In M.E. Szabo (Ed.) Studies in logic and the foundations of mathematics: North-Holland (English translation).
Goodman, N.D. (1981). The logic of contradiction. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 27, 119–126.
Gurevich, Y. (1977). Intuitionistic logic with strong negation. Studia Logica, 36, 49–59.
Gurfinkel, A., Wei, O., & Chechik, M. (2006). Yasm: a software model-checker for verification and refutation. Proceedings of the 18th International Conference on Computer Aided Verification (CAV, 2006, 170–174.
Horn, L.R., & Wansing, H. (2017). Negation, The Stanford encyclopedia of philosophy (Spring Edition). In E.N. Zalta (Ed.). Last modified on January 2017 https://plato.stanford.edu/archives/spr2017/entries/negation/.
Kamide, N. (2021). Cut-elimination, completeness, and Craig interpolation theorems for Gurevich’s extended first-order intuitionistic logic with strong negation. Journal of Applied Logics: IfColog Journal of Logics and their Applications, 8(5), 1101–1122.
Kamide, N., & Wansing, H. (2012). Proof theory of Nelson’s paraconsistent logic: A uniform perspective. Theoretical Computer Science, 415, 1–38.
Kamide, N., & Wansing, H. (2015). Proof theory of N4-related paraconsistent logics. Studies in Logic. College Publications, 54, 1–401.
Łukowski, P. (2002). A deductive-reductive form of logic: General theory and intuitionistic case. Logic and Logical Philosophy, 10, 59–78.
Nelson, D. (1949). Constructible falsity. Journal of Symbolic Logic, 14, 16–26.
Odintsov, S.P. (2002). On the embedding of Nelson’s logics. Bulletin of the Section of Logic, 31(4), 241–248.
Ono, H. (1994). Logic for information science (in Japanese), Nihon Hyouron Shya 297 pages.
Rauszer, C. (1974). A formalization of the propositional calculus of H-B logic. Studia Logica, 33, 23–34.
Rauszer, C. (1977). Applications of Kripke models to Heyting-Brouwer logic. Studia Logica, 36, 61–71.
Rauszer, C., & An, algebraic. (1980). Kripke-style approach to a certain extension of intuitionistic logic Dissertations Mathematicae. Polish Scientific Publishers, 1–67.
Rautenberg, W. (1979). Klassische und nicht-klassische Aussagenlogik. Braunschweig: Vieweg.
Seki, T. (2001). Some remarks on Maehara’s method. Bulletin of the Section of Logic, 30(3), 147–154.
Shramko, Y., & logic, Dual intuitionistic (2005). A variety of negations: The logic of scientific research. Studia Logica, 80(2-3), 347–367.
Takeuti, G. (2013). Proof theory, 2nd edn. New York: Dover Publications, Inc. Mineola.
Thomason, R.H. (1969). A semantical study of constructible falsity. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 15, 247–257.
Urbas, I. (1996). Dual-intuitionistic logic. Notre Dame Journal of Formal Logic, 37(3), 440–451.
Vorob’ev, N.N. (1952). A constructive propositional calculus with strong negation (in Russian). Doklady Akademii Nauk SSSR, 85, 465–468.
Wansing, H. (1993). The logic of information structures. Lecture Notes in Artificial Intelligence, 681, 163.
Wansing, H. (2016). Falsification, natural deduction and bi-intuitionistic logic. Journal of Logic and Computation, 26(1), 425–450.
Acknowledgments
We would like to thank the anonymous referees for their valuable comments. This research was supported by JSPS KAKENHI Grant Numbers JP18K11171 and JP16KK0007.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher’s Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
About this article
Cite this article
Kamide, N. Falsification-Aware Semantics and Sequent Calculi for Classical Logic. J Philos Logic 51, 99–126 (2022). https://doi.org/10.1007/s10992-021-09611-x
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10992-021-09611-x