Description

• Title:
  A Syntactic Proof of the Decidability of First-Order Monadic Logic
• Creator:
  Orlandelli, Eugenio;
  Tesi, Matteo
• Contributor:
  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
• Description:
  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.
• Object availability:
  free access
• Rights: https://creativecommons.org/licenses/by-nc-nd/4.0
• Date:
  2024.06.24;
  2024.02.09
• Type:
  Article
• Language:
  English
• Format:
  application/pdf
• Publisher:
  Wydawnictwo Uniwersytetu Łódzkiego
• Relation:
  Bulletin of the Section of Logic;2;
  53
• Subject:
  proof theory;
  classical logic;
  decidability;
  Herbrand theorem
• Identifier:
  0138-0680;
  http://hdl.handle.net/11089/52598 ;
  2449-836X;
  10.18778/0138-0680.2024.03
• Data provider:
  Repozytorium Uniwersytetu Łódzkiego
• Can I use it?:
  check license
• Type:
  image