Abstract
We combine a tableau based calculus for intuitionistic logic with the system of tableau calculi for all finite-valued propositional logics. It is shown that these new calculi correspond to a family of logics that arise if we generalize Kripke models for intuitionistic logic to many-valued evaluations. We thus obtain a unique “intuitionistic counterpart” for each finite-valued logic, if one truth value is distinguished in a certain way. We also show that these new logics themselves are not finite-valued, except for trivial cases.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Baaz, M., C. G. Fermüller, and R. Zach. [1993] Dual systems of sequents and tableaux for many-valued logics. Bull. EATCS, 51, 192–197.
Beth, E. [1959] The Foundations of Mathematics. North-Holland Publishing Co.
Carnielli, W. A. [1987] Systematization of finite many-valued logics through the method of tableaux. J. Symbolic Logic, 52(2), 473–493.
Carnielli, W. A. [1991] On sequents and tableaux for many-valued logics. J. Non-Classical Logic, 8(1), 59–76.
Fitting, M. [1983] Proof Methods Modal and Intuitionistic Logics, Synthese Library 169. Synthese Library. D. Reidel Publishing Company, Dordrecht, Boston, Lancaster.
Gentzen, G. [1934] Untersuchungen über das logische Schließen I–II. Math. Z., 39, 176–210, 405–431.
Gödel, K. [1932] Zum intuitionistischen Aussagenkalkül. Anzeiger der Akademie der Wissenschaften in Wien, 69, 65–66.
Hähnle, R. [1991] Uniform notation of tableaux rules for multiple-valued logics. In Proc. IEEE International Symposium on Multiple-valued Logic, pp. 238–245.
Hähnle, R. [1993] Automated Proof Search in Multiple-Valued Logic. Oxford University Press, Oxford.
Kripke, S. [1963] Semantical analysis of intuitionistic logics. In Formal Systems and Recursive Functions, J. Crossley and M. Dummet, editors, pp. 92–129, North-Holland, Amsterdam.
Miglioli, P., U. Moscato, and M. Ornaghi. [1994a] How to avoid duplications in refutation systems for intuitionistic logic and Kuroda logic. In Theorem Proving with Analytic Tableaux and Related Methods, 3rd intl. Workshop, TABLEAUX 94, Abington, UK, K. Broda, M. D'Agostino, R. Gore, R. Johnson, and S. Reeves, editors, Imperial College of Science, Technology and Medicine TR-94/5, Imperial College of Science, Technology and Medicine, pp. 169–187.
Miglioli, P., U. Moscato, and M. Ornaghi. [1994b] An improved refutation system for intuitionistic predicate logic. Journal of Automated Reasoning, 13, 361–373.
Miglioli, P., U. Moscato, and M. Ornaghi. [1995] Refutation systems for propositional modal logics. In Theorem Proving with Analytic Tableaux and Related Methods, 4th intl. Workshop, TABLEAUX 95, Schloss Rheinfels, P. Baumgartner, R. Hähnle, and J. Posegga, editors, LNAI 918, pp. 95–105, Springer, Berlin.
Takeuti, G. [1987] Proof Theory. Studies in Logic 81. North-Holland, Amsterdam, 2nd edition.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baaz, M., Fermüller, C.G. (1996). Combining many-valued and intuitionistic tableaux. In: Miglioli, P., Moscato, U., Mundici, D., Ornaghi, M. (eds) Theorem Proving with Analytic Tableaux and Related Methods. TABLEAUX 1996. Lecture Notes in Computer Science, vol 1071. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61208-4_5
Download citation
DOI: https://doi.org/10.1007/3-540-61208-4_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61208-7
Online ISBN: 978-3-540-68368-1
eBook Packages: Springer Book Archive