Comparing Calculi for First-Order Infinite-Valued Łukasiewicz Logic and First-Order Rational Pavelka Logic
DOI:
https://doi.org/10.12775/LLP.2022.030Keywords
many-valued logic, mathematical fuzzy logic, first-order infinite-valued Lukasiewicz logic, first-order rational Pavelka logic, proof theory, Hilbert-type calculus, Gentzen-type hypersequent calculus, density elimination, conservative extensionAbstract
We consider first-order infinite-valued Łukasiewicz logic and its expansion, first-order rational Pavelka logic RPL∀. From the viewpoint of provability, we compare several Gentzen-type hypersequent calculi for these logics with each other and with Hájek’s Hilbert-type calculi for the same logics. To facilitate comparing previously known calculi for the logics, we define two new analytic calculi for RPL∀ and include them in our comparison. The key part of the comparison is a density elimination proof that introduces no cuts for one of the hypersequent calculi considered.
References
Baaz, M., A. Ciabattoni, and C. G. Fermüller, “Hypersequent calculi for Gödel logics – a survey”, Journal of Logic and Computation 13, 6 (2003): 835–861. DOI: http://dx.doi.org/10.1093/logcom/13.6.835
Baaz, M., and G. Metcalfe, “Herbrand’s theorem, skolemization and proof systems for first-order Łukasiewicz logic”, Journal of Logic and Computation 20, 1 (2010): 35–54. DOI: http://dx.doi.org/10.1093/logcom/exn059
Baaz, M., and R. Zach, “Hypersequents and the proof theory of intuitionistic fuzzy logic”, pages 187–201 in P. G. Clote and H. Schwichtenberg (eds.), Computer Science Logic: 14th International Workshop, CSL 2000, Lecture Notes in Computer Science 1862, Springer, Berlin, 2000. DOI: http://dx.doi.org/10.1007/3-540-44622-2_12
Baldi, P., “A note on standard completeness for some extensions of uninorm logic”, Soft Computing 18, 8 (2014): 1463–1470. DOI: http://dx.doi.org/10.1007/s00500-014-1265-1
Baldi, P., and A. Ciabattoni, “Standard completeness for uninorm-based logics”, pages 78–83 in 2015 IEEE International Symposium on MultipleValued Logic, IEEE, 2015. DOI: http://dx.doi.org/10.1109/ISMVL.2015.20
Baldi, P., and A. Ciabattoni, “Uniform proofs of standard completeness for extensions of first-order MTL”, Theoretical Computer Science 603 (2015): 43–57. DOI: http://dx.doi.org/10.1016/j.tcs.2015.07.014
Baldi, P., A. Ciabattoni, and F. Gulisano, “Standard completeness for extensions of IMTL”, pages 1–6 in 2017 IEEE International Conference on Fuzzy Systems, IEEE, 2017. DOI: http://dx.doi.org/10.1109/FUZZ-IEEE.2017.8015625
Baldi, P., A. Ciabattoni, and L. Spendier, “Standard completeness for extensions of MTL: an automated approach”, pages 154–167 in L. Ong and R. de Queiroz (eds.), Logic, Language, Information and Computation: 19th International Workshop, WoLLIC 2012, Lecture Notes in Computer Science 7456, Springer, Berlin, 2012. DOI: http://dx.doi.org/10.1007/978-3-642-32621-9_12
Chang, C. C., “A new proof of the completeness of the Lukasiewicz axioms”, Transactions of the American Mathematical Society 93, 1 (1959): 74–80. DOI: http://dx.doi.org/10.1090/S0002-9947-1959-0122718-1
Ciabattoni, A., and G. Metcalfe, “Bounded Łukasiewicz logics”, pages 32–47 in M. Cialdea Mayer and F. Pirri (eds.), Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX 2003, Lecture Notes in Computer Science 2796, Springer, Berlin, 2003. DOI: http://dx.doi.org/10.1007/978-3-540-45206-5_6
Ciabattoni, A., and G. Metcalfe, “Density elimination”, Theoretical Computer Science 403, 2–3 (2008): 328–346. DOI: http://dx.doi.org/10.1016/j.tcs.2008.05.019
Cignoli, R. L. O., I. M. L. D’Ottaviano, and D. Mundici, Algebraic Foundations of Many-Valued Reasoning, Kluwer Academic Publishers, Dordrecht, 2000. DOI: http://dx.doi.org/10.1007/978-94-015-9480-6
Cintula, P., P. Hájek, and C. Noguera (eds.), Handbook of Mathematical Fuzzy Logic, Vol. 1 and 2, College Publications, London, 2011.
Cintula, P., C. G. Fermüller, and C. Noguera (eds.), Handbook of Mathematical Fuzzy Logic, Vol. 3, College Publications, London, 2015.
Gerasimov, A. S., “Free-variable semantic tableaux for the logic of fuzzy inequalities”, Algebra and Logic 55, 2 (2016): 103–127. DOI: http://dx.doi.org/10.1007/s10469-016-9382-9
Gerasimov, A. S., “Infinite-valued first-order Łukasiewicz logic: hypersequent calculi without structural rules and proof search for sentences in the prenex form”, Siberian Advances in Mathematics 28, 2 (2018): 79–100. DOI: http://dx.doi.org/10.3103/S1055134418020013 (For errata, see Appendix A in arXiv: https://arxiv.org/abs/1812.04861v2.)
Gerasimov, A. S., “Repetition-free and infinitary analytic calculi for first-order rational Pavelka logic”, Siberian Electronic Mathematical Reports 17 (2020): 1869–1899. DOI: http://dx.doi.org/10.33048/semi.2020.17.127
Hájek, P., Metamathematics of Fuzzy Logic, Kluwer Academic Publishers, Dordrecht, 1998. DOI: http://dx.doi.org/10.1007/978-94-011-5300-3
Hájek, P., J. Paris, and J. Shepherdson, “Rational Pavelka predicate logic is a conservative extension of Łukasiewicz predicate logic”, Journal of Symbolic Logic 65, 2 (2000): 669–682. DOI: href="http://dx.doi.org/10.2307/2586560
Kleene, S. C., Mathematical Logic, Dover Publications, New York, 2002.
Metcalfe, G., “Proof theory for mathematical fuzzy logic”, pages 209–282 in [13], Vol. 1.
Metcalfe, G., and F. Montagna, “Substructural fuzzy logics”, Journal of Symbolic Logic 72, 3 (2007): 834–864. DOI: http://dx.doi.org/10.2178/jsl/1191333844
Metcalfe, G., N. Olivetti, and D. M. Gabbay, Proof Theory for Fuzzy Logics, Springer, Dordrecht, 2009. DOI: http://dx.doi.org/10.1007/978-1-4020-9409-5
Metcalfe, G., and C. Tsinakis, “Density revisited”, Soft Computing 21, 1 (2017): 175–189. DOI: http://dx.doi.org/10.1007/s00500-016-2420-7
Ragaz, M. E., Arithmetische klassifikation von formelmengen der unendlichwertigen logik, PhD thesis, ETH Zürich, Zürich, 1981. DOI: http://dx.doi.org/10.3929/ethz-a-000226207
Scarpellini, B., “Die nichtaxiomatisierbarkeit des unendlichwertigen prädikatenkalküls von Łukasiewicz”, Journal of Symbolic Logic 27, 2 (1962), 159–170. DOI: http://dx.doi.org/10.2307/2964111
Troelstra, A. S., and H. Schwichtenberg, Basic Proof Theory, 2nd ed., Cambridge University Press, Cambridge, 2000. DOI: http://dx.doi.org/10.1017/CBO9781139168717
Wang, S., “The logic of pseudo-uninorms and their residua”, Symmetry 11, 3 (2019), 368. DOI: http://dx.doi.org/10.3390/sym11030368
Wang, S., “A proof of the standard completeness for the involutive uninorm logic”, Symmetry 11, 4 (2019), 445. DOI: http://dx.doi.org/10.3390/sym11040445
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2022 Logic and Logical Philosophy
This work is licensed under a Creative Commons Attribution-NoDerivatives 4.0 International License.
Stats
Number of views and downloads: 1206
Number of citations: 0
