A Syntactic Proof of the Decidability of First-Order Monadic Logic

Eugenio Orlandelli; Matteo Tesi

doi:10.18778/0138-0680.2024.03

Authors

Eugenio Orlandelli University of Bologna, Department of the Arts, Bologna, Italy Author https://orcid.org/0000-0002-4021-8667
Matteo Tesi Vienna University of Technology, Faculty of Informatics, Vienna, Austria Author

DOI:

https://doi.org/10.18778/0138-0680.2024.03

Keywords:

proof theory, classical logic, decidability, Herbrand theorem

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.

References

G. S. Boolos, J. P. Burgess, R. C. Jeffrey, Computability and Logic, 5th ed., Cambridge University Press, Cambridge (2007), DOI: https://doi.org/10.1017/CBO9780511804076 DOI: https://doi.org/10.1017/CBO9780511804076

T. Bräuner, A cut-free Gentzen formulation of the modal logic S5, Logic Journal of the IGPL, vol. 8(5) (2000), pp. 629–643, DOI: https://doi.org/10.1093/jigpal/8.5.629 DOI: https://doi.org/10.1093/jigpal/8.5.629

A. Church, A note on the Entscheidungsproblem, The Journal of Symbolic Logic, vol. 1(1) (1936), p. 40–41, DOI: https://doi.org/10.2307/2269326 DOI: https://doi.org/10.2307/2269326

H. R. Lewis, Complexity results for classes of quantificational formulas, Journal of Computer and System Sciences, vol. 21(3) (1980), pp. 317–353, DOI: https://doi.org/10.1016/0022-0000(80)90027-6 DOI: https://doi.org/10.1016/0022-0000(80)90027-6

C. Liang, D. Miller, Focusing and polarization in linear, intuitionistic, and classical logics, Theoretical Computer Science, vol. 410(46) (2009), pp. 4747–4768, DOI: https://doi.org/10.1016/j.tcs.2009.07.041, special issue: Abstract Interpretation and Logic Programming: In honor of professor Giorgio Levi. DOI: https://doi.org/10.1016/j.tcs.2009.07.041

L. Löwenheim, Über Möglichkeiten im Relativkalkül, Mathematische Annalen, vol. 76 (1915), pp. 447–470, DOI: https://doi.org/10.1007/BF01458217 DOI: https://doi.org/10.1007/BF01458217

W. V. Quine, On the logic of quantification, The Journal of Symbolic Logic, vol. 10(1) (1945), p. 1–12, DOI: https://doi.org/10.2307/2267200 DOI: https://doi.org/10.2307/2267200

A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, 2nd ed., Cambridge University Press, Cambridge (2000), DOI: https://doi.org/10.1017/CBO9781139168717 DOI: https://doi.org/10.1017/CBO9781139168717