Decidability of monadic first-order classical logic was established by L ̈owenheimin 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.
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 [10.18778/0138-0680.2024.03].
A Syntactic Proof of the Decidability of First-Order Monadic Logic
Orlandelli, Eugenio
;Tesi, Matteo
2024
Abstract
Decidability of monadic first-order classical logic was established by L ̈owenheimin 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.File | Dimensione | Formato | |
---|---|---|---|
E.+Orlandelli,+M.+Tesi,+BSL,+3,+2024.pdf
accesso aperto
Tipo:
Versione (PDF) editoriale
Licenza:
Licenza per Accesso Aperto. Creative Commons Attribuzione - Non commerciale - Non opere derivate (CCBYNCND)
Dimensione
823.94 kB
Formato
Adobe PDF
|
823.94 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.