A SYNTACTIC PROOF OF THE DECIDABILITY OF FIRST-ORDER MONADIC LOGIC.

Decidability of monadic first-order classical logic was established by L¨owenheim 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. [ABSTRACT FROM AUTHOR]