A Syntactic Proof of the Decidability of First-Order Monadic Logic
DOI:
https://doi.org/10.18778/0138-0680.2024.03Keywords:
proof theory, classical logic, decidability, Herbrand theoremAbstract
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
Downloads
Published
How to Cite
Issue
Section
License
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
Funding data
-
Austrian Science Fund
Grant numbers FWF Project I 6372-N