Geodesic
Repetition-free and infinitary analytic calculi for first-order rational Pavelka logic
Sibirskie èlektronnye matematičeskie izvestiâ, Tome 17 (2020), pp. 1869-1899.

Voir la notice de l'article provenant de la source Math-Net.Ru

We present an analytic hypersequent calculus $\textnormal{G}^3\textnormal{\L}\forall$ for first-order infinite-valued Łukasiewicz logic $\textnormal{\L}\forall$ and for an extension of it, first-order rational Pavelka logic $\textnormal{RPL}\forall$; the calculus is intended for bottom-up proof search. In $\textnormal{G}^3\textnormal{\L}\forall$, there are no structural rules, all the rules are invertible, and designations of multisets of formulas are not repeated in any premise of the rules. The calculus $\textnormal{G}^3\textnormal{\L}\forall$ proves any sentence that is provable in at least one of the previously known analytic calculi for $\textnormal{\L}\forall$ or $\textnormal{RPL}\forall$, including Baaz and Metcalfe's hypersequent calculus $\textnormal{G}\textnormal{\L}\forall$ for $\textnormal{\L}\forall$. We study proof-theoretic properties of $\textnormal{G}^3\textnormal{\L}\forall$ and thereby provide foundations for proof search algorithms. We also give the first correct proof of the completeness of the $\textnormal{G}\textnormal{\L}\forall$-based infinitary calculus for prenex $\textnormal{\L}\forall$-sentences, and establish the completeness of a $\textnormal{G}^3\textnormal{\L}\forall$-based infinitary calculus for prenex $\textnormal{RPL}\forall$-sentences.
Keywords: many-valued logic, mathematical fuzzy logic, first-order rational Pavelka logic, proof theory, hypersequent calculus, proof search, infinitary calculus.
Mots-clés : first-order infinite-valued Łukasiewicz logic 
@article{SEMR_2020_17_a40,
     author = {A. S. Gerasimov},
     title = {Repetition-free and infinitary analytic calculi for first-order rational {Pavelka} logic},
     journal = {Sibirskie \`elektronnye matemati\v{c}eskie izvesti\^a},
     pages = {1869--1899},
     publisher = {mathdoc},
     volume = {17},
     year = {2020},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/SEMR_2020_17_a40/}
}
TY  - JOUR
AU  - A. S. Gerasimov
TI  - Repetition-free and infinitary analytic calculi for first-order rational Pavelka logic
JO  - Sibirskie èlektronnye matematičeskie izvestiâ
PY  - 2020
SP  - 1869
EP  - 1899
VL  - 17
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/SEMR_2020_17_a40/
LA  - ru
ID  - SEMR_2020_17_a40
ER  - 
%0 Journal Article
%A A. S. Gerasimov
%T Repetition-free and infinitary analytic calculi for first-order rational Pavelka logic
%J Sibirskie èlektronnye matematičeskie izvestiâ
%D 2020
%P 1869-1899
%V 17
%I mathdoc
%U http://geodesic.mathdoc.fr/item/SEMR_2020_17_a40/
%G ru
%F SEMR_2020_17_a40
A. S. Gerasimov. Repetition-free and infinitary analytic calculi for first-order rational Pavelka logic. Sibirskie èlektronnye matematičeskie izvestiâ, Tome 17 (2020), pp. 1869-1899. http://geodesic.mathdoc.fr/item/SEMR_2020_17_a40/

[1] P. Hájek, Metamathematics of fuzzy logic, Kluwer Academic Publishers, Dordrecht, 1998 | MR | Zbl

[2] P. Cintula, P. Hájek, C. Noguera (ed.), Handbook of mathematical fuzzy logic, v. 1, College Publications, London, 2011 ; v. 2 | MR | Zbl | Zbl

[3] P. Cintula, C.G. Fermüller, C. Noguera (ed.), Handbook of mathematical fuzzy logic, v. 3, College Publications, London, 2015 | Zbl

[4] M. Baaz, G. Metcalfe, “Herbrand's theorem, Skolemization and proof systems for first-order Łukasiewicz logic”, J. Log. Comput., 20:1 (2010), 35–54 | DOI | MR | Zbl

[5] G. Metcalfe, N. Olivetti, D.M. Gabbay, Proof theory for fuzzy logics, Springer, Dordrecht, 2009 | MR | Zbl

[6] A.S. Gerasimov, “Free-variable semantic tableaux for the logic of fuzzy inequalities”, Algebra Logic, 55:2 (2016), 103–127 | DOI | MR | Zbl

[7] A.S. Gerasimov, “Infinite-valued first-order Łukasiewicz logic: hypersequent calculi without structural rules and proof search for prenex sentences”, Mat. Tr., 20:2 (2017), 3–34 (in Russian) ([8] is an English translation of this paper) | MR | Zbl

[8] A.S. Gerasimov, “Infinite-valued first-order Łukasiewicz logic: hypersequent calculi without structural rules and proof search for sentences in the prenex form”, Sib. Adv. Math., 28:2 (2018), 79–100 (this paper is an English translation of [7]) ; for errata, see Appendix A in arXiv: 1812.04861v2 | DOI | MR | Zbl

[9] B. Scarpellini, “Die nichtaxiomatisierbarkeit des unendlichwertigen prädikatenkalküls von Łukasiewicz”, J. Symb. Log., 27:2 (1963), 159–170 | DOI | MR | Zbl

[10] M.E. Ragaz, Arithmetische klassifikation von formelmengen der unendlichwertigen logik, PhD thesis, ETH Zürich, Zürich, 1981

[11] L.S. Hay, “Axiomatization of the infinite-valued predicate calculus”, J. Symb. Log., 28:1 (1964), 77–86 | DOI | MR | Zbl

[12] L.P. Belluce, C.C. Chang, “A weak completeness theorem for infinite valued first-order logic”, J. Symb. Log., 28:1 (1964), 43–50 | DOI | MR | Zbl

[13] G. Metcalfe, “Proof theory for mathematical fuzzy logic”, Handbook of mathematical fuzzy logic, v. 1, College Publications, London, 2011, 209–282 | MR | Zbl

[14] N.K. Kosovski, A.V. Tishkov, “Polynomial-time algorithms for verifying consistency of systems of strict and nonstrict linear inequalities in rationals and integers”, Current problems of modern mathematics, Collection of scientific works, v. 3, ed. V.P. Chuvakov, NII MIOO NGU, Novosibirsk, 1997, 95–100 | Zbl

[15] S.C. Kleene, Mathematical logic, Dover Publications, Mineola, NY, 2002 | MR | Zbl

[16] A.S. Troelstra, H. Schwichtenberg, Basic proof theory, Cambridge Tracts in Theoretical Computer Science, 43, 2nd ed., Cambridge University Press, Cambridge, 2000 | MR | Zbl

[17] G. Gentzen, “Untersuchungen über das logische schliessen. I; II”, Math. Zeitschrift, 39 (1934), 176–210 ; 405–431 | DOI | MR | Zbl | Zbl

[18] A.S. Gerasimov, Comparing several calculi for first-order infinite-valued Łukasiewicz logic, 2018, arXiv: 1812.05297 | MR

[19] V. Nigam, E. Pimentel, G. Reis, “An extended framework for specifying and reasoning about proof systems”, J. Log. Comput., 26:2 (2016), 539–576 | DOI | MR | Zbl

[20] C. Olarte, E. Pimentel, C. Rocha, “Proving structural properties of sequent systems in rewriting logic”, Lect. Notes Comp. Sci., 11152, ed. V. Rusu, 2018, 115–135 | DOI | MR