Orlandelli, E., & Tesi, M. (2024). A Syntactic Proof of the Decidability of First-Order Monadic Logic. Bulletin of the Section of Logic, 53(2), 223–244. https://doi.org/10.18778/0138-0680.2024.03
classical logic; decidability; Herbrand theorem; proof theory
en
Abstract:
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.
en
Project title:
Logical methods for Deontic Explanations: I 6372 (FWF - Österr. Wissenschaftsfonds)
