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.
2024
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].
Orlandelli, Eugenio; Tesi, Matteo
File in questo prodotto:
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/956479
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact