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 proofhas never been provided. In the present paper we introduce a syntactic proof ofdecidability of monadic first-order logic in innex normal form which exploitsG3-style sequent calculi. In particular, we introduce a cut- and contraction-freecalculus having a (complexity-optimal) terminating proof-search procedure. We also show that this logic can be faithfully embedded in the modal logic T.
Matteo Tesi
PostDoc Researcher (Marie Curie Individual Fellowship)
Matteo’s research focuses on non-classical (modal, intermediate, and substructural) logics, structural proof theory and their philosophical applications. He has worked with sequent calculi and their generalizations (hypersequents, nested sequents, and labelled sequents) to offer analytic presentations of families of non-classical logics.