Opis

• Tytuł:
  A Syntactic Proof of the Decidability of First-Order Monadic Logic
• Twórca:
  Orlandelli, Eugenio;
  Tesi, Matteo
• Współtwórca:
  Orlandelli, Eugenio - University of Bologna, Department of the Arts, Bologna, Italy;
  Tesi, Matteo - Vienna University of Technology, Faculty of Informatics, Vienna, Austria;
  Orlandelli, Eugenio - eugenio.orlandelli@unibo.it;
  Tesi, Matteo - tesi@logic.at
• Opis:
  Decidability of monadic first-order classical logic was established by Löwenheim in 1915. The proof made use of a semantic argument and a purely syntactic proof has never been provided. In the present paper we introduce a syntactic proof of decidability of monadic first-order logic in innex normal form which exploits G3-style sequent calculi. In particular, we introduce a cut- and contraction-free calculus having a (complexity-optimal) terminating proof-search procedure. We also show that this logic can be faithfully embedded in the modal logic T.
• Dostępność obiektu:
  Dostęp otwarty
• Prawa: https://creativecommons.org/licenses/by-nc-nd/4.0
• Data:
  2024.06.24;
  2024.02.09
• Typ:
  Article
• Język:
  angielski
• Format:
  application/pdf
• Wydawca:
  Wydawnictwo Uniwersytetu Łódzkiego
• Relacja:
  Bulletin of the Section of Logic;2;
  53
• Temat i słowa kluczowe:
  proof theory;
  classical logic;
  decidability;
  Herbrand theorem
• Identyfikator:
  0138-0680;
  http://hdl.handle.net/11089/52598 ;
  2449-836X;
  10.18778/0138-0680.2024.03
• Dostawca danych:
  Repozytorium Uniwersytetu Łódzkiego
• Czy mogę z tego obiektu skorzystać?:
  sprawdź warunki licencji
• Rodzaj zawartości:
  obrazy