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

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, but 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 (2007), DOI: https://doi.org/10.1017/CBO9780511804076.
Google Scholar DOI: https://doi.org/10.1017/CBO9780511804076

T. Braüner, 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 (2000), DOI: https://doi.org/10.1017/CBO9781139168717.
Google Scholar DOI: https://doi.org/10.1017/CBO9781139168717