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 https://orcid.org/0000-0002-4021-8667
Matteo Tesi Vienna University of Technology, Faculty of Informatics, Vienna, Austria

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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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.
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar DOI: https://doi.org/10.1017/CBO9781139168717