Sibirskie Èlektronnye Matematicheskie Izvestiya [Siberian Electronic Mathematical Reports]
RUS  ENG    JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB  
General information
Latest issue
Archive
Impact factor

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Sib. Èlektron. Mat. Izv.:
Year:
Volume:
Issue:
Page:
Find






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


Sib. Èlektron. Mat. Izv., 2020, Volume 17, Pages 1869–1899 (Mi semr1321)  

Mathematical logic, algebra and number theory

Repetition-free and infinitary analytic calculi for first-order rational Pavelka logic

A. S. Gerasimov

Peter the Great St.Petersburg Polytechnic University (SPbPU), 29, Polytechnicheskaya str., St. Petersburg, 195251, Russia

Abstract: We present an analytic hypersequent calculus $\textnormal{G}^3\textnormalŁ\forall$ for first-order infinite-valued Łukasiewicz logic $\textnormalŁ\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Ł\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Ł\forall$ proves any sentence that is provable in at least one of the previously known analytic calculi for $\textnormalŁ\forall$ or $\textnormal{RPL}\forall$, including Baaz and Metcalfe's hypersequent calculus $\textnormal{G}\textnormalŁ\forall$ for $\textnormalŁ\forall$. We study proof-theoretic properties of $\textnormal{G}^3\textnormalŁ\forall$ and thereby provide foundations for proof search algorithms. We also give the first correct proof of the completeness of the $\textnormal{G}\textnormalŁ\forall$-based infinitary calculus for prenex $\textnormalŁ\forall$-sentences, and establish the completeness of a $\textnormal{G}^3\textnormalŁ\forall$-based infinitary calculus for prenex $\textnormal{RPL}\forall$-sentences.

Keywords: many-valued logic, mathematical fuzzy logic, first-order infinite-valued Łukasiewicz logic, first-order rational Pavelka logic, proof theory, hypersequent calculus, proof search, infinitary calculus.

DOI: https://doi.org/10.33048/semi.2020.17.127

Full text: PDF file (597 kB)
References: PDF file   HTML file

Bibliographic databases:

UDC: 510.644, 510.662
MSC: 03B50, 03B52, 03F07, 03B35
Received March 30, 2020, published November 18, 2020

Citation: A. S. Gerasimov, “Repetition-free and infinitary analytic calculi for first-order rational Pavelka logic”, Sib. Èlektron. Mat. Izv., 17 (2020), 1869–1899

Citation in format AMSBIB
\Bibitem{Ger20}
\by A.~S.~Gerasimov
\paper Repetition-free and infinitary analytic calculi for first-order rational Pavelka logic
\jour Sib. \`Elektron. Mat. Izv.
\yr 2020
\vol 17
\pages 1869--1899
\mathnet{http://mi.mathnet.ru/semr1321}
\crossref{https://doi.org/10.33048/semi.2020.17.127}


Linking options:
  • http://mi.mathnet.ru/eng/semr1321
  • http://mi.mathnet.ru/eng/semr/v17/p1869

    SHARE: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Number of views:
    This page:40
    Full text:10
    References:1

     
    Contact us:
     Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2022