Abstract
We provide tools for a concise axiomatization of a broad class of quantifiers in many-valued logic, so-called distribution quantifiers. Although sound and complete axiomatizations for such quantifiers exist, their size renders them virtually useless for practical purposes. We show that for quantifiers based on finite distributive lattices compact axiomatizations can be obtained schematically. This is achieved by providing a link between skolemized signed formulas and filters/ideals in Boolean set lattices. Then lattice theoretic tools such as Birkhoff's representation theorem for finite distributive lattices are used to derive tableau-style axiomatizations of distribution quantifiers.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Baaz, M., and C. G. FermÜller, ‘Resolution-based theorem proving for many-valued logics’, Journal of Symbolic Computation 19(4):353–391, 1995.
Baaz, M., A. Leitsch, and R. Zach, ‘Incompleteness of a first-order Gödel logic and some temporal logics of programs’, in H. Kleine Büning, editor, Selected Papers from Computer Science Logic, CSL'95, Paderborn, Germany, volume 1092 of LNCS, p. 1–15. Springer-Verlag, 1996.
Birkhoff, G., Lattice Theory, volume XXV of AMS Colloquium Publications, American Mathematical Society, third (new) edition, 1970.
Carnielli, W. A., ‘Systematization of finite many-valued logics through the method of tableaux’, Journal of Symbolic Logic 52(2):473–493, 1987.
Carnielli, W. A., ‘On sequents and tableaux for many-valued logics’ Journal of Non-Classical Logic 8(1):59–76, 1991.
Davey, B. A., and H. A. Priestley, Introduction to Lattices and Order, Cambridge Mathematical Textbooks, Cambridge University Press, Cambridge, 1990.
Fitting, M. C., ‘Bilattices and the semantics of logic programming’ Journal of Logic Programming 11(2):91–116, 1991.
Fitting, M. C., First-Order Logic and Automated Theorem Proving, Springer-Verlag, New York, second edition, 1996.
Ginsberg, M. L., ‘Multi-valued logics’ Computational Intelligence 4(3), 1988.
HÄhnle, R., ‘Uniform notation of tableaux rules for multiple-valued logics’, in Proc. International Symposium on Multiple-Valued Logic, Victoria, p. 238–245, IEEE Press, Los Alamitos, 1991.
HÄhnle, R., Automated Deduction in Multiple-Valued Logics, volume 10 of International Series of Monographs on Computer Science, Oxford University Press, 1994.
Hay, L. S., ‘Axiomatization of the infinite-valued predicate calculus’ Journal of Symbolic Logic 28(1):77–86, 1963.
Mostowski A., ‘Axiomatizability of some many valued predicate calculi’, Fundamenta Mathematicœ L:165–190, 1961.
Ragaz, M. E., Arithmetische Klassifikation von Formelmengen der unendlichwertigen Logik, PhD thesis, ETH Zürich, 1981.
Rosser, J. B., and A. R. Turquette, Many-Valued Logics, North-Holland, Amsterdam, 1952.
Rousseau, G., ‘Sequents in many valued logic I’, Fundamenta Mathematicœ LX:23–33, 1967.
Salzer, G., ‘Optimal axiomatizations for multiple-valued operators and quantifiers based on semilattices’, in M. McRobbie and J. Slaney, editors, Proc. 13th Conference on Automated Deduction, New Brunswick/NJ, USA, volume 1104 of LNCS, p. 688–702, Springer-Verlag, 1996.
Scarpellini, B., ‘Die Nichtaxiomatisierbarkeit des unendlichwertigen Prädikatenkalküls von Łukasiewicz’, Journal of Symbolic Logic 27(2):159–170, 1962.
Smullyan, R. M., First-Order Logic, Dover Publications, New York, second corrected edition, 1995. First published 1968 by Springer-Verlag.
Takeuti, G., and S. Titani, ‘Intuitionistic fuzzy logic and intuitionistic fuzzy set theory’, Journal of Symbolic Logic 49(3):851–866, 1984.
Thiele, H., ‘On T-quantifiers and S-quantifiers’, in Proc. 24th International Symposium on Multiple-Valued Logics, Boston, USA, p. 264–269, IEEE Press, Los Alamitos, 1994.
WesterstÅhl, D., ‘Quantifiers in formal and natural languages’, in D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, Vol. IV: Topics in the Philosophy of Language, chapter 1, p. 1–131, Reidel, Dordrecht, 1989.
Zabel, N., Fr Nouvelles Techniques de Déduction Automatique en Logiques Polyvalentes Finies et Infinies du Premier Ordre, PhD thesis, Institut National Polytechnique de Grenoble, 1993.
Zach, R., ‘Proof theory of finite-valued logics’ Master's thesis, Institut für Algebra und Diskrete Mathematik, TU Wien, 1993. Available as Technical Report TUW-E185.2-Z.1-93.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Hähnle, R. Commodious Axiomatization of Quantifiers in Multiple-Valued Logic. Studia Logica 61, 101–121 (1998). https://doi.org/10.1023/A:1005086415447
Issue Date:
DOI: https://doi.org/10.1023/A:1005086415447