TY - JOUR
AU - Orlandelli, Eugenio
AU - Tesi, Matteo
PY - 2024/02/09
Y2 - 2024/10/14
TI - A Syntactic Proof of the Decidability of First-Order Monadic Logic
JF - Bulletin of the Section of Logic
JA - B Sect Log
VL - 53
IS - 2
SE - Article
DO - 10.18778/0138-0680.2024.03
UR - https://czasopisma.uni.lodz.pl/bulletin/article/view/18448
SP - 223-244
AB - <p>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 <strong>G3</strong>-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 <strong>T</strong>.</p>
ER -